Theorem: ψ_sq (LeanCourse/Lectures/Lecture7.lean)

State before:
n : ℕ
⊢ ψ ^ 2 = ψ + 1
Tactic:
simp [ψ, sub_sq]
State after:
n : ℕ
⊢ (1 - 2 * sqrt 5 + sqrt 5 ^ 2) / 2 ^ 2 = (1 - sqrt 5) / 2 + 1

State before:
n : ℕ
⊢ (1 - 2 * sqrt 5 + sqrt 5 ^ 2) / 2 ^ 2 = (1 - sqrt 5) / 2 + 1
Tactic:
field_simp
State after:
n : ℕ
⊢ (1 - 2 * sqrt 5 + 5) * 2 = (1 - sqrt 5 + 2) * 2 ^ 2

State before:
n : ℕ
⊢ (1 - 2 * sqrt 5 + 5) * 2 = (1 - sqrt 5 + 2) * 2 ^ 2
Tactic:
ring
State after:
no goals