mathlib-initiative/mathlib-tactics huggingface dataset:
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 0 M N
i✝ : ℕ
him✝ : i✝ < ⟨k, blocks_fun⟩.fst
hin✝ : i✝ < (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd.length
⊢ ((p (⟨k, blocks_fun⟩.snd ⟨i✝, him✝⟩)) fun _j ↦ z) =
    p.applyComposition (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd (fun _j ↦ z) ⟨i✝, hin✝⟩

Tactic:
← compChangeOfVariables_blocksFun 0 M N H,

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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 0 M N
i✝ : ℕ
him✝ : i✝ < ⟨k, blocks_fun⟩.fst
hin✝ : i✝ < (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd.length
⊢ ((p ((compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd.blocksFun ⟨↑⟨i✝, him✝⟩, ⋯⟩)) fun _j ↦ z) =
    p.applyComposition (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd (fun _j ↦ z) ⟨i✝, hin✝⟩
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mp.refine_1.refine_2.refine_3
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
e1 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (f (x + (y - x)))
⊢ f y = (fun y ↦ p.sum (y - x)) y

pp: case mp.refine_1.refine_2.refine_1
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
⊢ x + (y - x) ∈ insert x s

pp: case mp.refine_1.refine_2.refine_2
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
⊢ y - x ∈ eball 0 r

Tactic:
· simp only [add_sub_cancel] at e1
          exact e1.unique e0

Goal state after:
case mp.refine_1.refine_2.refine_1
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
⊢ x + (y - x) ∈ insert x s

case mp.refine_1.refine_2.refine_2
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
⊢ y - x ∈ eball 0 r
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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := min r0 ↑r1
this : Metric.eball 0 r ∈ 𝓝 0
y : E
hy : y ∈ Metric.eball 0 r
hy0 : y ∈ Metric.eball 0 r0
A : HasSum (fun i ↦ (q.compAlongComposition p i.snd) fun _j ↦ y) (f (x + y))
⊢ Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n.1 n.2, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (f (x + y)))

Tactic:
apply Tendsto.comp A compPartialSumTarget_tendsto_prod_atTop

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
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f pf s x
hg : HasFPowerSeriesWithinAt g pg s x
⊢ HasFPowerSeriesWithinAt (f + g) (pf + pg) s x

Tactic:
rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩

Goal state after:
𝕜 : 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
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f pf s x
hg : HasFPowerSeriesWithinAt g pg s x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f pf s x r ∧ HasFPowerSeriesWithinOnBall g pg s x r
⊢ HasFPowerSeriesWithinAt (f + g) (pf + pg) s x
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case refine_1
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
⊢ (∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) → ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

pp: case refine_2
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
⊢ (∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x) → ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x

Tactic:
· rintro ⟨g, hf, hg⟩
    rcases mem_nhdsWithin.1 hf with ⟨u, u_open, xu, hu⟩
    let g' := Set.piecewise u g f
    refine ⟨g', ?_, ?_, ?_⟩
    · have : x ∈ u ∩ insert x s := ⟨xu, by simp⟩
      simpa [g', xu, this] using hu this
    · intro y hy
      by_cases h'y : y ∈ u
      · have : y ∈ u ∩ insert x s := ⟨h'y, hy⟩
        simpa [g', h'y, this] using hu this
      · simp [g', h'y]
    · apply hg.congr
      filter_upwards [u_open.mem_nhds xu] with y hy using by simp [g', hy]

Goal state after:
case refine_2
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
⊢ (∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x) → ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x
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
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f pf x
hg : HasFPowerSeriesAt g pg x
⊢ HasFPowerSeriesAt (f + g) (pf + pg) x

Tactic:
rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩

Goal state after:
𝕜 : 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
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f pf x
hg : HasFPowerSeriesAt g pg x
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f pf x r ∧ HasFPowerSeriesOnBall g pg x r
⊢ HasFPowerSeriesAt (f + g) (pf + pg) x
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 ≤ p.radius ∧ ↑r ≤ q.radius

Tactic:
have := (p.prod q).isLittleO_one_of_lt_radius hr

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
this : (fun n ↦ ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x ↦ 1
⊢ ↑r ≤ p.radius ∧ ↑r ≤ q.radius
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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
A : ContinuousAt (fun y ↦ f (x + y) - f x) 0
⊢ Metric.eball 0 q.radius ∈ 𝓝 (f (x + 0) - f x)

Tactic:
simpa using Metric.eball_mem_nhds _ hq

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ HasFPowerSeriesAt (fun x x_1 ↦ f x_1 x) (FormalMultilinearSeries.pi p) e ↔ ∀ (i : ι), HasFPowerSeriesAt (f i) (p i) e

Tactic:
simp_rw [← hasFPowerSeriesWithinAt_univ]

Goal state after:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ HasFPowerSeriesWithinAt (fun x x_1 ↦ f x_1 x) (FormalMultilinearSeries.pi p) Set.univ e ↔
    ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) Set.univ e
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
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H :=
  fun c ↦ (r c.snd.length) (q.applyComposition c.snd (p.applyComposition c.fst v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun c ↦ (r c.fst.length) fun i ↦ (q (c.snd i).length) (p.applyComposition (c.snd i) (v ∘ ⇑(c.fst.embedding i)))
this : ∑ c, f c = ∑ c, g c
⊢ ((r.comp q).comp p n) v = (r.comp (q.comp p) n) v

Tactic:
by
    simpa +unfoldPartialApp only [FormalMultilinearSeries.comp, sum_apply,
      compAlongComposition_apply, Finset.sum_sigma', applyComposition,
      ContinuousMultilinearMap.map_sum]

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

Goal state before:
pp: case convert_16
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : HasSummableGeomSeries A
inst✝ : Nontrivial A
⊢ HasFPowerSeriesOnBall (fun x ↦ (1 - x)⁻¹ʳ) (formalMultilinearSeries_geometric 𝕜 A) ((-ContinuousLinearMap.id 𝕜 A) 0) 1

Tactic:
simpa using (hasFPowerSeriesOnBall_inverse_one_sub 𝕜 A)

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
h : DifferentiableWithinAt 𝕜 (fun y ↦ -f y) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
by simpa only [neg_neg] using h.fun_neg

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

Tactic:
by simpa only [neg_neg] using h.fun_neg

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
s : Set E
h : DifferentiableOn 𝕜 (fun y ↦ -f y) s
⊢ DifferentiableOn 𝕜 f s

Tactic:
by simpa only [neg_neg] using h.fun_neg

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
h : Differentiable 𝕜 fun y ↦ -f y
⊢ Differentiable 𝕜 f

Tactic:
by simpa only [neg_neg] using h.fun_neg

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝¹ : NormedField A
inst✝ : CompletableTopField A
x y : Completion A
⊢ ∀ (a b : A), ‖↑a * ↑b‖ = ‖↑a‖ * ‖↑b‖

Tactic:
simp [← coe_mul]

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

Tactic:
by
  ext
  apply derivWithin_sub_const

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
p : 𝕜[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x ↦ eval x p) s x = eval x (derivative p)

Tactic:
rw [DifferentiableAt.derivWithin p.differentiableAt hxs]

Goal state after:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
p : 𝕜[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv (fun x ↦ eval x p) x = eval x (derivative p)
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : MonotoneOn g s
⊢ 0 ≤ g'

Tactic:
by
  have : (𝓝[s \ {x}] x).NeBot := accPt_principal_iff_nhdsWithin.mp hx
  have h'g : MonotoneOn g (insert x s) :=
    hg.insert_of_continuousWithinAt hx.clusterPt hd.continuousWithinAt
  have : Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g') := hasDerivWithinAt_iff_tendsto_slope.mp hd
  apply ge_of_tendsto this
  filter_upwards [self_mem_nhdsWithin] with y hy
  simp only [Set.mem_sdiff, mem_singleton_iff] at hy
  exact h'g.slope_nonneg (by simp) (by simp [hy])

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, 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 •>
        ((pi fun i ↦ f' (l.get i)) m x_1 <•
          (List.drop (↑x_1).succ (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod) =
    ∑ x_1,
      (List.take (↑x_1) (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod •>
        ((f' (l.get x_1)) m <•
          (List.drop (↑x_1).succ (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod)

Tactic:
pi_apply,

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 •>
        ((f' (l.get x_1)) m <•
          (List.drop (↑x_1).succ (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod) =
    ∑ x_1,
      (List.take (↑x_1) (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod •>
        ((f' (l.get x_1)) m <•
          (List.drop (↑x_1).succ (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod)
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 •>
        ((pi fun i ↦ f' (l.get i)) m x_1 <•
          (List.drop (↑x_1).succ (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod) =
    ∑ x_1,
      (List.take (↑x_1) (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod •>
        ((f' (l.get x_1)) m <•
          (List.drop (↑x_1).succ (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod)

Tactic:
pi_apply,

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 •>
        ((f' (l.get x_1)) m <•
          (List.drop (↑x_1).succ (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod) =
    ∑ x_1,
      (List.take (↑x_1) (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod •>
        ((f' (l.get x_1)) m <•
          (List.drop (↑x_1).succ (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod)
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 •>
        ((pi fun i ↦ f' (l.get i)) m x_1 <•
          (List.drop (↑x_1).succ (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod) =
    ∑ x_1,
      (List.take (↑x_1) (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod •>
        ((f' (l.get x_1)) m <•
          (List.drop (↑x_1).succ (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod)

Tactic:
pi_apply,

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 •>
        ((f' (l.get x_1)) m <•
          (List.drop (↑x_1).succ (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod) =
    ∑ x_1,
      (List.take (↑x_1) (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod •>
        ((f' (l.get x_1)) m <•
          (List.drop (↑x_1).succ (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod)
Module: Mathlib.Analysis.Calculus.Deriv.Comp

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

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

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
s : Set E
x : E
hh : HasDerivAt h₂ h₂' y
hf : HasFDerivWithinAt f f' s x
hy : y = f x
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Tactic:
by
  rw [hy] at hh; exact hh.comp_hasFDerivWithinAt x hf

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

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ g =ᶠ[𝓝 z₀] fun {z₀} ↦ 0

Tactic:
rw [EventuallyEq, ← AnalyticAt.frequently_eq_iff_eventually_eq hg_an analyticAt_const]

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, g z = 0
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: n : ℕ
c : OrderedFinpartition n
⊢ Injective fun p ↦ c.emb p.fst p.snd

Tactic:
rintro ⟨m, r⟩ ⟨m', r'⟩ (h : c.emb m r = c.emb m' r')

Goal state after:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : c.emb m r = c.emb m' r'
⊢ ⟨m, r⟩ = ⟨m', r'⟩