f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ‖↑f z - 1‖ = ‖z - 1‖
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
have : ‖f z - 1‖ = ‖z - 1‖ := by rw [← f.norm_map (z - 1), f.map_sub, h]
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ‖↑f z - 1‖ ^ 2 = ‖z - 1‖ ^ 2
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ‖↑f z - 1‖ = ‖z - 1‖
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
apply_fun fun x => x ^ 2  at this
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ↑normSq (↑f z - 1) = ↑normSq (z - 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ‖↑f z - 1‖ ^ 2 = ‖z - 1‖ ^ 2
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
simp only [norm_eq_abs, ← normSq_eq_abs] at this
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : (↑f z - 1) * ↑(starRingEnd ℂ) (↑f z - 1) = (z - 1) * ↑(starRingEnd ℂ) (z - 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ↑normSq (↑f z - 1) = ↑normSq (z - 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
rw [← ofReal_inj, ← mul_conj, ← mul_conj] at this
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : (↑f z - 1) * (↑(starRingEnd ℂ) (↑f z) - ↑(starRingEnd ℂ) 1) = (z - 1) * (↑(starRingEnd ℂ) z - ↑(starRingEnd ℂ) 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : (↑f z - 1) * ↑(starRingEnd ℂ) (↑f z - 1) = (z - 1) * ↑(starRingEnd ℂ) (z - 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
rw [RingHom.map_sub, RingHom.map_sub] at this
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this :
  ↑f z * ↑(starRingEnd ℂ) (↑f z) - ↑(starRingEnd ℂ) (↑f z) - (↑f z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1) =
    z * ↑(starRingEnd ℂ) z - ↑(starRingEnd ℂ) z - (z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : (↑f z - 1) * (↑(starRingEnd ℂ) (↑f z) - ↑(starRingEnd ℂ) 1) = (z - 1) * (↑(starRingEnd ℂ) z - ↑(starRingEnd ℂ) 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
simp only [sub_mul, mul_sub, one_mul, mul_one] at this
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this :
  ↑(‖z‖ ^ 2) - ↑(starRingEnd ℂ) (↑f z) - (↑f z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1) =
    z * ↑(starRingEnd ℂ) z - ↑(starRingEnd ℂ) z - (z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this :
  ↑f z * ↑(starRingEnd ℂ) (↑f z) - ↑(starRingEnd ℂ) (↑f z) - (↑f z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1) =
    z * ↑(starRingEnd ℂ) z - ↑(starRingEnd ℂ) z - (z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
rw [mul_conj, normSq_eq_abs, ← norm_eq_abs, LinearIsometry.norm_map] at this
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this :
  ↑(‖z‖ ^ 2) - ↑(starRingEnd ℂ) (↑f z) - (↑f z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1) =
    ↑(‖z‖ ^ 2) - ↑(starRingEnd ℂ) z - (z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this :
  ↑(‖z‖ ^ 2) - ↑(starRingEnd ℂ) (↑f z) - (↑f z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1) =
    z * ↑(starRingEnd ℂ) z - ↑(starRingEnd ℂ) z - (z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
rw [mul_conj, normSq_eq_abs, ← norm_eq_abs] at this
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ↑(starRingEnd ℂ) (↑f z) + (↑f z - 1) = ↑(starRingEnd ℂ) z + (z - 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this :
  ↑(‖z‖ ^ 2) - ↑(starRingEnd ℂ) (↑f z) - (↑f z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1) =
    ↑(‖z‖ ^ 2) - ↑(starRingEnd ℂ) z - (z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
simp only [sub_sub, sub_right_inj, mul_one, ofReal_pow, RingHom.map_one, norm_eq_abs] at this
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ↑(starRingEnd ℂ) (↑f z) + ↑f z = ↑(starRingEnd ℂ) z + z
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ↑(starRingEnd ℂ) (↑f z) + (↑f z - 1) = ↑(starRingEnd ℂ) z + (z - 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
simp only [add_sub, sub_left_inj] at this
no goals
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ↑(starRingEnd ℂ) (↑f z) + ↑f z = ↑(starRingEnd ℂ) z + z
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
rw [add_comm, ← this, add_comm]
no goals
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
⊢ ‖↑f z - 1‖ = ‖z - 1‖
rw [← f.norm_map (z - 1), f.map_sub, h]