awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
r : ℝ
⊢ preimage.{u_5, u_6} (β := E₂) ((⇑f : (a : E) → E₂) : (a : E) → E₂) (Metric.ball ((f : (a : E) → E₂) x) r : Set E₂) =
    Metric.ball x r

Tactic:
f.isometry.preimage_ball x r

Premises used: Isometry.preimage_ball, 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
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
r : ℝ
⊢ preimage.{u_5, u_6} (β := E₂) ((⇑f : (a : E) → E₂) : (a : E) → E₂) (Metric.sphere ((f : (a : E) → E₂) x) r : Set E₂) =
    Metric.sphere x r

Tactic:
f.isometry.preimage_sphere x r

Premises used: Isometry.preimage_sphere, 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
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
r : ℝ
⊢ preimage.{u_5, u_6} (β := E₂) ((⇑f : (a : E) → E₂) : (a : E) → E₂)
      (Metric.closedBall ((f : (a : E) → E₂) x) r : Set E₂) =
    Metric.closedBall x r

Tactic:
f.isometry.preimage_closedBall x r

Premises used: Isometry.preimage_closedBall, 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
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
⊢ Metric.ediam.{u_6} (X := E₂) ((⇑f : (a : E) → E₂) '' s) = Metric.ediam s

Tactic:
f.isometry.ediam_image s

Premises used: LinearIsometry.isometry, Isometry.ediam_image
-- 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₂
⊢ 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:
f.isometry.ediam_range

Premises used: Isometry.ediam_range, 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
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
⊢ Metric.diam.{u_6} (α := E₂) ((⇑f : (a : E) → E₂) '' s) = Metric.diam s

Tactic:
Isometry.diam_image (LinearIsometry.isometry f) s

Premises used: LinearIsometry.isometry, Isometry.diam_image
-- 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₂
⊢ Metric.diam.{u_6} (α := E₂) (range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → E₂)) = Metric.diam.{u_5} (α := E) univ

Tactic:
Isometry.diam_range (LinearIsometry.isometry f)

Premises used: Isometry.diam_range, 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
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₂
⊢ Injective (α := E →ₛₗᵢ[σ₁₂] E₂) toContinuousLinearMap

Tactic:
fun x _ h =>
  coe_injective (congr_arg _ h : ⇑x.toContinuousLinearMap = _)

Premises used: congr_arg, LinearIsometry.coe_injective, Function.Injective, DFunLike.coe
-- 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.toContinuousLinearMap = g.toContinuousLinearMap ↔ f = g

Tactic:
toContinuousLinearMap_injective.eq_iff

Premises used: Function.Injective.eq_iff, LinearIsometry.toContinuousLinearMap_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.toContinuousLinearMap : (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₂
α : Type u_11
inst_6 : TopologicalSpace α
g : α → E
⊢ Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑f : (a : E) → E₂) ∘ g) ↔
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g

Tactic:
f.isometry.comp_continuous_iff

Premises used: Isometry.comp_continuous_iff, LinearIsometry.isometry
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
⊢ Eq.{u_5 + 1} (α := (a : E) → E) (⇑id : (a : E) → E) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
x : E
⊢ (id : (a : E) → E) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
⊢ Eq.{u_5 + 1} (α := E →ₗ[R] E) (toLinearMap id) LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
⊢ Eq (α := E →L[R] E) (toContinuousLinearMap id) (ContinuousLinearMap.id R E)

Tactic:
rfl

Premises used: ContinuousLinearMap.id, rfl, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R →+* R₂
σ₁₃ : R →+* R₃
σ₂₃ : R₂ →+* R₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : SeminormedAddCommGroup E₃
inst_7 : Module R E
inst_8 : Module R₂ E₂
inst_9 : Module R₃ E₃
g : E₂ →ₛₗᵢ[σ₂₃] E₃
f : E →ₛₗᵢ[σ₁₂] E₂
⊢ Eq (α := (a : E) → E₃) (⇑(g.comp f) : (a : E) → E₃)
    (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := E₂) (⇑g : (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₂
⊢ comp id f = f

Tactic:
ext fun _ => rfl

Premises used: LinearIsometry.ext, 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₂
⊢ f.comp id = f

Tactic:
ext fun _ => rfl

Premises used: LinearIsometry.ext, rfl
-- 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
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₄
inst_4 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_5 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst_6 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_7 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_8 : SeminormedAddCommGroup E
inst_9 : SeminormedAddCommGroup E₂
inst_10 : SeminormedAddCommGroup E₃
inst_11 : SeminormedAddCommGroup E₄
inst_12 : Module R E
inst_13 : Module R₂ E₂
inst_14 : Module R₃ E₃
inst_15 : Module R₄ E₄
f : E₃ →ₛₗᵢ[σ₃₄] E₄
g : E₂ →ₛₗᵢ[σ₂₃] E₃
h : E →ₛₗᵢ[σ₁₂] E₂
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: LinearIsometry.comp, rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
⊢ Eq.{u_5 + 1} (α := (a : E) → E) (⇑1 : (a : E) → E) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
f g : E →ₗᵢ[R] E
⊢ Eq (α := (a : E) → E) (⇑(f * g) : (a : E) → E) (Function.comp (β := E) (⇑f : (a : E) → E) (⇑g : (a : E) → E))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
⊢ Eq.{u_5 + 1} (α := E →ₗᵢ[R] E) 1 id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
f g : E →ₗᵢ[R] E
⊢ f * g = f.comp g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
f : E →ₗᵢ[R] E
n : ℕ
⊢ Eq (α := (a : E) → E) (⇑(f ^ n) : (a : E) → E) (⇑f : (a : E) → E)^[n]

Tactic:
hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _

Premises used: hom_coe_pow
-- 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₂
hf : Isometry.{u_5, u_6} (α := E) (β := E₂) (⇑f : (a : E) → E₂)
simp_rw : ∀ (x : E), dist.{u_6} (α := E₂) ((f : (a : E) → E₂) x : E₂) (0 : E₂) = dist x 0
⊢ ∀ (x : E), norm.{u_6} (E := E₂) ((f : (a : E) → E₂) x : E₂) = ‖x‖

Tactic:
simp_rw [← dist_zero_right]

Premises used: dist_zero_right
-- 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₂
hf : Isometry.{u_5, u_6} (α := E) (β := E₂) (⇑f : (a : E) → E₂)
⊢ ∀ (x : E), dist.{u_6} (α := E₂) ((f : (a : E) → E₂) x : E₂) (0 : E₂) = dist x 0

Tactic:
simpa using (hf.dist_eq · 0)

Premises used: Isometry.dist_eq, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
E : Type u_5
inst : SeminormedAddCommGroup E
R' : Type u_11
inst_1 : Ring R'
inst_2 : Module R' E
p : Submodule R' E
⊢ Eq (α := (a : ↥p) → E) (⇑p.subtypeₗᵢ : (a : ↥p) → E) (⇑p.subtype : (a : ↥p) → E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
E : Type u_5
inst : SeminormedAddCommGroup E
R' : Type u_11
inst_1 : Ring R'
inst_2 : Module R' E
p : Submodule R' E
⊢ p.subtypeₗᵢ.toLinearMap = p.subtype

Tactic:
rfl

Premises used: Submodule.subtype, rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
E : Type u_5
inst : SeminormedAddCommGroup E
R' : Type u_11
inst_1 : Ring R'
inst_2 : Module R' E
p : Submodule R' E
⊢ p.subtypeₗᵢ.toContinuousLinearMap = p.subtypeL

Tactic:
rfl

Premises used: Submodule.subtypeL, Submodule.subtype, rfl, LinearIsometry.toContinuousLinearMap
-- 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
inst_34 : EquivLike 𝓕 E E₂
s : SemilinearIsometryEquivClass 𝓕 σ₁₂ E E₂
⊢ SemilinearIsometryClass 𝓕 σ₁₂ E E₂

Tactic:
{ s with }

Premises used: SemilinearIsometryEquivClass.norm_map, SemilinearIsometryClass.mk
-- 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₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
f g : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ f.toLinearEquiv = g.toLinearEquiv ↔ f = g

Tactic:
toLinearEquiv_injective.eq_iff

Premises used: Function.Injective.eq_iff, LinearIsometryEquiv.toLinearEquiv_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₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
⊢ Injective (α := E ≃ₛₗᵢ[σ₁₂] E₂) (β := E → E₂) (DFunLike.coe (β := fun (a : E) ↦ E₂))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_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₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗ[σ₁₂] E₂
he : ∀ (x : E), norm.{u_6} (E := E₂) ((e : (a : E) → E₂) x : E₂) = ‖x‖
⊢ Eq (α := (a : E) → E₂) (⇑{ toLinearEquiv := e, norm_map' := he : E ≃ₛₗᵢ[σ₁₂] E₂ } : (a : E) → E₂) (⇑e : (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₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ Eq (α := (a : E) → E₂) (⇑e.toLinearEquiv : (a : E) → E₂) (⇑e : (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₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e e' : E ≃ₛₗᵢ[σ₁₂] E₂
h : ∀ (x : E), Eq.{u_6 + 1} (α := E₂) ((e : (a : E) → E₂) x : E₂) ((e' : (a : E) → E₂) x : E₂)
⊢ e = e'

Tactic:
toLinearEquiv_injective <| LinearEquiv.ext h

Premises used: LinearEquiv.ext, LinearIsometryEquiv.toLinearEquiv_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₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
f g : E ≃ₛₗᵢ[σ₁₂] E₂
h : f = g
x : E
⊢ Eq.{u_6 + 1} (α := E₂) ((f : (a : E) → E₂) x : E₂) ((g : (a : E) → E₂) x : E₂)

Tactic:
h ▸ rfl

Premises used: Eq.rec, rfl
-- 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
e_1 : E ≃ₛₗᵢ[σ₁₂] E₂
e : E ≃ₛₗ[σ₁₂] E₂
h₁ : ∀ (x : E), norm.{u_6} (E := E₂) ((e : (a : E) → E₂) x : E₂) ≤ ‖x‖
h₂ : ∀ (y : E₂), norm.{u_5} (E := E) ((e.symm : (a : E₂) → E) y : E) ≤ ‖y‖
x : E
⊢ ‖x‖ ≤ norm.{u_6} (E := E₂) ((e : (a : E) → E₂) x : E₂)

Tactic:
simpa only [e.symm_apply_apply] using h₂ (e x)

Premises used: LinearEquiv.symm_apply_apply, DFunLike.coe
-- 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₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x : E
⊢ norm.{u_6} (E := E₂) ((e : (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₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x : E
⊢ nnnorm.{u_6} (E := E₂) ((e : (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₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x : E
⊢ enorm.{u_6} (E := E₂) ((e : (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₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
⊢ Injective (α := E ≃ₛₗᵢ[σ₁₂] E₂) toLinearIsometry

Tactic:
fun x _ h => coe_injective (congr_arg _ h : ⇑x.toLinearIsometry = _)

Premises used: LinearIsometryEquiv.coe_injective, congr_arg, Function.Injective, DFunLike.coe
-- 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₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
f g : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ f.toLinearIsometry = g.toLinearIsometry ↔ f = g

Tactic:
toLinearIsometry_injective.eq_iff

Premises used: Function.Injective.eq_iff, LinearIsometryEquiv.toLinearIsometry_injective