awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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₂
x y : P
rw : ‖VSub.vsub.{u_5, u_11} (P := P₂) ((f : (a : P) → P₂) x : P₂) ((f : (a : P) → P₂) y : P₂)‖ = dist x y
rw₁ : ‖VSub.vsub.{u_5, u_11} (P := P₂) ((f : (a : P) → P₂) x : P₂) ((f : (a : P) → P₂) y : P₂)‖ = ‖x -ᵥ y‖
⊢ dist.{u_11} (α := P₂) ((f : (a : P) → P₂) x : P₂) ((f : (a : P) → P₂) y : P₂) = dist x y
have rw₂ : norm.{u_5} (E := V₂) ((f.linearIsometry : (a : V) → V₂) (x -ᵥ y) : V₂) = ‖x -ᵥ y‖
Tactic: rw [dist_eq_norm_vsub V₂, dist_eq_norm_vsub V, ← map_vsub, f.linearIsometry.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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₂
x y : P
rw : ‖VSub.vsub.{u_5, u_11} (P := P₂) ((f : (a : P) → P₂) x : P₂) ((f : (a : P) → P₂) y : P₂)‖ = dist x y
rw₁ : ‖VSub.vsub.{u_5, u_11} (P := P₂) ((f : (a : P) → P₂) x : P₂) ((f : (a : P) → P₂) y : P₂)‖ = ‖x -ᵥ y‖
rw₂ : norm.{u_5} (E := V₂) ((f.linearIsometry : (a : V) → V₂) (x -ᵥ y) : V₂) = ‖x -ᵥ y‖
⊢ dist.{u_11} (α := P₂) ((f : (a : P) → P₂) x : P₂) ((f : (a : P) → P₂) y : P₂) = dist x y
have rw₃ : ‖x -ᵥ y‖ = ‖x -ᵥ y‖
Tactic: rw [dist_eq_norm_vsub V₂, dist_eq_norm_vsub V, ← map_vsub, f.linearIsometry.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ e.linear = e.linearIsometryEquiv.toLinearEquiv
have h : ∀ (x : V),
  Eq.{u_5 + 1} (α := V₂) ((e.linear : (a : V) → V₂) x : V₂)
    ((e.linearIsometryEquiv.toLinearEquiv : (a : V) → V₂) x : V₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₁' : Type u_4
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
P₁ : Type u_8
P₁' : Type u_9
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
P₄ : Type u_13
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₁
inst_9 : SeminormedAddCommGroup V₁'
inst_10 : NormedSpace 𝕜 V₁'
inst_11 : MetricSpace P₁'
inst_12 : NormedAddTorsor V₁' P₁'
inst_13 : SeminormedAddCommGroup V₂
inst_14 : NormedSpace 𝕜 V₂
inst_15 : PseudoMetricSpace P₂
inst_16 : NormedAddTorsor V₂ P₂
inst_17 : SeminormedAddCommGroup V₃
inst_18 : NormedSpace 𝕜 V₃
inst_19 : PseudoMetricSpace P₃
inst_20 : NormedAddTorsor V₃ P₃
inst_21 : SeminormedAddCommGroup V₄
inst_22 : NormedSpace 𝕜 V₄
inst_23 : PseudoMetricSpace P₄
inst_24 : NormedAddTorsor V₄ P₄
e f g : P ≃ᵃⁱ[𝕜] P₂
h : f.toFun = g.toFun
h_1 : f.invFun = g.invFun
⊢ f = g
have mk : ∀ (toAffineEquiv : P ≃ᵃ[𝕜] P₂)
  (norm_map : ∀ (x : V), norm.{u_5} (E := V₂) ((toAffineEquiv.linear : (a : V) → V₂) x : V₂) = ‖x‖)
  (h : { toAffineEquiv := toAffineEquiv, norm_map := norm_map : P ≃ᵃⁱ[𝕜] P₂ }.toFun = g.toFun),
  { toAffineEquiv := toAffineEquiv, norm_map := norm_map : P ≃ᵃⁱ[𝕜] P₂ }.invFun = g.invFun →
    { toAffineEquiv := toAffineEquiv, norm_map := norm_map : P ≃ᵃⁱ[𝕜] P₂ } = g
Tactic: cases f
Cleared hypotheses: f, h, h_1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₁' : Type u_4
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
P₁ : Type u_8
P₁' : Type u_9
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
P₄ : Type u_13
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₁
inst_9 : SeminormedAddCommGroup V₁'
inst_10 : NormedSpace 𝕜 V₁'
inst_11 : MetricSpace P₁'
inst_12 : NormedAddTorsor V₁' P₁'
inst_13 : SeminormedAddCommGroup V₂
inst_14 : NormedSpace 𝕜 V₂
inst_15 : PseudoMetricSpace P₂
inst_16 : NormedAddTorsor V₂ P₂
inst_17 : SeminormedAddCommGroup V₃
inst_18 : NormedSpace 𝕜 V₃
inst_19 : PseudoMetricSpace P₃
inst_20 : NormedAddTorsor V₃ P₃
inst_21 : SeminormedAddCommGroup V₄
inst_22 : NormedSpace 𝕜 V₄
inst_23 : PseudoMetricSpace P₄
inst_24 : NormedAddTorsor V₄ P₄
e g : P ≃ᵃⁱ[𝕜] P₂
toAffineEquiv : P ≃ᵃ[𝕜] P₂
norm_map : ∀ (x : V), norm.{u_5} (E := V₂) ((toAffineEquiv.linear : (a : V) → V₂) x : V₂) = ‖x‖
h : { toAffineEquiv := toAffineEquiv, norm_map := norm_map : P ≃ᵃⁱ[𝕜] P₂ }.toFun = g.toFun
h_1 : { toAffineEquiv := toAffineEquiv, norm_map := norm_map : P ≃ᵃⁱ[𝕜] P₂ }.invFun = g.invFun
⊢ { toAffineEquiv := toAffineEquiv, norm_map := norm_map : P ≃ᵃⁱ[𝕜] P₂ } = g
have mk : ∀ (toAffineEquiv_1 : P ≃ᵃ[𝕜] P₂)
  (norm_map_1 : ∀ (x : V), norm.{u_5} (E := V₂) ((toAffineEquiv_1.linear : (a : V) → V₂) x : V₂) = ‖x‖)
  (h :
    { toAffineEquiv := toAffineEquiv, norm_map := norm_map : P ≃ᵃⁱ[𝕜] P₂ }.toFun =
      { toAffineEquiv := toAffineEquiv_1, norm_map := norm_map_1 : P ≃ᵃⁱ[𝕜] P₂ }.toFun),
  { toAffineEquiv := toAffineEquiv, norm_map := norm_map : P ≃ᵃⁱ[𝕜] P₂ }.invFun =
      { toAffineEquiv := toAffineEquiv_1, norm_map := norm_map_1 : P ≃ᵃⁱ[𝕜] P₂ }.invFun →
    { toAffineEquiv := toAffineEquiv, norm_map := norm_map : P ≃ᵃⁱ[𝕜] P₂ } =
      { toAffineEquiv := toAffineEquiv_1, norm_map := norm_map_1 }
Tactic: cases g
Cleared hypotheses: g, h, h_1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₁' : Type u_4
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
P₁ : Type u_8
P₁' : Type u_9
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
P₄ : Type u_13
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₁
inst_9 : SeminormedAddCommGroup V₁'
inst_10 : NormedSpace 𝕜 V₁'
inst_11 : MetricSpace P₁'
inst_12 : NormedAddTorsor V₁' P₁'
inst_13 : SeminormedAddCommGroup V₂
inst_14 : NormedSpace 𝕜 V₂
inst_15 : PseudoMetricSpace P₂
inst_16 : NormedAddTorsor V₂ P₂
inst_17 : SeminormedAddCommGroup V₃
inst_18 : NormedSpace 𝕜 V₃
inst_19 : PseudoMetricSpace P₃
inst_20 : NormedAddTorsor V₃ P₃
inst_21 : SeminormedAddCommGroup V₄
inst_22 : NormedSpace 𝕜 V₄
inst_23 : PseudoMetricSpace P₄
inst_24 : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
toAffineEquiv : P ≃ᵃ[𝕜] P₂
norm_map : ∀ (x : V), norm.{u_5} (E := V₂) ((toAffineEquiv.linear : (a : V) → V₂) x : V₂) = ‖x‖
toAffineEquiv_1 : P ≃ᵃ[𝕜] P₂
norm_map_1 : ∀ (x : V), norm.{u_5} (E := V₂) ((toAffineEquiv_1.linear : (a : V) → V₂) x : V₂) = ‖x‖
h :
  { toAffineEquiv := toAffineEquiv, norm_map := norm_map : P ≃ᵃⁱ[𝕜] P₂ }.toFun =
    { toAffineEquiv := toAffineEquiv_1, norm_map := norm_map_1 : P ≃ᵃⁱ[𝕜] P₂ }.toFun
h_1 :
  { toAffineEquiv := toAffineEquiv, norm_map := norm_map : P ≃ᵃⁱ[𝕜] P₂ }.invFun =
    { toAffineEquiv := toAffineEquiv_1, norm_map := norm_map_1 : P ≃ᵃⁱ[𝕜] P₂ }.invFun
⊢ { toAffineEquiv := toAffineEquiv, norm_map := norm_map : P ≃ᵃⁱ[𝕜] P₂ } =
    { toAffineEquiv := toAffineEquiv_1, norm_map := norm_map_1 }
have mk : toAffineEquiv = toAffineEquiv_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
Goal:
𝕜 : Type u_1
V₁ : Type u_3
V₂ : Type u_5
P₁ : Type u_8
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₂
e : P₁ → P₂
e' : V₁ ≃ₗᵢ[𝕜] V₂
p : P₁
h : ∀ (p' : P₁), e p' = HVAdd.hVAdd.{u_5, u_11, u_11} (α := V₂) ((e' : (a : V₁) → V₂) (p' -ᵥ p) : V₂) (e p)
⊢ (mk' e e' p h).linearIsometryEquiv = e'
have h₁ : ∀ (x : V₁),
  Eq.{u_5 + 1} (α := V₂) (((mk' e e' p h).linearIsometryEquiv : (a : V₁) → V₂) x : V₂) ((e' : (a : V₁) → V₂) x : V₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : SeminormedAddCommGroup V₂
inst_4 : NormedSpace 𝕜 V₂
e : V ≃ₗᵢ[𝕜] V₂
⊢ e.toAffineIsometryEquiv.linearIsometryEquiv = e
have h : ∀ (x : V),
  Eq.{u_5 + 1} (α := V₂) ((e.toAffineIsometryEquiv.linearIsometryEquiv : (a : V) → V₂) x : V₂)
    ((e : (a : V) → V₂) x : V₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ Eq.{u_11 + 1} (α := Set P₂) (range.{u_11, u_10 + 1} (ι := P) (⇑e : (a : P) → P₂)) univ
have rw : Eq.{u_11 + 1} (α := Set P₂) (range.{u_11, u_10 + 1} (ι := P) (⇑e.toIsometryEquiv : (a : P) → P₂)) univ
Tactic: rw [← coe_toIsometryEquiv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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) (symm (constVSub 𝕜 p))
    (trans (LinearIsometryEquiv.toAffineIsometryEquiv (LinearIsometryEquiv.neg 𝕜)) (vaddConst 𝕜 p))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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 g
have h : g = (⇑(symm (vaddConst 𝕜 (f p))) : (a : P₂) → V₂) ∘ f ∘ (⇑(vaddConst 𝕜 p) : (a : V) → P)
Tactic: convert! (vaddConst 𝕜 (f p)).symm.isometry.comp (hf.comp (vaddConst 𝕜 p).isometry)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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
⊢ dist ((pointReflection 𝕜 x : (a : P) → P) y) x = dist y x
have 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)
Tactic: rw [← (pointReflection 𝕜 x).dist_map y x, pointReflection_self]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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)
⊢ dist ((pointReflection 𝕜 x : (a : P) → P) y) x = dist y x
have rw₁ : dist ((pointReflection 𝕜 x : (a : P) → P) y) x = dist ((pointReflection 𝕜 x : (a : P) → P) y) x
Tactic: rw [← (pointReflection 𝕜 x).dist_map y x, pointReflection_self]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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
⊢ dist ((pointReflection 𝕜 x : (a : P) → P) y) y = ‖HSMul.hSMul (α := ℕ) 2 (x -ᵥ y)‖
have rw : dist ((x -ᵥ y) +ᵥ x) y = ‖HSMul.hSMul (α := ℕ) 2 (x -ᵥ y)‖
Tactic: rw [pointReflection_apply, dist_eq_norm_vsub V, vadd_vsub_assoc, two_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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)‖
⊢ dist ((pointReflection 𝕜 x : (a : P) → P) y) y = ‖HSMul.hSMul (α := ℕ) 2 (x -ᵥ y)‖
have rw₁ : ‖((x -ᵥ y) +ᵥ x) -ᵥ y‖ = ‖HSMul.hSMul (α := ℕ) 2 (x -ᵥ y)‖
Tactic: rw [pointReflection_apply, dist_eq_norm_vsub V, vadd_vsub_assoc, two_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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)‖
⊢ dist ((pointReflection 𝕜 x : (a : P) → P) y) y = ‖HSMul.hSMul (α := ℕ) 2 (x -ᵥ y)‖
have rw₂ : ‖x -ᵥ y + (x -ᵥ y)‖ = ‖HSMul.hSMul (α := ℕ) 2 (x -ᵥ y)‖
Tactic: rw [pointReflection_apply, dist_eq_norm_vsub V, vadd_vsub_assoc, two_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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)‖
⊢ dist ((pointReflection 𝕜 x : (a : P) → P) y) y = ‖HSMul.hSMul (α := ℕ) 2 (x -ᵥ y)‖
have rw₃ : ‖x -ᵥ y + (x -ᵥ y)‖ = ‖x -ᵥ y + (x -ᵥ y)‖
Tactic: rw [pointReflection_apply, dist_eq_norm_vsub V, vadd_vsub_assoc, two_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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
⊢ dist ((pointReflection 𝕜 x : (a : P) → P) y) y = norm.{u_1} (E := 𝕜) 2 * dist x y
have rw : ‖HSMul.hSMul (α := ℕ) 2 (x -ᵥ 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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
⊢ dist ((pointReflection 𝕜 x : (a : P) → P) y) y = norm.{u_1} (E := 𝕜) 2 * dist x y
have rw₁ : ‖x -ᵥ y + (x -ᵥ 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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
⊢ dist ((pointReflection 𝕜 x : (a : P) → P) y) y = norm.{u_1} (E := 𝕜) 2 * dist x y
have rw₂ : ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2 (x -ᵥ 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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
⊢ dist ((pointReflection 𝕜 x : (a : P) → P) y) y = norm.{u_1} (E := 𝕜) 2 * dist x y
have rw₃ : norm.{u_1} (E := 𝕜) 2 * ‖x -ᵥ 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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
⊢ dist ((pointReflection 𝕜 x : (a : P) → P) y) y = norm.{u_1} (E := 𝕜) 2 * dist x y
have rw₄ : norm.{u_1} (E := 𝕜) 2 * dist x 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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
⊢ dist ((pointReflection ℝ x : (a : P) → P) y) y = 2 * dist x y
have rw : norm (E := ℝ) 2 * dist x y = 2 * dist x y
Tactic: rw [dist_pointReflection_self, Real.norm_two]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
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
⊢ dist ((pointReflection ℝ x : (a : P) → P) y) y = 2 * dist x y
have rw₁ : 2 * dist x y = 2 * dist x y
Tactic: rw [dist_pointReflection_self, Real.norm_two]
-- 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}
⊢ ∀ (e : PE ≃ᵢ PE), (e : (a : PE) → PE) x = x → (e : (a : PE) → PE) y = y → (e : (a : PE) → PE) z = z
have this : Nonempty.{u_2 + 1} (↑s : Type u_2)
Tactic: haveI : Nonempty s := ⟨⟨IsometryEquiv.refl PE, rfl, rfl⟩⟩
-- 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)
⊢ BddAbove (α := ℝ) (range fun (e : (↑s : Type u_2)) ↦ dist (((↑e : PE ≃ᵢ PE) : (a : PE) → PE) z) z)
have 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
Tactic: refine ⟨dist x z + dist x z, forall_mem_range.2 <| Subtype.forall.2 ?_⟩
-- 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 ((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
have rw : dist ((e : (a : PE) → PE) z) x + dist x z = dist x ((e : (a : PE) → PE) z) + dist x z
Tactic: rw [hx, 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)
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
⊢ 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
have rw₁ : dist x ((e : (a : PE) → PE) z) + dist x z = dist x ((e : (a : PE) → PE) z) + dist x z
Tactic: rw [hx, 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)
e : PE ≃ᵢ PE
hx : (e : (a : PE) → PE) x = x
right : (e : (a : PE) → PE) y = y
⊢ dist (α := PE) ((e : (a : PE) → PE) x : PE) ((e : (a : PE) → PE) z : PE) + dist x z = dist x z + dist x z
have rw : dist x z + dist x z = dist x z + dist x z
Tactic: 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)
e : PE ≃ᵢ PE
hx : (e : (a : PE) → PE) x = x
right : (e : (a : PE) → PE) y = y
⊢ dist (((↑(Subtype.mk (p := fun (a : PE ≃ᵢ PE) ↦ a ∈ s) e ⋯) : PE ≃ᵢ PE) : (a : PE) → PE) z) z ≤ dist x z + dist x z
have dist : 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: 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]