harrywsanders/mathlib_extracted huggingface dataset:
-- 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
⊢ ∀ (e : PE ≃ᵢ PE), e x = x → e y = y → e (midpoint ℝ x y) = midpoint ℝ x y

Tactic:
set z := midpoint ℝ x y

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
⊢ ∀ (e : PE ≃ᵢ PE), e x = x → e y = y → e z = z

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
this : c ≤ c / 2
⊢ c ≤ 0

Tactic:
linarith

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
⊢ ∀ (e : PE ≃ᵢ PE), e x = x → e y = y → e z = z

Tactic:
set f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R

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
⊢ ∀ (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
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

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

Result:
no goals