Closed mhk119 closed 4 months ago
Before the tactic would fail on the following example:
example : (True ∧ p1) = p1 := sorry
The idea implemented is the following:
example : (True ∧ p1) = p1 := by have := @bool_and_true True' p1 rw [true'_and, true'_and] at this rw [this]
Before the tactic would fail on the following example:
example : (True ∧ p1) = p1 := sorryThe idea implemented is the following: