-- Mathlib/Analysis/Complex/Angle.lean
/-- Chord-length is a multiple of arc-length up to constants. -/
lemma norm_sub_mem_Icc_angle (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) :
    ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Proof state:
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 2 * (1 - Real.cos θ) = (Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2

Tactic:
linear_combination -θ.cos_sq_add_sin_sq

Result:
no goals

Proof state:
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 0 ≤ |θ|

Tactic:
positivity

Result:
no goals

Proof state:
case h.h
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ Real.cos θ ≤ 1 - 2 / π ^ 2 * θ ^ 2

Tactic:
exact Real.cos_le_one_sub_mul_cos_sq <| abs_le.2 <| Ioc_subset_Icc_self hθ

Result:
no goals

Proof state:
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 2 * (1 - (1 - θ ^ 2 / 2)) = θ ^ 2

Tactic:
ring

Result:
no goals

Proof state:
case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖x / y - 1‖ ∈ Icc (2 / π * angle x (1 * y)) (angle x (1 * y))
⊢ y ≠ 0

Tactic:
rintro rfl

Result:
case inr
x : ℂ
hx : ‖x‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
hy : ‖0‖ = 1
h : ¬0 = 1
this : ‖x / 0 - 1‖ ∈ Icc (2 / π * angle x (1 * 0)) (angle x (1 * 0))
⊢ False

Proof state:
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (2 / π) ^ 2 * θ ^ 2 = 2 * (1 - (1 - 2 / π ^ 2 * θ ^ 2))

Tactic:
ring

Result:
no goals

Proof state:
x✝ y x : ℂ
hx : ‖x‖ = 1
hy : ‖1‖ = 1
⊢ ‖x - 1‖ ∈ Icc (2 / π * angle x 1) (angle x 1)

Tactic:
rw [norm_eq_one_iff'] at hx

Result:
x✝ y x : ℂ
hx : ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x
hy : ‖1‖ = 1
⊢ ‖x - 1‖ ∈ Icc (2 / π * angle x 1) (angle x 1)

Proof state:
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2 = 2 * (1 - Real.cos θ)

Tactic:
linear_combination θ.cos_sq_add_sin_sq

Result:
no goals

Proof state:
case intro.intro.refine_2
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ √((Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2) ≤ |θ|

Tactic:
rw [Real.sqrt_le_left (by positivity), ← abs_pow, abs_sq]

Result:
case intro.intro.refine_2
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2 ≤ θ ^ 2

Proof state:
case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Tactic:
have := @this (x / y) 1 (by simp only [norm_div, hx, hy, div_one]) norm_one rfl

Result:
case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖x / y - 1‖ ∈ Icc (2 / π * angle (x / y) 1) (angle (x / y) 1)
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Proof state:
case intro.intro
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ √((Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2) ∈ Icc (2 / π * |θ|) |θ|

Tactic:
refine ⟨Real.le_sqrt_of_sq_le ?_, ?_⟩

Result:
case intro.intro.refine_1
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (2 / π * |θ|) ^ 2 ≤ (Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2

case intro.intro.refine_2
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ √((Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2) ≤ |θ|

Proof state:
case h.h
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 1 - θ ^ 2 / 2 ≤ Real.cos θ

Tactic:
exact Real.one_sub_sq_div_two_le_cos

Result:
no goals

Proof state:
x✝ y x : ℂ
hx : ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x
hy : ‖1‖ = 1
⊢ ‖x - 1‖ ∈ Icc (2 / π * angle x 1) (angle x 1)

Tactic:
obtain ⟨θ, hθ, rfl⟩ := hx

Result:
case intro.intro
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ ‖cexp (↑θ * I) - 1‖ ∈ Icc (2 / π * angle (cexp (↑θ * I)) 1) (angle (cexp (↑θ * I)) 1)

Proof state:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Tactic:
wlog h : y = 1

Result:
case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

x✝ y✝ x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h : y = 1
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Proof state:
case intro.intro
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ ‖↑(Real.cos θ - 1) + ↑(Real.sin θ) * I‖ ∈ Icc (2 / π * |θ|) |θ|

Tactic:
rw [norm_add_mul_I]

Result:
case intro.intro
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ √((Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2) ∈ Icc (2 / π * |θ|) |θ|

Proof state:
case inr
x : ℂ
hx : ‖x‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
hy : ‖0‖ = 1
h : ¬0 = 1
this : ‖x / 0 - 1‖ ∈ Icc (2 / π * angle x (1 * 0)) (angle x (1 * 0))
⊢ False

Tactic:
simp at hy

Result:
no goals

Proof state:
case h.e'_4.h.e'_4
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ -π + 2 * π = π

Tactic:
ring

Result:
no goals

Proof state:
case intro.intro
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ ‖cexp (↑θ * I) - 1‖ ∈ Icc (2 / π * angle (cexp (↑θ * I)) 1) (angle (cexp (↑θ * I)) 1)

Tactic:
rw [angle_exp_one, exp_mul_I, add_sub_right_comm, (toIocMod_eq_self _).2]

Result:
case intro.intro
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ ‖cos ↑θ - 1 + sin ↑θ * I‖ ∈ Icc (2 / π * |θ|) |θ|

case intro.intro
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ θ ∈ Ioc (-π) (-π + 2 * π)

Proof state:
case intro.intro
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ ‖cos ↑θ - 1 + sin ↑θ * I‖ ∈ Icc (2 / π * |θ|) |θ|

Tactic:
norm_cast

Result:
case intro.intro
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ ‖↑(Real.cos θ - 1) + ↑(Real.sin θ) * I‖ ∈ Icc (2 / π * |θ|) |θ|

Proof state:
x✝ y✝ x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h : y = 1
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Tactic:
subst y

Result:
x✝ y x : ℂ
hx : ‖x‖ = 1
hy : ‖1‖ = 1
⊢ ‖x - 1‖ ∈ Icc (2 / π * angle x 1) (angle x 1)

Proof state:
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 2 * (1 - Real.cos θ) ≤ 2 * (1 - (1 - θ ^ 2 / 2))

Tactic:
gcongr

Result:
case h.h
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 1 - θ ^ 2 / 2 ≤ Real.cos θ

Proof state:
case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖x / y - 1‖ ∈ Icc (2 / π * angle (x / y) 1) (angle (x / y) 1)
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Tactic:
rwa [angle_div_left_eq_angle_mul_right, div_sub_one, norm_div, hy, div_one, one_mul]
  at this

Result:
case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖x / y - 1‖ ∈ Icc (2 / π * angle x (1 * y)) (angle x (1 * y))
⊢ y ≠ 0

Proof state:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
⊢ ‖x / y‖ = 1

Tactic:
simp only [norm_div, hx, hy, div_one]

Result:
no goals

Proof state:
case intro.intro.refine_1
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (2 / π * |θ|) ^ 2 ≤ (Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2

Tactic:
rw [mul_pow, ← abs_pow, abs_sq]

Result:
case intro.intro.refine_1
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (2 / π) ^ 2 * θ ^ 2 ≤ (Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2

Proof state:
case intro.intro
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ θ ∈ Ioc (-π) (-π + 2 * π)

Tactic:
convert hθ

Result:
case h.e'_4.h.e'_4
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ -π + 2 * π = π

Proof state:
case intro.intro.refine_1
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (2 / π) ^ 2 * θ ^ 2 ≤ (Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2

Tactic:
calc
  _ = 2 * (1 - (1 - 2 / π ^ 2 * θ ^ 2)) := by ring
  _ ≤ 2 * (1 - θ.cos) := by
      gcongr; exact Real.cos_le_one_sub_mul_cos_sq <| abs_le.2 <| Ioc_subset_Icc_self hθ
  _  = _ := by linear_combination -θ.cos_sq_add_sin_sq

Result:
no goals