awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Extend
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
x_1 x : E
⊢ norm.{u_6} (E := Fₗ) ((e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F) : (a : E) → Fₗ) x : Fₗ) ≤
    1 * norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)

Tactic:
simp [h_norm x]
-- Module: Mathlib.Analysis.Normed.Operator.Extend
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
x_1 x : F
⊢ norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)

Tactic:
simpa using (h_norm (f.symm x)).symm

Premises used: LinearEquiv.symm, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.Extend
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
x_1 : F
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
x : F
⊢ norm.{u_4} (E := Eₗ) ((e₁ ∘ₛₗ (↑f.symm : F →ₛₗ[σ₂₁] E) : (a : F) → Eₗ) x : Eₗ) ≤
    1 * norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)

Tactic:
simp [h_norm₂ x]
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
𝓕 : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
inst_6 : FunLike 𝓕 E E₂
inst_7 : SemilinearIsometryClass 𝓕 σ₁₂ E E₂
f : 𝓕
⊢ Isometry.{u_5, u_6} (α := E) (β := E₂) (⇑f : (a : E) → E₂)

Tactic:
AddMonoidHomClass.isometry_of_norm _ (norm_map _)

Premises used: AddMonoidHomClass.isometry_of_norm, SemilinearIsometryClass.norm_map
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
𝓕 : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
inst_6 : FunLike 𝓕 E E₂
inst_7 : SemilinearIsometryClass 𝓕 σ₁₂ E E₂
f : 𝓕
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : E) → E₂)

Tactic:
(SemilinearIsometryClass.isometry f).continuous

Premises used: Isometry.continuous, SemilinearIsometryClass.isometry
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
𝓕 : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
inst_6 : FunLike 𝓕 E E₂
inst_7 : SemilinearIsometryClass 𝓕 σ₁₂ E E₂
f : 𝓕
x : E
⊢ nnnorm.{u_6} (E := E₂) ((f : (a : E) → E₂) x : E₂) = ‖x‖₊

Tactic:
NNReal.eq <| norm_map f x

Premises used: NNReal.eq, SemilinearIsometryClass.norm_map
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
𝓕 : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
inst_6 : FunLike 𝓕 E E₂
inst_7 : SemilinearIsometryClass 𝓕 σ₁₂ E E₂
f : 𝓕
⊢ LipschitzWith.{u_5, u_6} (α := E) (β := E₂) 1 (⇑f : (a : E) → E₂)

Tactic:
(SemilinearIsometryClass.isometry f).lipschitz

Premises used: Isometry.lipschitz, SemilinearIsometryClass.isometry
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
𝓕 : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
inst_6 : FunLike 𝓕 E E₂
inst_7 : SemilinearIsometryClass 𝓕 σ₁₂ E E₂
f : 𝓕
⊢ AntilipschitzWith.{u_5, u_6} (α := E) (β := E₂) 1 (⇑f : (a : E) → E₂)

Tactic:
(SemilinearIsometryClass.isometry f).antilipschitz

Premises used: Isometry.antilipschitz, SemilinearIsometryClass.isometry
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
𝓕 : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
inst_6 : FunLike 𝓕 E E₂
inst_7 : SemilinearIsometryClass 𝓕 σ₁₂ E E₂
f : 𝓕
s : Set E
⊢ Metric.ediam.{u_6} (X := E₂) ((⇑f : (a : E) → E₂) '' s) = Metric.ediam s

Tactic:
(SemilinearIsometryClass.isometry f).ediam_image s

Premises used: Isometry.ediam_image, SemilinearIsometryClass.isometry
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
𝓕 : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
inst_6 : FunLike 𝓕 E E₂
inst_7 : SemilinearIsometryClass 𝓕 σ₁₂ E E₂
f : 𝓕
⊢ Metric.ediam.{u_6} (X := E₂) (range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → E₂)) = Metric.ediam.{u_5} (X := E) univ

Tactic:
(SemilinearIsometryClass.isometry f).ediam_range

Premises used: Isometry.ediam_range, SemilinearIsometryClass.isometry
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
𝓕 : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
inst_6 : FunLike 𝓕 E E₂
inst_7 : SemilinearIsometryClass 𝓕 σ₁₂ E E₂
f : 𝓕
s : Set E
⊢ Metric.diam.{u_6} (α := E₂) ((⇑f : (a : E) → E₂) '' s) = Metric.diam s

Tactic:
(SemilinearIsometryClass.isometry f).diam_image s

Premises used: Isometry.diam_image, SemilinearIsometryClass.isometry
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
𝓕 : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
inst_6 : FunLike 𝓕 E E₂
inst_7 : SemilinearIsometryClass 𝓕 σ₁₂ E E₂
f : 𝓕
⊢ Metric.diam.{u_6} (α := E₂) (range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → E₂)) = Metric.diam.{u_5} (α := E) univ

Tactic:
(SemilinearIsometryClass.isometry f).diam_range

Premises used: Isometry.diam_range, SemilinearIsometryClass.isometry
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f g : E →ₛₗᵢ[σ₁₂] E₂
⊢ f.toLinearMap = g.toLinearMap ↔ f = g

Tactic:
toLinearMap_injective.eq_iff

Premises used: Function.Injective.eq_iff, LinearIsometry.toLinearMap_injective
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
⊢ Eq (α := (a : E) → E₂) (⇑f.toLinearMap : (a : E) → E₂) (⇑f : (a : E) → E₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗ[σ₁₂] E₂
hf : ∀ (x : E), norm.{u_6} (E := E₂) ((f : (a : E) → E₂) x : E₂) = ‖x‖
⊢ Eq (α := (a : E) → E₂) (⇑{ toLinearMap := f, norm_map' := hf : E →ₛₗᵢ[σ₁₂] E₂ } : (a : E) → E₂) (⇑f : (a : E) → E₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
toLinearMap : E →ₛₗ[σ₁₂] E₂
norm_map' : ∀ (x : E), norm.{u_6} (E := E₂) ((toLinearMap : (a : E) → E₂) x : E₂) = ‖x‖
toLinearMap_1 : E →ₛₗ[σ₁₂] E₂
norm_map'_1 : ∀ (x : E), norm.{u_6} (E := E₂) ((toLinearMap_1 : (a : E) → E₂) x : E₂) = ‖x‖
⊢ Eq (α := E → E₂)
      ((fun (f : E →ₛₗᵢ[σ₁₂] E₂) ↦ ((⇑f : (a : E) → E₂) : (a : E) → E₂))
        { toLinearMap := toLinearMap, norm_map' := norm_map' })
      ((fun (f : E →ₛₗᵢ[σ₁₂] E₂) ↦ ((⇑f : (a : E) → E₂) : (a : E) → E₂))
        { toLinearMap := toLinearMap_1, norm_map' := norm_map'_1 }) →
    { toLinearMap := toLinearMap, norm_map' := norm_map' : E →ₛₗᵢ[σ₁₂] E₂ } =
      { toLinearMap := toLinearMap_1, norm_map' := norm_map'_1 }

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f g : E →ₛₗᵢ[σ₁₂] E₂
h : ∀ (x : E), Eq.{u_6 + 1} (α := E₂) ((f : (a : E) → E₂) x : E₂) ((g : (a : E) → E₂) x : E₂)
⊢ f = g

Tactic:
coe_injective <| funext h

Premises used: LinearIsometry.coe_injective, funext
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
⊢ Eq.{u_6 + 1} (α := E₂) ((f : (a : E) → E₂) 0 : E₂) (0 : E₂)

Tactic:
f.toLinearMap.map_zero

Premises used: LinearMap.map_zero, LinearIsometry.toLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
x y : E
⊢ (f : (a : E) → E₂) (x + y) = HAdd.hAdd (α := E₂) (β := E₂) ((f : (a : E) → E₂) x : E₂) ((f : (a : E) → E₂) y : E₂)

Tactic:
f.toLinearMap.map_add x y

Premises used: LinearMap.map_add, LinearIsometry.toLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
x : E
⊢ Eq.{u_6 + 1} (α := E₂) ((f : (a : E) → E₂) (-x) : E₂) (-(f : (a : E) → E₂) x : E₂)

Tactic:
f.toLinearMap.map_neg x

Premises used: LinearMap.map_neg, LinearIsometry.toLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
x y : E
⊢ (f : (a : E) → E₂) (x - y) = HSub.hSub (α := E₂) (β := E₂) ((f : (a : E) → E₂) x : E₂) ((f : (a : E) → E₂) y : E₂)

Tactic:
f.toLinearMap.map_sub x y

Premises used: LinearIsometry.toLinearMap, LinearMap.map_sub
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
c : R
x : E
⊢ (f : (a : E) → E₂) (c • x) =
    HSMul.hSMul.{u_2, u_6, u_6} (α := R₂) (β := E₂) ((σ₁₂ : (a : R) → R₂) c : R₂) ((f : (a : E) → E₂) x : E₂)

Tactic:
f.toLinearMap.map_smulₛₗ c x

Premises used: LinearIsometry.toLinearMap, LinearMap.map_smulₛₗ
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup E₂
inst_3 : Module R E
inst_4 : Module R E₂
f : E →ₗᵢ[R] E₂
c : R
x : E
⊢ (f : (a : E) → E₂) (c • x) = HSMul.hSMul (β := E₂) c ((f : (a : E) → E₂) x : E₂)

Tactic:
f.toLinearMap.map_smul c x

Premises used: LinearIsometry.toLinearMap, LinearMap.map_smul
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
x : E
⊢ norm.{u_6} (E := E₂) ((f : (a : E) → E₂) x : E₂) = ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
x : E
⊢ nnnorm.{u_6} (E := E₂) ((f : (a : E) → E₂) x : E₂) = ‖x‖₊

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
x : E
⊢ enorm.{u_6} (E := E₂) ((f : (a : E) → E₂) x : E₂) = ‖x‖ₑ

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
⊢ Isometry.{u_5, u_6} (α := E) (β := E₂) (⇑f : (a : E) → E₂)

Tactic:
AddMonoidHomClass.isometry_of_norm f.toLinearMap f.norm_map

Premises used: LinearIsometry.norm_map, AddMonoidHomClass.isometry_of_norm, LinearIsometry.toLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E₂ : Type u_6
F : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E₂
inst_3 : Module R₂ E₂
inst_4 : NormedAddCommGroup F
inst_5 : Module R F
f : F →ₛₗᵢ[σ₁₂] E₂
⊢ IsEmbedding.{u_9, u_6} (X := F) (Y := E₂) (⇑f : (a : F) → E₂)

Tactic:
f.isometry.isEmbedding

Premises used: Isometry.isEmbedding, LinearIsometry.isometry
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
𝓕 : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
inst_6 : FunLike 𝓕 E E₂
inst_7 : SemilinearIsometryClass 𝓕 σ₁₂ E E₂
f : 𝓕
s : Set E
⊢ IsComplete.{u_6} (α := E₂) ((⇑f : (a : E) → E₂) '' s) ↔ IsComplete s

Tactic:
_root_.isComplete_image_iff (SemilinearIsometryClass.isometry f).isUniformInducing

Premises used: Isometry.isUniformInducing, isComplete_image_iff, SemilinearIsometryClass.isometry
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
s : Set E
⊢ IsComplete.{u_6} (α := E₂) ((⇑f : (a : E) → E₂) '' s) ↔ IsComplete s

Tactic:
LinearIsometry.isComplete_image_iff _

Premises used: LinearIsometry.isComplete_image_iff
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
inst_6 : RingHomSurjective σ₁₂
p : Submodule R E
⊢ IsComplete (↑(Submodule.map f.toLinearMap p) : Set E₂) ↔ IsComplete (↑p : Set E)

Tactic:
isComplete_image_iff f

Premises used: setOf, LinearIsometry.isComplete_image_iff, Set.image
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
inst_8 : RingHomInvPair σ₂₃ σ₃₂
inst_9 : RingHomInvPair σ₃₂ σ₂₃
inst_10 : RingHomInvPair σ₁₄ σ₄₁
inst_11 : RingHomInvPair σ₄₁ σ₁₄
inst_12 : RingHomInvPair σ₂₄ σ₄₂
inst_13 : RingHomInvPair σ₄₂ σ₂₄
inst_14 : RingHomInvPair σ₃₄ σ₄₃
inst_15 : RingHomInvPair σ₄₃ σ₃₄
inst_16 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_17 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst_18 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_19 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_20 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_21 : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst_22 : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst_23 : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst_24 : SeminormedAddCommGroup E
inst_25 : SeminormedAddCommGroup E₂
inst_26 : SeminormedAddCommGroup E₃
inst_27 : SeminormedAddCommGroup E₄
inst_28 : Module R E
inst_29 : Module R₂ E₂
inst_30 : Module R₃ E₃
inst_31 : Module R₄ E₄
inst_32 : NormedAddCommGroup F
inst_33 : Module R F
f : E →ₛₗᵢ[σ₁₂] E₂
f₁ : F →ₛₗᵢ[σ₁₂] E₂
inst_34 : FunLike 𝓕 E E₂
inst_35 : RingHomSurjective σ₁₂
p : Submodule R E
inst_36 : CompleteSpace.{u_5} ↥p
⊢ CompleteSpace.{u_6}
    ↥(Submodule.map
        (↑f :
          [inst_37 : FunLike (E →ₛₗᵢ[σ₁₂] E₂) E E₂] → [SemilinearMapClass (E →ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂] → E →ₛₗ[σ₁₂] E₂)
        p)

Tactic:
((isComplete_map_iff f).2 <| completeSpace_coe_iff_isComplete.1 ‹_›).completeSpace_coe

Premises used: Iff.mpr, IsComplete.completeSpace_coe, Set.Mem, LinearIsometry.isComplete_map_iff, Iff.mp, completeSpace_coe_iff_isComplete
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
x y : E
⊢ dist.{u_6} (α := E₂) ((f : (a : E) → E₂) x : E₂) ((f : (a : E) → E₂) y : E₂) = dist x y

Tactic:
f.isometry.dist_eq x y

Premises used: LinearIsometry.isometry, Isometry.dist_eq
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
x y : E
⊢ edist.{u_6} (α := E₂) ((f : (a : E) → E₂) x : E₂) ((f : (a : E) → E₂) y : E₂) = edist x y

Tactic:
f.isometry.edist_eq x y

Premises used: Isometry.edist_eq, LinearIsometry.isometry
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E₂ : Type u_6
F : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E₂
inst_3 : Module R₂ E₂
inst_4 : NormedAddCommGroup F
inst_5 : Module R F
f₁ : F →ₛₗᵢ[σ₁₂] E₂
⊢ Injective.{u_9 + 1, u_6 + 1} (α := F) (β := E₂) (⇑f₁ : (a : F) → E₂)

Tactic:
Isometry.injective (LinearIsometry.isometry f₁)

Premises used: Isometry.injective, LinearIsometry.isometry
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E₂ : Type u_6
F : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E₂
inst_3 : Module R₂ E₂
inst_4 : NormedAddCommGroup F
inst_5 : Module R F
f₁ : F →ₛₗᵢ[σ₁₂] E₂
x y : F
⊢ Eq.{u_6 + 1} (α := E₂) ((f₁ : (a : F) → E₂) x : E₂) ((f₁ : (a : F) → E₂) y : E₂) ↔ x = y

Tactic:
f₁.injective.eq_iff

Premises used: Function.Injective.eq_iff, LinearIsometry.injective
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E₂ : Type u_6
F : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E₂
inst_3 : Module R₂ E₂
inst_4 : NormedAddCommGroup F
inst_5 : Module R F
f₁ : F →ₛₗᵢ[σ₁₂] E₂
x y : F
h : x ≠ y
⊢ Ne.{u_6 + 1} (α := E₂) ((f₁ : (a : F) → E₂) x : E₂) ((f₁ : (a : F) → E₂) y : E₂)

Tactic:
f₁.injective.ne h

Premises used: Function.Injective.ne, LinearIsometry.injective
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
⊢ LipschitzWith.{u_5, u_6} (α := E) (β := E₂) 1 (⇑f : (a : E) → E₂)

Tactic:
f.isometry.lipschitz

Premises used: LinearIsometry.isometry, Isometry.lipschitz
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
⊢ AntilipschitzWith.{u_5, u_6} (α := E) (β := E₂) 1 (⇑f : (a : E) → E₂)

Tactic:
f.isometry.antilipschitz

Premises used: LinearIsometry.isometry, Isometry.antilipschitz
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup E₂
inst_4 : Module R E
inst_5 : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : E) → E₂)

Tactic:
f.isometry.continuous

Premises used: Isometry.continuous, LinearIsometry.isometry