awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p : P
⊢ Eq (α := V ≃ᵃ[𝕜] P) (toAffineEquiv (vaddConst 𝕜 p)) (AffineEquiv.vaddConst 𝕜 p)

Tactic:
rfl

Premises used: AffineEquiv.vaddConst, rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p : P
⊢ Eq (α := (a : P) → V) (⇑(constVSub 𝕜 p) : (a : P) → V) fun (x : P) ↦ p -ᵥ x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p : P
h :
  ∀ (x : V),
    Eq.{u_10 + 1} (α := P) ((symm (constVSub 𝕜 p) : (a : V) → P) x : P)
      ((trans (LinearIsometryEquiv.toAffineIsometryEquiv (LinearIsometryEquiv.neg 𝕜)) (vaddConst 𝕜 p) : (a : V) → P) x :
        P)
⊢ Eq (α := V ≃ᵃⁱ[𝕜] P) (symm (constVSub 𝕜 p))
    (trans (LinearIsometryEquiv.toAffineIsometryEquiv (LinearIsometryEquiv.neg 𝕜)) (vaddConst 𝕜 p))

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p : P
x : V
⊢ Eq.{u_10 + 1} (α := P) ((symm (constVSub 𝕜 p) : (a : V) → P) x : P)
    ((trans (LinearIsometryEquiv.toAffineIsometryEquiv (LinearIsometryEquiv.neg 𝕜)) (vaddConst 𝕜 p) : (a : V) → P) x :
      P)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
v : V
⊢ Eq.{u_10 + 1} (α := (a : P) → P) (⇑(constVAdd 𝕜 P v) : (a : P) → P) fun (x : P) ↦ v +ᵥ x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
⊢ Eq (α := P ≃ᵃⁱ[𝕜] P) (constVAdd 𝕜 P 0) (refl 𝕜 P)

Tactic:
ext <| zero_vadd V

Premises used: zero_vadd, AffineIsometryEquiv.ext
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : SeminormedAddCommGroup V₂
inst_6 : NormedSpace 𝕜 V₂
inst_7 : PseudoMetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
f : P → P₂
hf : Isometry f
p : P
g : V → V₂
hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p
⊢ Isometry.{u_2, u_5} (α := V) (β := V₂)
    ((⇑(symm (vaddConst 𝕜 (f p))) : (a : P₂) → V₂) ∘ f ∘ (⇑(vaddConst 𝕜 p) : (a : V) → P))

Tactic:
(vaddConst 𝕜 (f p)).symm.isometry.comp (hf.comp (vaddConst 𝕜 p).isometry)

Premises used: Isometry.comp, AffineIsometryEquiv.symm, AffineIsometryEquiv.vaddConst, AffineIsometryEquiv.isometry
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : SeminormedAddCommGroup V₂
inst_6 : NormedSpace 𝕜 V₂
inst_7 : PseudoMetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
f : P → P₂
hf : Isometry f
p : P
g : V → V₂
hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p
h : g = (⇑(symm (vaddConst 𝕜 (f p))) : (a : P₂) → V₂) ∘ f ∘ (⇑(vaddConst 𝕜 p) : (a : V) → P)
⊢ Isometry g

Tactic:
convert! (vaddConst 𝕜 (f p)).symm.isometry.comp (hf.comp (vaddConst 𝕜 p).isometry)

Premises used: Isometry.comp, AffineIsometryEquiv.symm, AffineIsometryEquiv.vaddConst, AffineIsometryEquiv.isometry
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : SeminormedAddCommGroup V₂
inst_6 : NormedSpace 𝕜 V₂
inst_7 : PseudoMetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
f : P → P₂
hf : Isometry f
p : P
g : V → V₂
hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p
⊢ g = (⇑(symm (vaddConst 𝕜 (f p))) : (a : P₂) → V₂) ∘ f ∘ (⇑(vaddConst 𝕜 p) : (a : V) → P)

Tactic:
funext hg

Premises used: funext
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : SeminormedAddCommGroup V₂
inst_6 : NormedSpace 𝕜 V₂
inst_7 : PseudoMetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
f : P → P₂
hf : Isometry f
p : P
g : V → V₂
hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p
⊢ g = (⇑(symm (vaddConst 𝕜 (f p))) : (a : P₂) → V₂) ∘ f ∘ (⇑(vaddConst 𝕜 p) : (a : V) → P)

Tactic:
exact funext hg

Premises used: funext
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
x y : P
⊢ (pointReflection 𝕜 x : (a : P) → P) y = (x -ᵥ y) +ᵥ x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
x : P
⊢ Eq (α := P ≃ᵃ[𝕜] P) (toAffineEquiv (pointReflection 𝕜 x)) (AffineEquiv.pointReflection 𝕜 x)

Tactic:
rfl

Premises used: AffineEquiv.trans, rfl, AffineEquiv.pointReflection
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
x : P
⊢ (pointReflection 𝕜 x : (a : P) → P) x = x

Tactic:
AffineEquiv.pointReflection_self 𝕜 x

Premises used: AffineEquiv.pointReflection_self
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
x : P
⊢ Involutive.{u_10 + 1} (α := P) (⇑(pointReflection 𝕜 x) : (a : P) → P)

Tactic:
Equiv.pointReflection_involutive x

Premises used: Equiv.vaddConst, Equiv.pointReflection_involutive, Equiv.constVSub
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
x : P
⊢ Eq (α := P ≃ᵃⁱ[𝕜] P) (symm (pointReflection 𝕜 x)) (pointReflection 𝕜 x)

Tactic:
toAffineEquiv_injective <| AffineEquiv.pointReflection_symm 𝕜 x

Premises used: AffineIsometryEquiv.toAffineEquiv_injective, AffineEquiv.pointReflection_symm
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
x y : P
rw :
  dist ((pointReflection 𝕜 x : (a : P) → P) y) x =
    dist (α := P) ((pointReflection 𝕜 x : (a : P) → P) y : P) ((pointReflection 𝕜 x : (a : P) → P) x : P)
rw₁ rw₂ : dist ((pointReflection 𝕜 x : (a : P) → P) y) x = dist ((pointReflection 𝕜 x : (a : P) → P) y) x
⊢ dist ((pointReflection 𝕜 x : (a : P) → P) y) x = dist y x

Tactic:
rw [← (pointReflection 𝕜 x).dist_map y x, pointReflection_self]

Premises used: AffineIsometryEquiv.pointReflection, AffineIsometryEquiv.dist_map, AffineIsometryEquiv.pointReflection_self
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
x y : P
rw : dist ((x -ᵥ y) +ᵥ x) y = ‖HSMul.hSMul (α := ℕ) 2 (x -ᵥ y)‖
rw₁ : ‖((x -ᵥ y) +ᵥ x) -ᵥ y‖ = ‖HSMul.hSMul (α := ℕ) 2 (x -ᵥ y)‖
rw₂ : ‖x -ᵥ y + (x -ᵥ y)‖ = ‖HSMul.hSMul (α := ℕ) 2 (x -ᵥ y)‖
rw₃ rw₄ : ‖x -ᵥ y + (x -ᵥ y)‖ = ‖x -ᵥ y + (x -ᵥ y)‖
⊢ dist ((pointReflection 𝕜 x : (a : P) → P) y) y = ‖HSMul.hSMul (α := ℕ) 2 (x -ᵥ y)‖

Tactic:
rw [pointReflection_apply, dist_eq_norm_vsub V, vadd_vsub_assoc, two_nsmul]

Premises used: AffineIsometryEquiv.pointReflection_apply, vadd_vsub_assoc, dist_eq_norm_vsub, two_nsmul
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
x y : P
rw : ‖HSMul.hSMul (α := ℕ) 2 (x -ᵥ y)‖ = norm.{u_1} (E := 𝕜) 2 * dist x y
rw₁ : ‖x -ᵥ y + (x -ᵥ y)‖ = norm.{u_1} (E := 𝕜) 2 * dist x y
rw₂ : ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2 (x -ᵥ y)‖ = norm.{u_1} (E := 𝕜) 2 * dist x y
rw₃ : norm.{u_1} (E := 𝕜) 2 * ‖x -ᵥ y‖ = norm.{u_1} (E := 𝕜) 2 * dist x y
rw₄ rw₅ : norm.{u_1} (E := 𝕜) 2 * dist x y = norm.{u_1} (E := 𝕜) 2 * dist x y
⊢ dist ((pointReflection 𝕜 x : (a : P) → P) y) y = norm.{u_1} (E := 𝕜) 2 * dist x y

Tactic:
rw [dist_pointReflection_self', two_nsmul, ← two_smul 𝕜, norm_smul, ← dist_eq_norm_vsub V]

Premises used: norm_smul, two_smul, dist_eq_norm_vsub, AffineIsometryEquiv.dist_pointReflection_self', two_nsmul
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : Invertible (α := 𝕜) 2
x y : P
⊢ (pointReflection 𝕜 x : (a : P) → P) y = y ↔ y = x

Tactic:
AffineEquiv.pointReflection_fixed_iff_of_module 𝕜

Premises used: AffineEquiv.pointReflection_fixed_iff_of_module
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
V : Type u_2
P : Type u_10
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
inst_3 : NormedSpace ℝ V
x y : P
rw : norm (E := ℝ) 2 * dist x y = 2 * dist x y
rw₁ rw₂ : 2 * dist x y = 2 * dist x y
⊢ dist ((pointReflection ℝ x : (a : P) → P) y) y = 2 * dist x y

Tactic:
rw [dist_pointReflection_self, Real.norm_two]

Premises used: Real.norm_two, AffineIsometryEquiv.dist_pointReflection_self
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
V : Type u_2
P : Type u_10
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
inst_3 : NormedSpace ℝ V
x y : P
⊢ (pointReflection ℝ (midpoint ℝ x y) : (a : P) → P) x = y

Tactic:
AffineEquiv.pointReflection_midpoint_left x y

Premises used: AffineEquiv.pointReflection_midpoint_left
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
V : Type u_2
P : Type u_10
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
inst_3 : NormedSpace ℝ V
x y : P
⊢ (pointReflection ℝ (midpoint ℝ x y) : (a : P) → P) y = x

Tactic:
AffineEquiv.pointReflection_midpoint_right x y

Premises used: AffineEquiv.pointReflection_midpoint_right
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V₁' : Type u_4
V₂ : Type u_5
P₁' : Type u_9
P₂ : Type u_11
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V₁'
inst_2 : NormedSpace 𝕜 V₁'
inst_3 : MetricSpace P₁'
inst_4 : NormedAddTorsor V₁' P₁'
inst_5 : SeminormedAddCommGroup V₂
inst_6 : NormedSpace 𝕜 V₂
inst_7 : PseudoMetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
E : AffineSubspace 𝕜 P₁'
inst_9 : Nonempty.{u_9 + 1} ↥E
φ : P₁' →ᵃⁱ[𝕜] P₂
x : ↥(map φ.toAffineMap E)
⊢ (φ : (a : P₁') → P₂)
      (↑((AffineIsometryEquiv.symm (isometryEquivMap φ E) : (a : ↥(map φ.toAffineMap E)) → ↥E) x) : P₁') =
    (↑x : P₂)

Tactic:
congr_arg Subtype.val <| (E.isometryEquivMap φ).apply_symm_apply _

Premises used: AffineIsometryEquiv.apply_symm_apply, congr_arg, AffineSubspace.isometryEquivMap, Subtype.val
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V₁' : Type u_4
V₂ : Type u_5
P₁' : Type u_9
P₂ : Type u_11
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V₁'
inst_2 : NormedSpace 𝕜 V₁'
inst_3 : MetricSpace P₁'
inst_4 : NormedAddTorsor V₁' P₁'
inst_5 : SeminormedAddCommGroup V₂
inst_6 : NormedSpace 𝕜 V₂
inst_7 : PseudoMetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
φ : P₁' →ᵃⁱ[𝕜] P₂
E : AffineSubspace 𝕜 P₁'
inst_9 : Nonempty.{u_9 + 1} ↥E
g : ↥E
⊢ Eq.{u_11 + 1} (α := P₂) ((↑((isometryEquivMap φ E : (a : ↥E) → ↥(map φ.toAffineMap E)) g) : P₂) : P₂)
    ((φ : (a : P₁') → P₂) (↑g : P₁') : P₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V₁' : Type u_4
V₂ : Type u_5
P₁' : Type u_9
P₂ : Type u_11
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V₁'
inst_2 : NormedSpace 𝕜 V₁'
inst_3 : MetricSpace P₁'
inst_4 : NormedAddTorsor V₁' P₁'
inst_5 : SeminormedAddCommGroup V₂
inst_6 : NormedSpace 𝕜 V₂
inst_7 : PseudoMetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
φ : P₁' →ᵃⁱ[𝕜] P₂
E : AffineSubspace 𝕜 P₁'
inst_9 : Nonempty.{u_9 + 1} ↥E
⊢ Eq (α := AffineMap.{u_1, u_4, u_9, u_5, u_11} 𝕜 ↥E ↥(map φ.toAffineMap E))
    (↑(AffineIsometryEquiv.toAffineEquiv (isometryEquivMap φ E)) : ↥E →ᵃ[𝕜] ↥(map φ.toAffineMap E))
    (↑(E.equivMapOfInjective φ.toAffineMap ⋯) : ↥E →ᵃ[𝕜] ↥(map φ.toAffineMap E))

Tactic:
rfl

Premises used: AffineSubspace.equivMapOfInjective, rfl
-- 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
set :
  let z := midpoint ℝ x y;
  ∀ (e : PE ≃ᵢ PE), (e : (a : PE) → PE) x = x → (e : (a : PE) → PE) y = y → (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) (midpoint ℝ x y) = midpoint ℝ x y

Tactic:
set z := midpoint ℝ x y

Premises used: Real, midpoint
-- 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}
⊢ Nonempty.{u_2 + 1} (↑s : Type u_2)

Tactic:
haveI : Nonempty s := ⟨⟨IsometryEquiv.refl PE, rfl, rfl⟩⟩
-- 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)
⊢ BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)

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

Premises used: Iff.mpr, Set.forall_mem_range, Subtype.forall, BddAbove, Set.Nonempty, HAdd.hAdd, Exists.intro, Dist.dist
-- 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)
refine :
  ∀ (a : PE ≃ᵢ PE) (b : a ∈ s),
    dist (((↑(Subtype.mk (p := fun (a : PE ≃ᵢ PE) ↦ a ∈ s) a b) : PE ≃ᵢ PE) : (a : PE) → PE) z) z ≤ dist x z + dist x z
⊢ BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)

Tactic:
refine ⟨dist x z + dist x z, forall_mem_range.2 <| Subtype.forall.2 ?_⟩
-- 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)
e : PE ≃ᵢ PE
hx : (e : (a : PE) → PE) x = x
right : (e : (a : PE) → PE) y = y
⊢ dist ((e : (a : PE) → PE) z) z ≤ dist ((e : (a : PE) → PE) z) x + dist x z

Tactic:
dist_triangle (e z) x z

Premises used: dist_triangle, DFunLike.coe
-- 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)
e : PE ≃ᵢ PE
hx : (e : (a : PE) → PE) x = x
right : (e : (a : PE) → PE) y = y
rw : dist ((e : (a : PE) → PE) z) x + dist x z = dist x ((e : (a : PE) → PE) z) + dist x z
rw₁ rw₂ : dist x ((e : (a : PE) → PE) z) + dist x z = dist x ((e : (a : PE) → PE) z) + dist x z
⊢ dist ((e : (a : PE) → PE) z) x + dist x z =
    dist (α := PE) ((e : (a : PE) → PE) x : PE) ((e : (a : PE) → PE) z : PE) + dist x z

Tactic:
rw [hx, dist_comm]

Premises used: dist_comm
-- 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)
e : PE ≃ᵢ PE
hx : (e : (a : PE) → PE) x = x
right : (e : (a : PE) → PE) y = y
rw rw₁ : dist x z + dist x z = dist x z + dist x z
⊢ dist (α := PE) ((e : (a : PE) → PE) x : PE) ((e : (a : PE) → PE) z : PE) + dist x z = dist x z + dist x z

Tactic:
rw [e.dist_eq x z]

Premises used: IsometryEquiv.dist_eq
-- 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)
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.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
⊢ 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

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]

Premises used: dist_triangle, Dist.dist, DFunLike.coe
-- 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)
⊢ 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]
-- 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
e : PE ≃ᵢ PE
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
⊢ dist ((f e : (a : PE) → PE) z) z = 2 * dist ((e : (a : PE) → PE) z) z

Tactic:
dsimp only [trans_apply, coe_toIsometryEquiv, f, R]

Premises used: AffineIsometryEquiv.coe_toIsometryEquiv, IsometryEquiv.trans_apply
-- 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
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
rw₄ rw₅ : 2 * dist ((e : (a : PE) → PE) z) 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

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

Premises used: IsometryEquiv.apply_symm_apply, AffineIsometryEquiv.dist_pointReflection_fixed, AffineIsometryEquiv.dist_pointReflection_self_real, dist_comm, IsometryEquiv.dist_eq
-- 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
⊢ ∀ (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]