Theorem: LoVe.All.proof_of_False (LoVe/Labs/Lab3Solution.lean)

State before:
⊢ False
Tactic:
have hwrong : (∀x, x = 0 ∧ True) ↔ True :=
  All.one_point_wrong 0 (fun _ ↦ True)
State after:
hwrong : (∀ (x : ℕ), x = 0 ∧ True) ↔ True
⊢ False

State before:
hwrong : (∀ (x : ℕ), x = 0 ∧ True) ↔ True
⊢ False
Tactic:
simp at hwrong
State after:
hwrong : ∀ (x : ℕ), x = 0
⊢ False

State before:
hwrong : ∀ (x : ℕ), x = 0
⊢ False
Tactic:
have hone_eq_zero : 1 = 0 :=
  hwrong 1
State after:
hwrong : ∀ (x : ℕ), x = 0
hone_eq_zero : 1 = 0
⊢ False

State before:
hwrong : ∀ (x : ℕ), x = 0
hone_eq_zero : 1 = 0
⊢ False
Tactic:
cases hone_eq_zero
State after:
no goals