awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
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
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
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
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
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 }
⊢ { toAffineEquiv := toAffineEquiv, norm_map := norm_map : P ≃ᵃⁱ[𝕜] P₂ } = g

Tactic:
cases g
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
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
mk : toAffineEquiv = toAffineEquiv_1
⊢ { toAffineEquiv := toAffineEquiv, norm_map := norm_map : P ≃ᵃⁱ[𝕜] P₂ } =
    { toAffineEquiv := toAffineEquiv_1, norm_map := norm_map_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
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_1

Tactic:
simpa [DFunLike.coe_injective.eq_iff] using h

Premises used: Function.Injective.eq_iff, DFunLike.coe_injective
-- 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₂
e : P ≃ᵃ[𝕜] P₂
he : ∀ (x : V), norm.{u_5} (E := V₂) ((e.linear : (a : V) → V₂) x : V₂) = ‖x‖
⊢ Eq (α := (a : P) → P₂) (⇑{ toAffineEquiv := e, norm_map := he : P ≃ᵃⁱ[𝕜] P₂ } : (a : P) → P₂) (⇑e : (a : P) → P₂)

Tactic:
rfl

Premises used: rfl
-- 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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ Eq (α := (a : P) → P₂) (⇑e.toAffineEquiv : (a : P) → P₂) (⇑e : (a : P) → P₂)

Tactic:
rfl

Premises used: rfl
-- 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₂
e e' : P ≃ᵃⁱ[𝕜] P₂
h : ∀ (x : P), Eq.{u_11 + 1} (α := P₂) ((e : (a : P) → P₂) x : P₂) ((e' : (a : P) → P₂) x : P₂)
⊢ e = e'

Tactic:
toAffineEquiv_injective <| AffineEquiv.ext h

Premises used: AffineIsometryEquiv.toAffineEquiv_injective, AffineEquiv.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₂
⊢ Injective (β := P → P₂) fun (f : P ≃ᵃⁱ[𝕜] P₂) ↦ (⇑f : (a : P) → P₂)

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- 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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ Eq (α := (a : P) → P₂) (⇑e.toAffineIsometry : (a : P) → P₂) (⇑e : (a : P) → P₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
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) : (a : P₁) → P₂) = e

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
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)
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₂)
⊢ (mk' e e' p h).linearIsometryEquiv = e'

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
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)
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:
rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
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₂
⊢ Eq (α := (a : V) → V₂) (⇑e.toAffineIsometryEquiv : (a : V) → V₂) (⇑e : (a : V) → V₂)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
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₂
h :
  ∀ (x : V),
    Eq.{u_5 + 1} (α := V₂) ((e.toAffineIsometryEquiv.linearIsometryEquiv : (a : V) → V₂) x : V₂)
      ((e : (a : V) → V₂) x : V₂)
⊢ e.toAffineIsometryEquiv.linearIsometryEquiv = e

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
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₂
x : V
⊢ Eq.{u_5 + 1} (α := V₂) ((e.toAffineIsometryEquiv.linearIsometryEquiv : (a : V) → V₂) x : V₂)
    ((e : (a : V) → V₂) x : V₂)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
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.toAffineEquiv = e.toAffineEquiv

Tactic:
rfl

Premises used: LinearEquiv.toAffineEquiv, rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
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.toAffineIsometry = e.toLinearIsometry.toAffineIsometry

Tactic:
rfl

Premises used: LinearMap.toAffineMap, AffineIsometryEquiv.toAffineIsometry, AffineEquiv.toAffineMap, LinearIsometry.toAffineIsometry, rfl
-- 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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ Isometry.{u_10, u_11} (α := P) (β := P₂) (⇑e : (a : P) → P₂)

Tactic:
e.toAffineIsometry.isometry

Premises used: AffineIsometryEquiv.toAffineIsometry, AffineIsometry.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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ Eq (α := (a : P) → P₂) (⇑e.toIsometryEquiv : (a : P) → P₂) (⇑e : (a : P) → P₂)

Tactic:
rfl

Premises used: rfl
-- 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₂
e : P ≃ᵃⁱ[𝕜] P₂
rw : Eq.{u_11 + 1} (α := Set P₂) (range.{u_11, u_10 + 1} (ι := P) (⇑e.toIsometryEquiv : (a : P) → P₂)) univ
⊢ Eq.{u_11 + 1} (α := Set P₂) (range.{u_11, u_10 + 1} (ι := P) (⇑e : (a : P) → P₂)) univ

Tactic:
rw [← coe_toIsometryEquiv]

Premises used: AffineIsometryEquiv.coe_toIsometryEquiv
-- 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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ Eq.{u_11 + 1} (α := Set P₂) (range.{u_11, u_10 + 1} (ι := P) (⇑e.toIsometryEquiv : (a : P) → P₂)) univ

Tactic:
IsometryEquiv.range_eq_univ _

Premises used: IsometryEquiv.range_eq_univ
-- 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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ Eq.{u_11 + 1} (α := Set P₂) (range.{u_11, u_10 + 1} (ι := P) (⇑e.toIsometryEquiv : (a : P) → P₂)) univ

Tactic:
exact IsometryEquiv.range_eq_univ _

Premises used: IsometryEquiv.range_eq_univ
-- 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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ Eq (α := (a : P) → P₂) (⇑e.toHomeomorph : (a : P) → P₂) (⇑e : (a : P) → P₂)

Tactic:
rfl

Premises used: rfl
-- 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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ Continuous.{u_10, u_11} (X := P) (Y := P₂) (⇑e : (a : P) → P₂)

Tactic:
e.isometry.continuous

Premises used: Isometry.continuous, 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₂
e : P ≃ᵃⁱ[𝕜] P₂
x : P
⊢ ContinuousAt.{u_10, u_11} (Y := P₂) (⇑e : (a : P) → P₂) x

Tactic:
e.continuous.continuousAt

Premises used: AffineIsometryEquiv.continuous, Continuous.continuousAt
-- 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₂
e : P ≃ᵃⁱ[𝕜] P₂
s : Set P
⊢ ContinuousOn.{u_10, u_11} (Y := P₂) (⇑e : (a : P) → P₂) s

Tactic:
e.continuous.continuousOn

Premises used: Continuous.continuousOn, AffineIsometryEquiv.continuous
-- 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₂
e : P ≃ᵃⁱ[𝕜] P₂
s : Set P
x : P
⊢ ContinuousWithinAt.{u_10, u_11} (Y := P₂) (⇑e : (a : P) → P₂) s x

Tactic:
e.continuous.continuousWithinAt

Premises used: AffineIsometryEquiv.continuous, Continuous.continuousWithinAt
-- 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₂
⊢ Injective (α := P ≃ᵃⁱ[𝕜] P₂) toContinuousAffineEquiv

Tactic:
fun x _ h =>
  coeFn_injective (congr_arg _ h : ⇑x.toContinuousAffineEquiv = _)

Premises used: congr_arg, Function.Injective, DFunLike.coe, AffineIsometryEquiv.coeFn_injective
-- 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 g : P ≃ᵃⁱ[𝕜] P₂
⊢ f.toContinuousAffineEquiv = g.toContinuousAffineEquiv ↔ f = g

Tactic:
toContinuousAffineEquiv_injective.eq_iff

Premises used: Function.Injective.eq_iff, AffineIsometryEquiv.toContinuousAffineEquiv_injective
-- 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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ Eq (α := (a : P) → P₂) (⇑e.toContinuousAffineEquiv : (a : P) → P₂) (⇑e : (a : P) → P₂)

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.{u_10 + 1} (α := (a : P) → P) (⇑(refl 𝕜 P) : (a : P) → P) id

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) (toAffineEquiv (refl 𝕜 P)) (AffineEquiv.refl 𝕜 P)

Tactic:
rfl

Premises used: AffineEquiv.refl, 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) (toContinuousAffineEquiv (refl 𝕜 P)) (ContinuousAffineEquiv.refl 𝕜 P)

Tactic:
rfl

Premises used: AffineEquiv.refl, AffineIsometryEquiv.toContinuousAffineEquiv, ContinuousAffineEquiv.refl, 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) (toIsometryEquiv (refl 𝕜 P)) (IsometryEquiv.refl P)

Tactic:
rfl

Premises used: AffineIsometryEquiv.toIsometryEquiv, IsometryEquiv.refl, Equiv.refl, 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) (toHomeomorph (refl 𝕜 P)) (Homeomorph.refl P)

Tactic:
rfl

Premises used: Homeomorph.refl, Equiv.refl, IsometryEquiv.toHomeomorph, rfl
-- 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₂
e : P ≃ᵃⁱ[𝕜] P₂
x : P₂
⊢ (e : (a : P) → P₂) ((e.symm : (a : P₂) → P) x : P) = x

Tactic:
e.toAffineEquiv.apply_symm_apply x

Premises used: AffineIsometryEquiv.toAffineEquiv, AffineEquiv.apply_symm_apply