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

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 : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : Metric.eball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (min r r')
y : E
h'y : y ∈ Metric.eball 0 (min r r')
hy : x + y ∈ t
⊢ x + y ∈ Metric.eball x r' ∩ t

Tactic:
simp only [Metric.mem_eball, edist_eq_enorm_sub, sub_zero, lt_min_iff, mem_inter_iff,
    add_sub_cancel_left, hy, and_true] at h'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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : Metric.eball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (min r r')
y : E
hy : x + y ∈ t
h'y : ‖y‖ₑ < r ∧ ‖y‖ₑ < r'
⊢ ‖y‖ₑ < r'
Module: Mathlib.Analysis.Analytic.Basic

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 : E → F
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
v : Fin 0 → E
v_eq : v = fun i ↦ 0
zero_mem : 0 ∈ Metric.eball 0 r
this : ∀ (i : ℕ), i ≠ 0 → ((pf i) fun x ↦ 0) = 0
A : f (x + 0) = (pf 0) fun x ↦ 0
⊢ (pf 0) v = f x

Tactic:
simpa [v_eq] using A.symm

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

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 : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
v : Fin 0 → E
⊢ (pf 0) v = f x

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf univ x r
v : Fin 0 → E
⊢ (pf 0) v = f x
Module: Mathlib.Analysis.Analytic.Basic

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 : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n
y : E
hy : y ∈ Metric.ball 0 ↑r'
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < ↑r'
hr'0 : 0 < ↑r'
this : y ∈ Metric.eball 0 r
ya : a * (‖y‖ / ↑r') ≤ a
⊢ ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n / (1 - a * (‖y‖ / ↑r'))

Tactic:
apply norm_sub_le_of_geometric_bound_of_hasSum (ya.trans_lt ha.2) _ (hf.hasSum ys this)

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n
y : E
hy : y ∈ Metric.ball 0 ↑r'
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < ↑r'
hr'0 : 0 < ↑r'
this : y ∈ Metric.eball 0 r
ya : a * (‖y‖ / ↑r') ≤ a
⊢ ∀ (n : ℕ), ‖(p n) fun x ↦ y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
Module: Mathlib.Analysis.Analytic.Basic

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 : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesOnBall f p x r
h : ↑r' < r
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑r' < r
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
Module: Mathlib.Analysis.Analytic.Basic

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 : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesOnBall f p x r
h : ↑r' < r
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑r' < r
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
Module: Mathlib.Analysis.Analytic.CPolynomial

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em F
y : (i : ι) → Em i
x✝ : y ∈ Metric.eball 0 ∞
m : ℕ
a✝ : m ∈ Finset.range (Fintype.card ι + 1)
⊢ m ≠ Fintype.card ι → ((f.toFormalMultilinearSeries m) fun x ↦ y) = 0

Tactic:
ne

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em F
y : (i : ι) → Em i
x✝ : y ∈ Metric.eball 0 ∞
m : ℕ
a✝ : m ∈ Finset.range (Fintype.card ι + 1)
ne : m ≠ Fintype.card ι
⊢ ((f.toFormalMultilinearSeries m) fun x ↦ y) = 0
Module: Mathlib.Analysis.Analytic.CPolynomial

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
y : G × ((i : ι) → Em i)
a✝¹ : y ∈ Metric.eball 0 ∞
m : ℕ
a✝ : m ∈ Finset.range (Fintype.card (Option ι) + 1)
⊢ m ≠ Fintype.card (Option ι) → ((f.toFormalMultilinearSeriesOfMultilinear m) fun x ↦ y) = 0

Tactic:
ne

Goal state after:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
y : G × ((i : ι) → Em i)
a✝¹ : y ∈ Metric.eball 0 ∞
m : ℕ
a✝ : m ∈ Finset.range (Fintype.card (Option ι) + 1)
ne : m ≠ Fintype.card (Option ι)
⊢ ((f.toFormalMultilinearSeriesOfMultilinear m) fun x ↦ y) = 0
Module: Mathlib.Analysis.Analytic.Basic

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 : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hr : r' < r
⊢ (fun y ↦ f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2) =O[𝓟 (Metric.eball (x, x) r')] fun y ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
hr : r' < r
⊢ (fun y ↦ f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2) =O[𝓟 (Metric.eball (x, x) r')] fun y ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖
Module: Mathlib.Analysis.Analytic.Basic

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 : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hr : r' < r
⊢ ∃ C,
    ∀ y ∈ Metric.eball x r',
      ∀ z ∈ Metric.eball x r', ‖f y - f z - (p 1) fun x ↦ y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
hr : r' < r
⊢ ∃ C,
    ∀ y ∈ Metric.eball x r',
      ∀ z ∈ Metric.eball x r', ‖f y - f z - (p 1) fun x ↦ y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖
Module: Mathlib.Analysis.Analytic.Basic

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 : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f p x
⊢ (fun y ↦ f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2) =O[𝓝 (x, x)] fun y ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
rw [← hasFPowerSeriesWithinAt_univ] at hf
  simpa using hf.isBigO_image_sub_norm_mul_norm_sub

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

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 : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesOnBall f p x r
h : ↑r' < r
⊢ TendstoUniformlyOn (fun n y ↦ p.partialSum n y) (fun y ↦ f (x + y)) atTop (Metric.ball 0 ↑r')

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑r' < r
⊢ TendstoUniformlyOn (fun n y ↦ p.partialSum n y) (fun y ↦ f (x + y)) atTop (Metric.ball 0 ↑r')
Module: Mathlib.Analysis.Analytic.Basic

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 : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ TendstoLocallyUniformlyOn (fun n y ↦ p.partialSum n y) (fun y ↦ f (x + y)) atTop (Metric.eball 0 r)

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ TendstoLocallyUniformlyOn (fun n y ↦ p.partialSum n y) (fun y ↦ f (x + y)) atTop (Metric.eball 0 r)
Module: Mathlib.Analysis.Analytic.Basic

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 : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesOnBall f p x r
h : ↑r' < r
⊢ TendstoUniformlyOn (fun n y ↦ p.partialSum n (y - x)) f atTop (Metric.ball x ↑r')

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑r' < r
⊢ TendstoUniformlyOn (fun n y ↦ p.partialSum n (y - x)) f atTop (Metric.ball x ↑r')
Module: Mathlib.Analysis.Analytic.Basic

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 : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ TendstoLocallyUniformlyOn (fun n y ↦ p.partialSum n (y - x)) f atTop (Metric.eball x r)

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ TendstoLocallyUniformlyOn (fun n y ↦ p.partialSum n (y - x)) f atTop (Metric.eball x r)
Module: Mathlib.Analysis.Analytic.Basic

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 : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ ContinuousOn f (Metric.eball x r)

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ ContinuousOn f (Metric.eball x r)
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case snd
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (fun i ↦ (b i).blocks) = fun i ↦ (b' i).blocks
⊢ b = b'

Tactic:
ext1 i

Goal state after:
case snd
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (fun i ↦ (b i).blocks) = fun i ↦ (b' i).blocks
i : Fin a.length
⊢ b i = b' i
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
s : Set E
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
hr : 0 < r
⊢ r ≤ (FormalMultilinearSeries.pi p).radius

Tactic:
apply FormalMultilinearSeries.le_radius_pi (fun i ↦ ?_)

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
s : Set E
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
hr : 0 < r
i : ι
⊢ r ≤ (p i).radius
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 : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ⇑iso) (f' ∘SL ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm
⊢ f' = (f' ∘SL ↑iso) ∘SL ↑iso.symm

Tactic:
rw [ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm, ContinuousLinearMap.comp_id]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ IsClosed {x | dist x.1 x.2.2 ≤ dist x.1 x.2.1 + dist x.2.1 x.2.2}

Tactic:
refine isClosed_le ?_ (Continuous.add ?_ ?_)

Goal state after:
case refine_1.refine_1
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x ↦ dist x.1 x.2.2

case refine_1.refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x ↦ dist x.1 x.2.1

case refine_1.refine_3
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x ↦ dist x.2.1 x.2.2
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ ‖id (x, x) - (x, x)‖ = 0

Tactic:
rw [_root_.id, sub_self, norm_zero]

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

Goal state before:
pp: case e'_9
𝕜 : 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
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
IH : AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s
⊢ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm = ⇑?g✝

pp: case g
𝕜 : 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
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
IH : AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s
⊢ (E →L[𝕜] E [×n]→L[𝕜] F) →L[𝕜] E [×n + 1]→L[𝕜] F

Tactic:
case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm

Goal state after:
case e'_9
𝕜 : 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
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
IH : AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s
⊢ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm =
    ⇑↑↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm
Module: Mathlib.Analysis.Calculus.Deriv.Mul

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

Tactic:
by_cases hu : DifferentiableAt 𝕜 u x

Goal state after:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
hu : DifferentiableAt 𝕜 u x
⊢ deriv (fun y ↦ u y * v) x = deriv u x * v

case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
hu : ¬DifferentiableAt 𝕜 u x
⊢ deriv (fun y ↦ u y * v) x = deriv u x * v
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x
⊢ HasDerivAt (∏ i ∈ u, f i) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x

Tactic:
convert! HasDerivAt.fun_finsetProd hf

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x
x✝ : 𝕜
⊢ (∏ i ∈ u, f i) x✝ = ∏ i ∈ u, f i x✝
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case e'_9
𝕜 : 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
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm = ⇑?g✝

pp: case g
𝕜 : 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
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ (E →L[𝕜] E [×n]→L[𝕜] F) →L[𝕜] E [×n + 1]→L[𝕜] F

Tactic:
case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm

Goal state after:
case e'_9
𝕜 : 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
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm =
    ⇑↑↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case inr
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 r : k
hab : a ≠ b
⊢ (lineMap (slope f ((lineMap a b) r) b) (slope f a ((lineMap a b) r))) r = slope f a b

Tactic:
rw [slope_comm _ a, slope_comm _ a, slope_comm _ _ b]

Goal state after:
case inr
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 r : k
hab : a ≠ b
⊢ (lineMap (slope f b ((lineMap a b) r)) (slope f ((lineMap a b) r) a)) r = slope f b a
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : DecidableEq 𝕜
f : 𝕜 → 𝕜
c a : 𝕜
hf : HasDerivAt f a c
⊢ ContinuousAt (Function.update (fun x ↦ (f x - f c) / (x - c)) c a) c

Tactic:
rw [← slope_fun_def_field]
  exact continuousAt_update_same.mpr <| hasDerivAt_iff_tendsto_slope.mp hf

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
hf : f a = 0
b : 𝕜
⊢ (b - a) • dslope f a b = f b

Tactic:
simp [hf]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a : ℕ → E
⊢ HasSum (fun n ↦ 0 ^ n • a n) (a 0)

Tactic:
convert! hasSum_single (α := E) 0 fun b h ↦ _ <;> simp [*]

Goal state after: