-- Mathlib/Analysis/Complex/Isometry.lean
theorem LinearIsometry.im_apply_eq_im {f : ℂ →ₗᵢ[ℝ] ℂ} (h : f 1 = 1) (z : ℂ) :
    z + conj z = f z + conj (f z)

Proof state:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
this : ‖f z - 1‖ = ‖z - 1‖
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Tactic:
apply_fun fun x => x ^ 2 at this

Result:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
this : ‖f z - 1‖ ^ 2 = ‖z - 1‖ ^ 2
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Proof state:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
⊢ ‖f z - 1‖ = ‖z - 1‖

Tactic:
rw [← f.norm_map (z - 1), f.map_sub, h]

Result:
no goals

Proof state:
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 ℂ) (f z)

Tactic:
simp only [sub_mul, mul_sub, one_mul, mul_one] at this

Result:
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 ℂ) (f z)

Proof state:
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 ℂ) (f z)

Tactic:
rw [RingHom.map_sub, RingHom.map_sub] at this

Result:
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 ℂ) (f z)

Proof state:
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 ℂ) (f z)

Tactic:
rw [mul_conj, normSq_eq_norm_sq] at this

Result:
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 ℂ) (f z)

Proof state:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
this : ‖f z - 1‖ ^ 2 = ‖z - 1‖ ^ 2
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Tactic:
simp only [← normSq_eq_norm_sq] at this

Result:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
this : normSq (f z - 1) = normSq (z - 1)
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Proof state:
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 ℂ) (f z)

Tactic:
rw [mul_conj, normSq_eq_norm_sq, LinearIsometry.norm_map] at this

Result:
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 ℂ) (f z)

Proof state:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
this : normSq (f z - 1) = normSq (z - 1)
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Tactic:
rw [← ofReal_inj, ← mul_conj, ← mul_conj] at this

Result:
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 ℂ) (f z)

Proof state:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Tactic:
have : ‖f z - 1‖ = ‖z - 1‖ := by rw [← f.norm_map (z - 1), f.map_sub, h]

Result:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
this : ‖f z - 1‖ = ‖z - 1‖
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Proof state:
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 ℂ) (f z)

Tactic:
simp only [sub_sub, sub_right_inj, mul_one, ofReal_pow, RingHom.map_one] at this

Result:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
this : (starRingEnd ℂ) (f z) + (f z - 1) = (starRingEnd ℂ) z + (z - 1)
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Proof state:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
this : (starRingEnd ℂ) (f z) + f z = (starRingEnd ℂ) z + z
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Tactic:
rw [add_comm, ← this, add_comm]

Result:
no goals

Proof state:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
this : (starRingEnd ℂ) (f z) + (f z - 1) = (starRingEnd ℂ) z + (z - 1)
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Tactic:
simp only [add_sub, sub_left_inj] at this

Result:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
this : (starRingEnd ℂ) (f z) + f z = (starRingEnd ℂ) z + z
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)