-- Mathlib/Analysis/Normed/Affine/MazurUlam.lean
theorem midpoint_fixed {x y : PE} :
    ∀ e : PE ≃ᵢ PE, e x = x → e y = y → e (midpoint ℝ x y) = midpoint ℝ x y

Proof state:
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
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 := (pointReflection ℝ z).toIsometryEquiv
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans 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

Tactic:
have hf_maps_to : MapsTo f s s := by
  rintro e ⟨hx, hy⟩
  constructor <;> simp [f, R, z, hx, hy, e.symm_apply_eq.2 hx.symm, e.symm_apply_eq.2 hy.symm]

Result:
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
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 := (pointReflection ℝ z).toIsometryEquiv
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans 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

Proof state:
case intro
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
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) z ≤ dist x z + dist x z

Tactic:
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 rw [e.dist_eq x z]

Result:
no goals

Proof state:
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
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 := (pointReflection ℝ z).toIsometryEquiv
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e) z) z = 2 * dist (e z) z
⊢ MapsTo f s s

Tactic:
rintro e ⟨hx, hy⟩

Result:
case intro
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
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 := (pointReflection ℝ z).toIsometryEquiv
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans 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

Proof state:
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
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 := (pointReflection ℝ z).toIsometryEquiv
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R
e : PE ≃ᵢ PE
⊢ dist ((pointReflection ℝ z) (e.symm ((pointReflection ℝ z) (e z)))) z = 2 * dist (e z) z

Tactic:
rw [dist_pointReflection_fixed, ← e.dist_eq, e.apply_symm_apply,
  dist_pointReflection_self_real, dist_comm]

Result:
no goals

Proof state:
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
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 := (pointReflection ℝ z).toIsometryEquiv
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans 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, dist (↑e z) z
⊢ c ≤ c / 2

Tactic:
apply ciSup_le

Result:
case H
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
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 := (pointReflection ℝ z).toIsometryEquiv
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans 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, dist (↑e z) z
⊢ ∀ (x : ↑s), dist (↑x z) z ≤ c / 2

Proof state:
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
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)

Tactic:
refine ⟨dist x z + dist x z, forall_mem_range.2 <| Subtype.forall.2 ?_⟩

Result:
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
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 (↑⟨a, b⟩ z) z ≤ dist x z + dist x z

Proof state:
case H.mk
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
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 := (pointReflection ℝ z).toIsometryEquiv
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans 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, dist (↑e z) z
e : PE ≃ᵢ PE
he : e ∈ s
⊢ dist (↑⟨e, he⟩ z) z ≤ c / 2

Tactic:
simp only [Subtype.coe_mk, le_div_iff₀' (zero_lt_two' ℝ), ← hf_dist]

Result:
case H.mk
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
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 := (pointReflection ℝ z).toIsometryEquiv
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans 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, dist (↑e z) z
e : PE ≃ᵢ PE
he : e ∈ s
⊢ dist ((f e) z) z ≤ c

Proof state:
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
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

Tactic:
rw [e.dist_eq x z]

Result:
no goals