awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
hg : IsLittleO (E := ℝ) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ ‖x_1.2 - x.2‖) fun (_x : E × F) ↦ 1
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ ‖x.1‖ * ‖x_1.2 - x.2‖) fun (_x : E × F) ↦ 1

Tactic:
apply IsLittleO.const_mul_left

Premises used: Asymptotics.IsLittleO.const_mul_left
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
hg : Tendsto (fun (x_1 : E × F) ↦ x_1.2 - x.2) (𝓝 x) (𝓝 (x.2 - x.2))
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ ‖x_1.2 - x.2‖) fun (_x : E × F) ↦ 1

Tactic:
rw [isLittleO_norm_left, isLittleO_one_iff, ← sub_self x.2]

Premises used: sub_self, Asymptotics.isLittleO_norm_left, Asymptotics.isLittleO_one_iff, Prod.snd
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Tendsto (fun (x_1 : E × F) ↦ x_1.2 - x.2) (𝓝 x) (𝓝 (x.2 - x.2))

Tactic:
continuous_snd.continuousAt.sub tendsto_const_nhds

Premises used: ContinuousAt, tendsto_const_nhds, ContinuousAt.sub, continuous_snd, Continuous.continuousAt
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Tendsto (fun (x_1 : E × F) ↦ x_1.2 - x.2) (𝓝 x) (𝓝 (x.2 - x.2))

Tactic:
exact continuous_snd.continuousAt.sub tendsto_const_nhds

Premises used: tendsto_const_nhds, ContinuousAt.sub, continuous_snd, Continuous.continuousAt
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
e₂ : F
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, instTopologicalSpaceProd] fun (e₁ : E) ↦ (e₁, e₂)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
e₁ : E
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, instTopologicalSpaceProd] (Prod.mk e₁)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : SeminormedRing A
inst_2 : Algebra 𝕜 A
E : Type u_3
inst_3 : SeminormedAddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : Module A E
inst_6 : IsBoundedSMul A E
inst_7 : IsScalarTower 𝕜 A E
x : A
y : E
grw : ‖(x, y).1 • (x, y).2‖ ≤ ‖x‖ * ‖y‖
grw₁ grw₂ : ‖(x, y).1‖ * ‖(x, y).2‖ ≤ ‖(x, y).1‖ * ‖(x, y).2‖
⊢ ‖(x, y).1 • (x, y).2‖ ≤ 1 * ‖x‖ * ‖y‖

Tactic:
grw [one_mul, norm_smul_le]

Premises used: norm_smul_le, one_mul
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : SeminormedRing A
inst_2 : Algebra 𝕜 A
⊢ IsBoundedBilinearMap.{u_1, u_2, u_2, u_2} 𝕜 (E := A) (F := A) (G := A) fun (p : A × A) ↦ p.1 * p.2

Tactic:
isBoundedBilinearMap_smul

Premises used: isBoundedBilinearMap_smul
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
⊢ IsBoundedLinearMap.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) (⇑f : (a : E) → F)

Tactic:
{ f.toLinearMap.isLinear with bound := f.bound }

Premises used: IsBoundedLinearMap.mk, ContinuousLinearMap.toLinearMap, LinearMap.isLinear, ContinuousLinearMap.bound
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
G : Type u_4
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
inst_5 : Fintype ι
E : ι → Type u_6
inst_6 : (i : ι) → SeminormedAddCommGroup (E i)
inst_7 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (E i)
⊢ IsBoundedLinearMap 𝕜 (F := ContinuousMultilinearMap 𝕜 E (F × G))
    fun (p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G) ↦ p.1.prod (M₁ := E) p.2

Tactic:
(ContinuousMultilinearMap.prodL 𝕜 E F G).toContinuousLinearEquiv
    |>.toContinuousLinearMap.isBoundedLinearMap

Premises used: setOf, ContinuousMultilinearMap.prodL, ContinuousLinearMap.isBoundedLinearMap, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousMultilinearMap.prod, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
ι : Type u_5
inst_7 : Fintype ι
g : G →L[𝕜] E
⊢ IsBoundedLinearMap 𝕜 (F := ContinuousMultilinearMap.{u_1, u_5, u_4, u_3} 𝕜 (fun (x : ι) ↦ G) F)
    fun (f : ContinuousMultilinearMap.{u_1, u_5, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F) ↦
    f.compContinuousLinearMap (M₁ := fun (x : ι) ↦ G) (M₁' := fun (x : ι) ↦ E) fun (x : ι) ↦ g

Tactic:
(ContinuousMultilinearMap.compContinuousLinearMapL (ι := ι) (F := F) (fun _ ↦ g))
    |>.isBoundedLinearMap

Premises used: ContinuousLinearMap.isBoundedLinearMap, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousMultilinearMap.compContinuousLinearMapL
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E
y : F
hbc : ‖f‖ ≤ max ‖f‖ 1
⊢ ‖f‖ * ‖x‖ * ‖y‖ ≤ max ‖f‖ 1 * ‖x‖ * ‖y‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E
y : F
⊢ ‖f‖ ≤ max ‖f‖ 1

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E × F → G
hf : IsBoundedBilinearMap 𝕜 f
x : E
y : F
⊢ (((hf.toContinuousLinearMap : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y = f (x, y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Function.uncurry fun (x : E) (y : F) ↦ (((f : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y)

Tactic:
f.isBoundedBilinearMap.continuous

Premises used: ContinuousLinearMap.isBoundedBilinearMap, IsBoundedBilinearMap.continuous
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
⊢ IsBoundedBilinearMap 𝕜 (E := F →L[𝕜] G) (F := E →L[𝕜] F) (G := E →L[𝕜] G) fun (p : (F →L[𝕜] G) × (E →L[𝕜] F)) ↦
    p.1 ∘SL p.2

Tactic:
(compL 𝕜 E F G).isBoundedBilinearMap

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.isBoundedBilinearMap, ContinuousLinearMap.compL
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F →L[𝕜] G
⊢ IsBoundedLinearMap 𝕜 (F := E →L[𝕜] G) fun (f : E →L[𝕜] F) ↦ g ∘SL f

Tactic:
isBoundedBilinearMap_comp.isBoundedLinearMap_right g

Premises used: isBoundedBilinearMap_comp, IsBoundedBilinearMap.isBoundedLinearMap_right
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F
⊢ IsBoundedLinearMap 𝕜 (F := E →L[𝕜] G) fun (g : F →L[𝕜] G) ↦ g ∘SL f

Tactic:
(isBoundedBilinearMap_comp (G := G)).isBoundedLinearMap_left f

Premises used: isBoundedBilinearMap_comp, IsBoundedBilinearMap.isBoundedLinearMap_left
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ IsBoundedBilinearMap 𝕜 (E := E →L[𝕜] F) (F := E) (G := F) fun (p : (E →L[𝕜] F) × E) ↦ (p.1 : (a : E) → F) p.2

Tactic:
(ContinuousLinearMap.flip (apply 𝕜 F : E →L[𝕜] (E →L[𝕜] F) →L[𝕜] F)).isBoundedBilinearMap

Premises used: ContinuousLinearMap.isBoundedBilinearMap, ContinuousLinearMap.apply, ContinuousLinearMap.flip
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ IsBoundedBilinearMap 𝕜 (E := E →L[𝕜] 𝕜) (F := F) (G := E →L[𝕜] F) fun (p : (E →L[𝕜] 𝕜) × F) ↦ p.1.smulRight p.2

Tactic:
(smulRightL 𝕜 E F).isBoundedBilinearMap

Premises used: ContinuousLinearMap.smulRight, ContinuousLinearMap.isBoundedBilinearMap, ContinuousLinearMap.smulRightL
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
G : Type u_4
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
E : ι → Type u_6
inst_5 : Fintype ι
inst_6 : (i : ι) → NormedAddCommGroup (E i)
inst_7 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (E i)
⊢ IsBoundedBilinearMap 𝕜 (E := F →L[𝕜] G) (F := ContinuousMultilinearMap 𝕜 E F) (G := ContinuousMultilinearMap 𝕜 E G)
    fun (p : (F →L[𝕜] G) × ContinuousMultilinearMap 𝕜 E F) ↦ p.1.compContinuousMultilinearMap (M₁ := E) p.2

Tactic:
(compContinuousMultilinearMapL 𝕜 E F G).isBoundedBilinearMap

Premises used: ContinuousLinearMap.compContinuousMultilinearMap, ContinuousLinearMap.isBoundedBilinearMap, ContinuousLinearMap.compContinuousMultilinearMapL
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
p q : E × F
⊢ (h.deriv p : (a : E × F) → G) q = f (p.1, q.2) + f (q.1, p.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_5
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
⊢ IsBoundedBilinearMap.{u_1, u_5, u_5, u_5} 𝕜 (E := 𝕜') (F := 𝕜') (G := 𝕜' →L[𝕜] 𝕜') fun (p : 𝕜' × 𝕜') ↦
    (((mulLeftRight 𝕜 𝕜' : (a : 𝕜') → 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜') p.1 : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜') : (a : 𝕜') → 𝕜' →L[𝕜] 𝕜') p.2

Tactic:
(ContinuousLinearMap.mulLeftRight 𝕜 𝕜').isBoundedBilinearMap

Premises used: ContinuousLinearMap.isBoundedBilinearMap, ContinuousLinearMap.mulLeftRight
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
⊢ IsBoundedLinearMap 𝕜 (F := E × F →L[𝕜] G) fun (p : E × F) ↦ h.deriv p

Tactic:
h.toContinuousLinearMap.deriv₂.isBoundedLinearMap

Premises used: IsBoundedBilinearMap.toContinuousLinearMap, setOf, ContinuousLinearMap.deriv₂, IsBoundedBilinearMap.deriv, ContinuousLinearMap.isBoundedLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_5
inst_7 : TopologicalSpace X
g : X → F →L[𝕜] G
f : X → E →L[𝕜] F
hg : Continuous[inst_7, _] g
hf : Continuous[inst_7, _] f
⊢ Continuous[inst_7, _] fun (x : X) ↦ g x ∘SL f x

Tactic:
(compL 𝕜 E F G).continuous₂.comp₂ hg hf

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.continuous₂, Continuous.comp₂, ContinuousLinearMap.compL
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_5
inst_7 : TopologicalSpace X
g : X → F →L[𝕜] G
f : X → E →L[𝕜] F
s : Set X
hg : ContinuousOn g s
hf : ContinuousOn f s
⊢ ContinuousOn (Y := E →L[𝕜] G) (fun (x : X) ↦ g x ∘SL f x) s

Tactic:
(compL 𝕜 E F G).continuous₂.comp_continuousOn (hg.prodMk hf)

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.continuous₂, Continuous.comp_continuousOn, ContinuousLinearMap.compL, ContinuousOn.prodMk
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_5
inst_7 : TopologicalSpace X
g : X → F →L[𝕜] G
f : X → E →L[𝕜] F
x : X
hg : ContinuousAt g x
hf : ContinuousAt f x
⊢ ContinuousAt (Y := E →L[𝕜] G) (fun (x : X) ↦ g x ∘SL f x) x

Tactic:
(compL 𝕜 E F G).continuous₂.continuousAt.comp (hg.prodMk hf)

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.continuous₂, ContinuousLinearMap.compL, Continuous.continuousAt, ContinuousAt.comp, ContinuousAt.prodMk
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_5
inst_7 : TopologicalSpace X
g : X → F →L[𝕜] G
f : X → E →L[𝕜] F
s : Set X
x : X
hg : ContinuousWithinAt g s x
hf : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (Y := E →L[𝕜] G) (fun (x : X) ↦ g x ∘SL f x) s x

Tactic:
(compL 𝕜 E F G).continuous₂.continuousAt.comp_continuousWithinAt (hg.prodMk hf)

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.continuous₂, ContinuousLinearMap.compL, Continuous.continuousAt, ContinuousAt.comp_continuousWithinAt, ContinuousWithinAt.prodMk
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
X : Type u_5
inst_5 : TopologicalSpace X
f : X → E →L[𝕜] F
g : X → E
hf : Continuous[inst_5, _] f
hg : Continuous[inst_5, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
⊢ Continuous[inst_5, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ (f x : (a : E) → F) (g x)

Tactic:
isBoundedBilinearMap_apply.continuous.comp₂ hf hg

Premises used: Continuous.comp₂, IsBoundedBilinearMap.continuous, isBoundedBilinearMap_apply
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
X : Type u_5
inst_5 : TopologicalSpace X
f : X → E →L[𝕜] F
g : X → E
s : Set X
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn.{u_5, u_3} (Y := F) (fun (x : X) ↦ (f x : (a : E) → F) (g x)) s

Tactic:
(isBoundedBilinearMap_apply (𝕜 := 𝕜) (F := F)).continuous.comp_continuousOn (hf.prodMk hg)

Premises used: Continuous.comp_continuousOn, IsBoundedBilinearMap.continuous, isBoundedBilinearMap_apply, ContinuousOn.prodMk
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
X : Type u_6
inst_5 : TopologicalSpace X
f : X → E →L[𝕜] F
g : X → E
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt.{u_6, u_3} (Y := F) (fun (x : X) ↦ (f x : (a : E) → F) (g x)) x

Tactic:
isBoundedBilinearMap_apply.continuous.continuousAt.comp₂ hf hg

Premises used: ContinuousAt.comp₂, IsBoundedBilinearMap.continuous, Continuous.continuousAt, isBoundedBilinearMap_apply
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
X : Type u_6
inst_5 : TopologicalSpace X
f : X → E →L[𝕜] F
g : X → E
s : Set X
x : X
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt.{u_6, u_3} (Y := F) (fun (x : X) ↦ (f x : (a : E) → F) (g x)) s x

Tactic:
(isBoundedBilinearMap_apply (𝕜 := 𝕜) (F := F)).continuous.continuousAt.comp_continuousWithinAt
    (hf.prodMk hg)

Premises used: IsBoundedBilinearMap.continuous, Continuous.continuousAt, isBoundedBilinearMap_apply, ContinuousAt.comp_continuousWithinAt, ContinuousWithinAt.prodMk
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_5
inst_7 : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
s : Set X
x : X
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
simp :
  ContinuousWithinAt (Y := E × F →L[𝕜] G)
    (fun (x : X) ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) s x
⊢ ContinuousWithinAt (Y := E × F →L[𝕜] G) (fun (x : X) ↦ (f x).coprod (g x)) s x

Tactic:
simp only [← comp_fst_add_comp_snd]

Premises used: ContinuousLinearMap.comp_fst_add_comp_snd
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_5
inst_7 : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
s : Set X
x : X
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt (Y := E × F →L[𝕜] G)
    (fun (x : X) ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) s x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_5
inst_7 : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
simp :
  ContinuousAt (Y := E × F →L[𝕜] G)
    (fun (x : X) ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) x
⊢ ContinuousAt (Y := E × F →L[𝕜] G) (fun (x : X) ↦ (f x).coprod (g x)) x

Tactic:
simp only [← comp_fst_add_comp_snd]

Premises used: ContinuousLinearMap.comp_fst_add_comp_snd
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_5
inst_7 : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt (Y := E × F →L[𝕜] G)
    (fun (x : X) ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_5
inst_7 : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
s : Set X
hf : ContinuousOn f s
hg : ContinuousOn g s
simp :
  ContinuousOn (Y := E × F →L[𝕜] G)
    (fun (x : X) ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) s
⊢ ContinuousOn (Y := E × F →L[𝕜] G) (fun (x : X) ↦ (f x).coprod (g x)) s

Tactic:
simp only [← comp_fst_add_comp_snd]

Premises used: ContinuousLinearMap.comp_fst_add_comp_snd
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_5
inst_7 : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
s : Set X
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn (Y := E × F →L[𝕜] G)
    (fun (x : X) ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) s

Tactic:
fun_prop