awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
⊢ Eq (α := (a : P) → P₂) (⇑f.toAffineMap : (a : P) → P₂) (⇑f : (a : P) → P₂)

Tactic:
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₂
f : P →ᵃ[𝕜] P₂
norm_map : ∀ (x : V), norm.{u_5} (E := V₂) ((f.linear : (a : V) → V₂) x : V₂) = ‖x‖
norm_map_1 :
  ∀ (x : V),
    norm.{u_5} (E := V₂) (({ toAffineMap := f, norm_map := norm_map : P →ᵃⁱ[𝕜] P₂ }.linear : (a : V) → V₂) x : V₂) = ‖x‖
⊢ { toAffineMap := f, norm_map := norm_map : P →ᵃⁱ[𝕜] P₂ } =
    { toAffineMap := { toAffineMap := f, norm_map := norm_map }.toAffineMap, norm_map := norm_map_1 }

Tactic:
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₂
⊢ Injective (α := P →ᵃⁱ[𝕜] P₂) (β := P → P₂) (DFunLike.coe (β := fun (x : P) ↦ P₂))

Tactic:
AffineMap.coeFn_injective.comp toAffineMap_injective

Premises used: Function.Injective.comp, AffineIsometry.toAffineMap_injective, AffineMap.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₂
h : ∀ (x : P), Eq.{u_11 + 1} (α := P₂) ((f : (a : P) → P₂) x : P₂) ((g : (a : P) → P₂) x : P₂)
⊢ f = g

Tactic:
coeFn_injective <| funext h

Premises used: AffineIsometry.coeFn_injective, funext
-- 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₂
f : V →ₗᵢ[𝕜] V₂
⊢ Eq (α := (a : V) → V₂) (⇑f.toAffineIsometry : (a : V) → V₂) (⇑f : (a : V) → V₂)

Tactic:
rfl

Premises used: 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₂
f : V →ₗᵢ[𝕜] V₂
h :
  ∀ (x : V),
    Eq.{u_5 + 1} (α := V₂) ((f.toAffineIsometry.linearIsometry : (a : V) → V₂) x : V₂) ((f : (a : V) → V₂) x : V₂)
⊢ f.toAffineIsometry.linearIsometry = f

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₂
f : V →ₗᵢ[𝕜] V₂
x : V
⊢ Eq.{u_5 + 1} (α := V₂) ((f.toAffineIsometry.linearIsometry : (a : V) → V₂) x : V₂) ((f : (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₂
f : V →ₗᵢ[𝕜] V₂
⊢ f.toAffineIsometry.toAffineMap = f.toAffineMap

Tactic:
rfl

Premises used: LinearMap.toAffineMap, 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₂
f : P →ᵃⁱ[𝕜] P₂
p : P
v : V
⊢ (f : (a : P) → P₂) (v +ᵥ p) =
    HVAdd.hVAdd.{u_5, u_11, u_11} (α := V₂) (β := P₂) ((f.linearIsometry : (a : V) → V₂) v : V₂)
      ((f : (a : P) → P₂) p : P₂)

Tactic:
f.toAffineMap.map_vadd p v

Premises used: AffineMap.map_vadd, AffineIsometry.toAffineMap
-- 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₂
p1 p2 : P
⊢ (f.linearIsometry : (a : V) → V₂) (p1 -ᵥ p2) =
    VSub.vsub.{u_5, u_11} (P := P₂) ((f : (a : P) → P₂) p1 : P₂) ((f : (a : P) → P₂) p2 : P₂)

Tactic:
f.toAffineMap.linearMap_vsub p1 p2

Premises used: AffineMap.linearMap_vsub, AffineIsometry.toAffineMap
-- 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₂
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‖
rw₃ rw₄ : ‖x -ᵥ y‖ = ‖x -ᵥ y‖
⊢ dist.{u_11} (α := P₂) ((f : (a : P) → P₂) x : P₂) ((f : (a : P) → P₂) y : P₂) = dist x y

Tactic:
rw [dist_eq_norm_vsub V₂, dist_eq_norm_vsub V, ← map_vsub, f.linearIsometry.norm_map]

Premises used: LinearIsometry.norm_map, AffineIsometry.linearIsometry, AffineIsometry.map_vsub, dist_eq_norm_vsub
-- 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₂
x y : P
⊢ nndist.{u_11} (α := P₂) ((f : (a : P) → P₂) x : P₂) ((f : (a : P) → P₂) y : P₂) = nndist x y

Tactic:
simp [nndist_dist]

Premises used: nndist_dist
-- 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₂
x y : P
⊢ edist.{u_11} (α := P₂) ((f : (a : P) → P₂) x : P₂) ((f : (a : P) → P₂) y : P₂) = edist x y

Tactic:
simp [edist_dist]

Premises used: edist_dist
-- 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₂
⊢ Isometry.{u_10, u_11} (α := P) (β := P₂) (⇑f : (a : P) → P₂)

Tactic:
f.edist_map

Premises used: AffineIsometry.edist_map, Isometry
-- 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₂
f₁ : P₁' →ᵃⁱ[𝕜] P₂
⊢ Injective.{u_9 + 1, u_11 + 1} (α := P₁') (β := P₂) (⇑f₁ : (a : P₁') → P₂)

Tactic:
f₁.isometry.injective

Premises used: Isometry.injective, AffineIsometry.isometry
-- 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₂
f₁ : P₁' →ᵃⁱ[𝕜] P₂
x y : P₁'
⊢ Eq.{u_11 + 1} (α := P₂) ((f₁ : (a : P₁') → P₂) x : P₂) ((f₁ : (a : P₁') → P₂) y : P₂) ↔ x = y

Tactic:
f₁.injective.eq_iff

Premises used: Function.Injective.eq_iff, AffineIsometry.injective
-- 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₂
f₁ : P₁' →ᵃⁱ[𝕜] P₂
x y : P₁'
h : x ≠ y
⊢ Ne.{u_11 + 1} (α := P₂) ((f₁ : (a : P₁') → P₂) x : P₂) ((f₁ : (a : P₁') → P₂) y : P₂)

Tactic:
f₁.injective.ne h

Premises used: Function.Injective.ne, AffineIsometry.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 : P →ᵃⁱ[𝕜] P₂
⊢ LipschitzWith.{u_10, u_11} (α := P) (β := P₂) 1 (⇑f : (a : P) → P₂)

Tactic:
f.isometry.lipschitz

Premises used: AffineIsometry.isometry, Isometry.lipschitz
-- 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₂
⊢ AntilipschitzWith.{u_10, u_11} (α := P) (β := P₂) 1 (⇑f : (a : P) → P₂)

Tactic:
f.isometry.antilipschitz

Premises used: AffineIsometry.isometry, Isometry.antilipschitz
-- 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₂
⊢ Continuous.{u_10, u_11} (X := P) (Y := P₂) (⇑f : (a : P) → P₂)

Tactic:
f.isometry.continuous

Premises used: Isometry.continuous, 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₂
f : P →ᵃⁱ[𝕜] P₂
s : Set P
⊢ ediam.{u_11} (X := P₂) ((⇑f : (a : P) → P₂) '' s) = ediam s

Tactic:
f.isometry.ediam_image s

Premises used: AffineIsometry.isometry, Isometry.ediam_image
-- 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₂
⊢ ediam.{u_11} (X := P₂) (range.{u_11, u_10 + 1} (ι := P) (⇑f : (a : P) → P₂)) = ediam.{u_10} (X := P) univ

Tactic:
f.isometry.ediam_range

Premises used: Isometry.ediam_range, 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₂
f : P →ᵃⁱ[𝕜] P₂
s : Set P
⊢ diam.{u_11} (α := P₂) ((⇑f : (a : P) → P₂) '' s) = diam s

Tactic:
f.isometry.diam_image s

Premises used: AffineIsometry.isometry, Isometry.diam_image
-- 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₂
⊢ diam.{u_11} (α := P₂) (range.{u_11, u_10 + 1} (ι := P) (⇑f : (a : P) → P₂)) = diam.{u_10} (α := P) univ

Tactic:
f.isometry.diam_range

Premises used: Isometry.diam_range, 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₂
⊢ Injective (α := P →ᵃⁱ[𝕜] P₂) toContinuousAffineMap

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

Premises used: AffineIsometry.coeFn_injective, congr_arg, Function.Injective, DFunLike.coe
-- 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.toContinuousAffineMap = g.toContinuousAffineMap ↔ f = g

Tactic:
toContinuousAffineMap_injective.eq_iff

Premises used: Function.Injective.eq_iff, AffineIsometry.toContinuousAffineMap_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 : P →ᵃⁱ[𝕜] P₂
⊢ Eq (α := (a : P) → P₂) (⇑f.toContinuousAffineMap : (a : P) → P₂) (⇑f : (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₂
f : P →ᵃⁱ[𝕜] P₂
α : Type u_14
inst_9 : TopologicalSpace α
g : α → P
⊢ Continuous.{u_14, u_11} (Y := P₂) ((⇑f : (a : P) → P₂) ∘ g) ↔ Continuous g

Tactic:
f.isometry.comp_continuous_iff

Premises used: Isometry.comp_continuous_iff, AffineIsometry.isometry
-- 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) (⇑id : (a : P) → P) _root_.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
x : P
⊢ (id : (a : P) → P) x = 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) (toAffineMap id) (AffineMap.id 𝕜 P)

Tactic:
rfl

Premises used: AffineMap.id, 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) (toContinuousAffineMap id) (ContinuousAffineMap.id 𝕜 P)

Tactic:
rfl

Premises used: ContinuousAffineMap.id, AffineMap.id, AffineIsometry.toContinuousAffineMap, rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
V₃ : Type u_6
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
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 : PseudoMetricSpace P₃
inst_12 : NormedAddTorsor V₃ P₃
g : P₂ →ᵃⁱ[𝕜] P₃
f : P →ᵃⁱ[𝕜] P₂
⊢ Eq (α := (a : P) → P₃) (⇑(g.comp f) : (a : P) → P₃)
    (Function.comp.{u_10 + 1, u_11 + 1, u_12 + 1} (β := P₂) (⇑g : (a : P₂) → P₃) (⇑f : (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₂
f : P →ᵃⁱ[𝕜] P₂
⊢ comp id f = f

Tactic:
ext fun _ => rfl

Premises used: AffineIsometry.ext, 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₂
f : P →ᵃⁱ[𝕜] P₂
⊢ f.comp id = f

Tactic:
ext fun _ => rfl

Premises used: AffineIsometry.ext, rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
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 : PseudoMetricSpace P₃
inst_12 : NormedAddTorsor V₃ P₃
inst_13 : SeminormedAddCommGroup V₄
inst_14 : NormedSpace 𝕜 V₄
inst_15 : PseudoMetricSpace P₄
inst_16 : NormedAddTorsor V₄ P₄
f : P₃ →ᵃⁱ[𝕜] P₄
g : P₂ →ᵃⁱ[𝕜] P₃
h : P →ᵃⁱ[𝕜] P₂
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: AffineIsometry.comp, AffineMap.comp, 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) (⇑1 : (a : P) → P) _root_.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
f g : P →ᵃⁱ[𝕜] P
⊢ Eq.{u_10 + 1} (α := (a : P) → P) (⇑(f * g) : (a : P) → P)
    (Function.comp (β := P) (⇑f : (a : P) → P) (⇑g : (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
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_10 + 1} ↥s
⊢ AffineMap.linear (AffineIsometry.toAffineMap s.subtypeₐᵢ) = s.direction.subtype

Tactic:
rfl

Premises used: Submodule.subtype, 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
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_10 + 1} ↥s
⊢ AffineIsometry.linearIsometry s.subtypeₐᵢ = s.direction.subtypeₗᵢ

Tactic:
rfl

Premises used: AffineIsometry.linearIsometry, Submodule.subtype, Submodule.subtypeₗᵢ, 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
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_10 + 1} ↥s
⊢ Eq.{u_10 + 1} (α := (a : ↥s) → P) (⇑s.subtypeₐᵢ : (a : ↥s) → P) (⇑s.subtype : (a : ↥s) → 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
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_10 + 1} ↥s
⊢ Eq (α := ↥s →ᵃ[𝕜] P) (AffineIsometry.toAffineMap s.subtypeₐᵢ) s.subtype

Tactic:
rfl

Premises used: AffineSubspace.subtype, 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
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_10 + 1} ↥s
⊢ Eq (α := ↥s →ᴬ[𝕜] P) (AffineIsometry.toContinuousAffineMap s.subtypeₐᵢ) s.subtypeA

Tactic:
rfl

Premises used: AffineSubspace.subtypeA, AffineSubspace.subtype, AffineIsometry.toContinuousAffineMap, 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₂
h :
  ∀ (x : V),
    Eq.{u_5 + 1} (α := V₂) ((e.linear : (a : V) → V₂) x : V₂)
      ((e.linearIsometryEquiv.toLinearEquiv : (a : V) → V₂) x : V₂)
⊢ e.linear = e.linearIsometryEquiv.toLinearEquiv

Tactic:
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₂
e : P ≃ᵃⁱ[𝕜] P₂
x : V
⊢ Eq.{u_5 + 1} (α := V₂) ((e.linear : (a : V) → V₂) x : V₂)
    ((e.linearIsometryEquiv.toLinearEquiv : (a : V) → V₂) x : V₂)

Tactic:
rfl