awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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)
e : PE ≃ᵢ PE
hx : (e : (a : PE) → PE) x = x
right : (e : (a : PE) → PE) y = y
dist :
  Dist.dist ((e : (a : PE) → PE) z) x + Dist.dist x z =
    Dist.dist (α := PE) ((e : (a : PE) → PE) x : PE) ((e : (a : PE) → PE) z : PE) + Dist.dist x z
⊢ Dist.dist (((↑(Subtype.mk (p := fun (a : PE ≃ᵢ PE) ↦ a ∈ s) e ⋯) : PE ≃ᵢ PE) : (a : PE) → PE) z) z ≤
    Dist.dist x z + Dist.dist x z
have dist₁ : Dist.dist (α := PE) ((e : (a : PE) → PE) x : PE) ((e : (a : PE) → PE) z : PE) + Dist.dist x z =
  Dist.dist x z + Dist.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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (hypothesis)
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)
⊢ ∀ (e : PE ≃ᵢ PE), (e : (a : PE) → PE) x = x → (e : (a : PE) → PE) y = y → (e : (a : PE) → PE) z = z
have h_bdd : BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
Tactic: have h_bdd : BddAbove (range fun e : s => dist ((e : PE ≃ᵢ PE) z) z) := by
    refine ⟨dist x z + dist x z, forall_mem_range.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 rw [e.dist_eq x z]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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
e : PE ≃ᵢ PE
⊢ dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
have dsimp : dist
    ((pointReflection ℝ z : (a : PE) → PE)
      ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE) : PE))
    z =
  2 * dist ((e : (a : PE) → PE) z) z
Tactic: dsimp only [trans_apply, coe_toIsometryEquiv, f, R]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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
e : PE ≃ᵢ PE
⊢ dist
      ((pointReflection ℝ z : (a : PE) → PE)
        ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE) : PE))
      z =
    2 * dist ((e : (a : PE) → PE) z) z
have rw : dist ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE)) z =
  2 * dist ((e : (a : PE) → PE) z) z
Tactic: rw [dist_pointReflection_fixed, ← e.dist_eq, e.apply_symm_apply,
      dist_pointReflection_self_real, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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
e : PE ≃ᵢ PE
rw :
  dist ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE)) z =
    2 * dist ((e : (a : PE) → PE) z) z
⊢ dist
      ((pointReflection ℝ z : (a : PE) → PE)
        ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE) : PE))
      z =
    2 * dist ((e : (a : PE) → PE) z) z
have rw₁ : dist (α := PE)
    ((e : (a : PE) → PE)
        ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE) : PE) :
      PE)
    ((e : (a : PE) → PE) z : PE) =
  2 * dist ((e : (a : PE) → PE) z) z
Tactic: rw [dist_pointReflection_fixed, ← e.dist_eq, e.apply_symm_apply,
      dist_pointReflection_self_real, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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
e : PE ≃ᵢ PE
rw :
  dist ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE)) z =
    2 * dist ((e : (a : PE) → PE) z) z
rw₁ :
  dist (α := PE)
      ((e : (a : PE) → PE)
          ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE) : PE) :
        PE)
      ((e : (a : PE) → PE) z : PE) =
    2 * dist ((e : (a : PE) → PE) z) z
⊢ dist
      ((pointReflection ℝ z : (a : PE) → PE)
        ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE) : PE))
      z =
    2 * dist ((e : (a : PE) → PE) z) z
have rw₂ : dist (α := PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE) ((e : (a : PE) → PE) z : PE) =
  2 * dist ((e : (a : PE) → PE) z) z
Tactic: rw [dist_pointReflection_fixed, ← e.dist_eq, e.apply_symm_apply,
      dist_pointReflection_self_real, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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
e : PE ≃ᵢ PE
rw :
  dist ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE)) z =
    2 * dist ((e : (a : PE) → PE) z) z
rw₁ :
  dist (α := PE)
      ((e : (a : PE) → PE)
          ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE) : PE) :
        PE)
      ((e : (a : PE) → PE) z : PE) =
    2 * dist ((e : (a : PE) → PE) z) z
rw₂ :
  dist (α := PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE)
      ((e : (a : PE) → PE) z : PE) =
    2 * dist ((e : (a : PE) → PE) z) z
⊢ dist
      ((pointReflection ℝ z : (a : PE) → PE)
        ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE) : PE))
      z =
    2 * dist ((e : (a : PE) → PE) z) z
have rw₃ : 2 * dist z ((e : (a : PE) → PE) z) = 2 * dist ((e : (a : PE) → PE) z) z
Tactic: rw [dist_pointReflection_fixed, ← e.dist_eq, e.apply_symm_apply,
      dist_pointReflection_self_real, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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
e : PE ≃ᵢ PE
rw :
  dist ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE)) z =
    2 * dist ((e : (a : PE) → PE) z) z
rw₁ :
  dist (α := PE)
      ((e : (a : PE) → PE)
          ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE) : PE) :
        PE)
      ((e : (a : PE) → PE) z : PE) =
    2 * dist ((e : (a : PE) → PE) z) z
rw₂ :
  dist (α := PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE)
      ((e : (a : PE) → PE) z : PE) =
    2 * dist ((e : (a : PE) → PE) z) z
rw₃ : 2 * dist z ((e : (a : PE) → PE) z) = 2 * dist ((e : (a : PE) → PE) z) z
⊢ dist
      ((pointReflection ℝ z : (a : PE) → PE)
        ((e.symm : (a : PE) → PE) ((pointReflection ℝ z : (a : PE) → PE) ((e : (a : PE) → PE) z : PE) : PE) : PE))
      z =
    2 * dist ((e : (a : PE) → PE) z) z
have rw₄ : 2 * dist ((e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
Tactic: rw [dist_pointReflection_fixed, ← e.dist_eq, e.apply_symm_apply,
      dist_pointReflection_self_real, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (hypothesis)
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
⊢ ∀ (e : PE ≃ᵢ PE), (e : (a : PE) → PE) x = x → (e : (a : PE) → PE) y = y → (e : (a : PE) → PE) z = z
have hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z
Tactic: have hf_dist : ∀ e, dist (f e z) z = 2 * dist (e z) z := by
    intro e
    dsimp only [trans_apply, coe_toIsometryEquiv, f, R]
    rw [dist_pointReflection_fixed, ← e.dist_eq, e.apply_symm_apply,
      dist_pointReflection_self_real, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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 ∈ s
have left : (f e : (a : PE) → PE) x = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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
⊢ f e ∈ s
have right : (f e : (a : PE) → PE) y = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (hypothesis)
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), (e : (a : PE) → PE) x = x → (e : (a : PE) → PE) y = y → (e : (a : PE) → PE) z = z
have hf_maps_to : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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
have H : ∀ (x : (↑s : Type u_2)), dist (((↑x : PE ≃ᵢ PE) : (a : PE) → PE) z) z ≤ c / 2
Tactic: apply ciSup_le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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 (((↑(Subtype.mk (p := fun (x : PE ≃ᵢ PE) ↦ x ∈ s) e he) : PE ≃ᵢ PE) : (a : PE) → PE) z) z ≤ c / 2
have H : dist ((f e : (a : PE) → PE) z) z ≤ c
Tactic: simp only [le_div_iff₀' (zero_lt_two' ℝ), ← hf_dist]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (hypothesis)
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), (e : (a : PE) → PE) x = x → (e : (a : PE) → PE) y = y → (e : (a : PE) → PE) z = z
have this₁ : 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⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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
have linarith : 0 < c → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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
⊢ c ≤ 0
have linarith₁ : 0 < c → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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
⊢ c ≤ 0
have linarith₂ : 0 < c → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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
⊢ c ≤ 0
have linarith₃ : 0 < c → 2 * c - 1 * c + (0 - c) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (hypothesis)
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
⊢ ∀ (e : PE ≃ᵢ PE), (e : (a : PE) → PE) x = x → (e : (a : PE) → PE) y = y → (e : (a : PE) → PE) z = z
have this₁ : c ≤ 0
Tactic: replace : c ≤ 0 := by linarith
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
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
have 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
Tactic: refine fun e hx hy => dist_le_zero.1 (le_trans ?_ this)