awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
⊢ deriv (f p.1) p.2 ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f p.1 '' univ)) : Set F)

Tactic:
apply range_deriv_subset_closure_span_image _ dense_univ (mem_range_self _)

Premises used: Set.mem_range_self, dense_univ, range_deriv_subset_closure_span_image
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
⊢ deriv (f p.1) p.2 ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (range (f p.1))) : Set F)

Tactic:
have A : deriv (f p.1) p.2 ∈ closure (Submodule.span 𝕜 (range (f p.1))) := by
        rw [← image_univ]
        apply range_deriv_subset_closure_span_image _ dense_univ (mem_range_self _)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
A :
  deriv (f p.1) p.2 ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (range (f p.1))) : Set F)
x : 𝕜
⊢ f p.1 x ∈ range (Function.uncurry f)

Tactic:
mem_range_self (p.1, x)

Premises used: Set.mem_range_self, Set.Mem, Prod.mk, Prod.fst
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
A :
  deriv (f p.1) p.2 ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (range (f p.1))) : Set F)
x : 𝕜
⊢ f p.1 x ∈ range (Function.uncurry f)

Tactic:
exact mem_range_self (p.1, x)

Premises used: Set.mem_range_self, Prod.mk, Prod.fst
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
A :
  deriv (f p.1) p.2 ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (range (f p.1))) : Set F)
⊢ range (f p.1) ⊆ range (Function.uncurry f)

Tactic:
have B : range (f p.1) ⊆ range (f.uncurry) := by
        rintro - ⟨x, rfl⟩
        exact mem_range_self (p.1, x)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
A :
  deriv (f p.1) p.2 ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (range (f p.1))) : Set F)
B : range (f p.1) ⊆ range (Function.uncurry f)
⊢ (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) p ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (↑(Submodule.span 𝕜 (range (Function.uncurry f))) : Set F)

Tactic:
closure_mono (Submodule.span_mono B) A

Premises used: closure_mono, Submodule.span_mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
A :
  deriv (f p.1) p.2 ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (range (f p.1))) : Set F)
B : range (f p.1) ⊆ range (Function.uncurry f)
⊢ (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) p ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (↑(Submodule.span 𝕜 (range (Function.uncurry f))) : Set F)

Tactic:
exact closure_mono (Submodule.span_mono B) A

Premises used: closure_mono, Submodule.span_mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
⊢ (range fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (↑(Submodule.span 𝕜 (range (Function.uncurry f))) : Set F)

Tactic:
have : range (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2)
        ⊆ closure (Submodule.span 𝕜 (range f.uncurry)) := by
      rintro - ⟨p, rfl⟩
      have A : deriv (f p.1) p.2 ∈ closure (Submodule.span 𝕜 (range (f p.1))) := by
        rw [← image_univ]
        apply range_deriv_subset_closure_span_image _ dense_univ (mem_range_self _)
      have B : range (f p.1) ⊆ range (f.uncurry) := by
        rintro - ⟨x, rfl⟩
        exact mem_range_self (p.1, x)
      exact closure_mono (Submodule.span_mono B) A
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this_3 : ProperSpace 𝕜
this :
  (range fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (↑(Submodule.span 𝕜 (range (Function.uncurry f))) : Set F)
⊢ IsSeparable.{u_3} (α := F) (range fun (p : α × 𝕜) ↦ deriv (f p.1) p.2)

Tactic:
(isSeparable_range hf).span.closure.mono this

Premises used: TopologicalSpace.IsSeparable.span, TopologicalSpace.IsSeparable.closure, TopologicalSpace.IsSeparable.mono, TopologicalSpace.isSeparable_range
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this_3 : ProperSpace 𝕜
this :
  (range fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (↑(Submodule.span 𝕜 (range (Function.uncurry f))) : Set F)
⊢ IsSeparable.{u_3} (α := F) (range fun (p : α × 𝕜) ↦ deriv (f p.1) p.2)

Tactic:
exact (isSeparable_range hf).span.closure.mono this

Premises used: TopologicalSpace.IsSeparable.span, TopologicalSpace.IsSeparable.closure, TopologicalSpace.IsSeparable.mono, TopologicalSpace.isSeparable_range
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
hF : SecondCountableTopology F
⊢ StronglyMeasurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2

Tactic:
(measurable_deriv_with_param hf).stronglyMeasurable

Premises used: measurable_deriv_with_param, Measurable.stronglyMeasurable
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
hF : SecondCountableTopology F
⊢ StronglyMeasurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2

Tactic:
exact (measurable_deriv_with_param hf).stronglyMeasurable

Premises used: measurable_deriv_with_param, Measurable.stronglyMeasurable
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
inst_10 : MeasurableSpace F
inst_11 : BorelSpace F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
μ : Measure (α × 𝕜)
⊢ AEMeasurable (β := F) (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) μ

Tactic:
(measurable_deriv_with_param hf).aemeasurable

Premises used: measurable_deriv_with_param, Measurable.aemeasurable
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
inst_10 : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
μ : Measure (α × 𝕜)
⊢ AEStronglyMeasurable (β := F) (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) μ

Tactic:
(stronglyMeasurable_deriv_with_param hf).aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, stronglyMeasurable_deriv_with_param
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasStrictFDerivAt c c' x
hf : HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt (c • f) (c x • f' + c'.smulRight (f x)) x

Tactic:
(isBoundedBilinearMap_smul.hasStrictFDerivAt (c x, f x)).comp x <| hc.prodMk hf

Premises used: ContinuousLinearMap.comp, HasStrictFDerivAt.prodMk, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivWithinAt c c' s x
hf : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (c • f) (c x • f' + c'.smulRight (f x)) s x

Tactic:
(isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x)).comp_hasFDerivWithinAt x <|
    hc.prodMk hf

Premises used: ContinuousLinearMap.comp, HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivWithinAt c c' s x
hf : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (c • f) (c x • f' + c'.smulRight (f x)) s x

Tactic:
exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x)).comp_hasFDerivWithinAt x <|
    hc.prodMk hf

Premises used: HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivAt c c' x
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (c • f) (c x • f' + c'.smulRight (f x)) x

Tactic:
(isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x)).comp x <| hc.prodMk hf

Premises used: ContinuousLinearMap.comp, HasFDerivAt.prodMk, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivAt c c' x
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (c • f) (c x • f' + c'.smulRight (f x)) x

Tactic:
exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x)).comp x <| hc.prodMk hf

Premises used: HasFDerivAt.prodMk, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (c • f) s x

Tactic:
(hc.hasFDerivWithinAt.smul hf.hasFDerivWithinAt).differentiableWithinAt

Premises used: HasFDerivWithinAt.differentiableWithinAt, HasFDerivWithinAt.smul, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
hc : DifferentiableAt 𝕜 c x
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (c • f) x

Tactic:
(hc.hasFDerivAt.smul hf.hasFDerivAt).differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
hc : DifferentiableOn 𝕜 c s
hf : DifferentiableOn 𝕜 f s
⊢ DifferentiableOn 𝕜 (c • f) s

Tactic:
fun x hx => (hc x hx).smul (hf x hx)

Premises used: DifferentiableOn, DifferentiableWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
hc : Differentiable 𝕜 c
hf : Differentiable 𝕜 f
⊢ Differentiable 𝕜 (c • f)

Tactic:
fun x => (hc x).smul (hf x)

Premises used: Differentiable, DifferentiableAt.smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (fun (y : E) ↦ c y • f y) s x =
    HSMul.hSMul (β := E →L[𝕜] F) (c x) (fderivWithin 𝕜 f s x) +
      smulRight.{u_2, u_3, u_1, u_5} (S := 𝕜') (fderivWithin 𝕜 c s x) (f x)

Tactic:
(hc.hasFDerivWithinAt.smul hf.hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.smul, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (c • f) s x =
    HSMul.hSMul (β := E →L[𝕜] F) (c x) (fderivWithin 𝕜 f s x) +
      smulRight.{u_2, u_3, u_1, u_5} (S := 𝕜') (fderivWithin 𝕜 c s x) (f x)

Tactic:
(hc.hasFDerivWithinAt.smul hf.hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.smul, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
hc : DifferentiableAt 𝕜 c x
hf : DifferentiableAt 𝕜 f x
⊢ fderiv 𝕜 (fun (y : E) ↦ c y • f y) x =
    HSMul.hSMul (β := E →L[𝕜] F) (c x) (fderiv 𝕜 f x) + smulRight.{u_2, u_3, u_1, u_5} (S := 𝕜') (fderiv 𝕜 c x) (f x)

Tactic:
(hc.hasFDerivAt.smul hf.hasFDerivAt).fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
hc : DifferentiableAt 𝕜 c x
hf : DifferentiableAt 𝕜 f x
⊢ fderiv 𝕜 (c • f) x =
    HSMul.hSMul (β := E →L[𝕜] F) (c x) (fderiv 𝕜 f x) + smulRight.{u_2, u_3, u_1, u_5} (S := 𝕜') (fderiv 𝕜 c x) (f x)

Tactic:
(hc.hasFDerivAt.smul hf.hasFDerivAt).fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasStrictFDerivAt c c' x
f : F
⊢ HasStrictFDerivAt (fun (y : E) ↦ c y • f) (c'.smulRight f) x

Tactic:
simpa only [smul_zero, zero_add] using hc.smul (hasStrictFDerivAt_const f x)

Premises used: smul_zero, zero_add, hasStrictFDerivAt_const, HasStrictFDerivAt.smul