mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case hbc
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
⊢ ∑ k ∈ Ico 2 (n + 1), a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j, ‖p.rightInv i x (c.blocksFun j)‖ ≤
    ∑ k ∈ Ico 2 (n + 1), (r * ∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ k

Tactic:
mul_pow

Goal state after:
case hbc
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
⊢ ∑ k ∈ Ico 2 (n + 1), a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j, ‖p.rightInv i x (c.blocksFun j)‖ ≤
    ∑ x_1 ∈ Ico 2 (n + 1), r ^ x_1 * (∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ x_1
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ⋯
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := ⋯
⊢ ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a → S (n + 1) ≤ (I + 1) * a

Tactic:
intro n

Goal state after:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := fun n ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
n : ℕ
⊢ 1 ≤ n → S n ≤ (I + 1) * a → S (n + 1) ≤ (I + 1) * a
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := ⋯
min_pos : 0 < min rf' ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ Metric.eball 0 (min rf' ↑r)
y_mem : y ∈ Metric.eball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A : Tendsto (fun n ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x ↦ y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
B : Tendsto (fun n ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b ↦ y)) atTop (𝓝 (g (f (x + y))))
C :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n n, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (g (f (x + y))))
D : HasSum (fun i ↦ (q.compAlongComposition p i.snd) fun _j ↦ y) (g (f (x + y)))
⊢ ∀ (b : ℕ), HasSum (fun c ↦ (q.compAlongComposition p ⟨b, c⟩.snd) fun _j ↦ y) ((q.comp p b) fun _j ↦ y)

Tactic:
intro n

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ Metric.eball 0 (min rf' ↑r)
y_mem : y ∈ Metric.eball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A : Tendsto (fun n ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x ↦ y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
B : Tendsto (fun n ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b ↦ y)) atTop (𝓝 (g (f (x + y))))
C :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n n, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (g (f (x + y))))
D : HasSum (fun i ↦ (q.compAlongComposition p i.snd) fun _j ↦ y) (g (f (x + y)))
n : ℕ
⊢ HasSum (fun c ↦ (q.compAlongComposition p ⟨n, c⟩.snd) fun _j ↦ y) ((q.comp p n) fun _j ↦ y)
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
⊢ ↑r ≤ min p.radius q.radius

Tactic:
rw [le_min_iff]

Goal state after:
case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
⊢ ↑r ≤ p.radius ∧ ↑r ≤ q.radius
Module: Mathlib.Analysis.Calculus.FDeriv.Comp

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) L
⊢ HasFDerivAtFilter f^[n + 1] (f' ^ (n + 1)) L

Tactic:
Function.iterate_succ,

Goal state after:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ (n + 1)) L
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case inr
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr'✝ : ↑r' < r
C : ι → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * ↑r' ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
n : ℕ
hr' : 0 < ↑r' ^ n
⊢ ‖pi p n‖ * ↑r' ^ n ≤ D

Tactic:
simp only [pi]
    rw [← le_div_iff₀ hr', ContinuousMultilinearMap.opNorm_pi,
      pi_norm_le_iff_of_nonneg (by positivity)]
    intro i
    exact (le_div_iff₀ hr').2 ((hC i n).trans (hD i))

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
c : F
⊢ fderivWithin 𝕜 (fun y ↦ f y + c) s x = fderivWithin 𝕜 f s x

Tactic:
simp [fderivWithin]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
a : E
⊢ fderivWithin 𝕜 (fun x ↦ f (x - a)) s x = fderivWithin 𝕜 f (-a +ᵥ s) (x - a)

Tactic:
by
  simpa [sub_eq_add_neg] using fderivWithin_comp_add_right (-a)

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case mpr.cont.zero
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
hm : ↑0 ≤ ↑n.succ
⊢ ContinuousOn (fun x ↦ p x 0) s

Tactic:
have : DifferentiableOn 𝕜 (fun x => p x 0) s := fun x hx =>
          (Hfderiv_zero x hx).differentiableWithinAt

Goal state after:
case mpr.cont.zero
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
hm : ↑0 ≤ ↑n.succ
this : DifferentiableOn 𝕜 (fun x ↦ p x 0) s
⊢ ContinuousOn (fun x ↦ p x 0) s
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
e₁ : E
⊢ f₁ =ᶠ[𝓝 e₁] f → ftaylorSeries 𝕜 f₁ e₁ = ftaylorSeries 𝕜 f e₁

Tactic:
he₁

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
e₁ : E
he₁ : f₁ =ᶠ[𝓝 e₁] f
⊢ ftaylorSeries 𝕜 f₁ e₁ = ftaylorSeries 𝕜 f e₁
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : HasDerivWithinAt u u' s x
hv : HasDerivWithinAt v v' s x
⊢ HasDerivWithinAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) s x

Tactic:
simpa using (B.hasFDerivWithinAt_of_bilinear
    hu.hasFDerivWithinAt hv.hasFDerivWithinAt).hasDerivWithinAt

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 : E → F
x : E
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
⊢ AnalyticAt 𝕜 (fderiv 𝕜 f) x

Tactic:
exact hp.fderiv.analyticAt

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case succ
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih : ∀ (a : 𝕜), iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s a = (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
a : 𝕜
ih' : iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s = fun a ↦ (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
g : 𝕜 → 𝕜 [×n]→L[𝕜] F := fun a ↦ iteratedFDerivWithin 𝕜 n f (-s) a
⊢ (continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ 𝕜) F).symm ((-1) ^ (n + 1) • fderivWithin 𝕜 g (-s) (-a)) =
    (-1) ^ (n + 1) •
      (continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ 𝕜) F).symm
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f (-s)) (-s) (-a))

Tactic:
map_smul

Goal state after:
case succ
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih : ∀ (a : 𝕜), iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s a = (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
a : 𝕜
ih' : iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s = fun a ↦ (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
g : 𝕜 → 𝕜 [×n]→L[𝕜] F := fun a ↦ iteratedFDerivWithin 𝕜 n f (-s) a
⊢ (-1) ^ (n + 1) • (continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ 𝕜) F).symm (fderivWithin 𝕜 g (-s) (-a)) =
    (-1) ^ (n + 1) •
      (continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ 𝕜) F).symm
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f (-s)) (-s) (-a))
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
f : F
⊢ HasDerivWithinAt (fun y ↦ c y • f) (c' • f) s x

Tactic:
by
  have := hc.smul (hasDerivWithinAt_const x s f)
  rwa [smul_zero, zero_add] at this

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
x : 𝕜
s : Set 𝕜
c : F
⊢ derivWithin (fun y ↦ f y + c) s x = derivWithin f s x

Tactic:
simp only [derivWithin, fderivWithin_add_const]

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 : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x ↦ f (- -x)) a

Tactic:
neg_neg

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

Goal state before:
pp: 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 : k
h : slope f a b = 0
⊢ f a = f b

Tactic:
← sub_smul_slope_vadd f a b,

Goal state after:
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 : k
h : slope f a b = 0
⊢ f a = (b - a) • slope f a b +ᵥ f a
Module: Mathlib.Analysis.Analytic.Uniqueness

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x ↦ y) = 0
⊢ ∀ (y : E), ((p k) fun x ↦ y) = 0

Tactic:
have psum_eq : p.partialSum (k + 1) = fun y => p k fun _ => y := by
    funext z
    refine Finset.sum_eq_single _ (fun b hb hnb => ?_) fun hn => ?_
    · have := Finset.mem_range_succ_iff.mp hb
      simp only [hk b (this.lt_of_ne hnb)]
    · exact False.elim (hn (Finset.mem_range.mpr (lt_add_one k)))

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x ↦ y) = 0
psum_eq : p.partialSum (k + 1) = fun y ↦ (p k) fun x ↦ y
⊢ ∀ (y : E), ((p k) fun x ↦ y) = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
⊢ 0 < slope f x y ↔ f x < f y

Tactic:
simp_rw [lt_iff_le_and_ne, slope_nonneg_iff_of_le hxy, Ne, eq_comm, slope_eq_zero_iff]

Goal state after:
Module: Mathlib.Analysis.Analytic.Uniqueness

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
⊢ EqOn f 0 U

Tactic:
suffices main : closure u ∩ U ⊆ u by
    have Uu : U ⊆ u :=
      hU.subset_of_closure_inter_subset isOpen_setOfPred_eventually_nhds ⟨z₀, h₀, hfz₀⟩ main
    intro z hz
    simpa using mem_of_mem_nhds (Uu hz)

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∩ U ⊆ u
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
⊢ ∀ {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (0! • (p 0) fun x ↦ y) = (iteratedFDeriv 𝕜 0 f x) fun x ↦ y

Tactic:
p

Goal state after:
case zero
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
⊢ ∀ {f : E → F}, HasFPowerSeriesOnBall f p x r → (0! • (p 0) fun x ↦ y) = (iteratedFDeriv 𝕜 0 f x) fun x ↦ y
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},
    HasFPowerSeriesOnBall f p x r → ((n + 1)! • (p (n + 1)) fun x ↦ y) = (iteratedFDeriv 𝕜 (n + 1) f x) fun x ↦ y

Tactic:
p

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},
    HasFPowerSeriesOnBall f p x r → ((n + 1)! • (p (n + 1)) fun x ↦ y) = (iteratedFDeriv 𝕜 (n + 1) f x) fun x ↦ y
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

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

Tactic:
| cons a l IH =>

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : g x ∈ s
i : ℕ
⊢ ‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (g x)‖

Tactic:
have : iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s) x =
      (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun _ => g :=
    g.toContinuousLinearEquiv.iteratedFDerivWithin_comp_right f hs hx i
  rw [this, ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : ↑i ≤ n
hxt : f x ∈ t
hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] f x)
H₁ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) u
H₂ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i) g (ftaylorSeriesWithin 𝕜 g t) (f '' u)
⊢ ∃ u,
    x ∈ u ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧
        HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
          HasFTaylorSeriesUpToOn (↑i) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))

Tactic:
rcases (nhdsWithin_basis_open _ _).smallSets.eventually_iff.mp (H₁.and H₂)
      with ⟨u, ⟨hxu, huo⟩, hu⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : ↑i ≤ n
hxt : f x ∈ t
hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] f x)
H₁ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) u
H₂ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i) g (ftaylorSeriesWithin 𝕜 g t) (f '' u)
u : Set E
hu :
  ∀ ⦃x : Set E⦄,
    x ∈ 𝒫 (u ∩ s) →
      HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) x ∧
        HasFTaylorSeriesUpToOn (↑i) g (ftaylorSeriesWithin 𝕜 g t) (f '' x)
hxu : x ∈ u
huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
⊢ ∃ u,
    x ∈ u ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧
        HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
          HasFTaylorSeriesUpToOn (↑i) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))