mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' univ x
hs : s ∈ 𝓝 x
⊢ HasFDerivAt f f' x

Tactic:
hasFDerivWithinAt_univ

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivAt f f' x
hs : s ∈ 𝓝 x
⊢ HasFDerivAt f f' x
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: case mp
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
f : α → E
inst✝ : ContinuousSMul 𝕜 E
⊢ f =o[𝕜; l] 1 → Tendsto f l (𝓝 0)

Tactic:
intro hf

Goal state after:
case mp
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
f : α → E
inst✝ : ContinuousSMul 𝕜 E
hf : f =o[𝕜; l] 1
⊢ Tendsto f l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: case mpr
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
f : α → E
inst✝ : ContinuousSMul 𝕜 E
⊢ Tendsto f l (𝓝 0) →
    ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (1 x)

Tactic:
intro hf

Goal state after:
case mpr
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
f : α → E
inst✝ : ContinuousSMul 𝕜 E
hf : Tendsto f l (𝓝 0)
⊢ ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (1 x)
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ (constFormalMultilinearSeries 𝕜 E 0).radius = ∞

Tactic:
exact constFormalMultilinearSeries_radius

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
y : E
x✝ : y ∈ Metric.eball 0 ∞
⊢ HasSum (fun n ↦ (p n) fun x ↦ y) (p.sum y)

Tactic:
exact p.hasSum_of_finite hn y

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
c : ℕ → 𝕜
r r' : ℝ≥0
hr' : r' ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
⊢ Tendsto (fun n ↦ ‖c (n + 1)‖ / ‖c n‖ * (‖↑r' ^ (n + 1)‖ / ‖↑r' ^ n‖)) atTop (𝓝 ↑(r' * r))

Tactic:
← norm_div,

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
c : ℕ → 𝕜
r r' : ℝ≥0
hr' : r' ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
⊢ Tendsto (fun n ↦ ‖c (n + 1) / c n‖ * ‖↑r' ^ (n + 1) / ↑r' ^ n‖) atTop (𝓝 ↑(r' * r))
Module: Mathlib.Analysis.Analytic.CPolynomialDef

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
finsupp : (Function.support f).Finite
k l : ℕ
⊢ HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)

Tactic:
changeOriginSeries,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
finsupp : (Function.support f).Finite
k l : ℕ
⊢ HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((∑ s, p.changeOriginSeriesTerm k l ↑s ⋯) fun x_1 ↦ x) fun x ↦ y)
Module: Mathlib.Analysis.Analytic.CPolynomialDef

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
hn : ∀ (m : ℕ), n✝ ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)
hfk : ∀ (k : ℕ), HasSum (fun x ↦ f ⟨k, x⟩) ((p.changeOrigin x k) fun x ↦ y)
hf : HasSum f ((p.changeOrigin x).sum y)
n : ℕ
⊢ HasSum (fun c ↦ (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩) ((p n) ((fun x_1 ↦ x) + fun x ↦ y))

Tactic:
(p n).map_add_univ (fun _ ↦ x) fun _ ↦ y

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
hn : ∀ (m : ℕ), n✝ ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)
hfk : ∀ (k : ℕ), HasSum (fun x ↦ f ⟨k, x⟩) ((p.changeOrigin x k) fun x ↦ y)
hf : HasSum f ((p.changeOrigin x).sum y)
n : ℕ
⊢ HasSum (fun c ↦ (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩) (∑ s, (p n) (s.piecewise (fun x_1 ↦ x) fun x ↦ y))
Module: Mathlib.Analysis.Analytic.CPolynomialDef

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
hn : ∀ (m : ℕ), n✝ ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)
hfk : ∀ (k : ℕ), HasSum (fun x ↦ f ⟨k, x⟩) ((p.changeOrigin x k) fun x ↦ y)
hf : HasSum f ((p.changeOrigin x).sum y)
n : ℕ
⊢ HasSum (fun c ↦ (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩)
    (∑ x_1,
      ((p.changeOriginSeriesTerm (changeOriginIndexEquiv.symm ⟨n, x_1⟩).fst
            (changeOriginIndexEquiv.symm ⟨n, x_1⟩).snd.fst ↑(changeOriginIndexEquiv.symm ⟨n, x_1⟩).snd.snd ⋯)
          fun x_2 ↦ x)
        fun x ↦ y)

Tactic:
exact hasSum_fintype fun c ↦ f (changeOriginIndexEquiv.symm ⟨n, c⟩)

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

Goal state before:
pp: case a.a
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
a✝¹ : k ∈ Ico 2 (n + 1)
c : Composition k
a✝ : c ∈ {c | 1 < c.length}.toFinset
⊢ a ^ k * (r ^ c.length * ∏ j, p (c.blocksFun j)) = ∏ j, r * (a ^ c.blocksFun j * p (c.blocksFun j))

Tactic:
prod_mul_distrib,

Goal state after:
case a.a
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
a✝¹ : k ∈ Ico 2 (n + 1)
c : Composition k
a✝ : c ∈ {c | 1 < c.length}.toFinset
⊢ a ^ k * (r ^ c.length * ∏ j, p (c.blocksFun j)) = (∏ x, r) * ∏ x, a ^ c.blocksFun x * p (c.blocksFun x)
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case a.a
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
a✝¹ : k ∈ Ico 2 (n + 1)
c : Composition k
a✝ : c ∈ {c | 1 < c.length}.toFinset
⊢ a ^ k * (r ^ c.length * ∏ j, p (c.blocksFun j)) = (∏ x, r) * ∏ x, a ^ c.blocksFun x * p (c.blocksFun x)

Tactic:
prod_mul_distrib,

Goal state after:
case a.a
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
a✝¹ : k ∈ Ico 2 (n + 1)
c : Composition k
a✝ : c ∈ {c | 1 < c.length}.toFinset
⊢ a ^ k * (r ^ c.length * ∏ j, p (c.blocksFun j)) = (∏ x, r) * ((∏ x, a ^ c.blocksFun x) * ∏ x, p (c.blocksFun x))
Module: Mathlib.Analysis.Analytic.Inverse

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
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 : ℕ → ℝ := ⋯
IRec : ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a
a' : NNReal := ⋯
H : ↑a' ≤ (p.rightInv i x).radius
⊢ 0 < ↑a'

Tactic:
simpa only [ENNReal.coe_pos]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ AnalyticOn 𝕜 f s → AnalyticOnNhd 𝕜 f s

Tactic:
intro hf

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : AnalyticOn 𝕜 f s
⊢ AnalyticOnNhd 𝕜 f s
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n : ℕ
a : Composition n
b : Composition a.length
j : List ℕ
⊢ j ∈ a.blocks.splitWrtComposition b → 0 < j.sum

Tactic:
hj

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n : ℕ
a : Composition n
b : Composition a.length
j : List ℕ
hj : j ∈ a.blocks.splitWrtComposition b
⊢ 0 < j.sum
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
s : Set E
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) s x

Tactic:
exact ⟨r, hr.restrictScalars⟩

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) x

Tactic:
exact ⟨r, hr.restrictScalars⟩

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
R : Type u_4
inst✝⁴ : Monoid R
inst✝³ : DistribMulAction R F
inst✝² : SMulCommClass 𝕜 R F
inst✝¹ : ContinuousConstSMul R F
c : R
inst✝ : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬DifferentiableWithinAt 𝕜 (c • f) s x

Tactic:
contrapose h

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
f : E → F
x : E
s : Set E
R : Type u_4
inst✝⁴ : Monoid R
inst✝³ : DistribMulAction R F
inst✝² : SMulCommClass 𝕜 R F
inst✝¹ : ContinuousConstSMul R F
c : R
inst✝ : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 (c • f) s x
⊢ DifferentiableWithinAt 𝕜 f s x
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
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ ‖iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x‖ = ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖

Tactic:
iteratedFDerivWithin_succ_eq_comp_right hs hx,

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
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ ‖iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x‖ =
    ‖(⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s)
        x‖
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 : E → F
⊢ ftaylorSeriesWithin 𝕜 f univ = ftaylorSeries 𝕜 f

Tactic:
ext1 x

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 : E → F
x : E
⊢ ftaylorSeriesWithin 𝕜 f univ x = ftaylorSeries 𝕜 f x
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
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f s) p.derivSeries s x r

Tactic:
have : insert x s = s := insert_eq_of_mem hx

Goal state after:
𝕜 : 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
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : insert x s = s
⊢ HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f s) p.derivSeries s x r
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
a : 𝕜
⊢ iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s a = (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)

Tactic:
induction n generalizing a with

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

Goal state before:
pp: case inl.refine_2
𝕜 : 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
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
n : ℕ
⊢ p.derivSeries n = 0

Tactic:
apply ContinuousMultilinearMap.ext; intro a
      change (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOriginSeries 1 n a) = 0
      rw [p.changeOriginSeries_finite_of_finite h.finite 1 (Nat.zero_le _)]
      exact map_zero _

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

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
⊢ IsSeparable (range (derivWithin f univ))

Tactic:
exact isSeparable_range_derivWithin _ _

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p ↦ (p.1 - p.2) * 1
y z : 𝕜
hy : (y, z).1 ∈ {y | y ≠ 0}
hz : (y, z).2 ∈ {y | y ≠ 0}
⊢ (fun p ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) (y, z) =
    (fun p ↦ p.1⁻¹ - p.2⁻¹ - (toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)) (p.1 - p.2)) (y, z)

Tactic:
simp only [mem_ofPred_eq] at hy hz

Goal state after:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p ↦ (p.1 - p.2) * 1
y z : 𝕜
hy : y ≠ 0
hz : z ≠ 0
⊢ (fun p ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) (y, z) =
    (fun p ↦ p.1⁻¹ - p.2⁻¹ - (toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)) (p.1 - p.2)) (y, z)
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableWithinAt 𝕜' g₁ t' y
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hy : y = h x
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Tactic:
rw [hy] at hg; exact derivWithin.scomp x hg hh hs

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
y : 𝕜'
hh₂ : DifferentiableAt 𝕜' h₂ y
hh : DifferentiableAt 𝕜 h x
hy : h x = y
⊢ deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x

Tactic:
by
  subst hy; exact deriv_comp x hh₂ hh

Goal state after:
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: case inr
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
hfr : f' x < r
hrB : r < B' x
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
⊢ ({x | f x ≤ B x} ∩ Ioc x y).Nonempty

Tactic:
obtain ⟨z, hfz, hzB, hz⟩ : ∃ z, slope f x z < r ∧ r < slope B x z ∧ z ∈ Ioc x y :=
      hf'.and_eventually (HB.and (Ioc_mem_nhdsGT hy)) |>.exists

Goal state after:
case inr
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
hfr : f' x < r
hrB : r < B' x
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
⊢ ({x | f x ≤ B x} ∩ Ioc x y).Nonempty
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
x : E
hx : x ∈ ball y r
z : E
hz : z ∈ ball y r
⊢ fderivWithin 𝕜 f (ball y r) z = 0

Tactic:
simpa only [fderivWithin_of_isOpen Metric.isOpen_ball hz] using! hf' (h hz)

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
f : E → F
g : F → G
x : E
n : ℕ∞ω
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDeriv 𝕜 i (g ∘ f) x = (ftaylorSeries 𝕜 g (f x)).taylorComp (ftaylorSeries 𝕜 f x) i

Tactic:
simp only [← iteratedFDerivWithin_univ, ← ftaylorSeriesWithin_univ]

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
f : E → F
g : F → G
x : E
n : ℕ∞ω
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDerivWithin 𝕜 i (g ∘ f) univ x =
    (ftaylorSeriesWithin 𝕜 g univ (f x)).taylorComp (ftaylorSeriesWithin 𝕜 f univ x) i
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

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
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : ContDiffWithinAt 𝕜 ω f s x
⊢ ContDiffWithinAt 𝕜 ω f₁ s x

Tactic:
obtain ⟨u, hu, p, H, H'⟩ := h
    exact ⟨{x ∈ u | f₁ x = f x}, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, h₁⟩), p,
      (H.mono (sep_subset _ _)).congr fun _ ↦ And.right,
      fun i ↦ (H' i).mono (sep_subset _ _)⟩

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

Goal state before:
pp: case refine_1
𝕜 : 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 : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
h' : E →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hf_emb : Topology.IsEmbedding ⇑f'
htendsto : Tendsto (Prod.map g g) lE lF
hh : HasFDerivAtFilter h h' lE
hf : HasFDerivAtFilter f f' lF
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
ho :
  (fun x ↦
      match x with
      | (x, y) => g x - g y - g' (x - y)) =O[𝕜;
    lE] fun x ↦
    match x with
    | (x, y) => f' (g x - g y) - h' (x - y)
⊢ (fun p ↦ f p.1 - f p.2 - f' (p.1 - p.2)) ∘ Prod.map g g =ᶠ[lE] (fun p ↦ h p.1 - h p.2) - fun x ↦ f' (g x.1 - g x.2)

Tactic:
refine hcomp.mono ?_
    simp +contextual

Goal state after: