awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
c : R
⊢ fderivWithin 𝕜 (fun (y : E) ↦ c • f y) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)

Tactic:
(h.hasFDerivWithinAt.const_smul c).fderivWithin hxs

Premises used: HasFDerivWithinAt.const_smul, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
c : R
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)

Tactic:
fderivWithin_fun_const_smul hxs h c

Premises used: fderivWithin_fun_const_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
⊢ DifferentiableWithinAt 𝕜 (c • f) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.const_smul c⟩

Premises used: DifferentiableWithinAt.const_smul, Iff.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
refine : ∀ (h : DifferentiableWithinAt 𝕜 (c • f) s x), DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (c • f) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.const_smul c⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
h : DifferentiableWithinAt 𝕜 (c • f) s x
⊢ f x = (@Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • c • f) x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
h : DifferentiableWithinAt 𝕜 (c • f) s x
apply : f =ᶠ[nhdsWithin x s] @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • c • f
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
apply (h.const_smul ⅟c).congr_of_eventuallyEq ?_ (by simp)

Premises used: Invertible.invOf, DifferentiableWithinAt.congr_of_eventuallyEq, DifferentiableWithinAt.const_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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_1 : E
s : Set E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
h : DifferentiableWithinAt 𝕜 (c • f) s x_1
x : E
⊢ f x = (@Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • c • f) x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
h : DifferentiableWithinAt 𝕜 (c • f) s x
h₁ :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E | (fun (x : E) ↦ f x = (@Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • c • f) x) x} a
h₂ h₃ : ∀ (x : E), f x = (@Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • c • f) x
⊢ f =ᶠ[nhdsWithin x s] @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • c • f

Tactic:
filter_upwards with x using by simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
pos :
  ∀ (h : DifferentiableWithinAt 𝕜 f s x),
    fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
neg :
  ∀ (h : ¬DifferentiableWithinAt 𝕜 f s x),
    fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)

Tactic:
by_cases h : DifferentiableWithinAt 𝕜 f s x

Premises used: DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)

Tactic:
(h.hasFDerivWithinAt.const_smul c).fderivWithin hs

Premises used: HasFDerivWithinAt.const_smul, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)

Tactic:
exact (h.hasFDerivWithinAt.const_smul c).fderivWithin hs

Premises used: HasFDerivWithinAt.const_smul, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
contrapose : ∀ (h : DifferentiableWithinAt 𝕜 (c • f) s x), DifferentiableWithinAt 𝕜 f s x
⊢ ¬DifferentiableWithinAt 𝕜 (c • f) s x

Tactic:
contrapose h
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 (c • f) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
(differentiableWithinAt_smul_iff c).mp h

Premises used: Iff.mp, differentiableWithinAt_smul_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 (c • f) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
exact (differentiableWithinAt_smul_iff c).mp h

Premises used: Iff.mp, differentiableWithinAt_smul_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬DifferentiableWithinAt 𝕜 (c • f) s x

Tactic:
have : ¬DifferentiableWithinAt 𝕜 (c • f) s x := by
      contrapose h
      exact (differentiableWithinAt_smul_iff c).mp h
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
this : ¬DifferentiableWithinAt 𝕜 (c • f) s x
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)

Tactic:
simp [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt this]

Premises used: fderivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
h : DifferentiableAt 𝕜 f x
c : R
⊢ fderiv 𝕜 (fun (y : E) ↦ c • f y) x = HSMul.hSMul (β := E →L[𝕜] F) c (fderiv 𝕜 f x)

Tactic:
(h.hasFDerivAt.const_smul c).fderiv

Premises used: HasFDerivAt.const_smul, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
h : DifferentiableAt 𝕜 f x
c : R
⊢ fderiv 𝕜 (c • f) x = HSMul.hSMul (β := E →L[𝕜] F) c (fderiv 𝕜 f x)

Tactic:
(h.hasFDerivAt.const_smul c).fderiv

Premises used: HasFDerivAt.const_smul, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
rw : DifferentiableWithinAt 𝕜 (c • f) Set.univ x ↔ DifferentiableAt 𝕜 f x
rw₁ : DifferentiableWithinAt 𝕜 f Set.univ x ↔ DifferentiableAt 𝕜 f x
rw₂ rw₃ : DifferentiableAt 𝕜 f x ↔ DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (c • f) x ↔ DifferentiableAt 𝕜 f x

Tactic:
rw [← differentiableWithinAt_univ, differentiableWithinAt_smul_iff, differentiableWithinAt_univ]

Premises used: differentiableWithinAt_smul_iff, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
⊢ fderiv 𝕜 (c • f) x = HSMul.hSMul (β := E →L[𝕜] F) c (fderiv 𝕜 f x)

Tactic:
simp [← fderivWithin_univ, fderivWithin_const_smul_of_invertible c uniqueDiffWithinAt_univ]

Premises used: fderivWithin_univ, fderivWithin_const_smul_of_invertible, uniqueDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : DivisionSemiring R
inst_6 : Module R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
hs : UniqueDiffWithinAt 𝕜 s x
inl : fderivWithin 𝕜 (HSMul.hSMul (α := R) 0 f) s x = HSMul.hSMul (α := R) (β := E →L[𝕜] F) 0 (fderivWithin 𝕜 f s x)
inr : ∀ (ha : c ≠ 0), fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)

Tactic:
obtain (rfl | ha) := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : DivisionSemiring R
inst_6 : Module R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (HSMul.hSMul (α := R) 0 f) s x = HSMul.hSMul (α := R) (β := E →L[𝕜] F) 0 (fderivWithin 𝕜 f s x)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : DivisionSemiring R
inst_6 : Module R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
hs : UniqueDiffWithinAt 𝕜 s x
ha : c ≠ 0
inr : ∀ (this : Invertible c), fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)

Tactic:
have : Invertible c := invertibleOfNonzero ha
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : DivisionSemiring R
inst_6 : Module R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
hs : UniqueDiffWithinAt 𝕜 s x
ha : c ≠ 0
this : Invertible c
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)

Tactic:
simp [fderivWithin_const_smul_of_invertible c hs]

Premises used: fderivWithin_const_smul_of_invertible
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
R : Type u_4
inst_3 : DivisionSemiring R
inst_4 : Module R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
s : Set 𝕜
f : 𝕜 → F
x : 𝕜
c : R
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := 𝕜 →L[𝕜] F) c (fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F)
neg :
  ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
    fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := 𝕜 →L[𝕜] F) c (fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F)
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := 𝕜 →L[𝕜] F) c (fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F)

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
R : Type u_4
inst_3 : DivisionSemiring R
inst_4 : Module R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
s : Set 𝕜
f : 𝕜 → F
x : 𝕜
c : R
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := 𝕜 →L[𝕜] F) c (fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F)

Tactic:
fderivWithin_const_smul_field c hsx

Premises used: fderivWithin_const_smul_field
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
R : Type u_4
inst_3 : DivisionSemiring R
inst_4 : Module R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
s : Set 𝕜
f : 𝕜 → F
x : 𝕜
c : R
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := 𝕜 →L[𝕜] F) c (fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F)

Tactic:
exact fderivWithin_const_smul_field c hsx

Premises used: fderivWithin_const_smul_field
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
R : Type u_4
inst_3 : DivisionSemiring R
inst_4 : Module R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
s : Set 𝕜
f : 𝕜 → F
x : 𝕜
c : R
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := 𝕜 →L[𝕜] F) c (fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F)

Tactic:
simp [fderivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: fderivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : DivisionSemiring R
inst_6 : Module R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
simp_rw : fderivWithin 𝕜 (c • f) Set.univ = HSMul.hSMul (β := (x : E) → E →L[𝕜] F) c (fderivWithin 𝕜 f Set.univ)
⊢ fderiv 𝕜 (c • f) = HSMul.hSMul (β := (x : E) → E →L[𝕜] F) c (fderiv 𝕜 f)

Tactic:
simp_rw [← fderivWithin_univ]

Premises used: fderivWithin_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : DivisionSemiring R
inst_6 : Module R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
h :
  ∀ (x x_1 : E),
    Eq.{u_3 + 1} (α := F) ((fderivWithin 𝕜 (c • f) Set.univ x : (a : E) → F) x_1 : F)
      ((HSMul.hSMul (β := (x : E) → E →L[𝕜] F) c (fderivWithin 𝕜 f Set.univ) x : (a : E) → F) x_1 : F)
⊢ fderivWithin 𝕜 (c • f) Set.univ = HSMul.hSMul (β := (x : E) → E →L[𝕜] F) c (fderivWithin 𝕜 f Set.univ)

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
R : Type u_4
inst_5 : DivisionSemiring R
inst_6 : Module R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
x x_1 : E
⊢ Eq.{u_3 + 1} (α := F) ((fderivWithin 𝕜 (c • f) Set.univ x : (a : E) → F) x_1 : F)
    ((HSMul.hSMul (β := (x : E) → E →L[𝕜] F) c (fderivWithin 𝕜 f Set.univ) x : (a : E) → F) x_1 : F)

Tactic:
simp [fderivWithin_const_smul_field c uniqueDiffWithinAt_univ]

Premises used: fderivWithin_const_smul_field, uniqueDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 g : E → F
f' g' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hg : HasFDerivAtFilter g g' L
x : E × E
⊢ HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F) +
      HSub.hSub (β := F) (g x.1 - g x.2) ((g' : (a : E) → F) (x.1 - x.2) : F) =
    HSub.hSub (β := F) ((f + g) x.1 - (f + g) x.2) ((f' + g' : (a : E) → F) (x.1 - x.2) : F)

Tactic:
grind [Pi.add_apply, add_apply]

Premises used: ContinuousLinearMap.add_apply, Pi.add_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 g : E → F
f' g' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
hg : HasStrictFDerivAt g g' x
⊢ HasStrictFDerivAt (f + g) (f' + g') x

Tactic:
HasFDerivAtFilter.add hf hg

Premises used: HasFDerivAtFilter.add, HasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 g : E → F
f' g' : E →L[𝕜] F
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
⊢ HasFDerivWithinAt (f + g) (f' + g') s x

Tactic:
HasFDerivAtFilter.add hf hg

Premises used: HasFDerivWithinAt, HasFDerivAtFilter.add
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 g : E → F
f' g' : E →L[𝕜] F
x : E
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
⊢ HasFDerivAt (f + g) (f' + g') x

Tactic:
HasFDerivAtFilter.add hf hg

Premises used: HasFDerivAt, HasFDerivAtFilter.add
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 g : E → F
x : E
s : Set E
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
⊢ DifferentiableWithinAt 𝕜 (f + g) s x

Tactic:
(hf.hasFDerivWithinAt.add hg.hasFDerivWithinAt).differentiableWithinAt

Premises used: HasFDerivWithinAt.add, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 g : E → F
x : E
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
⊢ DifferentiableAt 𝕜 (f + g) x

Tactic:
(hf.hasFDerivAt.add hg.hasFDerivAt).differentiableAt

Premises used: HasFDerivAt.add, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt