awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜' 𝕜
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜' 𝕜 E
inst_9 : NormedSpace 𝕜' Fₗ
inst_10 : IsScalarTower 𝕜' 𝕜 Fₗ
f : E →L[𝕜] Fₗ
⊢ norm (E := E →L[𝕜'] Fₗ) (restrictScalars 𝕜' f) = ‖f‖

Tactic:
le_antisymm (opNorm_le_bound _ (norm_nonneg _) fun x => f.le_opNorm x)
    (opNorm_le_bound _ (norm_nonneg _) fun x => f.le_opNorm x)

Premises used: ContinuousLinearMap.le_opNorm, ContinuousLinearMap.opNorm_le_bound, le_antisymm, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜' 𝕜
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜' 𝕜 E
inst_9 : NormedSpace 𝕜' Fₗ
inst_10 : IsScalarTower 𝕜' 𝕜 Fₗ
𝕜'' : Type u_10
inst_11 : Ring 𝕜''
inst_12 : Module 𝕜'' Fₗ
inst_13 : ContinuousConstSMul 𝕜'' Fₗ
inst_14 : SMulCommClass 𝕜 𝕜'' Fₗ
inst_15 : SMulCommClass 𝕜' 𝕜'' Fₗ
⊢ Eq (α := (a : E →L[𝕜] Fₗ) → E →L[𝕜'] Fₗ) (⇑(restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'') : (a : E →L[𝕜] Fₗ) → E →L[𝕜'] Fₗ)
    (restrictScalars 𝕜')

Tactic:
rfl

Premises used: ContinuousLinearMap.restrictScalars, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜' 𝕜
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜' 𝕜 E
inst_9 : NormedSpace 𝕜' Fₗ
inst_10 : IsScalarTower 𝕜' 𝕜 Fₗ
𝕜'' : Type u_10
inst_11 : Ring 𝕜''
inst_12 : Module 𝕜'' Fₗ
inst_13 : ContinuousConstSMul 𝕜'' Fₗ
inst_14 : SMulCommClass 𝕜 𝕜'' Fₗ
inst_15 : SMulCommClass 𝕜' 𝕜'' Fₗ
⊢ Eq (α := (E →L[𝕜] Fₗ) →ₗ[𝕜''] E →L[𝕜'] Fₗ)
    (LinearIsometry.toLinearMap (E := E →L[𝕜] Fₗ) (E₂ := E →L[𝕜'] Fₗ) (restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜''))
    (restrictScalarsₗ 𝕜 E Fₗ 𝕜' 𝕜'')

Tactic:
rfl

Premises used: ContinuousLinearMap.restrictScalarsₗ, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
M : ι → Type u_10
inst_4 : (i : ι) → SeminormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_10} 𝕜 (M i)
C : ℝ
L : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_10} (RingHom.id 𝕜) E (M i)
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
⊢ ‖pi (φ := M) L‖ ≤ C

Tactic:
opNorm_le_bound _ hC (fun x ↦ ?_)

Premises used: ContinuousLinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
M : ι → Type u_10
inst_4 : (i : ι) → SeminormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_10} 𝕜 (M i)
C : ℝ
L : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_10} (RingHom.id 𝕜) E (M i)
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
refine : ∀ (x : E), norm (E := (i : ι) → M i) ((pi (φ := M) L : (a : E) → (i : ι) → M i) x : (i : ι) → M i) ≤ C * ‖x‖
⊢ ‖pi (φ := M) L‖ ≤ C

Tactic:
refine opNorm_le_bound _ hC (fun x ↦ ?_)

Premises used: ContinuousLinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
M : ι → Type u_10
inst_4 : (i : ι) → SeminormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_10} 𝕜 (M i)
C : ℝ
L : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_10} (RingHom.id 𝕜) E (M i)
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
x : E
⊢ 0 ≤ C * ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
M : ι → Type u_10
inst_4 : (i : ι) → SeminormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_10} 𝕜 (M i)
C : ℝ
L : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_10} (RingHom.id 𝕜) E (M i)
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
x : E
refine : ∀ (i : ι), norm.{u_10} (E := M i) ((pi (φ := M) L : (a : E) → (i : ι) → M i) x i : M i) ≤ C * ‖x‖
⊢ norm (E := (i : ι) → M i) ((pi (φ := M) L : (a : E) → (i : ι) → M i) x : (i : ι) → M i) ≤ C * ‖x‖

Tactic:
refine (pi_norm_le_iff_of_nonneg (by positivity)).mpr (fun i ↦ ?_)

Premises used: Iff.mpr, pi_norm_le_iff_of_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
M : ι → Type u_10
inst_4 : (i : ι) → SeminormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_10} 𝕜 (M i)
C : ℝ
L : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_10} (RingHom.id 𝕜) E (M i)
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
x : E
i : ι
⊢ norm.{u_10} (E := M i) ((pi (φ := M) L : (a : E) → (i : ι) → M i) x i : M i) ≤ C * ‖x‖

Tactic:
(L i).le_of_opNorm_le (hL i) _

Premises used: ContinuousLinearMap.le_of_opNorm_le
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
M : ι → Type u_10
inst_4 : (i : ι) → SeminormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_10} 𝕜 (M i)
C : ℝ
L : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_10} (RingHom.id 𝕜) E (M i)
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
x : E
i : ι
⊢ norm.{u_10} (E := M i) ((pi (φ := M) L : (a : E) → (i : ι) → M i) x i : M i) ≤ C * ‖x‖

Tactic:
exact (L i).le_of_opNorm_le (hL i) _

Premises used: ContinuousLinearMap.le_of_opNorm_le
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →ₛₗ[σ₁₂] F
C : ℝ
hC : 0 ≤ C
h : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ ‖f.mkContinuous C h‖ ≤ C

Tactic:
ContinuousLinearMap.opNorm_le_bound _ hC h

Premises used: ContinuousLinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →ₛₗ[σ₁₂] F
C : ℝ
h : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
x : E
hbc : C ≤ max C 0
⊢ C * ‖x‖ ≤ max C 0 * ‖x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →ₛₗ[σ₁₂] F
C : ℝ
h : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
x : E
⊢ C ≤ max C 0

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →ₛₗᵢ[σ₁₂] F
x : E
⊢ norm.{u_5} (E := F) ((f.toContinuousLinearMap : (a : E) → F) x : F) ≤ 1 * ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
K : Submodule 𝕜 E
⊢ norm (E := ↥K →L[𝕜] E) K.subtypeL ≤ 1

Tactic:
K.subtypeₗᵢ.norm_toContinuousLinearMap_le

Premises used: Submodule.subtypeL, Set.Mem, Submodule.subtype, LinearIsometry.norm_toContinuousLinearMap_le, Submodule.subtypeₗᵢ, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₁₃
f : E →SL[σ₁₂] F
g : E →SL[σ₁₃] G
h : ∀ (x : E), Norm.norm.{u_6} (E := F) ((f : (a : E) → F) x : F) = Norm.norm.{u_8} (E := G) ((g : (a : E) → G) x : G)
x : E
rw : Norm.norm.{u_8} (E := G) ((g : (a : E) → G) x : G) ≤ ‖g‖ * ‖x‖
⊢ Norm.norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ ‖g‖ * ‖x‖

Tactic:
rw [h x]
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₁₃
f : E →SL[σ₁₂] F
g : E →SL[σ₁₃] G
h : ∀ (x : E), Norm.norm.{u_6} (E := F) ((f : (a : E) → F) x : F) = Norm.norm.{u_8} (E := G) ((g : (a : E) → G) x : G)
x : E
⊢ Norm.norm.{u_8} (E := G) ((g : (a : E) → G) x : G) ≤ ‖g‖ * ‖x‖

Tactic:
le_opNorm _ _

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₁₃
f : E →SL[σ₁₂] F
g : E →SL[σ₁₃] G
h : ∀ (x : E), Norm.norm.{u_6} (E := F) ((f : (a : E) → F) x : F) = Norm.norm.{u_8} (E := G) ((g : (a : E) → G) x : G)
x : E
⊢ Norm.norm.{u_8} (E := G) ((g : (a : E) → G) x : G) ≤ ‖g‖ * ‖x‖

Tactic:
exact le_opNorm _ _

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₁₃
f : E →SL[σ₁₂] F
g : E →SL[σ₁₃] G
h : ∀ (x : E), Norm.norm.{u_6} (E := F) ((f : (a : E) → F) x : F) = Norm.norm.{u_8} (E := G) ((g : (a : E) → G) x : G)
c : ℝ
hc : c ≥ 0
h₂ : ∀ (x : E), Norm.norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖
z : E
rw : Norm.norm.{u_6} (E := F) ((f : (a : E) → F) z : F) ≤ c * ‖z‖
⊢ Norm.norm.{u_8} (E := G) ((g : (a : E) → G) z : G) ≤ c * ‖z‖

Tactic:
rw [← h z]
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₁₃
f : E →SL[σ₁₂] F
g : E →SL[σ₁₃] G
h : ∀ (x : E), Norm.norm.{u_6} (E := F) ((f : (a : E) → F) x : F) = Norm.norm.{u_8} (E := G) ((g : (a : E) → G) x : G)
c : ℝ
hc : c ≥ 0
h₂ : ∀ (x : E), Norm.norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖
z : E
⊢ Norm.norm.{u_6} (E := F) ((f : (a : E) → F) z : F) ≤ c * ‖z‖

Tactic:
h₂ z
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₁₃
f : E →SL[σ₁₂] F
g : E →SL[σ₁₃] G
h : ∀ (x : E), Norm.norm.{u_6} (E := F) ((f : (a : E) → F) x : F) = Norm.norm.{u_8} (E := G) ((g : (a : E) → G) x : G)
c : ℝ
hc : c ≥ 0
h₂ : ∀ (x : E), Norm.norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖
z : E
⊢ Norm.norm.{u_6} (E := F) ((f : (a : E) → F) z : F) ≤ c * ‖z‖

Tactic:
exact h₂ z
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₂₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
C : ℝ
h0 : 0 ≤ C
hC :
  ∀ (x : E) (y : F),
    Norm.norm.{u_8} (E := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G) ≤ C * ‖x‖ * ‖y‖
x : E
⊢ 0 ≤ C * ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₂₃
inst_10 : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
⊢ Norm.norm.{u_8} (E := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G) ≤ ‖f‖ * ‖x‖ * ‖y‖

Tactic:
(f x).le_of_opNorm_le (f.le_opNorm x) y

Premises used: ContinuousLinearMap.le_opNorm, ContinuousLinearMap.le_of_opNorm_le, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₂₃
inst_10 : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
a b c : ℝ
hf : ‖f‖ ≤ a
hx : ‖x‖ ≤ b
hy : ‖y‖ ≤ c
⊢ Norm.norm.{u_8} (E := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G) ≤ a * b * c

Tactic:
(f x).le_of_opNorm_le_of_le (f.le_of_opNorm_le_of_le hf hx) hy

Premises used: ContinuousLinearMap.le_of_opNorm_le_of_le, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
C : ℝ
h :
  ∀ (x : E) (y : F),
    norm.{u_8} (E := G) ((((f : (a : E) → F →ₛₗ[σ₂₃] G) x : F →ₛₗ[σ₂₃] G) : (a : F) → G) y : G) ≤ C * ‖x‖ * ‖y‖
x : E
rw : max (C * ‖x‖) 0 = max (C * ‖x‖) (0 * ‖x‖)
rw₁ rw₂ : max (C * ‖x‖) 0 = max (C * ‖x‖) 0
⊢ max (C * ‖x‖) 0 = max C 0 * ‖x‖

Tactic:
rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]

Premises used: max_mul_of_nonneg, MulZeroClass.zero_mul, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Eₗ
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup Fₗ
inst_4 : SeminormedAddCommGroup G
inst_5 : SeminormedAddCommGroup Gₗ
inst_6 : NontriviallyNormedField 𝕜
inst_7 : NontriviallyNormedField 𝕜₂
inst_8 : NontriviallyNormedField 𝕜₃
inst_9 : NormedSpace 𝕜 E
inst_10 : NormedSpace 𝕜 Eₗ
inst_11 : NormedSpace 𝕜₂ F
inst_12 : NormedSpace 𝕜 Fₗ
inst_13 : NormedSpace 𝕜₃ G
inst_14 : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_16 : FunLike 𝓕 E F
inst_17 : RingHomIsometric σ₂₃
f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
h :
  ∃ (C : ℝ),
    ∀ (x : E) (y : F),
      norm.{u_8} (E := G) ((((f : (a : E) → F →ₛₗ[σ₂₃] G) x : F →ₛₗ[σ₂₃] G) : (a : F) → G) y : G) ≤ C * ‖x‖ * ‖y‖
x y : E
h₁ :
  ∀ (z : F),
    Eq.{u_8 + 1} (α := G) ((mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) (x + y)) ⋯ : (a : F) → G) z : G)
      ((HAdd.hAdd (α := F →SL[σ₂₃] G) (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) x) ⋯)
              (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) y) ⋯) :
            (a : F) → G)
          z :
        G)
⊢ mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) (x + y)) ⋯ =
    HAdd.hAdd (α := F →SL[σ₂₃] G) (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) x) ⋯)
      (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) y) ⋯)

Tactic:
ext z
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Eₗ
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup Fₗ
inst_4 : SeminormedAddCommGroup G
inst_5 : SeminormedAddCommGroup Gₗ
inst_6 : NontriviallyNormedField 𝕜
inst_7 : NontriviallyNormedField 𝕜₂
inst_8 : NontriviallyNormedField 𝕜₃
inst_9 : NormedSpace 𝕜 E
inst_10 : NormedSpace 𝕜 Eₗ
inst_11 : NormedSpace 𝕜₂ F
inst_12 : NormedSpace 𝕜 Fₗ
inst_13 : NormedSpace 𝕜₃ G
inst_14 : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_16 : FunLike 𝓕 E F
inst_17 : RingHomIsometric σ₂₃
f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
h :
  ∃ (C : ℝ),
    ∀ (x : E) (y : F),
      norm.{u_8} (E := G) ((((f : (a : E) → F →ₛₗ[σ₂₃] G) x : F →ₛₗ[σ₂₃] G) : (a : F) → G) y : G) ≤ C * ‖x‖ * ‖y‖
x y : E
z : F
⊢ Eq.{u_8 + 1} (α := G) ((mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) (x + y)) ⋯ : (a : F) → G) z : G)
    ((HAdd.hAdd (α := F →SL[σ₂₃] G) (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) x) ⋯)
            (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) y) ⋯) :
          (a : F) → G)
        z :
      G)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Eₗ
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup Fₗ
inst_4 : SeminormedAddCommGroup G
inst_5 : SeminormedAddCommGroup Gₗ
inst_6 : NontriviallyNormedField 𝕜
inst_7 : NontriviallyNormedField 𝕜₂
inst_8 : NontriviallyNormedField 𝕜₃
inst_9 : NormedSpace 𝕜 E
inst_10 : NormedSpace 𝕜 Eₗ
inst_11 : NormedSpace 𝕜₂ F
inst_12 : NormedSpace 𝕜 Fₗ
inst_13 : NormedSpace 𝕜₃ G
inst_14 : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_16 : FunLike 𝓕 E F
inst_17 : RingHomIsometric σ₂₃
f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
h :
  ∃ (C : ℝ),
    ∀ (x : E) (y : F),
      norm.{u_8} (E := G) ((((f : (a : E) → F →ₛₗ[σ₂₃] G) x : F →ₛₗ[σ₂₃] G) : (a : F) → G) y : G) ≤ C * ‖x‖ * ‖y‖
c : 𝕜
x : E
h₁ :
  ∀ (z : F),
    Eq.{u_8 + 1} (α := G) ((mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) (c • x)) ⋯ : (a : F) → G) z : G)
      ((HSMul.hSMul (α := 𝕜₃) (β := F →SL[σ₂₃] G) ((σ₁₃ : (a : 𝕜) → 𝕜₃) c : 𝕜₃)
              (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) x) ⋯) :
            (a : F) → G)
          z :
        G)
⊢ mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) (c • x)) ⋯ =
    HSMul.hSMul (α := 𝕜₃) (β := F →SL[σ₂₃] G) ((σ₁₃ : (a : 𝕜) → 𝕜₃) c : 𝕜₃)
      (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) x) ⋯)

Tactic:
ext z
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Eₗ
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup Fₗ
inst_4 : SeminormedAddCommGroup G
inst_5 : SeminormedAddCommGroup Gₗ
inst_6 : NontriviallyNormedField 𝕜
inst_7 : NontriviallyNormedField 𝕜₂
inst_8 : NontriviallyNormedField 𝕜₃
inst_9 : NormedSpace 𝕜 E
inst_10 : NormedSpace 𝕜 Eₗ
inst_11 : NormedSpace 𝕜₂ F
inst_12 : NormedSpace 𝕜 Fₗ
inst_13 : NormedSpace 𝕜₃ G
inst_14 : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_16 : FunLike 𝓕 E F
inst_17 : RingHomIsometric σ₂₃
f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
h :
  ∃ (C : ℝ),
    ∀ (x : E) (y : F),
      norm.{u_8} (E := G) ((((f : (a : E) → F →ₛₗ[σ₂₃] G) x : F →ₛₗ[σ₂₃] G) : (a : F) → G) y : G) ≤ C * ‖x‖ * ‖y‖
c : 𝕜
x : E
z : F
⊢ Eq.{u_8 + 1} (α := G) ((mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) (c • x)) ⋯ : (a : F) → G) z : G)
    ((HSMul.hSMul (α := 𝕜₃) (β := F →SL[σ₂₃] G) ((σ₁₃ : (a : 𝕜) → 𝕜₃) c : 𝕜₃)
            (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) x) ⋯) :
          (a : F) → G)
        z :
      G)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₂₃
f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
C : ℝ
hC :
  ∀ (x : E) (y : F),
    norm.{u_8} (E := G) ((((f : (a : E) → F →ₛₗ[σ₂₃] G) x : F →ₛₗ[σ₂₃] G) : (a : F) → G) y : G) ≤ C * ‖x‖ * ‖y‖
x : E
y : F
⊢ Eq.{u_8 + 1} (α := G) ((((f.mkContinuous₂ C hC : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
    ((((f : (a : E) → F →ₛₗ[σ₂₃] G) x : F →ₛₗ[σ₂₃] G) : (a : F) → G) y : G)

Tactic:
rfl

Premises used: rfl