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

State before:
⊢ False
Tactic:
have hwrong : (∃x, x ≠ 0) ↔ False :=
  Exists.one_point_wrong 0 (fun _ ↦ False)
State after:
hwrong : (∃ x, x ≠ 0) ↔ False
⊢ False

State before:
hwrong : (∃ x, x ≠ 0) ↔ False
⊢ 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