mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
⊢ deriv (fun y ↦ u * v y) x = u * deriv v x

Tactic:
simpa only [← derivWithin_univ] using derivWithin_const_mul_field u

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Add

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x ↦ f (b + x)) (-b + a)

Tactic:
by
  simp [differentiableAt_comp_add_left]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
h' : fderiv 𝕜 (↑f) a = ↑i
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt (↑f) p a
this : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ AnalyticAt 𝕜 (↑f.symm) (↑f a)

Tactic:
exact (f.hasFPowerSeriesAt_symm h0 hp this).analyticAt

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case neg
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c

Tactic:
rw [add_comm]

Goal state after:
case neg
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
⊢ ((c - b) / (c - a)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
inst✝² : DecidableEq ι
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : (i : ι) → G → E i
g' : (i : ι) → G →L[𝕜] E i
x : G
hg : ∀ (i : ι), HasFDerivAt (g i) (g' i) x
⊢ HasFDerivAt (fun x ↦ f fun i ↦ g i x) (∑ i, f.toContinuousLinearMap (fun j ↦ g j x) i ∘SL g' i) x

Tactic:
simpa using (hasFDerivAt_const f x).continuousMultilinearMap_apply hg

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x : (i : ι) → E i
H :
  (f.iteratedFDeriv n.succ x).curryLeft =
    ∑ e,
      (f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x) ∘SL
        Pi.compRightL 𝕜 E Subtype.val
A :
  HasFDerivAt (f.iteratedFDeriv n)
    (∑ e,
      (f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x) ∘SL
        Pi.compRightL 𝕜 E Subtype.val)
    x
⊢ HasFDerivAt (fun y ↦ f.iteratedFDeriv n y) (f.iteratedFDeriv n.succ x).curryLeft x

Tactic:
rwa [← H] at A

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
f' : E →L[𝕜'] F
s : Set E
x : E
g' : E →L[𝕜] F
h : HasFDerivWithinAt f g' s x
H : ContinuousLinearMap.restrictScalars 𝕜 f' = g'
⊢ HasFDerivWithinAt f f' s x

Tactic:
rw [← H] at h
  exact .of_isLittleO h.isLittleO

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
f' : E →L[𝕜'] F
x : E
g' : E →L[𝕜] F
h : HasFDerivAt f g' x
H : restrictScalars 𝕜 f' = g'
⊢ HasFDerivAt f f' x

Tactic:
rw [← H] at h
  exact .of_isLittleO h.isLittleO

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
⊢ iteratedFDeriv 𝕜 0 f x = p 0

Tactic:
by
  ext
  simpa using (coeff_zero h _).symm

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (n ! • (p n) fun x ↦ y) = (iteratedFDeriv 𝕜 n f x) fun x ↦ y
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ (n ! • (p.derivSeries n) fun x ↦ y) y = (iteratedFDeriv 𝕜 (n + 1) f x) fun x ↦ y

Tactic:
ih h.fderiv,

Goal state after:
case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (n ! • (p n) fun x ↦ y) = (iteratedFDeriv 𝕜 n f x) fun x ↦ y
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ ((iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) fun x ↦ y) y = (iteratedFDeriv 𝕜 (n + 1) f x) fun x ↦ y
Module: Mathlib.Analysis.Calculus.DSlope

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
a b : 𝕜
H : a = b → DifferentiableAt 𝕜 g a
⊢ dslope (⇑f ∘ g) a b = f (dslope g a b)

Tactic:
rcases eq_or_ne b a with (rfl | hne)
  · simp only [dslope_same]
    exact (f.hasFDerivAt.comp_hasDerivAt b (H rfl).hasDerivAt).deriv
  · simpa only [dslope_of_ne _ hne] using! f.toLinearMap.slope_comp g a b

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
⊢ HSMul.hSMul (d x) = HSMul.hSMul (MulOpposite.op (d x))

Tactic:
ext z

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
z : E →L[𝕜] 𝔸'
x✝ : E
⊢ (d x •> z) x✝ = (z <• d x) x✝
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ HSMul.hSMul (d x) = HSMul.hSMul (MulOpposite.op (d x))

Tactic:
ext z

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
z : E →L[𝕜] 𝔸'
x✝ : E
⊢ (d x •> z) x✝ = (z <• d x) x✝
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
⊢ HSMul.hSMul (d x) = HSMul.hSMul (MulOpposite.op (d x))

Tactic:
ext z

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
z : E →L[𝕜] 𝔸'
x✝ : E
⊢ (d x •> z) x✝ = (z <• d x) x✝
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
⊢ HasStrictFDerivAt (fun y ↦ c y * d) (d •> c') x

Tactic:
convert! hc.mul_const' d

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
⊢ HSMul.hSMul d = HSMul.hSMul (MulOpposite.op d)
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
⊢ HSMul.hSMul d = HSMul.hSMul (MulOpposite.op d)

Tactic:
ext z

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
z : E →L[𝕜] 𝔸'
x✝ : E
⊢ (d •> z) x✝ = (z <• d) x✝
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
⊢ HasFDerivWithinAt (fun y ↦ c y * d) (d •> c') s x

Tactic:
convert! hc.mul_const' d

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
⊢ HSMul.hSMul d = HSMul.hSMul (MulOpposite.op d)
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
⊢ HSMul.hSMul d = HSMul.hSMul (MulOpposite.op d)

Tactic:
ext z

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
z : E →L[𝕜] 𝔸'
x✝ : E
⊢ (d •> z) x✝ = (z <• d) x✝
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
⊢ HasFDerivAt (fun y ↦ c y * d) (d •> c') x

Tactic:
convert! hc.mul_const' d

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
⊢ HSMul.hSMul d = HSMul.hSMul (MulOpposite.op d)
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
⊢ HSMul.hSMul d = HSMul.hSMul (MulOpposite.op d)

Tactic:
ext z

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
z : E →L[𝕜] 𝔸'
x✝ : E
⊢ (d •> z) x✝ = (z <• d) x✝
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : Finite ι
l : List ι
x : ι → 𝔸
this : Fintype ι
⊢ HasStrictFDerivAt (fun x ↦ (List.map x l).prod)
    (∑ i, (List.map x (List.take (↑i) l)).prod •> (proj l[i] <• (List.map x (List.drop (↑i).succ l)).prod)) x

Tactic:
induction l with

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
| l

Tactic:
rw [← List.map_get_finRange l]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
| List.map l.get (List.finRange l.length)
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun x ↦ f i x) (f' i) x
m : E
⊢ ((∑ x_1,
          (List.take (↑x_1) (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod •>
            (proj x_1 <• (List.map (fun i ↦ f (l.get i) x) (List.drop (↑x_1).succ (List.finRange l.length))).prod)) ∘SL
        pi fun i ↦ f' (l.get i))
      m =
    (∑ x_1,
        (List.take (↑x_1) (List.map (fun x_2 ↦ f x_2 x) (List.map l.get (List.finRange l.length)))).prod •>
          (f' (l.get x_1) <•
            (List.map (fun x_2 ↦ f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod))
      m

Tactic:
List.map_drop,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun x ↦ f i x) (f' i) x
m : E
⊢ ((∑ x_1,
          (List.take (↑x_1) (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod •>
            (proj x_1 <• (List.drop (↑x_1).succ (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod)) ∘SL
        pi fun i ↦ f' (l.get i))
      m =
    (∑ x_1,
        (List.take (↑x_1) (List.map (fun x_2 ↦ f x_2 x) (List.map l.get (List.finRange l.length)))).prod •>
          (f' (l.get x_1) <•
            (List.drop (↑x_1).succ (List.map (fun x_2 ↦ f x_2 x) (List.map l.get (List.finRange l.length)))).prod))
      m
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m ↦ z ^ m • a (m + n)) t

Tactic:
exact ⟨a n, by simp [h, hn.ne', this], by simpa [h] using hasSum_at_zero fun m => a (m + n)⟩

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivAt (fun x ↦ f i x) (f' i) x
m : E
⊢ ((∑ x_1,
          (List.take (↑x_1) (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod •>
            (proj x_1 <• (List.map (fun i ↦ f (l.get i) x) (List.drop (↑x_1).succ (List.finRange l.length))).prod)) ∘SL
        pi fun i ↦ f' (l.get i))
      m =
    (∑ x_1,
        (List.take (↑x_1) (List.map (fun x_2 ↦ f x_2 x) (List.map l.get (List.finRange l.length)))).prod •>
          (f' (l.get x_1) <•
            (List.map (fun x_2 ↦ f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod))
      m

Tactic:
List.map_drop,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivAt (fun x ↦ f i x) (f' i) x
m : E
⊢ ((∑ x_1,
          (List.take (↑x_1) (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod •>
            (proj x_1 <• (List.drop (↑x_1).succ (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod)) ∘SL
        pi fun i ↦ f' (l.get i))
      m =
    (∑ x_1,
        (List.take (↑x_1) (List.map (fun x_2 ↦ f x_2 x) (List.map l.get (List.finRange l.length)))).prod •>
          (f' (l.get x_1) <•
            (List.drop (↑x_1).succ (List.map (fun x_2 ↦ f x_2 x) (List.map l.get (List.finRange l.length)))).prod))
      m
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivWithinAt (fun x ↦ f i x) (f' i) s x
m : E
⊢ ((∑ x_1,
          (List.take (↑x_1) (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod •>
            (proj x_1 <• (List.map (fun i ↦ f (l.get i) x) (List.drop (↑x_1).succ (List.finRange l.length))).prod)) ∘SL
        pi fun i ↦ f' (l.get i))
      m =
    (∑ x_1,
        (List.take (↑x_1) (List.map (fun x_2 ↦ f x_2 x) (List.map l.get (List.finRange l.length)))).prod •>
          (f' (l.get x_1) <•
            (List.map (fun x_2 ↦ f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod))
      m

Tactic:
List.map_drop,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivWithinAt (fun x ↦ f i x) (f' i) s x
m : E
⊢ ((∑ x_1,
          (List.take (↑x_1) (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod •>
            (proj x_1 <• (List.drop (↑x_1).succ (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod)) ∘SL
        pi fun i ↦ f' (l.get i))
      m =
    (∑ x_1,
        (List.take (↑x_1) (List.map (fun x_2 ↦ f x_2 x) (List.map l.get (List.finRange l.length)))).prod •>
          (f' (l.get x_1) <•
            (List.drop (↑x_1).succ (List.map (fun x_2 ↦ f x_2 x) (List.map l.get (List.finRange l.length)))).prod))
      m
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
L : Filter (𝕜 × 𝕜)
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
L' : Filter (𝕜' × 𝕜')
hh₂ : HasDerivAtFilter h₂ h₂' L'
hh : HasDerivAtFilter h h' L
hL : Tendsto (Prod.map h h) L L'
⊢ HasDerivAtFilter (h₂ ∘ h) (h₂' * h') L

Tactic:
by
  rw [mul_comm]
  exact hh₂.scomp hh hL

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Tactic:
rw [mul_comm]
  exact hh₂.scomp x hh hst

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.ZPow

Goal state before:
pp: case succ
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk : (deriv^[k] fun x ↦ (c * x + d)⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * c ^ k * (c * x + d) ^ (-1 - ↑k)
⊢ (deriv^[1] fun x ↦ (-1) ^ k * ↑k ! * c ^ k * (c * x + d) ^ (-1 - ↑k)) = fun x ↦
    (-1) ^ (1 + k) * ↑((1 + k) * k !) * c ^ (1 + k) * (c * x + d) ^ (-1 - ↑(1 + k))

Tactic:
ext z

Goal state after:
case succ
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk : (deriv^[k] fun x ↦ (c * x + d)⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * c ^ k * (c * x + d) ^ (-1 - ↑k)
z : 𝕜
⊢ deriv^[1] (fun x ↦ (-1) ^ k * ↑k ! * c ^ k * (c * x + d) ^ (-1 - ↑k)) z =
    (-1) ^ (1 + k) * ↑((1 + k) * k !) * c ^ (1 + k) * (c * z + d) ^ (-1 - ↑(1 + k))
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left✝ : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
this : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z
| fun z ↦ (z - z₀) ^ (m - n) • g z

Tactic:
z,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left✝ : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
this : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z
z : 𝕜
| (z - z₀) ^ (m - n) • g z