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₂
σ₂₁ : 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
r : ℝ
⊢ Eq.{u_6 + 1} (α := Set E₂) ((⇑e : (a : E) → E₂) '' Metric.closedBall x r : Set E₂)
    (Metric.closedBall ((e : (a : E) → E₂) x) r : Set E₂)

Tactic:
e.toIsometryEquiv.image_closedBall x r

Premises used: LinearIsometryEquiv.toIsometryEquiv, IsometryEquiv.image_closedBall
-- 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₂
α : Type u_11
inst_8 : TopologicalSpace α
f : α → E
s : Set α
⊢ ContinuousOn.{u_11, u_6} (Y := E₂) ((⇑e : (a : E) → E₂) ∘ f) s ↔ ContinuousOn f s

Tactic:
e.isometry.comp_continuousOn_iff

Premises used: LinearIsometryEquiv.isometry, Isometry.comp_continuousOn_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₂
σ₂₁ : 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₂
α : Type u_11
inst_8 : TopologicalSpace α
f : α → E
⊢ Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑e : (a : E) → E₂) ∘ f) ↔
    Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
e.isometry.comp_continuous_iff

Premises used: Isometry.comp_continuous_iff, LinearIsometryEquiv.isometry
-- 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 : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst_34 : TopologicalSpace α
p : Submodule R E
inst_35 : CompleteSpace.{u_5} ↥p
⊢ CompleteSpace.{u_6} ↥(Submodule.map (↑(↑(↑e : E ≃SL[σ₁₂] E₂) : E ≃ₛₗ[σ₁₂] E₂) : E →ₛₗ[σ₁₂] E₂) p)

Tactic:
e.toLinearIsometry.completeSpace_map p

Premises used: LinearIsometryEquiv.toLinearIsometry, Set.Mem, LinearIsometry.completeSpace_map
-- 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₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E₂
inst_5 : Module R₂ E₂
inst_6 : NormedAddCommGroup F
inst_7 : Module R F
f : F →ₛₗᵢ[σ₁₂] E₂
hfr : Surjective.{u_9 + 1, u_6 + 1} (α := F) (β := E₂) (⇑f : (a : F) → E₂)
h : ∀ (x : F), Eq.{u_6 + 1} (α := E₂) ((ofSurjective f hfr : (a : F) → E₂) x : E₂) ((f : (a : F) → E₂) x : E₂)
⊢ Eq (α := (a : F) → E₂) (⇑(ofSurjective f hfr) : (a : F) → E₂) (⇑f : (a : F) → E₂)

Tactic:
ext
-- 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₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E₂
inst_5 : Module R₂ E₂
inst_6 : NormedAddCommGroup F
inst_7 : Module R F
f : F →ₛₗᵢ[σ₁₂] E₂
hfr : Surjective.{u_9 + 1, u_6 + 1} (α := F) (β := E₂) (⇑f : (a : F) → E₂)
x : F
⊢ Eq.{u_6 + 1} (α := E₂) ((ofSurjective f hfr : (a : F) → E₂) x : E₂) ((f : (a : F) → E₂) x : E₂)

Tactic:
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₂
f : E →ₛₗᵢ[σ₁₂] E₂
g : E₂ →ₛₗ[σ₂₁] E
h₁ : f.toLinearMap ∘ₛₗ g = LinearMap.id
h₂ : g ∘ₛₗ f.toLinearMap = LinearMap.id
⊢ Eq (α := (a : E) → E₂) (⇑(ofLinearIsometry f g h₁ h₂) : (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₂
σ₂₁ : 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 : E →ₛₗᵢ[σ₁₂] E₂
g : E₂ →ₛₗ[σ₂₁] E
h₁ : f.toLinearMap ∘ₛₗ g = LinearMap.id
h₂ : g ∘ₛₗ f.toLinearMap = LinearMap.id
⊢ Eq (α := (a : E₂) → E) (⇑(symm (ofLinearIsometry f g h₁ h₂)) : (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} (α := (a : E) → E) (⇑(neg R) : (a : E) → E) fun (x : E) ↦ -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) (symm (neg R)) (neg R)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, LinearEquiv.neg, LinearIsometryEquiv.neg, 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 : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst_34 : TopologicalSpace α
inst_35 : Module R E₂
x : E × E₂
⊢ norm (E := E₂ × E) (((LinearEquiv.prodComm R E E₂ : (E × E₂) ≃ₗ[R] E₂ × E) : (a : E × E₂) → E₂ × E) x : E₂ × E) = ‖x‖

Tactic:
simp [norm, sup_comm]

Premises used: Norm.norm, sup_comm
-- 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₂
⊢ Eq (α := E₂ × E ≃ₗᵢ[R] E × E₂) (symm (prodComm R E E₂)) (prodComm R E₂ E)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, LinearEquiv.prodComm, Prod.swap, LinearIsometryEquiv.prodComm, 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₂
α : Type u_11
inst_34 : TopologicalSpace α
inst_35 : Module R E₂
inst_36 : Module R E₃
g : E₃
e : E
f : E₂
⊢ norm (E := E × E₂ × E₃)
      (((LinearEquiv.prodAssoc R E E₂ E₃ : ((E × E₂) × E₃) ≃ₗ[R] E × E₂ × E₃) : (a : (E × E₂) × E₃) → E × E₂ × E₃)
          ((e, f), g) :
        E × E₂ × E₃) =
    ‖((e, f), g)‖

Tactic:
simp only [LinearEquiv.prodAssoc_apply, AddEquiv.toEquiv_eq_coe,
        Equiv.toFun_as_coe, EquivLike.coe_coe, AddEquiv.coe_prodAssoc,
        Equiv.prodAssoc_apply, Prod.norm_def, max_assoc]

Premises used: Equiv.toFun_as_coe, Equiv.prodAssoc_apply, AddEquiv.coe_prodAssoc, Prod.norm_def, AddEquiv.toEquiv_eq_coe, LinearEquiv.prodAssoc_apply, max_assoc, EquivLike.coe_coe
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup E₂
inst_3 : SeminormedAddCommGroup E₃
inst_4 : Module R E
inst_5 : Module R E₂
inst_6 : Module R E₃
⊢ Eq (α := (a : (E × E₂) × E₃) → E × E₂ × E₃) (⇑(prodAssoc R E E₂ E₃) : (a : (E × E₂) × E₃) → E × E₂ × E₃)
    (⇑(Equiv.prodAssoc E E₂ E₃) : (a : (E × E₂) × E₃) → E × E₂ × E₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup E₂
inst_3 : SeminormedAddCommGroup E₃
inst_4 : Module R E
inst_5 : Module R E₂
inst_6 : Module R E₃
⊢ Eq (α := (a : E × E₂ × E₃) → (E × E₂) × E₃) (⇑(symm (prodAssoc R E E₂ E₃)) : (a : E × E₂ × E₃) → (E × E₂) × E₃)
    (⇑(Equiv.prodAssoc E E₂ E₃).symm : (a : E × E₂ × E₃) → (E × E₂) × E₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
E : Type u_5
inst : SeminormedAddCommGroup E
R' : Type u_12
inst_1 : Ring R'
inst_2 : Module R' E
p q : Submodule R' E
h : p = q
x : ↥p
⊢ (↑((ofEq p q h : (a : ↥p) → ↥q) x) : E) = (↑x : E)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
E : Type u_5
inst : SeminormedAddCommGroup E
R' : Type u_12
inst_1 : Ring R'
inst_2 : Module R' E
p q : Submodule R' E
h : p = q
⊢ (ofEq p q h).symm = ofEq q p ⋯

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, LinearIsometryEquiv.ofEq, LinearEquiv.ofEq, rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
E : Type u_5
inst : SeminormedAddCommGroup E
R' : Type u_12
inst_1 : Ring R'
inst_2 : Module R' E
p : Submodule R' E
⊢ ofEq p p ⋯ = refl R' ↥p

Tactic:
rfl

Premises used: LinearIsometryEquiv.refl, LinearIsometryEquiv.ofEq, LinearEquiv.ofEq, LinearEquiv.refl, 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₂
ι : Type u_11
b : Basis ι R E
f₁ f₂ : E →ₛₗᵢ[σ₁₂] E₂
h :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := E₂) ((f₁ : (a : E) → E₂) ((b : (a : ι) → E) i : E) : E₂)
      ((f₂ : (a : E) → E₂) ((b : (a : ι) → E) i : E) : E₂)
⊢ f₁ = f₂

Tactic:
LinearIsometry.toLinearMap_injective <| b.ext h

Premises used: LinearIsometry.toLinearMap_injective, Module.Basis.ext
-- 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₂
ι : Type u_11
b : Basis ι R E
f₁ f₂ : E ≃ₛₗᵢ[σ₁₂] E₂
h :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := E₂) ((f₁ : (a : E) → E₂) ((b : (a : ι) → E) i : E) : E₂)
      ((f₂ : (a : E) → E₂) ((b : (a : ι) → E) i : E) : E₂)
⊢ f₁ = f₂

Tactic:
LinearIsometryEquiv.toLinearEquiv_injective <| b.ext' h

Premises used: LinearIsometryEquiv.toLinearEquiv_injective, Module.Basis.ext'
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_11
H : Type u_12
inst : Semiring R
inst_1 : SeminormedAddCommGroup H
inst_2 : Module R H
⊢ Isometry.{u_12, u_12} (α := H) (β := Hᵐᵒᵖ) (⇑(opLinearEquiv R) : (a : H) → Hᵐᵒᵖ)

Tactic:
fun _ _ => rfl

Premises used: MulOpposite.unop, rfl, Isometry
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_11
H : Type u_12
inst : Semiring R
inst_1 : SeminormedAddCommGroup H
inst_2 : Module R H
⊢ Eq (α := H ≃ₗ[R] Hᵐᵒᵖ) (LinearIsometryEquiv.toLinearEquiv (opLinearIsometryEquiv R H)) (opLinearEquiv R)

Tactic:
rfl

Premises used: MulOpposite.opLinearEquiv, rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_11
H : Type u_12
inst : Semiring R
inst_1 : SeminormedAddCommGroup H
inst_2 : Module R H
⊢ Eq (α := H ≃L[R] Hᵐᵒᵖ) (↑(opLinearIsometryEquiv R H) : H ≃L[R] Hᵐᵒᵖ) (opContinuousLinearEquiv R)

Tactic:
rfl

Premises used: MulOpposite.opLinearEquiv, MulOpposite, MulOpposite.opContinuousLinearEquiv, MulOpposite.unop, LinearIsometryEquiv.toContinuousLinearEquiv, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : NonUnitalSeminormedRing R
inst_4 : NormedSpace 𝕜 R
inst_5 : IsScalarTower 𝕜 R R
inst_6 : SMulCommClass 𝕜 R R
x y : R
⊢ norm (E := R)
      (((((LinearMap.mul 𝕜 R : R →ₗ[𝕜] R →ₗ[𝕜] R) : (a : R) → R →ₗ[𝕜] R) x : R →ₗ[𝕜] R) : (a : R) → R) y : R) ≤
    1 * ‖x‖ * ‖y‖

Tactic:
simpa using norm_mul_le x y

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalSeminormedRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
x y : R
⊢ (((mul 𝕜 R : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R) : (a : R) → R) y = x * y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalSeminormedRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
x : R
⊢ norm (E := R →L[𝕜] R) ((mul 𝕜 R : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R) ≤ ‖x‖

Tactic:
opNorm_le_bound _ (norm_nonneg x) (norm_mul_le x)

Premises used: ContinuousLinearMap.opNorm_le_bound, norm_mul_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalSeminormedRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
⊢ norm (E := R →L[𝕜] R →L[𝕜] R) (mul 𝕜 R) ≤ 1

Tactic:
LinearMap.mkContinuous₂_norm_le _ zero_le_one _

Premises used: zero_le_one, LinearMap.mkContinuous₂_norm_le, ContinuousLinearMap.mul
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalSeminormedRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
⊢ Eq (α := (a : R) → R →L[𝕜] R) (⇑(NonUnitalAlgHom.Lmul 𝕜 R) : (a : R) → R →L[𝕜] R) (⇑(mul 𝕜 R) : (a : R) → R →L[𝕜] R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalSeminormedRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
x y z : R
⊢ (((((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) x : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R) y : R →L[𝕜] R) :
        (a : R) → R)
      z =
    x * z * y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalSeminormedRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
x y : R
⊢ norm (E := R →L[𝕜] R)
      ((((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) x : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R) y : R →L[𝕜] R) ≤
    ‖x‖ * ‖y‖

Tactic:
(opNorm_comp_le _ _).trans <|
    (mul_comm _ _).trans_le <|
      mul_le_mul (opNorm_mul_apply_le _ _ _)
        (opNorm_le_bound _ (norm_nonneg _) fun _ => (norm_mul_le _ _).trans_eq (mul_comm _ _))
        (norm_nonneg _) (norm_nonneg _)

Premises used: ContinuousLinearMap.comp, Norm.norm, LE.le.trans_eq, ContinuousLinearMap.opNorm_le_bound, ContinuousLinearMap.opNorm_comp_le, Eq.trans_le, mul_le_mul, ContinuousLinearMap.opNorm_mul_apply_le, mul_comm, LE.le.trans, norm_mul_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalSeminormedRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
x : R
⊢ norm (E := R →L[𝕜] R →L[𝕜] R) ((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) x : R →L[𝕜] R →L[𝕜] R) ≤ ‖x‖

Tactic:
opNorm_le_bound _ (norm_nonneg x) (opNorm_mulLeftRight_apply_apply_le 𝕜 R x)

Premises used: ContinuousLinearMap.opNorm_le_bound, ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
⊢ LE.le (α := ℕ) sorry 1

Tactic:
opNorm_le_bound _ zero_le_one fun x => (one_mul ‖x‖).symm ▸ opNorm_mulLeftRight_apply_le 𝕜 R x

Premises used: ContinuousLinearMap.opNorm_le_bound, zero_le_one
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜_1 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜_1
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜_1 E
R_1 : Type u_3
inst_3 : NonUnitalSeminormedRing R_1
inst_4 : NormedSpace 𝕜_1 R_1
inst_5 : IsScalarTower 𝕜_1 R_1 R_1
inst_6 : SMulCommClass 𝕜_1 R_1 R_1
𝕜 : Type u_4
R : Type u_5
inst_7 : NontriviallyNormedField 𝕜
inst_8 : SeminormedRing R
inst_9 : NormedAlgebra 𝕜 R
inst_10 : NormOneClass R
x : R
h : ‖x‖ = norm (E := R) ((((mul 𝕜 R : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R) : (a : R) → R) 1 : R) / norm.{u_5} (E := R) 1
⊢ ‖x‖ ≤ norm (E := R →L[𝕜] R) ((mul 𝕜 R : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R)

Tactic:
convert! ratio_le_opNorm ((mul 𝕜 R) x) (1 : R)

Premises used: ContinuousLinearMap.ratio_le_opNorm, ContinuousLinearMap.mul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜_1 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜_1
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜_1 E
R_1 : Type u_3
inst_3 : NonUnitalSeminormedRing R_1
inst_4 : NormedSpace 𝕜_1 R_1
inst_5 : IsScalarTower 𝕜_1 R_1 R_1
inst_6 : SMulCommClass 𝕜_1 R_1 R_1
𝕜 : Type u_4
R : Type u_5
inst_7 : NontriviallyNormedField 𝕜
inst_8 : SeminormedRing R
inst_9 : NormedAlgebra 𝕜 R
inst_10 : NormOneClass R
x : R
⊢ ‖x‖ = norm (E := R) ((((mul 𝕜 R : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R) : (a : R) → R) 1 : R) / norm.{u_5} (E := R) 1

Tactic:
simp [norm_one]

Premises used: NormOneClass.norm_one
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalSeminormedRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
inst_5 : RegularNormedAlgebra 𝕜 R
⊢ Isometry (α := R) (β := R →L[𝕜] R) (⇑(mul 𝕜 R) : (a : R) → R →L[𝕜] R)

Tactic:
RegularNormedAlgebra.isometry_mul'

Premises used: RegularNormedAlgebra.isometry_mul'
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalSeminormedRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
inst_5 : RegularNormedAlgebra 𝕜 R
x : R
⊢ norm (E := R →L[𝕜] R) ((mul 𝕜 R : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R) = ‖x‖

Tactic:
(AddMonoidHomClass.isometry_iff_norm (mul 𝕜 R)).mp (isometry_mul 𝕜 R) x

Premises used: ContinuousLinearMap.isometry_mul, ContinuousLinearMap.mul, AddMonoidHomClass.isometry_iff_norm, Iff.mp
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalSeminormedRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
inst_5 : RegularNormedAlgebra 𝕜 R
x : R
⊢ nnnorm (E := R →L[𝕜] R) ((mul 𝕜 R : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R) = ‖x‖₊

Tactic:
Subtype.ext <| opNorm_mul_apply 𝕜 R x

Premises used: ContinuousLinearMap.opNorm_mul_apply, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalSeminormedRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
inst_5 : RegularNormedAlgebra 𝕜 R
⊢ Eq (α := (a : R) → R →L[𝕜] R) (⇑(mulₗᵢ 𝕜 R) : (a : R) → R →L[𝕜] R) (⇑(mul 𝕜 R) : (a : R) → R →L[𝕜] R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalSeminormedCommRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
h :
  ∀ (x x_1 : R),
    Eq (α := R) ((((flip (mul 𝕜 R) : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R) : (a : R) → R) x_1 : R)
      ((((mul 𝕜 R : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R) : (a : R) → R) x_1 : R)
⊢ Eq.{u_3 + 1} (α := R →L[𝕜] R →L[𝕜] R) (flip (mul 𝕜 R)) (mul 𝕜 R)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Operator.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalSeminormedCommRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
x x_1 : R
⊢ Eq (α := R) ((((flip (mul 𝕜 R) : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R) : (a : R) → R) x_1 : R)
    ((((mul 𝕜 R : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R) : (a : R) → R) x_1 : R)

Tactic:
simp [mul_comm]

Premises used: mul_comm