/-- **The normal form of a plane isometry.** Every distance-preserving map `f : ℂ → ℂ` is
`z ↦ a z + b` or `z ↦ a z̄ + b` with `|a| = 1`. Proof as in the lesson: put `b = f 0` and
`a = f 1 - f 0`; then `g z = (f z - b) / a` preserves distances and fixes `0` and `1`, so `g i`
is at distance `1` from `0` and `√2` from `1`, i.e. `g i = ± i`. If `g i = i` then `g` is the
identity; if `g i = -i` then `z ↦ conj (g z)` fixes `0`, `1`, `i` and is the identity. -/
theorem isometry_normal_form (f : ℂ → ℂ) (hf : Isometry f) :
∃ a b : ℂ, ‖a‖ = 1 ∧ ((∀ z, f z = a * z + b) ∨ (∀ z, f z = a * conj z + b)) := by
have hd : ∀ z w, ‖f z - f w‖ = ‖z - w‖ := fun z w => by
rw [← Complex.dist_eq, ← Complex.dist_eq, hf.dist_eq]
set a := f 1 - f 0 with ha_def
set b := f 0 with hb_def
have ha : ‖a‖ = 1 := by simpa using hd 1 0
have ha0 : a ≠ 0 := by
intro h; rw [h, norm_zero] at ha; exact zero_ne_one ha
set g : ℂ → ℂ := fun z => (f z - b) / a with hg_def
have hfg : ∀ z, f z = a * g z + b := fun z => by
simp only [hg_def]; field_simp; ring
have hgd : ∀ z w, ‖g z - g w‖ = ‖z - w‖ := fun z w => by
have : g z - g w = (f z - f w) / a := by simp only [hg_def]; field_simp; ring
rw [this, norm_div, ha, div_one, hd]
have hg0 : g 0 = 0 := by simp [hg_def, hb_def]
have hg1 : g 1 = 1 := by simp only [hg_def]; rw [← ha_def]; exact div_self ha0
-- `g i` is `i` or `-i`.
have hgI : g I = I ∨ g I = -I := by
have e0 : normSq (g I) = 1 := by
have := hgd I 0; rw [hg0, sub_zero, sub_zero, norm_I] at this
rw [← Complex.sq_norm, this, one_pow]
have e1 : normSq (g I - 1) = 2 := by
have := hgd I 1; rw [hg1] at this
rw [← Complex.sq_norm, this, Complex.sq_norm]; simp [normSq_apply]; norm_num
simp only [normSq_apply, sub_re, sub_im, one_re, one_im] at e0 e1
have hre : (g I).re = 0 := by nlinarith
have him : (g I).im = 1 ∨ (g I).im = -1 := by
have : (g I).im * (g I).im = 1 := by rw [hre] at e0; linarith
rcases mul_self_eq_one_iff.mp this with h | h
· exact Or.inl h
· exact Or.inr h
rcases him with h | h
· left; apply Complex.ext <;> simp [hre, h]
· right; apply Complex.ext <;> simp [hre, h]
refine ⟨a, b, ha, ?_⟩
rcases hgI with hI | hI
· -- `g` is the identity: a direct isometry.
left; intro z
rw [hfg z, fix_three_eq_id g hgd hg0 hg1 hI z]
· -- `conj ∘ g` is the identity: an opposite isometry.
right; intro z
have hc := fix_three_eq_id (fun z => conj (g z))
(fun z w => by rw [← map_sub, Complex.norm_conj, hgd]) (by simp [hg0])
(by simp [hg1]) (by simp [hI]) z
have : g z = conj z := by rw [← Complex.conj_conj (g z), hc]
rw [hfg z, this]