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₂
e : P ≃ᵃⁱ[𝕜] P₂
x : P
⊢ (e.symm : (a : P₂) → P) ((e : (a : P) → P₂) x : P₂) = x

Tactic:
e.toAffineEquiv.symm_apply_apply x

Premises used: AffineIsometryEquiv.toAffineEquiv, AffineEquiv.symm_apply_apply
-- 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₂
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: LinearEquiv.symm, AffineIsometryEquiv.symm, AffineEquiv.symm, Equiv.symm, 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₂
⊢ Bijective (α := P₂ ≃ᵃⁱ[𝕜] P) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, AffineIsometryEquiv.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- 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₂
⊢ e.symm.toAffineEquiv = e.symm

Tactic:
rfl

Premises used: AffineEquiv.symm, 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.symm : (a : P₂) → P) (⇑e.symm : (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₂
⊢ e.symm.toContinuousAffineEquiv = e.toContinuousAffineEquiv.symm

Tactic:
rfl

Premises used: AffineIsometryEquiv.toContinuousAffineEquiv, AffineEquiv.symm, ContinuousAffineEquiv.symm, 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.toContinuousAffineEquiv.symm : (a : P₂) → P) (⇑e.symm : (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₂
⊢ e.symm.toIsometryEquiv = e.toIsometryEquiv.symm

Tactic:
rfl

Premises used: IsometryEquiv.symm, Equiv.symm, 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.toIsometryEquiv.symm : (a : P₂) → P) (⇑e.symm : (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₂
⊢ e.symm.toHomeomorph = e.toHomeomorph.symm

Tactic:
rfl

Premises used: Homeomorph.symm, Equiv.symm, IsometryEquiv.toHomeomorph, AffineIsometryEquiv.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₂
⊢ Eq (α := (a : P₂) → P) (⇑e.toHomeomorph.symm : (a : P₂) → P) (⇑e.symm : (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
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₃
e₁ : P ≃ᵃⁱ[𝕜] P₂
e₂ : P₂ ≃ᵃⁱ[𝕜] P₃
⊢ Eq (α := (a : P) → P₃) (⇑(e₁.trans e₂) : (a : P) → P₃)
    (comp.{u_10 + 1, u_11 + 1, u_12 + 1} (β := P₂) (⇑e₂ : (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₂
⊢ e.trans (refl 𝕜 P₂) = e

Tactic:
ext fun _ => rfl

Premises used: AffineIsometryEquiv.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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ trans (refl 𝕜 P) e = e

Tactic:
ext fun _ => rfl

Premises used: AffineIsometryEquiv.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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ e.trans e.symm = refl 𝕜 P

Tactic:
ext e.symm_apply_apply

Premises used: AffineIsometryEquiv.symm_apply_apply, 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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ e.symm.trans e = refl 𝕜 P₂

Tactic:
ext e.apply_symm_apply

Premises used: AffineIsometryEquiv.apply_symm_apply, AffineIsometryEquiv.ext
-- 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₃
e₁ : P ≃ᵃⁱ[𝕜] P₂
e₂ : P₂ ≃ᵃⁱ[𝕜] P₃
⊢ Eq (α := (a : P₃) → P) (⇑(e₁.trans e₂).symm : (a : P₃) → P)
    (comp.{u_12 + 1, u_11 + 1, u_10 + 1} (β := P₂) (⇑e₁.symm : (a : P₂) → P) (⇑e₂.symm : (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
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₄
ePP₂ : P ≃ᵃⁱ[𝕜] P₂
eP₂G : P₂ ≃ᵃⁱ[𝕜] P₃
eGG' : P₃ ≃ᵃⁱ[𝕜] P₄
⊢ ePP₂.trans (eP₂G.trans eGG') = (ePP₂.trans eP₂G).trans eGG'

Tactic:
rfl

Premises used: Equiv.trans, LinearEquiv.toEquiv, AffineIsometryEquiv.trans, AffineEquiv.trans, LinearEquiv.trans, 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) 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
e e' : P ≃ᵃⁱ[𝕜] P
⊢ Eq.{u_10 + 1} (α := (a : P) → P) (⇑(e * e') : (a : P) → P) (comp (β := P) (⇑e : (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
e : P ≃ᵃⁱ[𝕜] P
⊢ Eq.{u_10 + 1} (α := (a : P) → P) (⇑e⁻¹ : (a : P) → P) (⇑e.symm : (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₂
p : P
v : V
⊢ (e : (a : P) → P₂) (v +ᵥ p) =
    HVAdd.hVAdd.{u_5, u_11, u_11} (α := V₂) (β := P₂) ((e.linearIsometryEquiv : (a : V) → V₂) v : V₂)
      ((e : (a : P) → P₂) p : P₂)

Tactic:
e.toAffineIsometry.map_vadd p v

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

Tactic:
e.toAffineIsometry.map_vsub p1 p2

Premises used: AffineIsometry.map_vsub, AffineIsometryEquiv.toAffineIsometry
-- 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 y : P
⊢ dist.{u_11} (α := P₂) ((e : (a : P) → P₂) x : P₂) ((e : (a : P) → P₂) y : P₂) = dist x y

Tactic:
e.toAffineIsometry.dist_map x y

Premises used: AffineIsometryEquiv.toAffineIsometry, AffineIsometry.dist_map
-- 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 y : P
⊢ edist.{u_11} (α := P₂) ((e : (a : P) → P₂) x : P₂) ((e : (a : P) → P₂) y : P₂) = edist x y

Tactic:
e.toAffineIsometry.edist_map x y

Premises used: AffineIsometryEquiv.toAffineIsometry, AffineIsometry.edist_map
-- 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₂
⊢ Bijective.{u_10 + 1, u_11 + 1} (α := P) (β := P₂) (⇑e : (a : P) → P₂)

Tactic:
e.1.bijective

Premises used: AffineIsometryEquiv.toAffineEquiv, AffineEquiv.bijective
-- 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₂
⊢ Injective.{u_10 + 1, u_11 + 1} (α := P) (β := P₂) (⇑e : (a : P) → P₂)

Tactic:
e.1.injective

Premises used: AffineIsometryEquiv.toAffineEquiv, AffineEquiv.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₂
⊢ Surjective.{u_10 + 1, u_11 + 1} (α := P) (β := P₂) (⇑e : (a : P) → P₂)

Tactic:
e.1.surjective

Premises used: AffineIsometryEquiv.toAffineEquiv, AffineEquiv.surjective
-- 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 y : P
⊢ Eq.{u_11 + 1} (α := P₂) ((e : (a : P) → P₂) x : P₂) ((e : (a : P) → P₂) y : P₂) ↔ x = y

Tactic:
e.injective.eq_iff

Premises used: Function.Injective.eq_iff, AffineIsometryEquiv.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₂
x y : P
h : x ≠ y
⊢ Ne.{u_11 + 1} (α := P₂) ((e : (a : P) → P₂) x : P₂) ((e : (a : P) → P₂) y : P₂)

Tactic:
e.injective.ne h

Premises used: Function.Injective.ne, AffineIsometryEquiv.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₂
⊢ LipschitzWith.{u_10, u_11} (α := P) (β := P₂) 1 (⇑e : (a : P) → P₂)

Tactic:
e.isometry.lipschitz

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

Tactic:
e.isometry.antilipschitz

Premises used: Isometry.antilipschitz, 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₂
s : Set P
⊢ ediam.{u_11} (X := P₂) ((⇑e : (a : P) → P₂) '' s) = ediam s

Tactic:
e.isometry.ediam_image s

Premises used: Isometry.ediam_image, 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₂
s : Set P
⊢ diam.{u_11} (α := P₂) ((⇑e : (a : P) → P₂) '' s) = diam s

Tactic:
e.isometry.diam_image s

Premises used: Isometry.diam_image, 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₂
α : Type u_14
inst_9 : TopologicalSpace α
f : α → P
s : Set α
⊢ ContinuousOn.{u_14, u_11} (Y := P₂) ((⇑e : (a : P) → P₂) ∘ f) s ↔ ContinuousOn f s

Tactic:
e.isometry.comp_continuousOn_iff

Premises used: Isometry.comp_continuousOn_iff, 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₂
α : Type u_14
inst_9 : TopologicalSpace α
f : α → P
⊢ Continuous.{u_14, u_11} (Y := P₂) ((⇑e : (a : P) → P₂) ∘ f) ↔ Continuous f

Tactic:
e.isometry.comp_continuous_iff

Premises used: Isometry.comp_continuous_iff, AffineIsometryEquiv.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
s₁ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_10 + 1} ↥s₁
h : s₁ = ⊤
x : ↥s₁
⊢ (ofTop s₁ h : (a : ↥s₁) → P) x = (↑x : P)

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, 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₁
h : s₁ = ⊤
x : P
⊢ (↑((symm (ofTop s₁ h) : (a : P) → ↥s₁) x) : 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
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_10 + 1} ↥s₁
inst_6 : Nonempty.{u_10 + 1} ↥s₂
h : s₁ = s₂
x : ↥s₁
⊢ (↑((ofEq s₁ s₂ h : (a : ↥s₁) → ↥s₂) x) : P) = (↑x : P)

Tactic:
rfl

Premises used: Set.Mem, 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₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_10 + 1} ↥s₁
inst_6 : Nonempty.{u_10 + 1} ↥s₂
h : s₁ = s₂
⊢ Eq (α := AffineIsometryEquiv.{u_1, u_2, u_2, u_10, u_10} 𝕜 ↥s₂ ↥s₁) (symm (ofEq s₁ s₂ h)) (ofEq s₂ s₁ ⋯)

Tactic:
rfl

Premises used: LinearEquiv.symm, Equiv.setCongr, Equiv.subtypeEquiv, LinearEquiv.ofEq, AffineIsometryEquiv.symm, AffineEquiv.symm, AffineIsometryEquiv.ofEq, Equiv.subtypeEquivProp, Equiv.symm, rfl, AffineEquiv.ofEq
-- 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 (α := AffineIsometryEquiv.{u_1, u_2, u_2, u_10, u_10} 𝕜 ↥s₁ ↥s₁) (ofEq s₁ s₁ ⋯) (refl 𝕜 ↥s₁)

Tactic:
rfl

Premises used: AffineEquiv.refl, AffineIsometryEquiv.refl, Equiv.setCongr, LinearEquiv.ofEq, AffineIsometryEquiv.ofEq, Equiv.subtypeEquivProp, LinearEquiv.refl, Equiv.refl, rfl, AffineEquiv.ofEq
-- 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 : V) → P) (⇑(vaddConst 𝕜 p) : (a : V) → P) fun (v : V) ↦ v +ᵥ 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
p : P
⊢ Eq (α := (v : V) → P) (⇑(AffineEquiv.vaddConst 𝕜 p) : (a : V) → P) fun (v : V) ↦ v +ᵥ 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
p : P
⊢ Eq (α := (a : P) → V) (⇑(symm (vaddConst 𝕜 p)) : (a : P) → V) fun (p' : P) ↦ p' -ᵥ p

Tactic:
rfl

Premises used: rfl