awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomIsometric σ₂₃
inst_11 : RingHomIsometric σ₁₃
inst_12 : RingHomIsometric σ₁₂
X : Type u_11
inst_13 : TopologicalSpace X
g : X → F →SL[σ₂₃] G
hg : Continuous[inst_13, _] g
f : E →SL[σ₁₂] F
⊢ Continuous[inst_13, _] fun (x : X) ↦ g x ∘SL f

Tactic:
(@ContinuousLinearMap.flip _ _ _ _ _ (E →SL[σ₁₃] G) _ _ _ _ _ _ _ _ _ _ _ _ _
    (compSL E F G σ₁₂ σ₂₃) f).continuous.comp hg

Premises used: ContinuousLinearMap.comp, Continuous.comp, ContinuousLinearMap.compSL, ContinuousLinearMap.continuous, ContinuousLinearMap.flip, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
⊢ LE.le (α := ℕ) sorry 1

Tactic:
norm_compSL_le _ _ _ _ _

Premises used: ContinuousLinearMap.norm_compSL_le
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
Gₗ : Type u_9
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : SeminormedAddCommGroup Gₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace 𝕜 Gₗ
f : Fₗ →L[𝕜] Gₗ
g : E →L[𝕜] Fₗ
⊢ (((compL 𝕜 E Fₗ Gₗ : (a : Fₗ →L[𝕜] Gₗ) → (E →L[𝕜] Fₗ) →L[𝕜] E →L[𝕜] Gₗ) f : (E →L[𝕜] Fₗ) →L[𝕜] E →L[𝕜] Gₗ) :
        (a : E →L[𝕜] Fₗ) → E →L[𝕜] Gₗ)
      g =
    f ∘SL g

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
E : Type u_4
Eₗ : Type u_5
Fₗ : Type u_7
Gₗ : Type u_9
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Eₗ
inst_2 : SeminormedAddCommGroup Fₗ
inst_3 : SeminormedAddCommGroup Gₗ
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 Eₗ
inst_7 : NormedSpace 𝕜 Fₗ
inst_8 : NormedSpace 𝕜 Gₗ
L : E →L[𝕜] Fₗ →L[𝕜] Gₗ
u : Eₗ →L[𝕜] E
f : Fₗ
g : Eₗ
⊢ Eq.{u_9 + 1} (α := Gₗ)
    ((((((precompL Eₗ L : (a : Eₗ →L[𝕜] E) → Fₗ →L[𝕜] Eₗ →L[𝕜] Gₗ) u : Fₗ →L[𝕜] Eₗ →L[𝕜] Gₗ) : (a : Fₗ) → Eₗ →L[𝕜] Gₗ)
              f :
            Eₗ →L[𝕜] Gₗ) :
          (a : Eₗ) → Gₗ)
        g :
      Gₗ)
    ((((L : (a : E) → Fₗ →L[𝕜] Gₗ) ((u : (a : Eₗ) → E) g) : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) f : Gₗ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
Gₗ : Type u_9
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : SeminormedAddCommGroup Gₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace 𝕜 Gₗ
L : E →L[𝕜] Fₗ →L[𝕜] Gₗ
hbc : LE.le (α := ℝ) sorry 1
⊢ sorry * ‖L‖ ≤ 1 * ‖L‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
Gₗ : Type u_9
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : SeminormedAddCommGroup Gₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace 𝕜 Gₗ
L : E →L[𝕜] Fₗ →L[𝕜] Gₗ
rw rw₁ : ‖L‖ = ‖L‖
⊢ 1 * ‖L‖ = ‖L‖

Tactic:
rw [one_mul]

Premises used: one_mul
-- 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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst_9 : SeminormedAddCommGroup E'
inst_10 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_11 : NontriviallyNormedField 𝕜₁'
inst_12 : NontriviallyNormedField 𝕜₂'
inst_13 : NormedSpace 𝕜₁' E'
inst_14 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_16 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_17 : RingHomIsometric σ₂₃
inst_18 : RingHomIsometric σ₁₃'
inst_19 : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gE : E' →SL[σ₁'] E
gF : F' →SL[σ₂'] F
x : E'
y : F'
⊢ Eq.{u_8 + 1} (α := G) ((((f.bilinearComp gE gF : (a : E') → F' →SL[σ₂₃'] G) x : F' →SL[σ₂₃'] G) : (a : F') → G) y : G)
    ((((f : (a : E) → F →SL[σ₂₃] G) ((gE : (a : E') → E) x) : F →SL[σ₂₃] G) : (a : F) → G) ((gF : (a : F') → F) y : F) :
      G)

Tactic:
rfl

Premises used: rfl
-- 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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst_9 : SeminormedAddCommGroup E'
inst_10 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_11 : NontriviallyNormedField 𝕜₁'
inst_12 : NontriviallyNormedField 𝕜₂'
inst_13 : NormedSpace 𝕜₁' E'
inst_14 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_16 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_17 : RingHomIsometric σ₂₃
inst_18 : RingHomIsometric σ₁₃'
inst_19 : RingHomIsometric σ₂₃'
gE : E' →SL[σ₁'] E
gF : F' →SL[σ₂'] F
⊢ Eq (α := E' →SL[σ₁₃'] F' →SL[σ₂₃'] G) (bilinearComp (σ₂₃ := σ₂₃) (σ₁₃ := σ₁₃) 0 gE gF) 0

Tactic:
rfl

Premises used: LinearMap.mkContinuous₂, LinearMap.mkContinuousOfExistsBound, LinearMap.mkContinuousOfExistsBound₂, ContinuousLinearMap.flip, ContinuousLinearMap.bilinearComp, rfl
-- 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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst_9 : SeminormedAddCommGroup E'
inst_10 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_11 : NontriviallyNormedField 𝕜₁'
inst_12 : NontriviallyNormedField 𝕜₂'
inst_13 : NormedSpace 𝕜₁' E'
inst_14 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_16 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_17 : RingHomIsometric σ₂₃
inst_18 : RingHomIsometric σ₁₃'
inst_19 : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gF : F' →SL[σ₂'] F
h :
  ∀ (x : E') (x_1 : F'),
    Eq.{u_8 + 1} (α := G)
      ((((f.bilinearComp (σ₁' := σ₁') 0 gF : (a : E') → F' →SL[σ₂₃'] G) x : F' →SL[σ₂₃'] G) : (a : F') → G) x_1 : G)
      ((((0 : (a : E') → F' →SL[σ₂₃'] G) x : F' →SL[σ₂₃'] G) : (a : F') → G) x_1 : G)
⊢ Eq (α := E' →SL[σ₁₃'] F' →SL[σ₂₃'] G) (f.bilinearComp (σ₁' := σ₁') 0 gF) 0

Tactic:
ext
-- 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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst_9 : SeminormedAddCommGroup E'
inst_10 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_11 : NontriviallyNormedField 𝕜₁'
inst_12 : NontriviallyNormedField 𝕜₂'
inst_13 : NormedSpace 𝕜₁' E'
inst_14 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_16 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_17 : RingHomIsometric σ₂₃
inst_18 : RingHomIsometric σ₁₃'
inst_19 : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gF : F' →SL[σ₂'] F
x : E'
x_1 : F'
⊢ Eq.{u_8 + 1} (α := G)
    ((((f.bilinearComp (σ₁' := σ₁') 0 gF : (a : E') → F' →SL[σ₂₃'] G) x : F' →SL[σ₂₃'] G) : (a : F') → G) x_1 : G)
    ((((0 : (a : E') → F' →SL[σ₂₃'] G) x : F' →SL[σ₂₃'] G) : (a : F') → G) x_1 : 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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst_9 : SeminormedAddCommGroup E'
inst_10 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_11 : NontriviallyNormedField 𝕜₁'
inst_12 : NontriviallyNormedField 𝕜₂'
inst_13 : NormedSpace 𝕜₁' E'
inst_14 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_16 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_17 : RingHomIsometric σ₂₃
inst_18 : RingHomIsometric σ₁₃'
inst_19 : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gE : E' →SL[σ₁'] E
h :
  ∀ (x : E') (x_1 : F'),
    Eq.{u_8 + 1} (α := G)
      ((((f.bilinearComp (σ₂' := σ₂') gE 0 : (a : E') → F' →SL[σ₂₃'] G) x : F' →SL[σ₂₃'] G) : (a : F') → G) x_1 : G)
      ((((0 : (a : E') → F' →SL[σ₂₃'] G) x : F' →SL[σ₂₃'] G) : (a : F') → G) x_1 : G)
⊢ Eq (α := E' →SL[σ₁₃'] F' →SL[σ₂₃'] G) (f.bilinearComp (σ₂' := σ₂') gE 0) 0

Tactic:
ext
-- 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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst_9 : SeminormedAddCommGroup E'
inst_10 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_11 : NontriviallyNormedField 𝕜₁'
inst_12 : NontriviallyNormedField 𝕜₂'
inst_13 : NormedSpace 𝕜₁' E'
inst_14 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_16 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_17 : RingHomIsometric σ₂₃
inst_18 : RingHomIsometric σ₁₃'
inst_19 : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gE : E' →SL[σ₁'] E
x : E'
x_1 : F'
⊢ Eq.{u_8 + 1} (α := G)
    ((((f.bilinearComp (σ₂' := σ₂') gE 0 : (a : E') → F' →SL[σ₂₃'] G) x : F' →SL[σ₂₃'] G) : (a : F') → G) x_1 : G)
    ((((0 : (a : E') → F' →SL[σ₂₃'] G) x : F' →SL[σ₂₃'] G) : (a : F') → G) x_1 : G)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
Gₗ : Type u_9
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : SeminormedAddCommGroup Gₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace 𝕜 Gₗ
f : E →L[𝕜] Fₗ →L[𝕜] Gₗ
p : E × Fₗ
⊢ Eq (α := (a : E × Fₗ) → Gₗ) (⇑((f.deriv₂ : (a : E × Fₗ) → E × Fₗ →L[𝕜] Gₗ) p : E × Fₗ →L[𝕜] Gₗ) : (a : E × Fₗ) → Gₗ)
    fun (q : E × Fₗ) ↦
    HAdd.hAdd (α := Gₗ) (β := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) p.1 : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) q.2 : Gₗ)
      ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) q.1 : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) p.2 : Gₗ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
Gₗ : Type u_9
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : SeminormedAddCommGroup Gₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace 𝕜 Gₗ
f : E →L[𝕜] Fₗ →L[𝕜] Gₗ
x x' : E
y y' : Fₗ
simp :
  HAdd.hAdd (α := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y : Gₗ)
      (HAdd.hAdd (α := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x' : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y : Gₗ)
        (HAdd.hAdd (α := Gₗ) (β := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y' : Gₗ)
          ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x' : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y' : Gₗ))) =
    HAdd.hAdd (α := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y : Gₗ)
      (HAdd.hAdd (α := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y' : Gₗ)
        (HAdd.hAdd (α := Gₗ) (β := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x' : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y : Gₗ)
          ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x' : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y' : Gₗ)))
⊢ (((f : (a : E) → Fₗ →L[𝕜] Gₗ) (x + x') : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) (y + y') =
    HAdd.hAdd (β := Gₗ)
      (HAdd.hAdd (α := Gₗ) (β := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y : Gₗ)
        ((((f.deriv₂ : (a : E × Fₗ) → E × Fₗ →L[𝕜] Gₗ) (x, y) : E × Fₗ →L[𝕜] Gₗ) : (a : E × Fₗ) → Gₗ) (x', y') : Gₗ))
      ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x' : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y' : Gₗ)

Tactic:
simp only [map_add, add_apply, coe_deriv₂, add_assoc]

Premises used: add_assoc, map_add, ContinuousLinearMap.add_apply, ContinuousLinearMap.coe_deriv₂
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
Gₗ : Type u_9
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : SeminormedAddCommGroup Gₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace 𝕜 Gₗ
f : E →L[𝕜] Fₗ →L[𝕜] Gₗ
x x' : E
y y' : Fₗ
⊢ HAdd.hAdd (α := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y : Gₗ)
      (HAdd.hAdd (α := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x' : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y : Gₗ)
        (HAdd.hAdd (α := Gₗ) (β := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y' : Gₗ)
          ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x' : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y' : Gₗ))) =
    HAdd.hAdd (α := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y : Gₗ)
      (HAdd.hAdd (α := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y' : Gₗ)
        (HAdd.hAdd (α := Gₗ) (β := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x' : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y : Gₗ)
          ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x' : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y' : Gₗ)))

Tactic:
abel
-- 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ₗ
⊢ norm (E := E →L[𝕜] Fₗ) (smulRight c f) = ‖c‖ * ‖f‖

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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ₗ
refine_1 : norm (E := E →L[𝕜] Fₗ) (smulRight c f) ≤ ‖c‖ * ‖f‖
refine_2 : ‖c‖ * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f)
⊢ norm (E := E →L[𝕜] Fₗ) (smulRight c f) = ‖c‖ * ‖f‖

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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ₗ
⊢ 0 ≤ ‖c‖ * ‖f‖

Tactic:
positivity
-- 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ₗ
refine_1 : ∀ (x : E), norm.{u_7} (E := Fₗ) ((smulRight c f : (a : E) → Fₗ) x : Fₗ) ≤ ‖c‖ * ‖f‖ * ‖x‖
⊢ norm (E := E →L[𝕜] Fₗ) (smulRight c f) ≤ ‖c‖ * ‖f‖

Tactic:
refine opNorm_le_bound _ (by positivity) fun x => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound
-- 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ₗ
x : E
⊢ ‖HSMul.hSMul.{u_1, u_7, u_7} (α := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) f‖ =
    norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) * ‖f‖

Tactic:
norm_smul _ _

Premises used: norm_smul
-- 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ₗ
x : E
hbc : norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) ≤ ‖c‖ * ‖x‖
⊢ norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) * ‖f‖ ≤ ‖c‖ * ‖x‖ * ‖f‖

Tactic:
gcongr
-- 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ₗ
x : E
⊢ norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) ≤ ‖c‖ * ‖x‖

Tactic:
apply le_opNorm

Premises used: ContinuousLinearMap.le_opNorm
-- 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ₗ
x : E
⊢ ‖c‖ * ‖x‖ * ‖f‖ = ‖c‖ * ‖f‖ * ‖x‖

Tactic:
ring
-- 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ₗ
x : E
x₁ : norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) * ‖f‖ ≤ ‖c‖ * ‖x‖ * ‖f‖
x₂ : ‖c‖ * ‖x‖ * ‖f‖ = ‖c‖ * ‖f‖ * ‖x‖
⊢ norm.{u_7} (E := Fₗ) ((smulRight c f : (a : E) → Fₗ) x : Fₗ) ≤ ‖c‖ * ‖f‖ * ‖x‖

Tactic:
calc
      ‖c x • f‖ = ‖c x‖ * ‖f‖ := norm_smul _ _
      _ ≤ ‖c‖ * ‖x‖ * ‖f‖ := by gcongr; apply le_opNorm
      _ = ‖c‖ * ‖f‖ * ‖x‖ := by ring

Premises used: norm_smul, DFunLike.coe
-- 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ₗ
refine_2 : ∀ (hf : ‖f‖ = 0), ‖c‖ * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f)
refine_2₁ : ∀ (hf : 0 < ‖f‖), ‖c‖ * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f)
⊢ ‖c‖ * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f)

Tactic:
obtain hf | hf := (norm_nonneg f).eq_or_lt'

Premises used: LE.le.eq_or_lt', norm_nonneg
-- 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ₗ
hf : ‖f‖ = 0
⊢ ‖c‖ * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f)

Tactic:
simp [hf]
-- 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ₗ
hf : 0 < ‖f‖
refine_2 : ‖c‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f) / ‖f‖
⊢ ‖c‖ * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f)

Tactic:
rw [← le_div_iff₀ hf]

Premises used: le_div_iff₀
-- 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ₗ
hf : 0 < ‖f‖
⊢ 0 ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f) / ‖f‖

Tactic:
positivity
-- 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ₗ
hf : 0 < ‖f‖
refine_2 : ∀ (x : E), norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f) / ‖f‖ * ‖x‖
⊢ ‖c‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f) / ‖f‖

Tactic:
refine opNorm_le_bound _ (by positivity) fun x => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound
-- 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ₗ
hf : 0 < ‖f‖
x : E
refine_2 : norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f) * ‖x‖
⊢ norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f) / ‖f‖ * ‖x‖

Tactic:
rw [div_mul_eq_mul_div, le_div_iff₀ hf]

Premises used: div_mul_eq_mul_div, le_div_iff₀
-- 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ₗ
hf : 0 < ‖f‖
x : E
⊢ norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) * ‖f‖ =
    ‖HSMul.hSMul.{u_1, u_7, u_7} (α := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) f‖

Tactic:
(norm_smul _ _).symm

Premises used: norm_smul, Eq.symm
-- 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ₗ
hf : 0 < ‖f‖
x : E
⊢ ‖HSMul.hSMul.{u_1, u_7, u_7} (α := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) f‖ =
    norm.{u_7} (E := Fₗ) ((smulRight c f : (a : E) → Fₗ) x : Fₗ)

Tactic:
rfl

Premises used: rfl
-- 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ₗ
hf : 0 < ‖f‖
x : E
⊢ norm.{u_7} (E := Fₗ) ((smulRight c f : (a : E) → Fₗ) x : Fₗ) ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f) * ‖x‖

Tactic:
le_opNorm _ _

Premises used: ContinuousLinearMap.le_opNorm
-- 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ₗ
hf : 0 < ‖f‖
x : E
⊢ norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f) * ‖x‖

Tactic:
calc
        ‖c x‖ * ‖f‖ = ‖c x • f‖ := (norm_smul _ _).symm
        _ = ‖smulRight c f x‖ := rfl
        _ ≤ ‖smulRight c f‖ * ‖x‖ := le_opNorm _ _

Premises used: norm_smul, ContinuousLinearMap.smulRight, ContinuousLinearMap.le_opNorm, Eq.symm, DFunLike.coe, rfl