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

Goal state before:
pp: case neg.refine_1.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ Tendsto (fun n ↦ ‖‖‖c (n + 1)‖ * ↑r' ^ (n + 1)‖‖ / ‖‖‖c n‖ * ↑r' ^ n‖‖) atTop (𝓝 ↑(r' * r))

Tactic:
simp_rw [norm_norm]

Goal state after:
case neg.refine_1.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ Tendsto (fun n ↦ ‖‖c (n + 1)‖ * ↑r' ^ (n + 1)‖ / ‖‖c n‖ * ↑r' ^ n‖) atTop (𝓝 ↑(r' * r))
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : 0 < n
v : Fin n → E
i : ℕ
hi2 : i < n
j_val : ℕ
j_property : j_val < (Composition.single n hn).length
hi1 : i < (Composition.single n hn).blocksFun ⟨j_val, j_property⟩
⊢ ((Composition.single n hn).embedding ⟨j_val, j_property⟩) ⟨i, hi1⟩ = ((Composition.single n hn).embedding 0) ⟨i, hi2⟩

Tactic:
have : j_val = 0 := le_bot_iff.1 (Nat.lt_succ_iff.1 j_property)

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : 0 < n
v : Fin n → E
i : ℕ
hi2 : i < n
j_val : ℕ
j_property : j_val < (Composition.single n hn).length
hi1 : i < (Composition.single n hn).blocksFun ⟨j_val, j_property⟩
this : j_val = 0
⊢ ((Composition.single n hn).embedding ⟨j_val, j_property⟩) ⟨i, hi1⟩ = ((Composition.single n hn).embedding 0) ⟨i, hi2⟩
Module: Mathlib.Analysis.Analytic.CPolynomial

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
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n m : ℕ
hf : HasFiniteFPowerSeriesOnBall f pf x n r
hg : HasFiniteFPowerSeriesOnBall g pg x m r
⊢ HasFiniteFPowerSeriesOnBall (f - g) (pf - pg) x (max n m) r

Tactic:
by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

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

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
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
n m : ℕ
hf : HasFiniteFPowerSeriesAt f pf x n
hg : HasFiniteFPowerSeriesAt g pg x m
⊢ HasFiniteFPowerSeriesAt (f - g) (pf - pg) x (max n m)

Tactic:
by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

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

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
f g : E → F
x : E
hf : CPolynomialAt 𝕜 f x
hg : CPolynomialAt 𝕜 g x
⊢ CPolynomialAt 𝕜 (f - g) x

Tactic:
by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Goal state after:
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
hq : 0 < q.radius
hp : 0 < p.radius
⊢ ∃ r > 0, Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 (lt_min zero_lt_one hq) with ⟨rq, rq_pos, hrq⟩

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
hq : 0 < q.radius
hp : 0 < p.radius
rq : ℝ≥0
rq_pos : 0 < ↑rq
hrq : ↑rq < min 1 q.radius
⊢ ∃ r > 0, Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: case inr
𝕜 : 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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
hL : ∀ y ∈ Metric.eball (x, x) ↑r' ∩ insert x s ×ˢ insert x s, ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L y
⊢ (fun y ↦
      C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) *
        (a / (1 - a) ^ 2 + 2 / (1 - a))) =O[𝓟 (Metric.eball (x, x) ↑r' ∩ insert x s ×ˢ insert x s)]
    fun y ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
mul_right_comm _ (_ * _)

Goal state after:
case inr
𝕜 : 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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
hL : ∀ y ∈ Metric.eball (x, x) ↑r' ∩ insert x s ×ˢ insert x s, ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L y
⊢ (fun y ↦
      C * (a / ↑r') ^ 2 * (a / (1 - a) ^ 2 + 2 / (1 - a)) *
        (‖y - (x, x)‖ * ‖y.1 - y.2‖)) =O[𝓟 (Metric.eball (x, x) ↑r' ∩ insert x s ×ˢ insert x s)]
    fun y ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: m M N : ℕ
a : (n : ℕ) × Composition n
⊢ a ∈ compPartialSumTarget m M N ↔ m ≤ a.snd.length ∧ a.snd.length < M ∧ ∀ (j : Fin a.snd.length), a.snd.blocksFun j < N

Tactic:
by
  simp [compPartialSumTarget, compPartialSumTargetSet]

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

Goal state before:
pp: case refine_1.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 : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x ↦ f x = g x) x}
g' : E → F := u.piecewise g f
⊢ f x = g' x

Tactic:
have : x ∈ u ∩ insert x s := ⟨xu, by simp⟩

Goal state after:
case refine_1.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 : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x ↦ f x = g x) x}
g' : E → F := u.piecewise g f
this : x ∈ u ∩ insert x s
⊢ f x = g' x
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b : Composition a.length
a' : Composition n
b' : Composition a'.length
h : ⟨a, b⟩.fst.blocks = ⟨a', b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a', b'⟩.snd.blocks
⊢ a.blocks = a'.blocks

Tactic:
exact h

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
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
hg : HasFPowerSeriesWithinOnBall g pg s x r
⊢ HasFPowerSeriesWithinOnBall (f - g) (pf - pg) s x r

Tactic:
by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

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
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
hg : HasFPowerSeriesOnBall g pg x r
⊢ HasFPowerSeriesOnBall (f - g) (pf - pg) x r

Tactic:
by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

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:
by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

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
x : E
hf : HasFPowerSeriesAt f pf x
hg : HasFPowerSeriesAt g pg x
⊢ HasFPowerSeriesAt (f - g) (pf - pg) x

Tactic:
by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

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
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
hg : AnalyticWithinAt 𝕜 g s x
⊢ AnalyticWithinAt 𝕜 (f - g) s x

Tactic:
by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

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
x : E
hf : AnalyticAt 𝕜 f x
hg : AnalyticAt 𝕜 g x
⊢ AnalyticAt 𝕜 (f - g) x

Tactic:
by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Goal state after:
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
i✝ : Fin (a.gather b).length
i : ℕ
hi : i ∈ (a.blocks.splitWrtComposition b)[↑i✝]
⊢ i ∈ a.blocks

Tactic:
rw [← a.blocks.flatten_splitWrtComposition b]
        exact mem_flatten_of_mem (List.getElem_mem _) hi

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

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
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : E → F
x : E
s : Set E
g' : G → G'
g : F → G
t : Set F
u : Set G
y : F
y' : G
hg' : DifferentiableWithinAt 𝕜 g' u y'
hg : DifferentiableWithinAt 𝕜 g t y
hf : DifferentiableWithinAt 𝕜 f s x
h2g : MapsTo g t u
h2f : MapsTo f s t
h3g : g y = y'
h3f : f x = y
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (g' ∘ g ∘ f) s x = fderivWithin 𝕜 g' u y' ∘SL fderivWithin 𝕜 g t y ∘SL fderivWithin 𝕜 f s x

Tactic:
subst h3g h3f
  exact (hg'.hasFDerivWithinAt.comp x (hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h2f) <|
    h2g.comp h2f).fderivWithin hxs

Goal state after:
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
this✝ : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ Metric.eball 0 q.radius
y : E
hy : Tendsto (fun a ↦ q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x ↦ 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ Metric.eball 0 q.radius
u : Set G
hu : u ∈ 𝓝 (g (f (x + y)))
u_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
v : Set G
vu : v ⊆ u
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
hv : g (f (x + y)) ∈ v
a₀ b₀ : ℕ
hab : ∀ (a b : ℕ), a₀ ≤ a → b₀ ≤ b → q.partialSum a (p.partialSum b y - (p 0) fun x ↦ 0) ∈ v
a : ℕ
ha : a₀ ≤ a
this : ContinuousAt (q.partialSum a) (f (x + y) - f x)
⊢ Tendsto (fun x ↦ (p 0) fun x ↦ 0) atTop (𝓝 (f x))

Tactic:
convert! tendsto_const_nhds

Goal state after:
case e'_5.e'_3
𝕜 : 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
this✝ : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ Metric.eball 0 q.radius
y : E
hy : Tendsto (fun a ↦ q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x ↦ 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ Metric.eball 0 q.radius
u : Set G
hu : u ∈ 𝓝 (g (f (x + y)))
u_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
v : Set G
vu : v ⊆ u
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
hv : g (f (x + y)) ∈ v
a₀ b₀ : ℕ
hab : ∀ (a b : ℕ), a₀ ≤ a → b₀ ≤ b → q.partialSum a (p.partialSum b y - (p 0) fun x ↦ 0) ∈ v
a : ℕ
ha : a₀ ≤ a
this : ContinuousAt (q.partialSum a) (f (x + y) - f x)
⊢ f x = (p 0) fun x ↦ 0
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_7
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
hf : AnalyticAt 𝕜 f z
n : ℕ
⊢ AnalyticAt 𝕜 (f ^ n) z

Tactic:
rw [← analyticWithinAt_univ] at hf ⊢

Goal state after:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_7
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
hf : AnalyticWithinAt 𝕜 f Set.univ z
n : ℕ
⊢ AnalyticWithinAt 𝕜 (f ^ n) Set.univ z
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

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
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
⊢ DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
refine ⟨fun H => ?_, fun H => iso.differentiable.differentiableAt.comp_differentiableWithinAt x H⟩
  have : DifferentiableWithinAt 𝕜 (iso.symm ∘ iso ∘ f) s x :=
    iso.symm.differentiable.differentiableAt.comp_differentiableWithinAt x H
  rwa [← Function.comp_assoc iso.symm iso f, iso.symm_comp_self] at this

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

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
iso : E ≃L[𝕜] F
f : G → E
x : G
f' : G →L[𝕜] E
H : HasStrictFDerivAt (⇑iso ∘ f) (↑iso ∘SL f') x
⊢ HasStrictFDerivAt f f' x

Tactic:
convert! iso.symm.hasStrictFDerivAt.comp x H using 1 <;>
    ext z <;> apply (iso.symm_apply_apply _).symm

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

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
iso : E ≃L[𝕜] F
f : G → E
x : G
f' : G →L[𝕜] E
⊢ HasFDerivWithinAt (⇑iso ∘ f) (↑iso ∘SL f') univ x ↔ HasFDerivWithinAt f f' univ x

Tactic:
iso.comp_hasFDerivWithinAt_iff

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 g : E → F
f' g' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hg : HasFDerivAtFilter g g' L
⊢ HasFDerivAtFilter (f - g) (f' - g') L

Tactic:
by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

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

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
f' : E →L[𝕜] F
x : E
c : 𝕜
⊢ HasFDerivWithinAt (fun x ↦ f (c • x)) (c • f') s x ↔ HasFDerivWithinAt f f' (c • s) (c • x)

Tactic:
rcases eq_or_ne c 0 with rfl | hc
  · simp [hasFDerivWithinAt_const, HasFDerivWithinAt.of_subsingleton (subsingleton_zero_smul_set _)]
  · lift c to 𝕜ˣ using IsUnit.mk0 c hc
    have A : f'.comp ((ContinuousLinearEquiv.smulLeft c : E ≃L[𝕜] E) : E →L[𝕜] E) = c • f' := by
      ext; simp
    rw [← Units.smul_def c x, ← ContinuousLinearEquiv.smulLeft_apply_apply (R₁ := 𝕜),
      ← ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff, A]
    simp [Function.comp_def, ← Units.smul_def, ← preimage_smul_inv, preimage_preimage]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ DifferentiableAt 𝕜 (fun x ↦ Fin.cons (φ x) (φs x)) x ↔ DifferentiableAt 𝕜 φ x ∧ DifferentiableAt 𝕜 φs x

Tactic:
rw [differentiableAt_pi, Fin.forall_fin_succ, differentiableAt_pi]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ (DifferentiableAt 𝕜 (fun x ↦ Fin.cons (φ x) (φs x) 0) x ∧
      ∀ (i : Fin n), DifferentiableAt 𝕜 (fun x ↦ Fin.cons (φ x) (φs x) i.succ) x) ↔
    DifferentiableAt 𝕜 φ x ∧ ∀ (i : Fin n), DifferentiableAt 𝕜 (fun x ↦ φs x i) 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
x : E
f : E → F
h : UniqueDiffWithinAt 𝕜 s x
⊢ ‖iteratedFDerivWithin 𝕜 1 f s x‖ = ‖fderivWithin 𝕜 f s x‖

Tactic:
simp only [← norm_fderivWithin_iteratedFDerivWithin,
    iteratedFDerivWithin_zero_eq_comp, LinearIsometryEquiv.comp_fderivWithin _ h]

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
x : E
f : E → F
h : UniqueDiffWithinAt 𝕜 s x
⊢ ‖↑↑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘SL fderivWithin 𝕜 f s x‖ = ‖fderivWithin 𝕜 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
f : E → F
z : E
m : Fin 2 → E
⊢ (iteratedFDeriv 𝕜 2 f z) m = ((fderiv 𝕜 (fderiv 𝕜 f) z) (m 0)) (m 1)

Tactic:
by
  simp [iteratedFDeriv_succ_apply_right, init]

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
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := UniformSpace.Completion.toComplₗᵢ.postcomp
this : HasFPowerSeriesWithinOnBall (⇑a ∘ f) (a.compFormalMultilinearSeries p) s x r
Z :
  HasSum (fun n ↦ ((a.compFormalMultilinearSeries p).derivSeries n) fun x ↦ y)
    (fderivWithin 𝕜 (⇑a ∘ f) (insert x s) (x + y))
⊢ HasSum (⇑b ∘ fun n ↦ (p.derivSeries n) fun x ↦ y) (b f')

Tactic:
have : fderivWithin 𝕜 (a ∘ f) (insert x s) (x + y) = a ∘L f' := by
    apply HasFDerivWithinAt.fderivWithin _ (hu _ h'y)
    exact a.hasFDerivAt.comp_hasFDerivWithinAt (x + y) hf'

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
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := UniformSpace.Completion.toComplₗᵢ.postcomp
this✝ : HasFPowerSeriesWithinOnBall (⇑a ∘ f) (a.compFormalMultilinearSeries p) s x r
Z :
  HasSum (fun n ↦ ((a.compFormalMultilinearSeries p).derivSeries n) fun x ↦ y)
    (fderivWithin 𝕜 (⇑a ∘ f) (insert x s) (x + y))
this : fderivWithin 𝕜 (⇑a ∘ f) (insert x s) (x + y) = a ∘SL f'
⊢ HasSum (⇑b ∘ fun n ↦ (p.derivSeries n) fun x ↦ y) (b f')
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd 𝕜 (deriv^[0] f) s

Tactic:
exact h

Goal state after: