awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
⊢ nnnorm (E := E →L[𝕜] Fₗ) (smulRight c f) = ‖c‖₊ * ‖f‖₊

Tactic:
NNReal.eq <| c.norm_smulRight_apply f

Premises used: ContinuousLinearMap.norm_smulRight_apply, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
x : E
⊢ norm (E := 𝕜 →L[𝕜] E) (toSpanSingleton 𝕜 x) = ‖x‖

Tactic:
simp [← smulRight_id, norm_id]

Premises used: ContinuousLinearMap.norm_id, ContinuousLinearMap.smulRight_id
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
x : E
⊢ nnnorm (E := 𝕜 →L[𝕜] E) (toSpanSingleton 𝕜 x) = ‖x‖₊

Tactic:
NNReal.eq <| norm_toSpanSingleton _

Premises used: ContinuousLinearMap.norm_toSpanSingleton, NNReal.eq
-- 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 : RingHomInvPair σ₁₂ σ₂₁
inst_18 : RingHomInvPair σ₂₁ σ₁₂
E' : Type u_11
F' : Type u_12
inst_19 : SeminormedAddCommGroup E'
inst_20 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_21 : NontriviallyNormedField 𝕜₁'
inst_22 : NontriviallyNormedField 𝕜₂'
inst_23 : NormedSpace 𝕜₁' E'
inst_24 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_25 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_26 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_27 : RingHomIsometric σ₂₃
inst_28 : RingHomIsometric σ₁₃'
inst_29 : RingHomIsometric σ₂₃'
inst_30 : RingHomIsometric σ₁₃
inst_31 : RingHomIsometric σ₁'
inst_32 : RingHomIsometric σ₂'
c₁ c₂ : StrongDual 𝕜 E
h :
  ∀ (x : Fₗ) (x_1 : E),
    Eq.{u_7 + 1} (α := Fₗ) ((((smulRightₗ (c₁ + c₂) : (a : Fₗ) → E →L[𝕜] Fₗ) x : E →L[𝕜] Fₗ) : (a : E) → Fₗ) x_1 : Fₗ)
      ((((HAdd.hAdd (α := Fₗ →ₗ[𝕜] E →L[𝕜] Fₗ) (smulRightₗ c₁) (smulRightₗ c₂) : (a : Fₗ) → E →L[𝕜] Fₗ) x :
              E →L[𝕜] Fₗ) :
            (a : E) → Fₗ)
          x_1 :
        Fₗ)
⊢ smulRightₗ (c₁ + c₂) = HAdd.hAdd (α := Fₗ →ₗ[𝕜] E →L[𝕜] Fₗ) (smulRightₗ c₁) (smulRightₗ c₂)

Tactic:
ext x
-- 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 : RingHomInvPair σ₁₂ σ₂₁
inst_18 : RingHomInvPair σ₂₁ σ₁₂
E' : Type u_11
F' : Type u_12
inst_19 : SeminormedAddCommGroup E'
inst_20 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_21 : NontriviallyNormedField 𝕜₁'
inst_22 : NontriviallyNormedField 𝕜₂'
inst_23 : NormedSpace 𝕜₁' E'
inst_24 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_25 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_26 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_27 : RingHomIsometric σ₂₃
inst_28 : RingHomIsometric σ₁₃'
inst_29 : RingHomIsometric σ₂₃'
inst_30 : RingHomIsometric σ₁₃
inst_31 : RingHomIsometric σ₁'
inst_32 : RingHomIsometric σ₂'
c₁ c₂ : StrongDual 𝕜 E
x : Fₗ
x_1 : E
⊢ Eq.{u_7 + 1} (α := Fₗ) ((((smulRightₗ (c₁ + c₂) : (a : Fₗ) → E →L[𝕜] Fₗ) x : E →L[𝕜] Fₗ) : (a : E) → Fₗ) x_1 : Fₗ)
    ((((HAdd.hAdd (α := Fₗ →ₗ[𝕜] E →L[𝕜] Fₗ) (smulRightₗ c₁) (smulRightₗ c₂) : (a : Fₗ) → E →L[𝕜] Fₗ) x : E →L[𝕜] Fₗ) :
          (a : E) → Fₗ)
        x_1 :
      Fₗ)

Tactic:
simp only [add_smul, coe_smulRightₗ, add_apply, smulRight_apply, LinearMap.add_apply]

Premises used: LinearMap.add_apply, ContinuousLinearMap.coe_smulRightₗ, ContinuousLinearMap.add_apply, add_smul, ContinuousLinearMap.smulRight_apply
-- 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 : RingHomInvPair σ₁₂ σ₂₁
inst_18 : RingHomInvPair σ₂₁ σ₁₂
E' : Type u_11
F' : Type u_12
inst_19 : SeminormedAddCommGroup E'
inst_20 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_21 : NontriviallyNormedField 𝕜₁'
inst_22 : NontriviallyNormedField 𝕜₂'
inst_23 : NormedSpace 𝕜₁' E'
inst_24 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_25 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_26 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_27 : RingHomIsometric σ₂₃
inst_28 : RingHomIsometric σ₁₃'
inst_29 : RingHomIsometric σ₂₃'
inst_30 : RingHomIsometric σ₁₃
inst_31 : RingHomIsometric σ₁'
inst_32 : RingHomIsometric σ₂'
m : 𝕜
c : StrongDual 𝕜 E
h :
  ∀ (x : Fₗ) (x_1 : E),
    Eq.{u_7 + 1} (α := Fₗ) ((((smulRightₗ (m • c) : (a : Fₗ) → E →L[𝕜] Fₗ) x : E →L[𝕜] Fₗ) : (a : E) → Fₗ) x_1 : Fₗ)
      ((((HSMul.hSMul (α := 𝕜) (β := Fₗ →ₗ[𝕜] E →L[𝕜] Fₗ) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) m : 𝕜) (smulRightₗ c) :
                  (a : Fₗ) → E →L[𝕜] Fₗ)
                x :
              E →L[𝕜] Fₗ) :
            (a : E) → Fₗ)
          x_1 :
        Fₗ)
⊢ smulRightₗ (m • c) =
    HSMul.hSMul (α := 𝕜) (β := Fₗ →ₗ[𝕜] E →L[𝕜] Fₗ) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) m : 𝕜) (smulRightₗ c)

Tactic:
ext x
-- 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 : RingHomInvPair σ₁₂ σ₂₁
inst_18 : RingHomInvPair σ₂₁ σ₁₂
E' : Type u_11
F' : Type u_12
inst_19 : SeminormedAddCommGroup E'
inst_20 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_21 : NontriviallyNormedField 𝕜₁'
inst_22 : NontriviallyNormedField 𝕜₂'
inst_23 : NormedSpace 𝕜₁' E'
inst_24 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_25 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_26 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_27 : RingHomIsometric σ₂₃
inst_28 : RingHomIsometric σ₁₃'
inst_29 : RingHomIsometric σ₂₃'
inst_30 : RingHomIsometric σ₁₃
inst_31 : RingHomIsometric σ₁'
inst_32 : RingHomIsometric σ₂'
m : 𝕜
c : StrongDual 𝕜 E
x : Fₗ
x_1 : E
h :
  HMul.hMul (β := 𝕜) m ((c : (a : E) → 𝕜) x_1 : 𝕜) • x =
    m • HSMul.hSMul.{u_1, u_7, u_7} (α := 𝕜) ((c : (a : E) → 𝕜) x_1 : 𝕜) x
⊢ Eq.{u_7 + 1} (α := Fₗ) ((((smulRightₗ (m • c) : (a : Fₗ) → E →L[𝕜] Fₗ) x : E →L[𝕜] Fₗ) : (a : E) → Fₗ) x_1 : Fₗ)
    ((((HSMul.hSMul (α := 𝕜) (β := Fₗ →ₗ[𝕜] E →L[𝕜] Fₗ) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) m : 𝕜) (smulRightₗ c) :
                (a : Fₗ) → E →L[𝕜] Fₗ)
              x :
            E →L[𝕜] Fₗ) :
          (a : E) → Fₗ)
        x_1 :
      Fₗ)

Tactic:
dsimp
-- 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 : RingHomInvPair σ₁₂ σ₂₁
inst_18 : RingHomInvPair σ₂₁ σ₁₂
E' : Type u_11
F' : Type u_12
inst_19 : SeminormedAddCommGroup E'
inst_20 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_21 : NontriviallyNormedField 𝕜₁'
inst_22 : NontriviallyNormedField 𝕜₂'
inst_23 : NormedSpace 𝕜₁' E'
inst_24 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_25 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_26 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_27 : RingHomIsometric σ₂₃
inst_28 : RingHomIsometric σ₁₃'
inst_29 : RingHomIsometric σ₂₃'
inst_30 : RingHomIsometric σ₁₃
inst_31 : RingHomIsometric σ₁'
inst_32 : RingHomIsometric σ₂'
m : 𝕜
c : StrongDual 𝕜 E
x : Fₗ
x_1 : E
h h₁ : HMul.hMul (β := 𝕜) m ((c : (a : E) → 𝕜) x_1 : 𝕜) • x = HMul.hMul (β := 𝕜) m ((c : (a : E) → 𝕜) x_1 : 𝕜) • x
⊢ HMul.hMul (β := 𝕜) m ((c : (a : E) → 𝕜) x_1 : 𝕜) • x =
    m • HSMul.hSMul.{u_1, u_7, u_7} (α := 𝕜) ((c : (a : E) → 𝕜) x_1 : 𝕜) x

Tactic:
rw [smul_smul]

Premises used: smul_smul
-- 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 : RingHomInvPair σ₁₂ σ₂₁
inst_18 : RingHomInvPair σ₂₁ σ₁₂
E' : Type u_11
F' : Type u_12
inst_19 : SeminormedAddCommGroup E'
inst_20 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_21 : NontriviallyNormedField 𝕜₁'
inst_22 : NontriviallyNormedField 𝕜₂'
inst_23 : NormedSpace 𝕜₁' E'
inst_24 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_25 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_26 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_27 : RingHomIsometric σ₂₃
inst_28 : RingHomIsometric σ₁₃'
inst_29 : RingHomIsometric σ₂₃'
inst_30 : RingHomIsometric σ₁₃
inst_31 : RingHomIsometric σ₁'
inst_32 : RingHomIsometric σ₂'
c : StrongDual 𝕜 E
x : Fₗ
⊢ norm (E := E →L[𝕜] Fₗ)
      (((({ toFun := smulRightₗ, map_add' := ⋯, map_smul' := ⋯ : StrongDual 𝕜 E →ₗ[𝕜] Fₗ →ₗ[𝕜] E →L[𝕜] Fₗ } :
                  (a : StrongDual 𝕜 E) → Fₗ →ₗ[𝕜] E →L[𝕜] Fₗ)
                c :
              Fₗ →ₗ[𝕜] E →L[𝕜] Fₗ) :
            (a : Fₗ) → E →L[𝕜] Fₗ)
          x :
        E →L[𝕜] Fₗ) ≤
    1 * ‖c‖ * ‖x‖

Tactic:
simp only [coe_smulRightₗ, one_mul, norm_smulRight_apply, LinearMap.coe_mk, AddHom.coe_mk,
        le_refl]

Premises used: LinearMap.coe_mk, le_refl, ContinuousLinearMap.coe_smulRightₗ, ContinuousLinearMap.norm_smulRight_apply, AddHom.coe_mk, one_mul
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
E : Type u_4
F : Type u_6
G : Type u_8
𝕜' : Type u_11
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : SeminormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
inst_7 : SeminormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
inst_11 : SeminormedAddCommGroup G
inst_12 : NormedSpace 𝕜 G
inst_13 : NormedSpace 𝕜' G
inst_14 : IsScalarTower 𝕜 𝕜' G
B : E →L[𝕜'] F →L[𝕜'] G
⊢ Eq (α := E →L[𝕜] F →L[𝕜] G) (bilinearRestrictScalars 𝕜 B) (restrictScalarsL 𝕜' F G 𝕜 𝕜 ∘SL restrictScalars 𝕜 B)

Tactic:
rfl

Premises used: ContinuousLinearMap.bilinearRestrictScalars, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
E : Type u_4
F : Type u_6
G : Type u_8
𝕜' : Type u_11
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : SeminormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
inst_7 : SeminormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
inst_11 : SeminormedAddCommGroup G
inst_12 : NormedSpace 𝕜 G
inst_13 : NormedSpace 𝕜' G
inst_14 : IsScalarTower 𝕜 𝕜' G
B : E →L[𝕜'] F →L[𝕜'] G
⊢ Eq (α := E →L[𝕜] F →L[𝕜] G) (bilinearRestrictScalars 𝕜 B) (restrictScalars 𝕜 (restrictScalarsL 𝕜' F G 𝕜 𝕜' ∘SL B))

Tactic:
rfl

Premises used: LinearMap.restrictScalars, ContinuousLinearMap.restrictScalars, ContinuousLinearMap.bilinearRestrictScalars, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
E : Type u_4
F : Type u_6
G : Type u_8
𝕜' : Type u_11
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : SeminormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
inst_7 : SeminormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
inst_11 : SeminormedAddCommGroup G
inst_12 : NormedSpace 𝕜 G
inst_13 : NormedSpace 𝕜' G
inst_14 : IsScalarTower 𝕜 𝕜' G
B : E →L[𝕜'] F →L[𝕜'] G
x : E
y : F
⊢ Eq.{u_8 + 1} (α := G) ((((bilinearRestrictScalars 𝕜 B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
    ((((B : (a : E) → F →L[𝕜'] G) x : F →L[𝕜'] G) : (a : F) → G) y : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
E : Type u_4
F : Type u_6
G : Type u_8
𝕜' : Type u_11
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : SeminormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
inst_7 : SeminormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
inst_11 : SeminormedAddCommGroup G
inst_12 : NormedSpace 𝕜 G
inst_13 : NormedSpace 𝕜' G
inst_14 : IsScalarTower 𝕜 𝕜' G
B : E →L[𝕜'] F →L[𝕜'] G
⊢ norm (E := E →L[𝕜] F →L[𝕜] G) (bilinearRestrictScalars 𝕜 B) = ‖B‖

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.restrictScalars, setOf, ContinuousLinearMap.opNorm, ContinuousLinearMap.bilinearRestrictScalars, rfl
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
f : E → F
⊢ IsBoundedLinearMap 𝕜 f ↔ IsLinearMap 𝕜 f ∧ ∃ (M : ℝ), 0 < M ∧ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖

Tactic:
⟨fun hf ↦ ⟨hf.toIsLinearMap, hf.bound⟩, fun ⟨hl, hm⟩ ↦ ⟨hl, hm⟩⟩

Premises used: IsBoundedLinearMap.mk, IsBoundedLinearMap.bound, IsBoundedLinearMap, And.intro, Iff.intro, _private.0.isBoundedLinearMap_iff.match_1, IsBoundedLinearMap.toIsLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
f : E → F
hf : IsLinearMap 𝕜 f
M : ℝ
h : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
⊢ IsBoundedLinearMap 𝕜 f

Tactic:
⟨hf,
    by_cases
      (fun (this : M ≤ 0) =>
        ⟨1, zero_lt_one, fun x =>
          (h x).trans <| mul_le_mul_of_nonneg_right (this.trans zero_le_one) (norm_nonneg x)⟩)
      fun (this : ¬M ≤ 0) => ⟨M, lt_of_not_ge this, h⟩⟩

Premises used: lt_of_not_ge, by_cases, IsBoundedLinearMap.mk, zero_le_one, zero_lt_one, mul_le_mul_of_nonneg_right, And.intro, Exists.intro, LE.le.trans, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
⊢ ∀ (x : E), norm.{u_3} (E := F) ((0 : (a : E) → F) x : F) ≤ 0 * ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
⊢ ∀ (x : E), norm (E := E) ((LinearMap.id : (a : E) → E) x : E) ≤ 1 * ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
⊢ IsBoundedLinearMap 𝕜 (F := E) fun (x : E × F) ↦ x.1

Tactic:
(LinearMap.fst 𝕜 E F).isLinear.with_bound 1 fun x => ?_

Premises used: LinearMap.fst, IsLinearMap.with_bound, LinearMap.isLinear, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
refine : ∀ (x : E × F), norm.{u_2} (E := E) ((LinearMap.fst 𝕜 E F : (a : E × F) → E) x : E) ≤ 1 * ‖x‖
⊢ IsBoundedLinearMap 𝕜 (F := E) fun (x : E × F) ↦ x.1

Tactic:
refine (LinearMap.fst 𝕜 E F).isLinear.with_bound 1 fun x => ?_

Premises used: LinearMap.fst, IsLinearMap.with_bound, LinearMap.isLinear, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
x : E × F
rw : norm.{u_2} (E := E) ((LinearMap.fst 𝕜 E F : (a : E × F) → E) x : E) ≤ ‖x‖
⊢ norm.{u_2} (E := E) ((LinearMap.fst 𝕜 E F : (a : E × F) → E) x : E) ≤ 1 * ‖x‖

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
x : E × F
⊢ norm.{u_2} (E := E) ((LinearMap.fst 𝕜 E F : (a : E × F) → E) x : E) ≤ ‖x‖

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
x : E × F
⊢ norm.{u_2} (E := E) ((LinearMap.fst 𝕜 E F : (a : E × F) → E) x : E) ≤ ‖x‖

Tactic:
exact le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
⊢ IsBoundedLinearMap 𝕜 (F := F) fun (x : E × F) ↦ x.2

Tactic:
(LinearMap.snd 𝕜 E F).isLinear.with_bound 1 fun x => ?_

Premises used: LinearMap.snd, IsLinearMap.with_bound, LinearMap.isLinear, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
refine : ∀ (x : E × F), norm.{u_3} (E := F) ((LinearMap.snd 𝕜 E F : (a : E × F) → F) x : F) ≤ 1 * ‖x‖
⊢ IsBoundedLinearMap 𝕜 (F := F) fun (x : E × F) ↦ x.2

Tactic:
refine (LinearMap.snd 𝕜 E F).isLinear.with_bound 1 fun x => ?_

Premises used: LinearMap.snd, IsLinearMap.with_bound, LinearMap.isLinear, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
x : E × F
rw : norm.{u_3} (E := F) ((LinearMap.snd 𝕜 E F : (a : E × F) → F) x : F) ≤ ‖x‖
⊢ norm.{u_3} (E := F) ((LinearMap.snd 𝕜 E F : (a : E × F) → F) x : F) ≤ 1 * ‖x‖

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
x : E × F
⊢ norm.{u_3} (E := F) ((LinearMap.snd 𝕜 E F : (a : E × F) → F) x : F) ≤ ‖x‖

Tactic:
le_max_right _ _

Premises used: le_max_right
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
x : E × F
⊢ norm.{u_3} (E := F) ((LinearMap.snd 𝕜 E F : (a : E × F) → F) x : F) ≤ ‖x‖

Tactic:
exact le_max_right _ _

Premises used: le_max_right
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
f : E → F
𝕜' : Type u_5
c : 𝕜'
inst_5 : SeminormedRing 𝕜'
inst_6 : Module 𝕜' F
inst_7 : IsBoundedSMul 𝕜' F
inst_8 : SMulCommClass 𝕜 𝕜' F
hf : IsBoundedLinearMap 𝕜 f
hlf : IsLinearMap 𝕜 f
M : ℝ
left : 0 < M
hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
x : E
h₁ : 0 ≤ ‖c‖
grw grw₁ : ‖c‖ * (M * ‖x‖) ≤ ‖c‖ * (M * ‖x‖)
⊢ ‖c‖ * ‖f x‖ ≤ ‖c‖ * (M * ‖x‖)

Tactic:
grw [hM]
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
f : E → F
hf : IsBoundedLinearMap 𝕜 f
⊢ ∃ (M : ℝ), 0 < M ∧ ∀ (x : E), ‖-f x‖ ≤ M * ‖x‖

Tactic:
simpa using hf.2

Premises used: IsBoundedLinearMap.bound
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
hg : IsBoundedLinearMap 𝕜 g
hlf : IsLinearMap 𝕜 f
Mf : ℝ
left : 0 < Mf
hMf : ∀ (x : E), ‖f x‖ ≤ Mf * ‖x‖
hlg : IsLinearMap 𝕜 g
Mg : ℝ
left_1 : 0 < Mg
hMg : ∀ (x : E), ‖g x‖ ≤ Mg * ‖x‖
x : E
rw rw₁ : Mf * ‖x‖ + Mg * ‖x‖ ≤ Mf * ‖x‖ + Mg * ‖x‖
⊢ Mf * ‖x‖ + Mg * ‖x‖ ≤ (Mf + Mg) * ‖x‖

Tactic:
rw [add_mul]

Premises used: add_mul