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 : 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‖
⊢ ‖f.mkContinuous₂ C hC‖ ≤ max C 0

Tactic:
mkContinuous_norm_le _ (le_max_iff.2 <| Or.inr le_rfl) (norm_mkContinuous₂_aux f C hC)

Premises used: Iff.mpr, le_rfl, LinearMap.mkContinuous₂, LinearMap.mkContinuousOfExistsBound, LinearMap.mkContinuousOfExistsBound₂, LinearMap.mkContinuous_norm_le, le_max_iff, Or.inr
-- 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 : ℝ
h0 : 0 ≤ 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‖
⊢ ‖f.mkContinuous₂ C hC‖ ≤ C

Tactic:
(f.mkContinuous₂_norm_le' hC).trans_eq <| max_eq_left h0

Premises used: LinearMap.mkContinuous₂_norm_le', LE.le.trans_eq, max_eq_left
-- 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 σ₂₃
inst_18 : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
z : F
x y : E
⊢ (fun (y : F) (x : E) ↦ ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)) z (x + y) =
    HAdd.hAdd (α := G)
      ((fun (y : F) (x : E) ↦ ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)) z x)
      ((fun (y : F) (x : E) ↦ ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)) z y)

Tactic:
simp only [f.map_add, add_apply]

Premises used: ContinuousLinearMap.add_apply, ContinuousLinearMap.map_add
-- 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 σ₂₃
inst_18 : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
c : 𝕜
y : F
x : E
⊢ (fun (y : F) (x : E) ↦ ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)) y (c • x) =
    HSMul.hSMul.{u_3, u_8, u_8} (α := 𝕜₃) (β := G) ((σ₁₃ : (a : 𝕜) → 𝕜₃) c : 𝕜₃)
      ((fun (y : F) (x : E) ↦ ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)) y x)

Tactic:
simp only [f.map_smulₛₗ, smul_apply]

Premises used: ContinuousLinearMap.smul_apply, ContinuousLinearMap.map_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 : RingHomIsometric σ₂₃
inst_18 : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
y : F
x : E
⊢ ‖f‖ * ‖x‖ * ‖y‖ = ‖f‖ * ‖y‖ * ‖x‖

Tactic:
simp only [mul_right_comm]

Premises used: mul_right_comm
-- 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
rw : norm.{u_8} (E := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G) ≤ ‖f.flip‖ * ‖y‖ * ‖x‖
⊢ norm.{u_8} (E := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G) ≤ ‖f.flip‖ * ‖x‖ * ‖y‖

Tactic:
rw [mul_right_comm]

Premises used: mul_right_comm
-- 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.{u_8} (E := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G) ≤ ‖f.flip‖ * ‖y‖ * ‖x‖

Tactic:
(flip f).le_opNorm₂ y x

Premises used: ContinuousLinearMap.le_opNorm₂, ContinuousLinearMap.flip
-- 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.{u_8} (E := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G) ≤ ‖f.flip‖ * ‖y‖ * ‖x‖

Tactic:
exact (flip f).le_opNorm₂ y x

Premises used: ContinuousLinearMap.le_opNorm₂, ContinuousLinearMap.flip
-- 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
⊢ Eq.{u_8 + 1} (α := G) ((((f.flip : (a : F) → E →SL[σ₁₃] G) y : E →SL[σ₁₃] G) : (a : E) → G) x : G)
    ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : 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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₂₃
inst_10 : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
h :
  ∀ (x : E) (x_1 : F),
    Eq.{u_8 + 1} (α := G) ((((f.flip.flip : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) x_1 : G)
      ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) x_1 : G)
⊢ f.flip.flip = f

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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₂₃
inst_10 : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
x_1 : F
⊢ Eq.{u_8 + 1} (α := G) ((((f.flip.flip : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) x_1 : G)
    ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) x_1 : G)

Tactic:
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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₂₃
inst_10 : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
⊢ ‖f.flip‖ ≤ ‖f‖

Tactic:
simpa only [flip_flip] using le_norm_flip f.flip

Premises used: _private.0.ContinuousLinearMap.le_norm_flip, ContinuousLinearMap.flip, ContinuousLinearMap.flip_flip
-- 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 σ₁₃
⊢ Eq (α := F →SL[σ₂₃] E →SL[σ₁₃] G) (flip 0) 0

Tactic:
rfl

Premises used: LinearMap.mkContinuous₂, LinearMap.mkContinuousOfExistsBound, LinearMap.mkContinuousOfExistsBound₂, ContinuousLinearMap.flip, 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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₂₃
inst_10 : RingHomIsometric σ₁₃
f g : E →SL[σ₁₃] F →SL[σ₂₃] G
⊢ (f + g).flip = f.flip + g.flip

Tactic:
rfl

Premises used: LinearMap.mkContinuous₂, LinearMap.mkContinuousOfExistsBound, LinearMap.mkContinuousOfExistsBound₂, ContinuousLinearMap.flip, 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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₂₃
inst_10 : RingHomIsometric σ₁₃
c : 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
⊢ (c • f).flip = c • f.flip

Tactic:
rfl

Premises used: LinearMap.mkContinuous₂, LinearMap.mkContinuousOfExistsBound, LinearMap.mkContinuousOfExistsBound₂, ContinuousLinearMap.flip, 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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₂₃
inst_10 : RingHomIsometric σ₁₃
⊢ Eq (α := (F →SL[σ₂₃] E →SL[σ₁₃] G) ≃ₗᵢ[𝕜₃] E →SL[σ₁₃] F →SL[σ₂₃] G) (LinearIsometryEquiv.symm (flipₗᵢ' E F G σ₂₃ σ₁₃))
    (flipₗᵢ' F E G σ₁₃ σ₂₃)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, LinearMap.mkContinuous₂, LinearMap.mkContinuousOfExistsBound, LinearMap.mkContinuousOfExistsBound₂, ContinuousLinearMap.flip, ContinuousLinearMap.flipₗᵢ', 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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₂₃
inst_10 : RingHomIsometric σ₁₃
⊢ Eq (α := (a : E →SL[σ₁₃] F →SL[σ₂₃] G) → F →SL[σ₂₃] E →SL[σ₁₃] G)
    (⇑(flipₗᵢ' E F G σ₂₃ σ₁₃) : (a : E →SL[σ₁₃] F →SL[σ₂₃] G) → F →SL[σ₂₃] E →SL[σ₁₃] G) flip

Tactic:
rfl

Premises used: LinearMap.mkContinuous₂, LinearMap.mkContinuousOfExistsBound, LinearMap.mkContinuousOfExistsBound₂, ContinuousLinearMap.flip, 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ₗ
⊢ Eq (α := (Fₗ →L[𝕜] E →L[𝕜] Gₗ) ≃ₗᵢ[𝕜] E →L[𝕜] Fₗ →L[𝕜] Gₗ) (LinearIsometryEquiv.symm (flipₗᵢ 𝕜 E Fₗ Gₗ))
    (flipₗᵢ 𝕜 Fₗ E Gₗ)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, ContinuousLinearMap.flipₗᵢ, LinearMap.mkContinuous₂, LinearMap.mkContinuousOfExistsBound, LinearMap.mkContinuousOfExistsBound₂, ContinuousLinearMap.flip, 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ₗ
⊢ Eq (α := (a : E →L[𝕜] Fₗ →L[𝕜] Gₗ) → Fₗ →L[𝕜] E →L[𝕜] Gₗ)
    (⇑(flipₗᵢ 𝕜 E Fₗ Gₗ) : (a : E →L[𝕜] Fₗ →L[𝕜] Gₗ) → Fₗ →L[𝕜] E →L[𝕜] Gₗ) flip

Tactic:
rfl

Premises used: LinearMap.mkContinuous₂, LinearMap.mkContinuousOfExistsBound, LinearMap.mkContinuousOfExistsBound₂, ContinuousLinearMap.flip, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Bilinear
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
v : E
f : E →SL[σ₁₂] F
⊢ Eq.{u_6 + 1} (α := F)
    ((((apply' F σ₁₂ : (a : E) → (E →SL[σ₁₂] F) →L[𝕜₂] F) v : (E →SL[σ₁₂] F) →L[𝕜₂] F) : (a : E →SL[σ₁₂] F) → F) f : F)
    ((f : (a : E) → F) v : 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ₗ
v : E
f : E →L[𝕜] Fₗ
⊢ Eq.{u_7 + 1} (α := Fₗ)
    ((((apply 𝕜 Fₗ : (a : E) → (E →L[𝕜] Fₗ) →L[𝕜] Fₗ) v : (E →L[𝕜] Fₗ) →L[𝕜] Fₗ) : (a : E →L[𝕜] Fₗ) → Fₗ) f : Fₗ)
    ((f : (a : E) → Fₗ) v : Fₗ)

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
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 σ₂₃
inst_18 : RingHomIsometric σ₁₃
inst_19 : RingHomIsometric σ₁₂
c : 𝕜₂
f : F →SL[σ₂₃] G
g : E →SL[σ₁₂] F
h :
  ∀ (x : E),
    Eq.{u_8 + 1} (α := G) ((f ∘SL (c • g) : (a : E) → G) x : G)
      ((HSMul.hSMul (α := 𝕜₃) ((σ₂₃ : (a : 𝕜₂) → 𝕜₃) c : 𝕜₃) (f ∘SL g) : (a : E) → G) x : G)
⊢ f ∘SL (c • g) = HSMul.hSMul (α := 𝕜₃) ((σ₂₃ : (a : 𝕜₂) → 𝕜₃) c : 𝕜₃) (f ∘SL g)

Tactic:
ext
-- 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 σ₂₃
inst_18 : RingHomIsometric σ₁₃
inst_19 : RingHomIsometric σ₁₂
c : 𝕜₂
f : F →SL[σ₂₃] G
g : E →SL[σ₁₂] F
x : E
⊢ Eq.{u_8 + 1} (α := G) ((f ∘SL (c • g) : (a : E) → G) x : G)
    ((HSMul.hSMul (α := 𝕜₃) ((σ₂₃ : (a : 𝕜₂) → 𝕜₃) c : 𝕜₃) (f ∘SL g) : (a : E) → G) x : G)

Tactic:
simp only [map_smulₛₗ, coe_smul', coe_comp', Function.comp_apply, Pi.smul_apply]

Premises used: ContinuousLinearMap.coe_comp', ContinuousLinearMap.coe_smul', MulActionSemiHomClass.map_smulₛₗ, Function.comp_apply, Pi.smul_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 : RingHomIsometric σ₂₃
inst_18 : RingHomIsometric σ₁₃
inst_19 : RingHomIsometric σ₁₂
f : F →SL[σ₂₃] G
g : E →SL[σ₁₂] F
⊢ norm (E := E →SL[σ₁₃] G)
      ((((LinearMap.mk₂'ₛₗ (RingHom.id 𝕜₃) σ₂₃ comp ⋯ ⋯ ⋯ ⋯ : (a : F →SL[σ₂₃] G) → (E →SL[σ₁₂] F) →ₛₗ[σ₂₃] E →SL[σ₁₃] G)
                f :
              (E →SL[σ₁₂] F) →ₛₗ[σ₂₃] E →SL[σ₁₃] G) :
            (a : E →SL[σ₁₂] F) → E →SL[σ₁₃] G)
          g :
        E →SL[σ₁₃] G) ≤
    1 * ‖f‖ * ‖g‖

Tactic:
simpa only [one_mul] using opNorm_comp_le f g

Premises used: ContinuousLinearMap.opNorm_comp_le, 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
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomIsometric σ₂₃
inst_11 : RingHomIsometric σ₁₃
inst_12 : RingHomIsometric σ₁₂
⊢ norm (E := (F →SL[σ₂₃] G) →L[𝕜₃] (E →SL[σ₁₂] F) →SL[σ₂₃] E →SL[σ₁₃] G) (compSL E F G σ₁₂ σ₂₃) ≤ 1

Tactic:
LinearMap.mkContinuous₂_norm_le _ zero_le_one _

Premises used: ContinuousLinearMap.compSL, zero_le_one, LinearMap.mkContinuous₂_norm_le
-- 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 σ₁₂
f : F →SL[σ₂₃] G
g : E →SL[σ₁₂] F
⊢ (((compSL E F G σ₁₂ σ₂₃ : (a : F →SL[σ₂₃] G) → (E →SL[σ₁₂] F) →SL[σ₂₃] E →SL[σ₁₃] G) f :
          (E →SL[σ₁₂] F) →SL[σ₂₃] E →SL[σ₁₃] G) :
        (a : E →SL[σ₁₂] F) → E →SL[σ₁₃] G)
      g =
    f ∘SL g

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, 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
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomIsometric σ₂₃
inst_11 : RingHomIsometric σ₁₃
inst_12 : RingHomIsometric σ₁₂
X : Type u_11
inst_13 : TopologicalSpace X
f : X → E →SL[σ₁₂] F
hf : Continuous[inst_13, _] f
g : F →SL[σ₂₃] G
⊢ Continuous[inst_13, _] fun (x : X) ↦ g ∘SL f x

Tactic:
(compSL E F G σ₁₂ σ₂₃ g).continuous.comp hf

Premises used: ContinuousLinearMap.comp, Continuous.comp, ContinuousLinearMap.compSL, ContinuousLinearMap.continuous, DFunLike.coe