[GOAL]
⊢ Continuous sin
[PROOFSTEP]
change Continuous fun z => (exp (-z * I) - exp (z * I)) * I / 2
[GOAL]
⊢ Continuous fun z => (exp (-z * I) - exp (z * I)) * I / 2
[PROOFSTEP]
continuity
[GOAL]
⊢ Continuous cos
[PROOFSTEP]
change Continuous fun z => (exp (z * I) + exp (-z * I)) / 2
[GOAL]
⊢ Continuous fun z => (exp (z * I) + exp (-z * I)) / 2
[PROOFSTEP]
continuity
[GOAL]
⊢ Continuous sinh
[PROOFSTEP]
change Continuous fun z => (exp z - exp (-z)) / 2
[GOAL]
⊢ Continuous fun z => (exp z - exp (-z)) / 2
[PROOFSTEP]
continuity
[GOAL]
⊢ Continuous cosh
[PROOFSTEP]
change Continuous fun z => (exp z + exp (-z)) / 2
[GOAL]
⊢ Continuous fun z => (exp z + exp (-z)) / 2
[PROOFSTEP]
continuity
[GOAL]
⊢ 1 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
⊢ cos (π / 2) = 0
[PROOFSTEP]
rw [Real.pi, mul_div_cancel_left _ (two_ne_zero' ℝ)]
[GOAL]
⊢ cos (choose exists_cos_eq_zero) = 0
[PROOFSTEP]
exact (Classical.choose_spec exists_cos_eq_zero).2
[GOAL]
⊢ 1 ≤ π / 2
[PROOFSTEP]
rw [Real.pi, mul_div_cancel_left _ (two_ne_zero' ℝ)]
[GOAL]
⊢ 1 ≤ choose exists_cos_eq_zero
[PROOFSTEP]
exact (Classical.choose_spec exists_cos_eq_zero).1.1
[GOAL]
⊢ π / 2 ≤ 2
[PROOFSTEP]
rw [Real.pi, mul_div_cancel_left _ (two_ne_zero' ℝ)]
[GOAL]
⊢ choose exists_cos_eq_zero ≤ 2
[PROOFSTEP]
exact (Classical.choose_spec exists_cos_eq_zero).1.2
[GOAL]
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
⊢ 2 / 2 ≤ π / 2
[PROOFSTEP]
rw [div_self (two_ne_zero' ℝ)]
[GOAL]
⊢ 1 ≤ π / 2
[PROOFSTEP]
exact one_le_pi_div_two
[GOAL]
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
⊢ 2 = 4 / 2
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 < 2 * π
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
⊢ 0 < pi
[PROOFSTEP]
exact_mod_cast Real.pi_pos
[GOAL]
⊢ sin π = 0
[PROOFSTEP]
rw [← mul_div_cancel_left π (two_ne_zero' ℝ), two_mul, add_div, sin_add, cos_pi_div_two]
[GOAL]
⊢ sin (π / 2) * 0 + 0 * sin (π / 2) = 0
[PROOFSTEP]
simp
[GOAL]
⊢ cos π = -1
[PROOFSTEP]
rw [← mul_div_cancel_left π (two_ne_zero' ℝ), mul_div_assoc, cos_two_mul, cos_pi_div_two]
[GOAL]
⊢ 2 * 0 ^ 2 - 1 = -1
[PROOFSTEP]
norm_num
[GOAL]
⊢ sin (2 * π) = 0
[PROOFSTEP]
simp [two_mul, sin_add]
[GOAL]
⊢ cos (2 * π) = 1
[PROOFSTEP]
simp [two_mul, cos_add]
[GOAL]
⊢ Function.Antiperiodic sin π
[PROOFSTEP]
simp [sin_add]
[GOAL]
⊢ Function.Antiperiodic cos π
[PROOFSTEP]
simp [cos_add]
[GOAL]
n : ℕ
⊢ cos (↑n * (2 * π) + π) = -1
[PROOFSTEP]
simpa only [cos_zero] using (cos_periodic.nat_mul n).add_antiperiod_eq cos_antiperiodic
[GOAL]
n : ℤ
⊢ cos (↑n * (2 * π) + π) = -1
[PROOFSTEP]
simpa only [cos_zero] using (cos_periodic.int_mul n).add_antiperiod_eq cos_antiperiodic
[GOAL]
n : ℕ
⊢ cos (↑n * (2 * π) - π) = -1
[PROOFSTEP]
simpa only [cos_zero] using (cos_periodic.nat_mul n).sub_antiperiod_eq cos_antiperiodic
[GOAL]
n : ℤ
⊢ cos (↑n * (2 * π) - π) = -1
[PROOFSTEP]
simpa only [cos_zero] using (cos_periodic.int_mul n).sub_antiperiod_eq cos_antiperiodic
[GOAL]
x : ℝ
h0x : 0 < x
hxp : x < π
hx2 : ¬x ≤ 2
⊢ 2 + 2 = 4
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
hx : x ∈ Icc 0 π
⊢ 0 ≤ sin x
[PROOFSTEP]
rw [← closure_Ioo pi_ne_zero.symm] at hx
[GOAL]
x : ℝ
hx : x ∈ closure (Ioo 0 π)
⊢ 0 ≤ sin x
[PROOFSTEP]
exact closure_lt_subset_le continuous_const continuous_sin (closure_mono (fun y => sin_pos_of_mem_Ioo) hx)
[GOAL]
⊢ sin (π / 2) = 1 ∨ sin (π / 2) = -1
[PROOFSTEP]
simpa [sq, mul_self_eq_one_iff] using sin_sq_add_cos_sq (π / 2)
[GOAL]
this : sin (π / 2) = 1 ∨ sin (π / 2) = -1
h : sin (π / 2) = -1
⊢ ¬0 < -1
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
⊢ sin (x + π / 2) = cos x
[PROOFSTEP]
simp [sin_add]
[GOAL]
x : ℝ
⊢ sin (x - π / 2) = -cos x
[PROOFSTEP]
simp [sub_eq_add_neg, sin_add]
[GOAL]
x : ℝ
⊢ sin (π / 2 - x) = cos x
[PROOFSTEP]
simp [sub_eq_add_neg, sin_add]
[GOAL]
x : ℝ
⊢ cos (x + π / 2) = -sin x
[PROOFSTEP]
simp [cos_add]
[GOAL]
x : ℝ
⊢ cos (x - π / 2) = sin x
[PROOFSTEP]
simp [sub_eq_add_neg, cos_add]
[GOAL]
x : ℝ
⊢ cos (π / 2 - x) = sin x
[PROOFSTEP]
rw [← cos_neg, neg_sub, cos_sub_pi_div_two]
[GOAL]
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ 0 < x + π / 2
[PROOFSTEP]
linarith [hx.1]
[GOAL]
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ x + π / 2 < π
[PROOFSTEP]
linarith [hx.2]
[GOAL]
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ 0 ≤ x + π / 2
[PROOFSTEP]
linarith [hx.1]
[GOAL]
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ x + π / 2 ≤ π
[PROOFSTEP]
linarith [hx.2]
[GOAL]
x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
⊢ -(π / 2) < π - x
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
⊢ π - x < π / 2
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
⊢ -(π / 2) ≤ π - x
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
⊢ π - x ≤ π / 2
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
hl : 0 ≤ x
hu : x ≤ π
⊢ sin x = sqrt (1 - cos x ^ 2)
[PROOFSTEP]
rw [← abs_sin_eq_sqrt_one_sub_cos_sq, abs_of_nonneg (sin_nonneg_of_nonneg_of_le_pi hl hu)]
[GOAL]
x : ℝ
hl : -(π / 2) ≤ x
hu : x ≤ π / 2
⊢ cos x = sqrt (1 - sin x ^ 2)
[PROOFSTEP]
rw [← abs_cos_eq_sqrt_one_sub_sin_sq, abs_of_nonneg (cos_nonneg_of_mem_Icc ⟨hl, hu⟩)]
[GOAL]
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x = 0
⊢ sin x = 0
[PROOFSTEP]
simp [h]
[GOAL]
x : ℝ
h : sin x = 0
h₃ : x - ↑⌊x / π⌋ * π > 0
⊢ 0 = sin (x - ↑⌊x / π⌋ * π)
[PROOFSTEP]
simp [sub_eq_add_neg, sin_add, h, sin_int_mul_pi]
[GOAL]
x : ℝ
⊢ sin x ≠ 0 ↔ ∀ (n : ℤ), ↑n * π ≠ x
[PROOFSTEP]
rw [← not_exists, not_iff_not, sin_eq_zero_iff]
[GOAL]
x : ℝ
⊢ sin x = 0 ↔ cos x = 1 ∨ cos x = -1
[PROOFSTEP]
rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq x, sq, sq, ← sub_eq_iff_eq_add, sub_self]
[GOAL]
x : ℝ
⊢ sin x = 0 ↔ 0 = sin x * sin x
[PROOFSTEP]
exact ⟨fun h => by rw [h, mul_zero], eq_zero_of_mul_self_eq_zero ∘ Eq.symm⟩
[GOAL]
x : ℝ
h : sin x = 0
⊢ 0 = sin x * sin x
[PROOFSTEP]
rw [h, mul_zero]
[GOAL]
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑n * π = x
hn0 : n % 2 = 0
⊢ ↑(n / 2) * (2 * π) = x
[PROOFSTEP]
rwa [← mul_assoc, ← @Int.cast_two ℝ, ← Int.cast_mul, Int.ediv_mul_cancel ((Int.dvd_iff_emod_eq_zero _ _).2 hn0)]
[GOAL]
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑n * π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x
[PROOFSTEP]
rw [← Int.emod_add_ediv n 2, hn1, Int.cast_add, Int.cast_one, add_mul, one_mul, add_comm, mul_comm (2 : ℤ),
  Int.cast_mul, mul_assoc, Int.cast_two] at hn
[GOAL]
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑(n / 2) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x
[PROOFSTEP]
rw [← hn, cos_int_mul_two_pi_add_pi] at h
[GOAL]
x : ℝ
n : ℤ
h : -1 = 1
hn : ↑(n / 2) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x
[PROOFSTEP]
exact absurd h (by norm_num)
[GOAL]
x : ℝ
n : ℤ
h : -1 = 1
hn : ↑(n / 2) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ ¬-1 = 1
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
hx₁ : -(2 * π) < x
hx₂ : x < 2 * π
h : cos x = 1
⊢ x = 0
[PROOFSTEP]
rcases(cos_eq_one_iff _).1 h with ⟨n, rfl⟩
[GOAL]
case intro
n : ℤ
hx₁ : -(2 * π) < ↑n * (2 * π)
hx₂ : ↑n * (2 * π) < 2 * π
h : cos (↑n * (2 * π)) = 1
⊢ ↑n * (2 * π) = 0
[PROOFSTEP]
rw [mul_lt_iff_lt_one_left two_pi_pos] at hx₂
[GOAL]
case intro
n : ℤ
hx₁ : -(2 * π) < ↑n * (2 * π)
hx₂ : ↑n < 1
h : cos (↑n * (2 * π)) = 1
⊢ ↑n * (2 * π) = 0
[PROOFSTEP]
rw [neg_lt, neg_mul_eq_neg_mul, mul_lt_iff_lt_one_left two_pi_pos] at hx₁
[GOAL]
case intro
n : ℤ
hx₁ : -↑n < 1
hx₂ : ↑n < 1
h : cos (↑n * (2 * π)) = 1
⊢ ↑n * (2 * π) = 0
[PROOFSTEP]
norm_cast at hx₁ hx₂
[GOAL]
case intro
n : ℤ
h : cos (↑n * (2 * π)) = 1
hx₁ : -n < 1
hx₂ : n < 1
⊢ ↑n * (2 * π) = 0
[PROOFSTEP]
obtain rfl : n = 0 := le_antisymm (by linarith) (by linarith)
[GOAL]
n : ℤ
h : cos (↑n * (2 * π)) = 1
hx₁ : -n < 1
hx₂ : n < 1
⊢ n ≤ 0
[PROOFSTEP]
linarith
[GOAL]
n : ℤ
h : cos (↑n * (2 * π)) = 1
hx₁ : -n < 1
hx₂ : n < 1
⊢ 0 ≤ n
[PROOFSTEP]
linarith
[GOAL]
case intro
h : cos (↑0 * (2 * π)) = 1
hx₁ : -0 < 1
hx₂ : 0 < 1
⊢ ↑0 * (2 * π) = 0
[PROOFSTEP]
simp
[GOAL]
x : ℝ
hx₁ : -(2 * π) < x
hx₂ : x < 2 * π
h : x = 0
⊢ cos x = 1
[PROOFSTEP]
simp [h]
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ cos y < cos x
[PROOFSTEP]
rw [← sub_lt_zero, cos_sub_cos]
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ -2 * sin ((y + x) / 2) * sin ((y - x) / 2) < 0
[PROOFSTEP]
have : 0 < sin ((y + x) / 2) := by refine' sin_pos_of_pos_of_lt_pi _ _ <;> linarith
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ 0 < sin ((y + x) / 2)
[PROOFSTEP]
refine' sin_pos_of_pos_of_lt_pi _ _
[GOAL]
case refine'_1
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ 0 < (y + x) / 2
[PROOFSTEP]
linarith
[GOAL]
case refine'_2
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ (y + x) / 2 < π
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y + x) / 2)
⊢ -2 * sin ((y + x) / 2) * sin ((y - x) / 2) < 0
[PROOFSTEP]
have : 0 < sin ((y - x) / 2) := by refine' sin_pos_of_pos_of_lt_pi _ _ <;> linarith
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y + x) / 2)
⊢ 0 < sin ((y - x) / 2)
[PROOFSTEP]
refine' sin_pos_of_pos_of_lt_pi _ _
[GOAL]
case refine'_1
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y + x) / 2)
⊢ 0 < (y - x) / 2
[PROOFSTEP]
linarith
[GOAL]
case refine'_2
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y + x) / 2)
⊢ (y - x) / 2 < π
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this✝ : 0 < sin ((y + x) / 2)
this : 0 < sin ((y - x) / 2)
⊢ -2 * sin ((y + x) / 2) * sin ((y - x) / 2) < 0
[PROOFSTEP]
nlinarith
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx✝ : x ≤ π / 2
hy : π / 2 ≤ y
hx : x < π / 2
⊢ y ≤ π + π / 2
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx✝ : x ≤ π / 2
hy : π / 2 ≤ y
hx : x < π / 2
⊢ -(π / 2) < x
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx✝ : x ≤ π / 2
hy : π / 2 ≤ y
hx : x = π / 2
⊢ π / 2 < y
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx✝ : x ≤ π / 2
hy : π / 2 ≤ y
hx : x = π / 2
⊢ y < π + π / 2
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx✝ : x ≤ π / 2
hy : π / 2 ≤ y
hx : x = π / 2
⊢ 0 = cos x
[PROOFSTEP]
rw [hx, cos_pi_div_two]
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx : π / 2 ≤ x
hy : y ≤ π / 2
⊢ cos y < cos x
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx : π / 2 ≤ x
hy : π / 2 ≤ y
⊢ -cos x < -cos y
[PROOFSTEP]
rw [← cos_pi_sub, ← cos_pi_sub]
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx : π / 2 ≤ x
hy : π / 2 ≤ y
⊢ cos (π - x) < cos (π - y)
[PROOFSTEP]
apply cos_lt_cos_of_nonneg_of_le_pi_div_two
[GOAL]
case hx₁
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx : π / 2 ≤ x
hy : π / 2 ≤ y
⊢ 0 ≤ π - y
[PROOFSTEP]
linarith
[GOAL]
case hy₂
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx : π / 2 ≤ x
hy : π / 2 ≤ y
⊢ π - x ≤ π / 2
[PROOFSTEP]
linarith
[GOAL]
case hxy
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx : π / 2 ≤ x
hy : π / 2 ≤ y
⊢ π - y < π - x
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ sin x < sin y
[PROOFSTEP]
rw [← cos_sub_pi_div_two, ← cos_sub_pi_div_two, ← cos_neg (x - _), ← cos_neg (y - _)]
[GOAL]
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ cos (-(x - π / 2)) < cos (-(y - π / 2))
[PROOFSTEP]
apply cos_lt_cos_of_nonneg_of_le_pi
[GOAL]
case hx₁
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ 0 ≤ -(y - π / 2)
[PROOFSTEP]
linarith
[GOAL]
case hy₂
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ -(x - π / 2) ≤ π
[PROOFSTEP]
linarith
[GOAL]
case hxy
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ -(y - π / 2) < -(x - π / 2)
[PROOFSTEP]
linarith
[GOAL]
⊢ SurjOn sin (Icc (-(π / 2)) (π / 2)) (Icc (-1) 1)
[PROOFSTEP]
simpa only [sin_neg, sin_pi_div_two] using
  intermediate_value_Icc (neg_le_self pi_div_two_pos.le) continuous_sin.continuousOn
[GOAL]
⊢ SurjOn cos (Icc 0 π) (Icc (-1) 1)
[PROOFSTEP]
simpa only [cos_zero, cos_pi] using intermediate_value_Icc' pi_pos.le continuous_cos.continuousOn
[GOAL]
⊢ Set.Infinite (range cos)
[PROOFSTEP]
rw [Real.range_cos]
[GOAL]
⊢ Set.Infinite (Icc (-1) 1)
[PROOFSTEP]
exact Icc_infinite (by norm_num)
[GOAL]
⊢ -1 < 1
[PROOFSTEP]
norm_num
[GOAL]
⊢ Set.Infinite (range sin)
[PROOFSTEP]
rw [Real.range_sin]
[GOAL]
⊢ Set.Infinite (Icc (-1) 1)
[PROOFSTEP]
exact Icc_infinite (by norm_num)
[GOAL]
⊢ -1 < 1
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
⊢ sqrtTwoAddSeries x 0 = x
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ sqrtTwoAddSeries 0 1 = sqrt 2
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ sqrtTwoAddSeries 0 2 = sqrt (2 + sqrt 2)
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ sqrtTwoAddSeries 0 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 (n + 1) < 2
[PROOFSTEP]
refine' lt_of_lt_of_le _ (sqrt_sq zero_lt_two.le).le
[GOAL]
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 (n + 1) < sqrt (2 ^ 2)
[PROOFSTEP]
rw [sqrtTwoAddSeries, sqrt_lt_sqrt_iff, ← lt_sub_iff_add_lt']
[GOAL]
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 n < 2 ^ 2 - 2
[PROOFSTEP]
refine' (sqrtTwoAddSeries_lt_two n).trans_le _
[GOAL]
x : ℝ
n : ℕ
⊢ 2 ≤ 2 ^ 2 - 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
[PROOFSTEP]
exact add_nonneg zero_le_two (sqrtTwoAddSeries_zero_nonneg n)
[GOAL]
x✝ x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries x (n + 1 + 1) = sqrtTwoAddSeries (sqrt (2 + x)) (n + 1)
[PROOFSTEP]
rw [sqrtTwoAddSeries, sqrtTwoAddSeries_succ _ _, sqrtTwoAddSeries]
[GOAL]
x✝ x y : ℝ
h : x ≤ y
n : ℕ
⊢ sqrtTwoAddSeries x (n + 1) ≤ sqrtTwoAddSeries y (n + 1)
[PROOFSTEP]
rw [sqrtTwoAddSeries, sqrtTwoAddSeries]
[GOAL]
x✝ x y : ℝ
h : x ≤ y
n : ℕ
⊢ sqrt (2 + sqrtTwoAddSeries x n) ≤ sqrt (2 + sqrtTwoAddSeries y n)
[PROOFSTEP]
exact sqrt_le_sqrt (add_le_add_left (sqrtTwoAddSeries_monotone_left h _) _)
[GOAL]
x : ℝ
⊢ cos (π / 2 ^ (0 + 1)) = sqrtTwoAddSeries 0 0 / 2
[PROOFSTEP]
simp
[GOAL]
x : ℝ
n : ℕ
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
[PROOFSTEP]
have : (2 : ℝ) ≠ 0 := two_ne_zero
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
[PROOFSTEP]
symm
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ sqrtTwoAddSeries 0 (n + 1) / 2 = cos (π / 2 ^ (n + 1 + 1))
[PROOFSTEP]
rw [div_eq_iff_mul_eq this]
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ cos (π / 2 ^ (n + 1 + 1)) * 2 = sqrtTwoAddSeries 0 (n + 1)
[PROOFSTEP]
symm
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ sqrtTwoAddSeries 0 (n + 1) = cos (π / 2 ^ (n + 1 + 1)) * 2
[PROOFSTEP]
rw [sqrtTwoAddSeries, sqrt_eq_iff_sq_eq, mul_pow, cos_sq, ← mul_div_assoc, Nat.add_succ, pow_succ,
  mul_div_mul_left _ _ this, cos_pi_over_two_pow _, add_mul]
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 / 2 * 2 ^ 2 + sqrtTwoAddSeries 0 n / 2 / 2 * 2 ^ 2 = 2 + sqrtTwoAddSeries 0 n
case hx
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
case hy x : ℝ n : ℕ this : 2 ≠ 0 ⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
[PROOFSTEP]
congr
[GOAL]
case e_a
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 / 2 * 2 ^ 2 = 2
[PROOFSTEP]
norm_num
[GOAL]
case e_a
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ sqrtTwoAddSeries 0 n / 2 / 2 * 2 ^ 2 = sqrtTwoAddSeries 0 n
[PROOFSTEP]
rw [mul_comm, sq, mul_assoc, ← mul_div_assoc, mul_div_cancel_left, ← mul_div_assoc, mul_div_cancel_left]
[GOAL]
case e_a.ha
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 2 ≠ 0
[PROOFSTEP]
try exact this
[GOAL]
case e_a.ha
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 2 ≠ 0
[PROOFSTEP]
exact this
[GOAL]
case e_a.ha
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 2 ≠ 0
[PROOFSTEP]
try exact this
[GOAL]
case e_a.ha
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 2 ≠ 0
[PROOFSTEP]
exact this
[GOAL]
case hx
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
case hy x : ℝ n : ℕ this : 2 ≠ 0 ⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
[PROOFSTEP]
apply add_nonneg
[GOAL]
case hx.ha
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ 2
case hx.hb
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ sqrtTwoAddSeries 0 n
case hy x : ℝ n : ℕ this : 2 ≠ 0 ⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
[PROOFSTEP]
norm_num
[GOAL]
case hx.hb
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ sqrtTwoAddSeries 0 n
case hy x : ℝ n : ℕ this : 2 ≠ 0 ⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
[PROOFSTEP]
apply sqrtTwoAddSeries_zero_nonneg
[GOAL]
case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
[PROOFSTEP]
norm_num
[GOAL]
case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1))
[PROOFSTEP]
apply le_of_lt
[GOAL]
case hy.a
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < cos (π / 2 ^ (n + 1 + 1))
[PROOFSTEP]
apply cos_pos_of_mem_Ioo ⟨_, _⟩
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ -(π / 2) < π / 2 ^ (n + 1 + 1)
[PROOFSTEP]
trans (0 : ℝ)
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ -(π / 2) < 0
x : ℝ n : ℕ this : 2 ≠ 0 ⊢ 0 < π / 2 ^ (n + 1 + 1)
[PROOFSTEP]
rw [neg_lt_zero]
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < π / 2
x : ℝ n : ℕ this : 2 ≠ 0 ⊢ 0 < π / 2 ^ (n + 1 + 1)
[PROOFSTEP]
apply pi_div_two_pos
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < π / 2 ^ (n + 1 + 1)
[PROOFSTEP]
apply div_pos pi_pos
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2 ^ (n + 1 + 1)
[PROOFSTEP]
apply pow_pos
[GOAL]
case H
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ π / 2 ^ (n + 1 + 1) < π / 2
[PROOFSTEP]
apply div_lt_div' (le_refl π) _ pi_pos _
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 2 < 2 ^ (n + 1 + 1)
x : ℝ n : ℕ this : 2 ≠ 0 ⊢ 0 < 2
[PROOFSTEP]
refine' lt_of_le_of_lt (le_of_eq (pow_one _).symm) _
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 2 ^ 1 < 2 ^ (n + 1 + 1)
x : ℝ n : ℕ this : 2 ≠ 0 ⊢ 0 < 2
[PROOFSTEP]
apply pow_lt_pow
[GOAL]
case h
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 < 2
case h2
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 < n + 1 + 1
x : ℝ n : ℕ this : 2 ≠ 0 ⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case h2
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 < n + 1 + 1
x : ℝ n : ℕ this : 2 ≠ 0 ⊢ 0 < 2
[PROOFSTEP]
apply Nat.succ_lt_succ
[GOAL]
case h2.a
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < n + 1
x : ℝ n : ℕ this : 2 ≠ 0 ⊢ 0 < 2
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
[PROOFSTEP]
all_goals norm_num
[GOAL]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
n : ℕ
⊢ sin (π / 2 ^ (n + 1)) ^ 2 = 1 - (sqrtTwoAddSeries 0 n / 2) ^ 2
[PROOFSTEP]
rw [sin_sq, cos_pi_over_two_pow]
[GOAL]
x : ℝ
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4
[PROOFSTEP]
rw [sin_sq_pi_over_two_pow, sqrtTwoAddSeries, div_pow, sq_sqrt, add_div, ← sub_sub]
[GOAL]
x : ℝ
n : ℕ
⊢ 1 - 2 / 2 ^ 2 - sqrtTwoAddSeries 0 n / 2 ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4
x : ℝ n : ℕ ⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
[PROOFSTEP]
congr
[GOAL]
case e_a
x : ℝ
n : ℕ
⊢ 1 - 2 / 2 ^ 2 = 1 / 2
case e_a.e_a
x : ℝ
n : ℕ
⊢ 2 ^ 2 = 4
x : ℝ n : ℕ ⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
[PROOFSTEP]
norm_num
[GOAL]
case e_a.e_a
x : ℝ
n : ℕ
⊢ 2 ^ 2 = 4
x : ℝ n : ℕ ⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
[PROOFSTEP]
apply add_nonneg
[GOAL]
case ha
x : ℝ
n : ℕ
⊢ 0 ≤ 2
case hb x : ℝ n : ℕ ⊢ 0 ≤ sqrtTwoAddSeries 0 n
[PROOFSTEP]
norm_num
[GOAL]
case hb
x : ℝ
n : ℕ
⊢ 0 ≤ sqrtTwoAddSeries 0 n
[PROOFSTEP]
apply sqrtTwoAddSeries_zero_nonneg
[GOAL]
x : ℝ
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) = sqrt (2 - sqrtTwoAddSeries 0 n) / 2
[PROOFSTEP]
symm
[GOAL]
x : ℝ
n : ℕ
⊢ sqrt (2 - sqrtTwoAddSeries 0 n) / 2 = sin (π / 2 ^ (n + 2))
[PROOFSTEP]
rw [div_eq_iff_mul_eq]
[GOAL]
x : ℝ
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) * 2 = sqrt (2 - sqrtTwoAddSeries 0 n)
x : ℝ n : ℕ ⊢ 2 ≠ 0
[PROOFSTEP]
symm
[GOAL]
x : ℝ
n : ℕ
⊢ sqrt (2 - sqrtTwoAddSeries 0 n) = sin (π / 2 ^ (n + 2)) * 2
x : ℝ n : ℕ ⊢ 2 ≠ 0
[PROOFSTEP]
rw [sqrt_eq_iff_sq_eq, mul_pow, sin_sq_pi_over_two_pow_succ, sub_mul]
[GOAL]
x : ℝ
n : ℕ
⊢ 1 / 2 * 2 ^ 2 - sqrtTwoAddSeries 0 n / 4 * 2 ^ 2 = 2 - sqrtTwoAddSeries 0 n
[PROOFSTEP]
congr
[GOAL]
case e_a
x : ℝ
n : ℕ
⊢ 1 / 2 * 2 ^ 2 = 2
[PROOFSTEP]
norm_num
[GOAL]
case e_a
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 n / 4 * 2 ^ 2 = sqrtTwoAddSeries 0 n
[PROOFSTEP]
norm_num
[GOAL]
case hx
x : ℝ
n : ℕ
⊢ 0 ≤ 2 - sqrtTwoAddSeries 0 n
[PROOFSTEP]
rw [sub_nonneg]
[GOAL]
case hx
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 n ≤ 2
[PROOFSTEP]
apply le_of_lt
[GOAL]
case hx.a
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 n < 2
[PROOFSTEP]
apply sqrtTwoAddSeries_lt_two
[GOAL]
case hy
x : ℝ
n : ℕ
⊢ 0 ≤ sin (π / 2 ^ (n + 2)) * 2
x : ℝ n : ℕ ⊢ 2 ≠ 0
[PROOFSTEP]
apply le_of_lt
[GOAL]
case hy.a
x : ℝ
n : ℕ
⊢ 0 < sin (π / 2 ^ (n + 2)) * 2
x : ℝ n : ℕ ⊢ 2 ≠ 0
[PROOFSTEP]
apply mul_pos
[GOAL]
case hy.a.ha
x : ℝ
n : ℕ
⊢ 0 < sin (π / 2 ^ (n + 2))
case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2
x : ℝ n : ℕ ⊢ 2 ≠ 0
[PROOFSTEP]
apply sin_pos_of_pos_of_lt_pi
[GOAL]
case hy.a.ha.h0x
x : ℝ
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)
[PROOFSTEP]
apply div_pos pi_pos
[GOAL]
case hy.a.ha.h0x
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_pos
[GOAL]
case hy.a.ha.h0x.H
x : ℝ
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case hy.a.ha.hxp
x : ℝ
n : ℕ
⊢ π / 2 ^ (n + 2) < π
case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2
x : ℝ n : ℕ ⊢ 2 ≠ 0
[PROOFSTEP]
refine' lt_of_lt_of_le _ (le_of_eq (div_one _))
[GOAL]
case hy.a.ha.hxp
x : ℝ
n : ℕ
⊢ π / 2 ^ (n + 2) < π / 1
case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2
x : ℝ n : ℕ ⊢ 2 ≠ 0
[PROOFSTEP]
rw [div_lt_div_left]
[GOAL]
case hy.a.ha.hxp
x : ℝ
n : ℕ
⊢ 1 < 2 ^ (n + 2)
case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π
case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)
case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1
case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2
x : ℝ n : ℕ ⊢ 2 ≠ 0
[PROOFSTEP]
refine' lt_of_le_of_lt (le_of_eq (pow_zero 2).symm) _
[GOAL]
case hy.a.ha.hxp
x : ℝ
n : ℕ
⊢ 2 ^ 0 < 2 ^ (n + 2)
case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π
case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)
case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1
case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2
x : ℝ n : ℕ ⊢ 2 ≠ 0
[PROOFSTEP]
apply pow_lt_pow
[GOAL]
case hy.a.ha.hxp.h
x : ℝ
n : ℕ
⊢ 1 < 2
case hy.a.ha.hxp.h2
x : ℝ
n : ℕ
⊢ 0 < n + 2
case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π
case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)
case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1
case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2
x : ℝ n : ℕ ⊢ 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
case hy.a.ha.hxp.h2
x : ℝ
n : ℕ
⊢ 0 < n + 2
case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π
case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)
case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1
case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2
x : ℝ n : ℕ ⊢ 2 ≠ 0
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π
case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)
case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1
case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2
x : ℝ n : ℕ ⊢ 2 ≠ 0
[PROOFSTEP]
apply pi_pos
[GOAL]
case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)
case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1
case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2
x : ℝ n : ℕ ⊢ 2 ≠ 0
[PROOFSTEP]
apply pow_pos
[GOAL]
case hy.a.ha.hxp.hb.H
x : ℝ
n : ℕ
⊢ 0 < 2
case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1
case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2
x : ℝ n : ℕ ⊢ 2 ≠ 0
[PROOFSTEP]
all_goals norm_num
[GOAL]
case hy.a.ha.hxp.hb.H
x : ℝ
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1
[PROOFSTEP]
norm_num
[GOAL]
case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
n : ℕ
⊢ 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
⊢ cos (π / 4) = sqrt 2 / 2
[PROOFSTEP]
trans cos (π / 2 ^ 2)
[GOAL]
x : ℝ
⊢ cos (π / 4) = cos (π / 2 ^ 2)
x : ℝ ⊢ cos (π / 2 ^ 2) = sqrt 2 / 2
[PROOFSTEP]
congr
[GOAL]
case e_x.e_a
x : ℝ
⊢ 4 = 2 ^ 2
x : ℝ ⊢ cos (π / 2 ^ 2) = sqrt 2 / 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
⊢ cos (π / 2 ^ 2) = sqrt 2 / 2
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ sin (π / 4) = sqrt 2 / 2
[PROOFSTEP]
trans sin (π / 2 ^ 2)
[GOAL]
x : ℝ
⊢ sin (π / 4) = sin (π / 2 ^ 2)
x : ℝ ⊢ sin (π / 2 ^ 2) = sqrt 2 / 2
[PROOFSTEP]
congr
[GOAL]
case e_x.e_a
x : ℝ
⊢ 4 = 2 ^ 2
x : ℝ ⊢ sin (π / 2 ^ 2) = sqrt 2 / 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
⊢ sin (π / 2 ^ 2) = sqrt 2 / 2
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ cos (π / 8) = sqrt (2 + sqrt 2) / 2
[PROOFSTEP]
trans cos (π / 2 ^ 3)
[GOAL]
x : ℝ
⊢ cos (π / 8) = cos (π / 2 ^ 3)
x : ℝ ⊢ cos (π / 2 ^ 3) = sqrt (2 + sqrt 2) / 2
[PROOFSTEP]
congr
[GOAL]
case e_x.e_a
x : ℝ
⊢ 8 = 2 ^ 3
x : ℝ ⊢ cos (π / 2 ^ 3) = sqrt (2 + sqrt 2) / 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
⊢ cos (π / 2 ^ 3) = sqrt (2 + sqrt 2) / 2
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ sin (π / 8) = sqrt (2 - sqrt 2) / 2
[PROOFSTEP]
trans sin (π / 2 ^ 3)
[GOAL]
x : ℝ
⊢ sin (π / 8) = sin (π / 2 ^ 3)
x : ℝ ⊢ sin (π / 2 ^ 3) = sqrt (2 - sqrt 2) / 2
[PROOFSTEP]
congr
[GOAL]
case e_x.e_a
x : ℝ
⊢ 8 = 2 ^ 3
x : ℝ ⊢ sin (π / 2 ^ 3) = sqrt (2 - sqrt 2) / 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
⊢ sin (π / 2 ^ 3) = sqrt (2 - sqrt 2) / 2
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ cos (π / 16) = sqrt (2 + sqrt (2 + sqrt 2)) / 2
[PROOFSTEP]
trans cos (π / 2 ^ 4)
[GOAL]
x : ℝ
⊢ cos (π / 16) = cos (π / 2 ^ 4)
x : ℝ ⊢ cos (π / 2 ^ 4) = sqrt (2 + sqrt (2 + sqrt 2)) / 2
[PROOFSTEP]
congr
[GOAL]
case e_x.e_a
x : ℝ
⊢ 16 = 2 ^ 4
x : ℝ ⊢ cos (π / 2 ^ 4) = sqrt (2 + sqrt (2 + sqrt 2)) / 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
⊢ cos (π / 2 ^ 4) = sqrt (2 + sqrt (2 + sqrt 2)) / 2
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ sin (π / 16) = sqrt (2 - sqrt (2 + sqrt 2)) / 2
[PROOFSTEP]
trans sin (π / 2 ^ 4)
[GOAL]
x : ℝ
⊢ sin (π / 16) = sin (π / 2 ^ 4)
x : ℝ ⊢ sin (π / 2 ^ 4) = sqrt (2 - sqrt (2 + sqrt 2)) / 2
[PROOFSTEP]
congr
[GOAL]
case e_x.e_a
x : ℝ
⊢ 16 = 2 ^ 4
x : ℝ ⊢ sin (π / 2 ^ 4) = sqrt (2 - sqrt (2 + sqrt 2)) / 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
⊢ sin (π / 2 ^ 4) = sqrt (2 - sqrt (2 + sqrt 2)) / 2
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ cos (π / 32) = sqrt (2 + sqrt (2 + sqrt (2 + sqrt 2))) / 2
[PROOFSTEP]
trans cos (π / 2 ^ 5)
[GOAL]
x : ℝ
⊢ cos (π / 32) = cos (π / 2 ^ 5)
x : ℝ ⊢ cos (π / 2 ^ 5) = sqrt (2 + sqrt (2 + sqrt (2 + sqrt 2))) / 2
[PROOFSTEP]
congr
[GOAL]
case e_x.e_a
x : ℝ
⊢ 32 = 2 ^ 5
x : ℝ ⊢ cos (π / 2 ^ 5) = sqrt (2 + sqrt (2 + sqrt (2 + sqrt 2))) / 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
⊢ cos (π / 2 ^ 5) = sqrt (2 + sqrt (2 + sqrt (2 + sqrt 2))) / 2
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ sin (π / 32) = sqrt (2 - sqrt (2 + sqrt (2 + sqrt 2))) / 2
[PROOFSTEP]
trans sin (π / 2 ^ 5)
[GOAL]
x : ℝ
⊢ sin (π / 32) = sin (π / 2 ^ 5)
x : ℝ ⊢ sin (π / 2 ^ 5) = sqrt (2 - sqrt (2 + sqrt (2 + sqrt 2))) / 2
[PROOFSTEP]
congr
[GOAL]
case e_x.e_a
x : ℝ
⊢ 32 = 2 ^ 5
x : ℝ ⊢ sin (π / 2 ^ 5) = sqrt (2 - sqrt (2 + sqrt (2 + sqrt 2))) / 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
⊢ sin (π / 2 ^ 5) = sqrt (2 - sqrt (2 + sqrt (2 + sqrt 2))) / 2
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ cos (π / 3) = 1 / 2
[PROOFSTEP]
have h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0 :=
  by
  have : cos (3 * (π / 3)) = cos π := by
    congr 1
    ring
  linarith [cos_pi, cos_three_mul (π / 3)]
[GOAL]
x : ℝ
⊢ (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
[PROOFSTEP]
have : cos (3 * (π / 3)) = cos π := by
  congr 1
  ring
[GOAL]
x : ℝ
⊢ cos (3 * (π / 3)) = cos π
[PROOFSTEP]
congr 1
[GOAL]
case e_x
x : ℝ
⊢ 3 * (π / 3) = π
[PROOFSTEP]
ring
[GOAL]
x : ℝ
this : cos (3 * (π / 3)) = cos π
⊢ (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
[PROOFSTEP]
linarith [cos_pi, cos_three_mul (π / 3)]
[GOAL]
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
⊢ cos (π / 3) = 1 / 2
[PROOFSTEP]
cases' mul_eq_zero.mp h₁ with h h
[GOAL]
case inl
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : (2 * cos (π / 3) - 1) ^ 2 = 0
⊢ cos (π / 3) = 1 / 2
[PROOFSTEP]
linarith [pow_eq_zero h]
[GOAL]
case inr
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos (π / 3) = 1 / 2
[PROOFSTEP]
have : cos π < cos (π / 3) := by refine' cos_lt_cos_of_nonneg_of_le_pi _ rfl.ge _ <;> linarith [pi_pos]
[GOAL]
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos π < cos (π / 3)
[PROOFSTEP]
refine' cos_lt_cos_of_nonneg_of_le_pi _ rfl.ge _
[GOAL]
case refine'_1
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ 0 ≤ π / 3
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
case refine'_2
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ π / 3 < π
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
case inr
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
⊢ cos (π / 3) = 1 / 2
[PROOFSTEP]
linarith [cos_pi]
[GOAL]
x : ℝ
⊢ cos (π / 6) ^ 2 = 3 / 4
[PROOFSTEP]
have h1 : cos (π / 6) ^ 2 = 1 / 2 + 1 / 2 / 2 :=
  by
  convert cos_sq (π / 6) using 3
  have h2 : 2 * (π / 6) = π / 3 := by linarith
  rw [h2, cos_pi_div_three]
[GOAL]
x : ℝ
⊢ cos (π / 6) ^ 2 = 1 / 2 + 1 / 2 / 2
[PROOFSTEP]
convert cos_sq (π / 6) using 3
[GOAL]
case h.e'_3.h.e'_6.h.e'_5
x : ℝ
⊢ 1 / 2 = cos (2 * (π / 6))
[PROOFSTEP]
have h2 : 2 * (π / 6) = π / 3 := by linarith
[GOAL]
x : ℝ
⊢ 2 * (π / 6) = π / 3
[PROOFSTEP]
linarith
[GOAL]
case h.e'_3.h.e'_6.h.e'_5
x : ℝ
h2 : 2 * (π / 6) = π / 3
⊢ 1 / 2 = cos (2 * (π / 6))
[PROOFSTEP]
rw [h2, cos_pi_div_three]
[GOAL]
x : ℝ
h1 : cos (π / 6) ^ 2 = 1 / 2 + 1 / 2 / 2
⊢ cos (π / 6) ^ 2 = 3 / 4
[PROOFSTEP]
rw [← sub_eq_zero] at h1 ⊢
[GOAL]
x : ℝ
h1✝ : cos (π / 6) ^ 2 = 1 / 2 + 1 / 2 / 2
h1 : cos (π / 6) ^ 2 - (1 / 2 + 1 / 2 / 2) = 0
⊢ cos (π / 6) ^ 2 - 3 / 4 = 0
[PROOFSTEP]
convert h1 using 1
[GOAL]
case h.e'_2
x : ℝ
h1✝ : cos (π / 6) ^ 2 = 1 / 2 + 1 / 2 / 2
h1 : cos (π / 6) ^ 2 - (1 / 2 + 1 / 2 / 2) = 0
⊢ cos (π / 6) ^ 2 - 3 / 4 = cos (π / 6) ^ 2 - (1 / 2 + 1 / 2 / 2)
[PROOFSTEP]
ring
[GOAL]
x : ℝ
⊢ cos (π / 6) = sqrt 3 / 2
[PROOFSTEP]
suffices sqrt 3 = cos (π / 6) * 2 by
  field_simp [(by norm_num : 0 ≠ 2)]
  exact this.symm
[GOAL]
x : ℝ
this : sqrt 3 = cos (π / 6) * 2
⊢ cos (π / 6) = sqrt 3 / 2
[PROOFSTEP]
field_simp [(by norm_num : 0 ≠ 2)]
[GOAL]
x : ℝ
this : sqrt 3 = cos (π / 6) * 2
⊢ 0 ≠ 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
this : sqrt 3 = cos (π / 6) * 2
⊢ cos (π / 6) * 2 = sqrt 3
[PROOFSTEP]
exact this.symm
[GOAL]
x : ℝ
⊢ sqrt 3 = cos (π / 6) * 2
[PROOFSTEP]
rw [sqrt_eq_iff_sq_eq]
[GOAL]
x : ℝ
⊢ (cos (π / 6) * 2) ^ 2 = 3
[PROOFSTEP]
have h1 := (mul_right_inj' (by norm_num : (4 : ℝ) ≠ 0)).mpr sq_cos_pi_div_six
[GOAL]
x : ℝ
⊢ 4 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
h1 : 4 * cos (π / 6) ^ 2 = 4 * (3 / 4)
⊢ (cos (π / 6) * 2) ^ 2 = 3
[PROOFSTEP]
rw [← sub_eq_zero] at h1 ⊢
[GOAL]
x : ℝ
h1✝ : 4 * cos (π / 6) ^ 2 = 4 * (3 / 4)
h1 : 4 * cos (π / 6) ^ 2 - 4 * (3 / 4) = 0
⊢ (cos (π / 6) * 2) ^ 2 - 3 = 0
[PROOFSTEP]
convert h1 using 1
[GOAL]
case h.e'_2
x : ℝ
h1✝ : 4 * cos (π / 6) ^ 2 = 4 * (3 / 4)
h1 : 4 * cos (π / 6) ^ 2 - 4 * (3 / 4) = 0
⊢ (cos (π / 6) * 2) ^ 2 - 3 = 4 * cos (π / 6) ^ 2 - 4 * (3 / 4)
[PROOFSTEP]
ring
[GOAL]
case hx
x : ℝ
⊢ 0 ≤ 3
[PROOFSTEP]
norm_num
[GOAL]
case hy
x : ℝ
⊢ 0 ≤ cos (π / 6) * 2
[PROOFSTEP]
have : 0 < cos (π / 6) := by apply cos_pos_of_mem_Ioo; constructor <;> linarith [pi_pos]
[GOAL]
x : ℝ
⊢ 0 < cos (π / 6)
[PROOFSTEP]
apply cos_pos_of_mem_Ioo
[GOAL]
case hx
x : ℝ
⊢ π / 6 ∈ Ioo (-(π / 2)) (π / 2)
[PROOFSTEP]
constructor
[GOAL]
case hx.left
x : ℝ
⊢ -(π / 2) < π / 6
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
case hx.right
x : ℝ
⊢ π / 6 < π / 2
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
case hy
x : ℝ
this : 0 < cos (π / 6)
⊢ 0 ≤ cos (π / 6) * 2
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
⊢ sin (π / 6) = 1 / 2
[PROOFSTEP]
rw [← cos_pi_div_two_sub, ← cos_pi_div_three]
[GOAL]
x : ℝ
⊢ cos (π / 2 - π / 6) = cos (π / 3)
[PROOFSTEP]
congr
[GOAL]
case e_x
x : ℝ
⊢ π / 2 - π / 6 = π / 3
[PROOFSTEP]
ring
[GOAL]
x : ℝ
⊢ sin (π / 3) ^ 2 = 3 / 4
[PROOFSTEP]
rw [← cos_pi_div_two_sub, ← sq_cos_pi_div_six]
[GOAL]
x : ℝ
⊢ cos (π / 2 - π / 3) ^ 2 = cos (π / 6) ^ 2
[PROOFSTEP]
congr
[GOAL]
case e_a.e_x
x : ℝ
⊢ π / 2 - π / 3 = π / 6
[PROOFSTEP]
ring
[GOAL]
x : ℝ
⊢ sin (π / 3) = sqrt 3 / 2
[PROOFSTEP]
rw [← cos_pi_div_two_sub, ← cos_pi_div_six]
[GOAL]
x : ℝ
⊢ cos (π / 2 - π / 3) = cos (π / 6)
[PROOFSTEP]
congr
[GOAL]
case e_x
x : ℝ
⊢ π / 2 - π / 3 = π / 6
[PROOFSTEP]
ring
[GOAL]
⊢ tan (π / 4) = 1
[PROOFSTEP]
rw [tan_eq_sin_div_cos, cos_pi_div_four, sin_pi_div_four]
[GOAL]
⊢ sqrt 2 / 2 / (sqrt 2 / 2) = 1
[PROOFSTEP]
have h : sqrt 2 / 2 > 0 := by cancel_denoms
[GOAL]
⊢ sqrt 2 / 2 > 0
[PROOFSTEP]
cancel_denoms
[GOAL]
⊢ sqrt 2 / 2 > 0
[PROOFSTEP]
cancel_denoms
[GOAL]
h : sqrt 2 / 2 > 0
⊢ sqrt 2 / 2 / (sqrt 2 / 2) = 1
[PROOFSTEP]
exact div_self (ne_of_gt h)
[GOAL]
⊢ tan (π / 2) = 0
[PROOFSTEP]
simp [tan_eq_sin_div_cos]
[GOAL]
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ 0 < tan x
[PROOFSTEP]
rw [tan_eq_sin_div_cos]
[GOAL]
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ 0 < sin x / cos x
[PROOFSTEP]
exact div_pos (sin_pos_of_pos_of_lt_pi h0x (by linarith)) (cos_pos_of_mem_Ioo ⟨by linarith, hxp⟩)
[GOAL]
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ x < π
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ -(π / 2) < x
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
h0x : 0 ≤ x
hxp✝ : x ≤ π / 2
h✝ : 0 < x
hxp : x = π / 2
⊢ 0 ≤ tan x
[PROOFSTEP]
simp [hxp, tan_eq_sin_div_cos]
[GOAL]
x : ℝ
h0x : 0 ≤ x
hxp : x ≤ π / 2
hx0 : 0 = x
x✝ : x < π / 2 ∨ x = π / 2
⊢ 0 ≤ tan x
[PROOFSTEP]
simp [hx0.symm]
[GOAL]
x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
⊢ 0 < -x
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
⊢ -x < π / 2
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
⊢ 0 ≤ -x
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
⊢ -x ≤ π / 2
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ tan x < tan y
[PROOFSTEP]
rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos]
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ sin x / cos x < sin y / cos y
[PROOFSTEP]
exact
  div_lt_div (sin_lt_sin_of_lt_of_le_pi_div_two (by linarith) (le_of_lt hy₂) hxy)
    (cos_le_cos_of_nonneg_of_le_pi hx₁ (by linarith) (le_of_lt hxy))
    (sin_nonneg_of_nonneg_of_le_pi (by linarith) (by linarith)) (cos_pos_of_mem_Ioo ⟨by linarith, hy₂⟩)
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ -(π / 2) ≤ x
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ y ≤ π
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ 0 ≤ y
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ y ≤ π
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ -(π / 2) < y
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hx₁ : -(π / 2) < x
hy₂ : y < π / 2
hxy : x < y
hx0 : x ≤ 0
hy0 : y ≤ 0
⊢ -tan y < -tan x
[PROOFSTEP]
rw [← tan_neg, ← tan_neg]
[GOAL]
x y : ℝ
hx₁ : -(π / 2) < x
hy₂ : y < π / 2
hxy : x < y
hx0 : x ≤ 0
hy0 : y ≤ 0
⊢ tan (-y) < tan (-x)
[PROOFSTEP]
exact tan_lt_tan_of_nonneg_of_lt_pi_div_two (neg_nonneg.2 hy0) (neg_lt.2 hx₁) (neg_lt_neg hxy)
[GOAL]
x y : ℝ
hx₁ : -(π / 2) < x
hy₂ : y < π / 2
hxy : x < y
hx0 : x ≤ 0
hy0✝ : 0 ≤ y
hy0 : 0 = y
⊢ tan x < tan y
[PROOFSTEP]
rw [← hy0, tan_zero]
[GOAL]
x y : ℝ
hx₁ : -(π / 2) < x
hy₂ : y < π / 2
hxy : x < y
hx0 : x ≤ 0
hy0✝ : 0 ≤ y
hy0 : 0 = y
⊢ tan x < 0
[PROOFSTEP]
exact tan_neg_of_neg_of_pi_div_two_lt (hy0.symm ▸ hxy) hx₁
[GOAL]
x y : ℝ
hx₁ : -(π / 2) < x
hy₂ : y < π / 2
hxy : x < y
hx0 : 0 ≤ x
hy0 : y ≤ 0
⊢ tan x < tan y
[PROOFSTEP]
linarith
[GOAL]
⊢ Function.Periodic tan π
[PROOFSTEP]
simpa only [Function.Periodic, tan_eq_sin_div_cos] using sin_antiperiodic.div cos_antiperiodic
[GOAL]
⊢ tan π = 0
[PROOFSTEP]
rw [tan_periodic.eq, tan_zero]
[GOAL]
x : ℝ
⊢ tan (π / 2 - x) = (tan x)⁻¹
[PROOFSTEP]
rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]
[GOAL]
⊢ Tendsto sin (𝓝[Iio (π / 2)] (π / 2)) (𝓝 1)
[PROOFSTEP]
convert continuous_sin.continuousWithinAt.tendsto
[GOAL]
case h.e'_5.h.e'_3
⊢ 1 = sin (π / 2)
[PROOFSTEP]
simp
[GOAL]
⊢ Tendsto cos (𝓝[Iio (π / 2)] (π / 2)) (𝓝[Ioi 0] 0)
[PROOFSTEP]
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
[GOAL]
case h1
⊢ Tendsto cos (𝓝[Iio (π / 2)] (π / 2)) (𝓝 0)
[PROOFSTEP]
convert continuous_cos.continuousWithinAt.tendsto
[GOAL]
case h.e'_5.h.e'_3
⊢ 0 = cos (π / 2)
[PROOFSTEP]
simp
[GOAL]
case h2
⊢ ∀ᶠ (x : ℝ) in 𝓝[Iio (π / 2)] (π / 2), cos x ∈ Ioi 0
[PROOFSTEP]
filter_upwards [Ioo_mem_nhdsWithin_Iio (right_mem_Ioc.mpr (neg_lt_self pi_div_two_pos))] with x hx using
  cos_pos_of_mem_Ioo hx
[GOAL]
⊢ Tendsto tan (𝓝[Iio (π / 2)] (π / 2)) atTop
[PROOFSTEP]
convert tendsto_cos_pi_div_two.inv_tendsto_zero.atTop_mul zero_lt_one tendsto_sin_pi_div_two using 1
[GOAL]
case h.e'_3
⊢ tan = fun x => cos⁻¹ x * sin x
[PROOFSTEP]
simp only [Pi.inv_apply, ← div_eq_inv_mul, ← tan_eq_sin_div_cos]
[GOAL]
⊢ Tendsto sin (𝓝[Ioi (-(π / 2))] (-(π / 2))) (𝓝 (-1))
[PROOFSTEP]
convert continuous_sin.continuousWithinAt.tendsto using 2
[GOAL]
case h.e'_5.h.e'_3
⊢ -1 = sin (-(π / 2))
[PROOFSTEP]
simp
[GOAL]
⊢ Tendsto cos (𝓝[Ioi (-(π / 2))] (-(π / 2))) (𝓝[Ioi 0] 0)
[PROOFSTEP]
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
[GOAL]
case h1
⊢ Tendsto cos (𝓝[Ioi (-(π / 2))] (-(π / 2))) (𝓝 0)
[PROOFSTEP]
convert continuous_cos.continuousWithinAt.tendsto
[GOAL]
case h.e'_5.h.e'_3
⊢ 0 = cos (-(π / 2))
[PROOFSTEP]
simp
[GOAL]
case h2
⊢ ∀ᶠ (x : ℝ) in 𝓝[Ioi (-(π / 2))] (-(π / 2)), cos x ∈ Ioi 0
[PROOFSTEP]
filter_upwards [Ioo_mem_nhdsWithin_Ioi (left_mem_Ico.mpr (neg_lt_self pi_div_two_pos))] with x hx using
  cos_pos_of_mem_Ioo hx
[GOAL]
⊢ Tendsto tan (𝓝[Ioi (-(π / 2))] (-(π / 2))) atBot
[PROOFSTEP]
convert tendsto_cos_neg_pi_div_two.inv_tendsto_zero.atTop_mul_neg (by norm_num) tendsto_sin_neg_pi_div_two using 1
[GOAL]
⊢ -1 < 0
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_3
⊢ tan = fun x => cos⁻¹ x * sin x
[PROOFSTEP]
simp only [Pi.inv_apply, ← div_eq_inv_mul, ← tan_eq_sin_div_cos]
[GOAL]
z : ℂ
⊢ sin z = 0 ↔ cos z = 1 ∨ cos z = -1
[PROOFSTEP]
rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, ← sub_eq_iff_eq_add, sub_self]
[GOAL]
z : ℂ
⊢ sin z = 0 ↔ 0 = sin z * sin z
[PROOFSTEP]
exact ⟨fun h => by rw [h, mul_zero], eq_zero_of_mul_self_eq_zero ∘ Eq.symm⟩
[GOAL]
z : ℂ
h : sin z = 0
⊢ 0 = sin z * sin z
[PROOFSTEP]
rw [h, mul_zero]
[GOAL]
⊢ cos (↑π / 2) = ↑(Real.cos (π / 2))
[PROOFSTEP]
rw [ofReal_cos]
[GOAL]
⊢ cos (↑π / 2) = cos ↑(π / 2)
[PROOFSTEP]
simp
[GOAL]
⊢ ↑(Real.cos (π / 2)) = 0
[PROOFSTEP]
simp
[GOAL]
⊢ sin (↑π / 2) = ↑(Real.sin (π / 2))
[PROOFSTEP]
rw [ofReal_sin]
[GOAL]
⊢ sin (↑π / 2) = sin ↑(π / 2)
[PROOFSTEP]
simp
[GOAL]
⊢ ↑(Real.sin (π / 2)) = 1
[PROOFSTEP]
simp
[GOAL]
⊢ sin ↑π = 0
[PROOFSTEP]
rw [← ofReal_sin, Real.sin_pi]
[GOAL]
⊢ ↑0 = 0
[PROOFSTEP]
simp
[GOAL]
⊢ cos ↑π = -1
[PROOFSTEP]
rw [← ofReal_cos, Real.cos_pi]
[GOAL]
⊢ ↑(-1) = -1
[PROOFSTEP]
simp
[GOAL]
⊢ sin (2 * ↑π) = 0
[PROOFSTEP]
simp [two_mul, sin_add]
[GOAL]
⊢ cos (2 * ↑π) = 1
[PROOFSTEP]
simp [two_mul, cos_add]
[GOAL]
⊢ Function.Antiperiodic sin ↑π
[PROOFSTEP]
simp [sin_add]
[GOAL]
⊢ Function.Antiperiodic cos ↑π
[PROOFSTEP]
simp [cos_add]
[GOAL]
n : ℕ
⊢ cos (↑n * (2 * ↑π) + ↑π) = -1
[PROOFSTEP]
simpa only [cos_zero] using (cos_periodic.nat_mul n).add_antiperiod_eq cos_antiperiodic
[GOAL]
n : ℤ
⊢ cos (↑n * (2 * ↑π) + ↑π) = -1
[PROOFSTEP]
simpa only [cos_zero] using (cos_periodic.int_mul n).add_antiperiod_eq cos_antiperiodic
[GOAL]
n : ℕ
⊢ cos (↑n * (2 * ↑π) - ↑π) = -1
[PROOFSTEP]
simpa only [cos_zero] using (cos_periodic.nat_mul n).sub_antiperiod_eq cos_antiperiodic
[GOAL]
n : ℤ
⊢ cos (↑n * (2 * ↑π) - ↑π) = -1
[PROOFSTEP]
simpa only [cos_zero] using (cos_periodic.int_mul n).sub_antiperiod_eq cos_antiperiodic
[GOAL]
x : ℂ
⊢ sin (x + ↑π / 2) = cos x
[PROOFSTEP]
simp [sin_add]
[GOAL]
x : ℂ
⊢ sin (x - ↑π / 2) = -cos x
[PROOFSTEP]
simp [sub_eq_add_neg, sin_add]
[GOAL]
x : ℂ
⊢ sin (↑π / 2 - x) = cos x
[PROOFSTEP]
simp [sub_eq_add_neg, sin_add]
[GOAL]
x : ℂ
⊢ cos (x + ↑π / 2) = -sin x
[PROOFSTEP]
simp [cos_add]
[GOAL]
x : ℂ
⊢ cos (x - ↑π / 2) = sin x
[PROOFSTEP]
simp [sub_eq_add_neg, cos_add]
[GOAL]
x : ℂ
⊢ cos (↑π / 2 - x) = sin x
[PROOFSTEP]
rw [← cos_neg, neg_sub, cos_sub_pi_div_two]
[GOAL]
⊢ Function.Periodic tan ↑π
[PROOFSTEP]
simpa only [tan_eq_sin_div_cos] using sin_antiperiodic.div cos_antiperiodic
[GOAL]
x : ℂ
⊢ tan (↑π / 2 - x) = (tan x)⁻¹
[PROOFSTEP]
rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]
[GOAL]
⊢ Function.Antiperiodic exp (↑π * I)
[PROOFSTEP]
simp [exp_add, exp_mul_I]
[GOAL]
⊢ Function.Antiperiodic (fun x => exp (x * I)) ↑π
[PROOFSTEP]
simpa only [mul_inv_cancel_right₀ I_ne_zero] using exp_antiperiodic.mul_const I_ne_zero
[GOAL]
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
⊢ ↑abs (exp (↑a * (exp z + exp (-z)))) ≤ Real.exp (a * Real.cos b * Real.exp |z.re|)
[PROOFSTEP]
simp only [abs_exp, Real.exp_le_exp, ofReal_mul_re, add_re, exp_re, neg_im, Real.cos_neg, ← add_mul, mul_assoc,
  mul_comm (Real.cos b), neg_re, ← Real.cos_abs z.im]
[GOAL]
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
⊢ a * ((Real.exp z.re + Real.exp (-z.re)) * Real.cos |z.im|) ≤ a * (Real.exp |z.re| * Real.cos b)
[PROOFSTEP]
have : Real.exp |z.re| ≤ Real.exp z.re + Real.exp (-z.re) :=
  apply_abs_le_add_of_nonneg (fun x => (Real.exp_pos x).le) z.re
[GOAL]
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : Real.exp |z.re| ≤ Real.exp z.re + Real.exp (-z.re)
⊢ a * ((Real.exp z.re + Real.exp (-z.re)) * Real.cos |z.im|) ≤ a * (Real.exp |z.re| * Real.cos b)
[PROOFSTEP]
refine' mul_le_mul_of_nonpos_left (mul_le_mul this _ _ ((Real.exp_pos _).le.trans this)) ha
[GOAL]
case refine'_1
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : Real.exp |z.re| ≤ Real.exp z.re + Real.exp (-z.re)
⊢ Real.cos b ≤ Real.cos |z.im|
[PROOFSTEP]
exact Real.cos_le_cos_of_nonneg_of_le_pi (_root_.abs_nonneg _) (hb.trans <| half_le_self <| Real.pi_pos.le) hz
[GOAL]
case refine'_2
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : Real.exp |z.re| ≤ Real.exp z.re + Real.exp (-z.re)
⊢ 0 ≤ Real.cos b
[PROOFSTEP]
refine' Real.cos_nonneg_of_mem_Icc ⟨_, hb⟩
[GOAL]
case refine'_2
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : Real.exp |z.re| ≤ Real.exp z.re + Real.exp (-z.re)
⊢ -(π / 2) ≤ b
[PROOFSTEP]
exact (neg_nonpos.2 <| Real.pi_div_two_pos.le).trans ((_root_.abs_nonneg _).trans hz)


[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
⊢ ∀ (e : PE ≃ᵢ PE), ↑e x = x → ↑e y = y → ↑e (midpoint ℝ x y) = midpoint ℝ x y
[PROOFSTEP]
set z := midpoint ℝ x y
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
⊢ ∀ (e : PE ≃ᵢ PE), ↑e x = x → ↑e y = y → ↑e z = z
[PROOFSTEP]
set s := {e : PE ≃ᵢ PE | e x = x ∧ e y = y}
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
⊢ ∀ (e : PE ≃ᵢ PE), ↑e x = x → ↑e y = y → ↑e z = z
[PROOFSTEP]
haveI : Nonempty s :=
  ⟨⟨IsometryEquiv.refl PE, rfl, rfl⟩⟩
    -- On the one hand, `e` cannot send the midpoint `z` of `[x, y]` too far
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
⊢ ∀ (e : PE ≃ᵢ PE), ↑e x = x → ↑e y = y → ↑e z = z
[PROOFSTEP]
have h_bdd : BddAbove (range fun e : s => dist ((e : PE ≃ᵢ PE) z) z) :=
  by
  refine' ⟨dist x z + dist x z, forall_range_iff.2 <| Subtype.forall.2 _⟩
  rintro e ⟨hx, _⟩
  calc
    dist (e z) z ≤ dist (e z) x + dist x z := dist_triangle (e z) x z
    _ = dist (e x) (e z) + dist x z := by rw [hx, dist_comm]
    _ = dist x z + dist x z := by
      erw [e.dist_eq x z]
        -- On the other hand, consider the map `f : (E ≃ᵢ E) → (E ≃ᵢ E)`
          -- sending each `e` to `R ∘ e⁻¹ ∘ R ∘ e`, where `R` is the point reflection in the
          -- midpoint `z` of `[x, y]`.
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
⊢ BddAbove (range fun e => dist (↑↑e z) z)
[PROOFSTEP]
refine' ⟨dist x z + dist x z, forall_range_iff.2 <| Subtype.forall.2 _⟩
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
⊢ ∀ (a : PE ≃ᵢ PE) (b : a ∈ s), dist (↑↑{ val := a, property := b } z) z ≤ dist x z + dist x z
[PROOFSTEP]
rintro e ⟨hx, _⟩
[GOAL]
case intro
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
e : PE ≃ᵢ PE
hx : ↑e x = x
right✝ : ↑e y = y
⊢ dist (↑↑{ val := e, property := (_ : ↑e x = x ∧ ↑e y = y) } z) z ≤ dist x z + dist x z
[PROOFSTEP]
calc
  dist (e z) z ≤ dist (e z) x + dist x z := dist_triangle (e z) x z
  _ = dist (e x) (e z) + dist x z := by rw [hx, dist_comm]
  _ = dist x z + dist x z := by
    erw [e.dist_eq x z]
      -- On the other hand, consider the map `f : (E ≃ᵢ E) → (E ≃ᵢ E)`
        -- sending each `e` to `R ∘ e⁻¹ ∘ R ∘ e`, where `R` is the point reflection in the
        -- midpoint `z` of `[x, y]`.
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
e : PE ≃ᵢ PE
hx : ↑e x = x
right✝ : ↑e y = y
⊢ dist (↑e z) x + dist x z = dist (↑e x) (↑e z) + dist x z
[PROOFSTEP]
rw [hx, dist_comm]
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
e : PE ≃ᵢ PE
hx : ↑e x = x
right✝ : ↑e y = y
⊢ dist (↑e x) (↑e z) + dist x z = dist x z + dist x z
[PROOFSTEP]
erw [e.dist_eq x z]
  -- On the other hand, consider the map `f : (E ≃ᵢ E) → (E ≃ᵢ E)`
    -- sending each `e` to `R ∘ e⁻¹ ∘ R ∘ e`, where `R` is the point reflection in the
    -- midpoint `z` of `[x, y]`.
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
⊢ ∀ (e : PE ≃ᵢ PE), ↑e x = x → ↑e y = y → ↑e z = z
[PROOFSTEP]
set R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
⊢ ∀ (e : PE ≃ᵢ PE), ↑e x = x → ↑e y = y → ↑e z = z
[PROOFSTEP]
set f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
⊢ ∀ (e : PE ≃ᵢ PE), ↑e x = x → ↑e y = y → ↑e z = z
[PROOFSTEP]
have hf_dist : ∀ e, dist (f e z) z = 2 * dist (e z) z :=
  by
  intro e
  dsimp
  rw [dist_pointReflection_fixed, ← e.dist_eq, e.apply_symm_apply, dist_pointReflection_self_real, dist_comm]
    -- Also note that `f` maps `s` to itself
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
⊢ ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
[PROOFSTEP]
intro e
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
e : PE ≃ᵢ PE
⊢ dist (↑(f e) z) z = 2 * dist (↑e z) z
[PROOFSTEP]
dsimp
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
e : PE ≃ᵢ PE
⊢ dist
      (↑(pointReflection ℝ (midpoint ℝ x y))
        (↑(IsometryEquiv.symm e) (↑(pointReflection ℝ (midpoint ℝ x y)) (↑e (midpoint ℝ x y)))))
      (midpoint ℝ x y) =
    2 * dist (↑e (midpoint ℝ x y)) (midpoint ℝ x y)
[PROOFSTEP]
rw [dist_pointReflection_fixed, ← e.dist_eq, e.apply_symm_apply, dist_pointReflection_self_real, dist_comm]
  -- Also note that `f` maps `s` to itself
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
⊢ ∀ (e : PE ≃ᵢ PE), ↑e x = x → ↑e y = y → ↑e z = z
[PROOFSTEP]
have hf_maps_to : MapsTo f s s := by
  rintro e ⟨hx, hy⟩
  constructor <;>
    simp [hx, hy, e.symm_apply_eq.2 hx.symm, e.symm_apply_eq.2 hy.symm]
      -- Therefore, `dist (e z) z = 0` for all `e ∈ s`.
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
⊢ MapsTo f s s
[PROOFSTEP]
rintro e ⟨hx, hy⟩
[GOAL]
case intro
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
e : PE ≃ᵢ PE
hx : ↑e x = x
hy : ↑e y = y
⊢ f e ∈ s
[PROOFSTEP]
constructor
[GOAL]
case intro.left
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
e : PE ≃ᵢ PE
hx : ↑e x = x
hy : ↑e y = y
⊢ ↑(f e) x = x
[PROOFSTEP]
simp [hx, hy, e.symm_apply_eq.2 hx.symm, e.symm_apply_eq.2 hy.symm]
  -- Therefore, `dist (e z) z = 0` for all `e ∈ s`.
[GOAL]
case intro.right
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
e : PE ≃ᵢ PE
hx : ↑e x = x
hy : ↑e y = y
⊢ ↑(f e) y = y
[PROOFSTEP]
simp [hx, hy, e.symm_apply_eq.2 hx.symm, e.symm_apply_eq.2 hy.symm]
  -- Therefore, `dist (e z) z = 0` for all `e ∈ s`.
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
hf_maps_to : MapsTo f s s
⊢ ∀ (e : PE ≃ᵢ PE), ↑e x = x → ↑e y = y → ↑e z = z
[PROOFSTEP]
set c := ⨆ e : s, dist ((e : PE ≃ᵢ PE) z) z
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : ↑s), dist (↑↑e z) z
⊢ ∀ (e : PE ≃ᵢ PE), ↑e x = x → ↑e y = y → ↑e z = z
[PROOFSTEP]
have : c ≤ c / 2 := by
  apply ciSup_le
  rintro ⟨e, he⟩
  simp only [Subtype.coe_mk, le_div_iff' (zero_lt_two' ℝ), ← hf_dist]
  exact le_ciSup h_bdd ⟨f e, hf_maps_to he⟩
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : ↑s), dist (↑↑e z) z
⊢ c ≤ c / 2
[PROOFSTEP]
apply ciSup_le
[GOAL]
case H
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : ↑s), dist (↑↑e z) z
⊢ ∀ (x : ↑s), dist (↑↑x z) z ≤ c / 2
[PROOFSTEP]
rintro ⟨e, he⟩
[GOAL]
case H.mk
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : ↑s), dist (↑↑e z) z
e : PE ≃ᵢ PE
he : e ∈ s
⊢ dist (↑↑{ val := e, property := he } z) z ≤ c / 2
[PROOFSTEP]
simp only [Subtype.coe_mk, le_div_iff' (zero_lt_two' ℝ), ← hf_dist]
[GOAL]
case H.mk
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : ↑s), dist (↑↑e z) z
e : PE ≃ᵢ PE
he : e ∈ s
⊢ dist
      (↑(IsometryEquiv.trans
            (IsometryEquiv.trans (IsometryEquiv.trans e (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y))))
              (IsometryEquiv.symm e))
            (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y))))
        (midpoint ℝ x y))
      (midpoint ℝ x y) ≤
    ⨆ (e : ↑{e | ↑e x = x ∧ ↑e y = y}), dist (↑↑e (midpoint ℝ x y)) (midpoint ℝ x y)
[PROOFSTEP]
exact le_ciSup h_bdd ⟨f e, hf_maps_to he⟩
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this✝ : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : ↑s), dist (↑↑e z) z
this : c ≤ c / 2
⊢ ∀ (e : PE ≃ᵢ PE), ↑e x = x → ↑e y = y → ↑e z = z
[PROOFSTEP]
replace : c ≤ 0
[GOAL]
case this
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this✝ : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : ↑s), dist (↑↑e z) z
this : c ≤ c / 2
⊢ c ≤ 0
[PROOFSTEP]
linarith
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this✝ : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : ↑s), dist (↑↑e z) z
this : c ≤ 0
⊢ ∀ (e : PE ≃ᵢ PE), ↑e x = x → ↑e y = y → ↑e z = z
[PROOFSTEP]
refine' fun e hx hy => dist_le_zero.1 (le_trans _ this)
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | ↑e x = x ∧ ↑e y = y}
this✝ : Nonempty ↑s
h_bdd : BddAbove (range fun e => dist (↑↑e z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE :=
  fun e => IsometryEquiv.trans (IsometryEquiv.trans (IsometryEquiv.trans e R) (IsometryEquiv.symm e)) R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist (↑(f e) z) z = 2 * dist (↑e z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : ↑s), dist (↑↑e z) z
this : c ≤ 0
e : PE ≃ᵢ PE
hx : ↑e x = x
hy : ↑e y = y
⊢ dist (↑e z) z ≤ c
[PROOFSTEP]
exact le_ciSup h_bdd ⟨e, hx, hy⟩
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
⊢ ↑f (midpoint ℝ x y) = midpoint ℝ (↑f x) (↑f y)
[PROOFSTEP]
set e : PE ≃ᵢ PE :=
  ((f.trans <| (pointReflection ℝ <| midpoint ℝ (f x) (f y)).toIsometryEquiv).trans f.symm).trans
    (pointReflection ℝ <| midpoint ℝ x y).toIsometryEquiv
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  IsometryEquiv.trans
    (IsometryEquiv.trans (IsometryEquiv.trans f (toIsometryEquiv (pointReflection ℝ (midpoint ℝ (↑f x) (↑f y)))))
      (IsometryEquiv.symm f))
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
⊢ ↑f (midpoint ℝ x y) = midpoint ℝ (↑f x) (↑f y)
[PROOFSTEP]
have hx : e x = x := by simp
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  IsometryEquiv.trans
    (IsometryEquiv.trans (IsometryEquiv.trans f (toIsometryEquiv (pointReflection ℝ (midpoint ℝ (↑f x) (↑f y)))))
      (IsometryEquiv.symm f))
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
⊢ ↑e x = x
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  IsometryEquiv.trans
    (IsometryEquiv.trans (IsometryEquiv.trans f (toIsometryEquiv (pointReflection ℝ (midpoint ℝ (↑f x) (↑f y)))))
      (IsometryEquiv.symm f))
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
hx : ↑e x = x
⊢ ↑f (midpoint ℝ x y) = midpoint ℝ (↑f x) (↑f y)
[PROOFSTEP]
have hy : e y = y := by simp
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  IsometryEquiv.trans
    (IsometryEquiv.trans (IsometryEquiv.trans f (toIsometryEquiv (pointReflection ℝ (midpoint ℝ (↑f x) (↑f y)))))
      (IsometryEquiv.symm f))
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
hx : ↑e x = x
⊢ ↑e y = y
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  IsometryEquiv.trans
    (IsometryEquiv.trans (IsometryEquiv.trans f (toIsometryEquiv (pointReflection ℝ (midpoint ℝ (↑f x) (↑f y)))))
      (IsometryEquiv.symm f))
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
hx : ↑e x = x
hy : ↑e y = y
⊢ ↑f (midpoint ℝ x y) = midpoint ℝ (↑f x) (↑f y)
[PROOFSTEP]
have hm := e.midpoint_fixed hx hy
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  IsometryEquiv.trans
    (IsometryEquiv.trans (IsometryEquiv.trans f (toIsometryEquiv (pointReflection ℝ (midpoint ℝ (↑f x) (↑f y)))))
      (IsometryEquiv.symm f))
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
hx : ↑e x = x
hy : ↑e y = y
hm : ↑e (midpoint ℝ x y) = midpoint ℝ x y
⊢ ↑f (midpoint ℝ x y) = midpoint ℝ (↑f x) (↑f y)
[PROOFSTEP]
simp only [trans_apply] at hm
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  IsometryEquiv.trans
    (IsometryEquiv.trans (IsometryEquiv.trans f (toIsometryEquiv (pointReflection ℝ (midpoint ℝ (↑f x) (↑f y)))))
      (IsometryEquiv.symm f))
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
hx : ↑e x = x
hy : ↑e y = y
hm :
  ↑(toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
      (↑(IsometryEquiv.symm f)
        (↑(toIsometryEquiv (pointReflection ℝ (midpoint ℝ (↑f x) (↑f y)))) (↑f (midpoint ℝ x y)))) =
    midpoint ℝ x y
⊢ ↑f (midpoint ℝ x y) = midpoint ℝ (↑f x) (↑f y)
[PROOFSTEP]
rwa [← eq_symm_apply, toIsometryEquiv_symm, pointReflection_symm, coe_toIsometryEquiv, coe_toIsometryEquiv,
  pointReflection_self, symm_apply_eq, @pointReflection_fixed_iff] at hm
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : E ≃ᵢ F
h0 : ↑f 0 = 0
src✝ : E →L[ℝ] F :=
  AddMonoidHom.toRealLinearMap
    (AddMonoidHom.ofMapMidpoint ℝ ℝ (↑f) h0 (_ : ∀ (x y : E), ↑f (midpoint ℝ x y) = midpoint ℝ (↑f x) (↑f y)))
    (_ : Continuous ↑f)
x : E
⊢ ‖↑f x‖ = ‖x‖
[PROOFSTEP]
simp only [← dist_zero_right, ← h0, f.dist_eq]
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : E ≃ᵢ F
⊢ ↑(IsometryEquiv.trans f (IsometryEquiv.symm (addRight (↑f 0)))) 0 = 0
[PROOFSTEP]
simpa only [sub_eq_add_neg] using sub_self (f 0)
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
p : PE
⊢ ↑f p =
    ↑(toRealLinearIsometryEquiv
            (IsometryEquiv.trans (vaddConst (Classical.arbitrary PE))
              (IsometryEquiv.trans f (IsometryEquiv.symm (vaddConst (↑f (Classical.arbitrary PE)))))))
        (p -ᵥ Classical.arbitrary PE) +ᵥ
      ↑f (Classical.arbitrary PE)
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
⊢ toIsometryEquiv (toRealAffineIsometryEquiv f) = f
[PROOFSTEP]
ext
[GOAL]
case H
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x✝ : PE
⊢ ↑(toIsometryEquiv (toRealAffineIsometryEquiv f)) x✝ = ↑f x✝
[PROOFSTEP]
rfl


[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
⊢ CompactSpace ↑(characterSpace 𝕜 A)
[PROOFSTEP]
rw [← isCompact_iff_compactSpace]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
⊢ IsCompact (characterSpace 𝕜 A)
[PROOFSTEP]
have h : characterSpace 𝕜 A ⊆ toNormedDual ⁻¹' Metric.closedBall 0 ‖(1 : A)‖ :=
  by
  intro φ hφ
  rw [Set.mem_preimage, mem_closedBall_zero_iff]
  exact (norm_le_norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ : _)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
⊢ characterSpace 𝕜 A ⊆ ↑toNormedDual ⁻¹' Metric.closedBall 0 ‖1‖
[PROOFSTEP]
intro φ hφ
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
φ : WeakDual 𝕜 A
hφ : φ ∈ characterSpace 𝕜 A
⊢ φ ∈ ↑toNormedDual ⁻¹' Metric.closedBall 0 ‖1‖
[PROOFSTEP]
rw [Set.mem_preimage, mem_closedBall_zero_iff]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
φ : WeakDual 𝕜 A
hφ : φ ∈ characterSpace 𝕜 A
⊢ ‖↑toNormedDual φ‖ ≤ ‖1‖
[PROOFSTEP]
exact (norm_le_norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ : _)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
h : characterSpace 𝕜 A ⊆ ↑toNormedDual ⁻¹' Metric.closedBall 0 ‖1‖
⊢ IsCompact (characterSpace 𝕜 A)
[PROOFSTEP]
exact isCompact_of_isClosed_subset (isCompact_closedBall 𝕜 0 _) CharacterSpace.isClosed h


[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.239
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : E
h : SameRay ℝ x y
⊢ ‖x + y‖ = ‖x‖ + ‖y‖
[PROOFSTEP]
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.239
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ ‖a • u + b • u‖ = ‖a • u‖ + ‖b • u‖
[PROOFSTEP]
rw [← add_smul, norm_smul_of_nonneg (add_nonneg ha hb), norm_smul_of_nonneg ha, norm_smul_of_nonneg hb, add_mul]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.3876
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : E
h : SameRay ℝ x y
⊢ ‖x - y‖ = |‖x‖ - ‖y‖|
[PROOFSTEP]
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.3876
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
[PROOFSTEP]
wlog hab : b ≤ a with H
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.3876
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
H :
  ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type ?u.3876}
    [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
[PROOFSTEP]
rw [SameRay.sameRay_comm] at h
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.3876
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H :
  ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type ?u.3876}
    [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
[PROOFSTEP]
rw [norm_sub_rev, abs_sub_comm]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.3876
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H :
  ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type ?u.3876}
    [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖b • u - a • u‖ = |‖b • u‖ - ‖a • u‖|
[PROOFSTEP]
have := @H E _ _ ℝ
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H :
  ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type}
    [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
this :
  ∀ [inst : NormedAddCommGroup ℝ] [inst : NormedSpace ℝ ℝ] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
⊢ ‖b • u - a • u‖ = |‖b • u‖ - ‖a • u‖|
[PROOFSTEP]
exact this u b a hb ha h (le_of_not_le hab)
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab : b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
[PROOFSTEP]
rw [← sub_nonneg] at hab
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab✝ : b ≤ a
hab : 0 ≤ a - b
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
[PROOFSTEP]
rw [← sub_smul, norm_smul_of_nonneg hab, norm_smul_of_nonneg ha, norm_smul_of_nonneg hb, ← sub_mul,
  abs_of_nonneg (mul_nonneg hab (norm_nonneg _))]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.8734
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : E
h : SameRay ℝ x y
⊢ ‖x‖ • y = ‖y‖ • x
[PROOFSTEP]
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.8734
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ ‖a • u‖ • b • u = ‖b • u‖ • a • u
[PROOFSTEP]
simp only [norm_smul_of_nonneg, *, mul_smul]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.8734
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ a • ‖u‖ • b • u = b • ‖u‖ • a • u
[PROOFSTEP]
rw [smul_comm, smul_comm b, smul_comm a b u]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
⊢ Set.InjOn Norm.norm {y | SameRay ℝ x y}
[PROOFSTEP]
rintro y hy z hz h
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y✝ : F
hx : x ≠ 0
y : F
hy : y ∈ {y | SameRay ℝ x y}
z : F
hz : z ∈ {y | SameRay ℝ x y}
h : ‖y‖ = ‖z‖
⊢ y = z
[PROOFSTEP]
rcases hy.exists_nonneg_left hx with ⟨r, hr, rfl⟩
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
z : F
hz : z ∈ {y | SameRay ℝ x y}
r : ℝ
hr : 0 ≤ r
hy : r • x ∈ {y | SameRay ℝ x y}
h : ‖r • x‖ = ‖z‖
⊢ r • x = z
[PROOFSTEP]
rcases hz.exists_nonneg_left hx with ⟨s, hs, rfl⟩
[GOAL]
case intro.intro.intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
r : ℝ
hr : 0 ≤ r
hy : r • x ∈ {y | SameRay ℝ x y}
s : ℝ
hs : 0 ≤ s
hz : s • x ∈ {y | SameRay ℝ x y}
h : ‖r • x‖ = ‖s • x‖
⊢ r • x = s • x
[PROOFSTEP]
rw [norm_smul, norm_smul, mul_left_inj' (norm_ne_zero_iff.2 hx), norm_of_nonneg hr, norm_of_nonneg hs] at h
[GOAL]
case intro.intro.intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
r : ℝ
hr : 0 ≤ r
hy : r • x ∈ {y | SameRay ℝ x y}
s : ℝ
hs : 0 ≤ s
hz : s • x ∈ {y | SameRay ℝ x y}
h : r = s
⊢ r • x = s • x
[PROOFSTEP]
rw [h]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hy : y ≠ 0
⊢ Set.InjOn Norm.norm {x | SameRay ℝ x y}
[PROOFSTEP]
simpa only [SameRay.sameRay_comm] using norm_injOn_ray_left hy
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
[PROOFSTEP]
rw [inv_smul_eq_iff₀, smul_comm, eq_comm, inv_smul_eq_iff₀, sameRay_iff_norm_smul_eq]
[GOAL]
case ha
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖y‖ ≠ 0
[PROOFSTEP]
rwa [norm_ne_zero_iff]
[GOAL]
case ha
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x‖ ≠ 0
[PROOFSTEP]
rwa [norm_ne_zero_iff]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case inl
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
y : F
⊢ SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ ‖0‖⁻¹ • 0 = ‖y‖⁻¹ • y
[PROOFSTEP]
simp [SameRay.zero_left]
[GOAL]
case inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy)
[GOAL]
case inr.inl
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ ‖x‖⁻¹ • x = ‖0‖⁻¹ • 0
[PROOFSTEP]
simp [SameRay.zero_right]
[GOAL]
case inr.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
[PROOFSTEP]
simp only [sameRay_iff_inv_norm_smul_eq_of_ne hx hy, *, false_or_iff]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
⊢ SameRay ℝ x y ↔ x = y
[PROOFSTEP]
obtain rfl | hy := eq_or_ne y 0
[GOAL]
case inl
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
h : ‖x‖ = ‖0‖
⊢ SameRay ℝ x 0 ↔ x = 0
[PROOFSTEP]
rw [norm_zero, norm_eq_zero] at h
[GOAL]
case inl
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
h : x = 0
⊢ SameRay ℝ x 0 ↔ x = 0
[PROOFSTEP]
exact iff_of_true (SameRay.zero_right _) h
[GOAL]
case inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = y
[PROOFSTEP]
exact ⟨fun hxy => norm_injOn_ray_right hy hxy SameRay.rfl h, fun hxy => hxy ▸ SameRay.rfl⟩


[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
E : Type u_2
inst✝ : NormedAddCommGroup E
z : E
⊢ ‖↑‖z‖‖ = ‖z‖
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ‖(↑‖x‖)⁻¹ • x‖ = 1
[PROOFSTEP]
have : ‖x‖ ≠ 0 := by simp [hx]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ‖x‖ ≠ 0
[PROOFSTEP]
simp [hx]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖(↑‖x‖)⁻¹ • x‖ = 1
[PROOFSTEP]
field_simp [norm_smul]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
⊢ ‖(↑r * (↑‖x‖)⁻¹) • x‖ = r
[PROOFSTEP]
have : ‖x‖ ≠ 0 := by simp [hx]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
⊢ ‖x‖ ≠ 0
[PROOFSTEP]
simp [hx]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖(↑r * (↑‖x‖)⁻¹) • x‖ = r
[PROOFSTEP]
field_simp [norm_smul, r_nonneg, isROrC_simps]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
[PROOFSTEP]
by_cases z_zero : z = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : z = 0
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
[PROOFSTEP]
rw [z_zero]
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : z = 0
⊢ ‖↑f 0‖ ≤ c / r * ‖0‖
[PROOFSTEP]
simp only [LinearMap.map_zero, norm_zero, mul_zero]
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : z = 0
⊢ 0 ≤ 0
[PROOFSTEP]
exact le_rfl
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
[PROOFSTEP]
set z₁ := ((r : 𝕜) * (‖z‖ : 𝕜)⁻¹) • z with hz₁
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
[PROOFSTEP]
have norm_f_z₁ : ‖f z₁‖ ≤ c := by
  apply h
  rw [mem_sphere_zero_iff_norm]
  exact norm_smul_inv_norm' r_pos.le z_zero
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖↑f z₁‖ ≤ c
[PROOFSTEP]
apply h
[GOAL]
case a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ z₁ ∈ sphere 0 r
[PROOFSTEP]
rw [mem_sphere_zero_iff_norm]
[GOAL]
case a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖z₁‖ = r
[PROOFSTEP]
exact norm_smul_inv_norm' r_pos.le z_zero
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
[PROOFSTEP]
have r_ne_zero : (r : 𝕜) ≠ 0 := IsROrC.ofReal_ne_zero.mpr r_pos.ne'
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
[PROOFSTEP]
have eq : f z = ‖z‖ / r * f z₁ := by
  rw [hz₁, LinearMap.map_smul, smul_eq_mul]
  rw [← mul_assoc, ← mul_assoc, div_mul_cancel _ r_ne_zero, mul_inv_cancel, one_mul]
  simp only [z_zero, IsROrC.ofReal_eq_zero, norm_eq_zero, Ne.def, not_false_iff]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ↑f z = ↑‖z‖ / ↑r * ↑f z₁
[PROOFSTEP]
rw [hz₁, LinearMap.map_smul, smul_eq_mul]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ↑f z = ↑‖z‖ / ↑r * (↑r * (↑‖z‖)⁻¹ * ↑f z)
[PROOFSTEP]
rw [← mul_assoc, ← mul_assoc, div_mul_cancel _ r_ne_zero, mul_inv_cancel, one_mul]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ↑‖z‖ ≠ 0
[PROOFSTEP]
simp only [z_zero, IsROrC.ofReal_eq_zero, norm_eq_zero, Ne.def, not_false_iff]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
[PROOFSTEP]
rw [eq, norm_mul, norm_div, IsROrC.norm_coe_norm, IsROrC.norm_of_nonneg r_pos.le, div_mul_eq_mul_div,
  div_mul_eq_mul_div, mul_comm]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ ‖↑f z₁‖ * ‖z‖ / r ≤ c * ‖z‖ / r
[PROOFSTEP]
apply div_le_div _ _ r_pos rfl.ge
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ 0 ≤ c * ‖z‖
[PROOFSTEP]
exact mul_nonneg ((norm_nonneg _).trans norm_f_z₁) (norm_nonneg z)
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ ‖↑f z₁‖ * ‖z‖ ≤ c * ‖z‖
[PROOFSTEP]
apply mul_le_mul norm_f_z₁ rfl.le (norm_nonneg z) ((norm_nonneg _).trans norm_f_z₁)
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ (z : E), z ∈ closedBall 0 r → ‖↑f z‖ ≤ c
⊢ ‖f‖ ≤ c / r
[PROOFSTEP]
apply ContinuousLinearMap.op_norm_le_bound
[GOAL]
case hMp
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ (z : E), z ∈ closedBall 0 r → ‖↑f z‖ ≤ c
⊢ 0 ≤ c / r
[PROOFSTEP]
apply div_nonneg _ r_pos.le
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ (z : E), z ∈ closedBall 0 r → ‖↑f z‖ ≤ c
⊢ 0 ≤ c
[PROOFSTEP]
exact (norm_nonneg _).trans (h 0 (by simp only [norm_zero, mem_closedBall, dist_zero_left, r_pos.le]))
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ (z : E), z ∈ closedBall 0 r → ‖↑f z‖ ≤ c
⊢ 0 ∈ closedBall 0 r
[PROOFSTEP]
simp only [norm_zero, mem_closedBall, dist_zero_left, r_pos.le]
[GOAL]
case hM
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ (z : E), z ∈ closedBall 0 r → ‖↑f z‖ ≤ c
⊢ ∀ (x : E), ‖↑f x‖ ≤ c / r * ‖x‖
[PROOFSTEP]
apply LinearMap.bound_of_ball_bound' r_pos
[GOAL]
case hM.h
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ (z : E), z ∈ closedBall 0 r → ‖↑f z‖ ≤ c
⊢ ∀ (z : E), z ∈ closedBall 0 r → ‖↑↑f z‖ ≤ c
[PROOFSTEP]
exact fun z hz => h z hz