E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
set z := midpoint ℝ x y
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
set s := { e : PE ≃ᵢ PE | e x = x ∧ e y = y }
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
haveI : Nonempty s := ⟨⟨IsometryEquiv.refl PE, rfl, rfl⟩⟩
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
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]
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
set R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
set f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
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]
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
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]
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
set c := ⨆ e : s, dist ((e : PE ≃ᵢ PE) z) z
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
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⟩
case this
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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

E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
replace : c ≤ 0
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
refine' fun e hx hy => dist_le_zero.1 (le_trans _ this)
no goals
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
exact le_ciSup h_bdd ⟨e, hx, hy⟩
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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)
refine' ⟨dist x z + dist x z, forall_range_iff.2 <| Subtype.forall.2 _⟩
case intro
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
rintro e ⟨hx, _⟩
no goals
case intro
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
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]
no goals
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
rw [hx, dist_comm]
no goals
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
erw [e.dist_eq x z]
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
intro e
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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)
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
dsimp
no goals
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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)
rw [dist_pointReflection_fixed, ← e.dist_eq, e.apply_symm_apply,
  dist_pointReflection_self_real, dist_comm]
case intro
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
rintro e ⟨hx, hy⟩
no goals
case intro
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
constructor <;> simp [hx, hy, e.symm_apply_eq.2 hx.symm, e.symm_apply_eq.2 hy.symm]
case H
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
apply ciSup_le
case H.mk
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
case H
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
rintro ⟨e, he⟩
case H.mk
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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)
case H.mk
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
simp only [Subtype.coe_mk, le_div_iff' (zero_lt_two' ℝ), ← hf_dist]
no goals
case H.mk
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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)
exact le_ciSup h_bdd ⟨f e, hf_maps_to he⟩
no goals
case this
E : Type u_2
PE : Type u_1
F : Type ?u.569
PF : Type ?u.572
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
linarith