⊢ ((1 - sqrt 5) / 2) ^ 2 - ((1 - sqrt 5) / 2 + 1) = 0
⊢ ψ ^ 2 = ψ + 1
rw [goldenConj, ← sub_eq_zero]
⊢ sqrt 5 ^ 2 * (↑(Int.ofNat 1) / ↑4) + ↑(Int.negOfNat 5) * (↑(Int.ofNat 1) / ↑4) = 0
⊢ ((1 - sqrt 5) / 2) ^ 2 - ((1 - sqrt 5) / 2 + 1) = 0
ring_nf
no goals
⊢ sqrt 5 ^ 2 * (↑(Int.ofNat 1) / ↑4) + ↑(Int.negOfNat 5) * (↑(Int.ofNat 1) / ↑4) = 0
rw [Real.sq_sqrt] <;> norm_num