Theorem: ϕ_sub_ψ_ne_zero (LeanCourse/Lectures/Lecture7.lean)

State before:
n : ℕ
⊢ ϕ - ψ ≠ 0
Tactic:
simp [ϕ, ψ, sub_eq_zero]
State after:
n : ℕ
⊢ ¬1 + sqrt 5 = 1 - sqrt 5

State before:
n : ℕ
⊢ ¬1 + sqrt 5 = 1 - sqrt 5
Tactic:
simp [sub_eq_add_neg]
State after:
n : ℕ
⊢ 0 < 5

State before:
n : ℕ
⊢ 0 < 5
Tactic:
norm_num
State after:
no goals