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

State before:
n : ℕ
⊢ ϕ ^ 2 = ϕ + 1
Tactic:
simp [ϕ, add_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