Theorem: normSq_sub_normSq (RMT4/etape2.lean)

State before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
⊢ normSq (z - u) - normSq (1 - z * (starRingEnd ℂ) u) = (normSq z - 1) * (1 - normSq u)
Tactic:
field_simp [← ofReal_inj, normSq_eq_conj_mul_self]
State after:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
⊢ ((starRingEnd ℂ) z - (starRingEnd ℂ) u) * (z - u) - (1 - (starRingEnd ℂ) z * u) * (1 - z * (starRingEnd ℂ) u) =
    ((starRingEnd ℂ) z * z - 1) * (1 - (starRingEnd ℂ) u * u)

State before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
⊢ ((starRingEnd ℂ) z - (starRingEnd ℂ) u) * (z - u) - (1 - (starRingEnd ℂ) z * u) * (1 - z * (starRingEnd ℂ) u) =
    ((starRingEnd ℂ) z * z - 1) * (1 - (starRingEnd ℂ) u * u)
Tactic:
ring
State after:
no goals