awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
e : PE ≃ᵢ PE
hx : (e : (a : PE) → PE) x = x
hy : (e : (a : PE) → PE) y = y
left : (f e : (a : PE) → PE) x = x
right : (f e : (a : PE) → PE) y = y
⊢ f e ∈ s

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
e : PE ≃ᵢ PE
hx : (e : (a : PE) → PE) x = x
hy : (e : (a : PE) → PE) y = y
⊢ (f e : (a : PE) → PE) x = x

Tactic:
simp [f, R, z, hx, hy, e.symm_apply_eq.2 hx.symm, e.symm_apply_eq.2 hy.symm]

Premises used: Iff.mpr, IsometryEquiv.symm_apply_eq, Eq.symm
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
e : PE ≃ᵢ PE
hx : (e : (a : PE) → PE) x = x
hy : (e : (a : PE) → PE) y = y
⊢ (f e : (a : PE) → PE) y = y

Tactic:
simp [f, R, z, hx, hy, e.symm_apply_eq.2 hx.symm, e.symm_apply_eq.2 hy.symm]

Premises used: Iff.mpr, IsometryEquiv.symm_apply_eq, Eq.symm
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
⊢ MapsTo f s s

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]
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : (↑s : Type u_2)), dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z
H : ∀ (x : (↑s : Type u_2)), dist (((↑x : PE ≃ᵢ PE) : (a : PE) → PE) z) z ≤ c / 2
⊢ c ≤ c / 2

Tactic:
apply ciSup_le

Premises used: ciSup_le
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : (↑s : Type u_2)), dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z
e : PE ≃ᵢ PE
he : e ∈ s
H : dist ((f e : (a : PE) → PE) z) z ≤ c
⊢ dist (((↑(Subtype.mk (p := fun (x : PE ≃ᵢ PE) ↦ x ∈ s) e he) : PE ≃ᵢ PE) : (a : PE) → PE) z) z ≤ c / 2

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

Premises used: Real, le_div_iff₀', zero_lt_two'
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : (↑s : Type u_2)), dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z
e : PE ≃ᵢ PE
he : e ∈ s
⊢ dist ((f e : (a : PE) → PE) z) z ≤ c

Tactic:
le_ciSup h_bdd ⟨f e, hf_maps_to he⟩

Premises used: Subtype.mk, le_ciSup
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : (↑s : Type u_2)), dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z
e : PE ≃ᵢ PE
he : e ∈ s
⊢ dist ((f e : (a : PE) → PE) z) z ≤ c

Tactic:
exact le_ciSup h_bdd ⟨f e, hf_maps_to he⟩

Premises used: Subtype.mk, le_ciSup
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : (↑s : Type u_2)), dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z
⊢ c ≤ c / 2

Tactic:
have : c ≤ c / 2 := by
    apply ciSup_le
    rintro ⟨e, he⟩
    simp only [le_div_iff₀' (zero_lt_two' ℝ), ← hf_dist]
    exact le_ciSup h_bdd ⟨f e, hf_maps_to he⟩
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this_1 : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : (↑s : Type u_2)), dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z
this : c ≤ c / 2
linarith : 0 < c → 2 / 2 = 1
linarith₁ : 0 < c → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 0 < c → GT.gt (α := ℝ) 2 0
linarith₃ : 0 < c → 2 * c - 1 * c + (0 - c) = 0
⊢ c ≤ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this_1 : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : (↑s : Type u_2)), dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z
this : c ≤ c / 2
⊢ c ≤ 0

Tactic:
replace : c ≤ 0 := by linarith
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this_1 : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : (↑s : Type u_2)), dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z
this : c ≤ 0
⊢ ∀ (e : PE ≃ᵢ PE), (e : (a : PE) → PE) x = x → (e : (a : PE) → PE) y = y → (e : (a : PE) → PE) z = z

Tactic:
fun e hx hy => dist_le_zero.1 (le_trans ?_ this)

Premises used: dist_le_zero, Iff.mp, le_trans
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this_1 : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : (↑s : Type u_2)), dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z
this : c ≤ 0
refine :
  ∀ (e : PE ≃ᵢ PE) (hx : (e : (a : PE) → PE) x = x) (hy : (e : (a : PE) → PE) y = y), dist ((e : (a : PE) → PE) z) z ≤ c
⊢ ∀ (e : PE ≃ᵢ PE), (e : (a : PE) → PE) x = x → (e : (a : PE) → PE) y = y → (e : (a : PE) → PE) z = z

Tactic:
refine fun e hx hy => dist_le_zero.1 (le_trans ?_ this)

Premises used: dist_le_zero, Iff.mp, le_trans
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this_1 : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : (↑s : Type u_2)), dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z
this : c ≤ 0
e : PE ≃ᵢ PE
hx : (e : (a : PE) → PE) x = x
hy : (e : (a : PE) → PE) y = y
⊢ dist ((e : (a : PE) → PE) z) z ≤ c

Tactic:
le_ciSup h_bdd ⟨e, hx, hy⟩

Premises used: Subtype.mk, le_ciSup, And.intro
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e : PE ≃ᵢ PE | (e : (a : PE) → PE) x = x ∧ (e : (a : PE) → PE) y = y}
this_1 : Nonempty.{u_2 + 1} (↑s : Type u_2)
h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
R : PE ≃ᵢ PE := toIsometryEquiv (pointReflection ℝ z)
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun (e : PE ≃ᵢ PE) ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
hf_maps_to : MapsTo f s s
c : ℝ := ⨆ (e : (↑s : Type u_2)), dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z
this : c ≤ 0
e : PE ≃ᵢ PE
hx : (e : (a : PE) → PE) x = x
hy : (e : (a : PE) → PE) y = y
⊢ dist ((e : (a : PE) → PE) z) z ≤ c

Tactic:
exact le_ciSup h_bdd ⟨e, hx, hy⟩

Premises used: Subtype.mk, le_ciSup, And.intro
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  (IsometryEquiv.trans
        (f.trans
          (toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y)))))
        f.symm).trans
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
⊢ (e : (a : PE) → PE) x = x

Tactic:
simp [e]
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  (IsometryEquiv.trans
        (f.trans
          (toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y)))))
        f.symm).trans
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
⊢ (e : (a : PE) → PE) x = x

Tactic:
have hx : e x = x := by simp [e]
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  (IsometryEquiv.trans
        (f.trans
          (toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y)))))
        f.symm).trans
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
hx : (e : (a : PE) → PE) x = x
⊢ (e : (a : PE) → PE) y = y

Tactic:
simp [e]
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  (IsometryEquiv.trans
        (f.trans
          (toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y)))))
        f.symm).trans
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
hx : (e : (a : PE) → PE) x = x
⊢ (e : (a : PE) → PE) y = y

Tactic:
have hy : e y = y := by simp [e]
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  (IsometryEquiv.trans
        (f.trans
          (toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y)))))
        f.symm).trans
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
hx : (e : (a : PE) → PE) x = x
hy : (e : (a : PE) → PE) y = y
⊢ (e : (a : PE) → PE) (midpoint ℝ x y) = midpoint ℝ x y

Tactic:
have hm := e.midpoint_fixed hx hy
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : E ≃ᵢ F
h0 : Eq.{u_3 + 1} (α := F) ((f : (a : E) → F) 0 : F) (0 : F)
x : E
⊢ norm.{u_3} (E := F) ((f : (a : E) → F) x : F) = ‖x‖

Tactic:
simp only [← dist_zero_right, ← h0, f.dist_eq]

Premises used: IsometryEquiv.dist_eq, dist_zero_right
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E ≃ᵢ F
h0 : Eq.{u_3 + 1} (α := F) ((f : (a : E) → F) 0 : F) (0 : F)
⊢ Eq (α := (a : E) → F) (⇑(f.toRealLinearIsometryEquivOfMapZero h0) : (a : E) → F) (⇑f : (a : E) → F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E ≃ᵢ F
h0 : Eq.{u_3 + 1} (α := F) ((f : (a : E) → F) 0 : F) (0 : F)
⊢ Eq (α := (a : F) → E) (⇑(LinearIsometryEquiv.symm (f.toRealLinearIsometryEquivOfMapZero h0)) : (a : F) → E)
    (⇑f.symm : (a : F) → E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : E ≃ᵢ F
⊢ Eq.{u_3 + 1} (α := F) ((f.trans (IsometryEquiv.symm (addRight ((f : (a : E) → F) 0))) : (a : E) → F) 0 : F) (0 : F)

Tactic:
simpa only [sub_eq_add_neg] using sub_self (f 0)

Premises used: sub_self, sub_eq_add_neg, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E ≃ᵢ F
x : E
⊢ (f.toRealLinearIsometryEquiv : (a : E) → F) x =
    HSub.hSub (α := F) (β := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) 0 : F)

Tactic:
(sub_eq_add_neg (f x) (f 0)).symm

Premises used: sub_eq_add_neg, OfNat.ofNat, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E ≃ᵢ F
y : F
⊢ Eq.{u_1 + 1} (α := E) ((LinearIsometryEquiv.symm f.toRealLinearIsometryEquiv : (a : F) → E) y : E)
    ((f.symm : (a : F) → E) (HAdd.hAdd (β := F) y ((f : (a : E) → F) 0 : F)) : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
p : PE
⊢ (f : (a : PE) → PF) p =
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := F) (β := PF)
      ((toRealLinearIsometryEquiv
              (IsometryEquiv.trans (vaddConst (Classical.arbitrary PE))
                (f.trans (IsometryEquiv.symm (vaddConst ((f : (a : PE) → PF) (Classical.arbitrary PE)))))) :
            (a : E) → F)
          (p -ᵥ Classical.arbitrary PE) :
        F)
      ((f : (a : PE) → PF) (Classical.arbitrary PE) : PF)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
⊢ Eq (α := (a : PE) → PF) (⇑f.toRealAffineIsometryEquiv : (a : PE) → PF) (⇑f : (a : PE) → PF)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
H :
  ∀ (x : PE),
    Eq.{u_4 + 1} (α := PF) ((toIsometryEquiv f.toRealAffineIsometryEquiv : (a : PE) → PF) x : PF)
      ((f : (a : PE) → PF) x : PF)
⊢ toIsometryEquiv f.toRealAffineIsometryEquiv = f

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x : PE
⊢ Eq.{u_4 + 1} (α := PF) ((toIsometryEquiv f.toRealAffineIsometryEquiv : (a : PE) → PF) x : PF)
    ((f : (a : PE) → PF) x : PF)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬(i₁ = i₃ ∧ i₂ = i₄)
h₁₂₄₃ : ¬(i₁ = i₄ ∧ i₂ = i₃)
⊢ ¬i₁ = i₃ ∨ ¬i₂ = i₄

Tactic:
rw [Classical.not_and_iff_not_or_not] at h₁₂₃₄ h₁₂₄₃

Premises used: Classical.not_and_iff_not_or_not
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬(i₁ = i₃ ∧ i₂ = i₄)
h₁₂₄₃ : ¬(i₁ = i₄ ∧ i₂ = i₃)
h₁₂₃₅ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
⊢ ¬i₁ = i₄ ∨ ¬i₂ = i₃

Tactic:
rw [Classical.not_and_iff_not_or_not] at h₁₂₃₄ h₁₂₄₃

Premises used: Classical.not_and_iff_not_or_not