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

Goal state before:
pp: 𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
z : F
n : ℕ
⊢ ((continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm (p n)).curryRight = p n

Tactic:
exact LinearIsometryEquiv.apply_symm_apply (continuousMultilinearCurryRightEquiv' 𝕜 n E F) (p n)

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V' : Type u_3
W : Type u_4
W' : Type u_5
inst✝¹⁰ : NontriviallyNormedField 𝕜
σ σ' : 𝕜 →+* 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : NormedAddCommGroup V'
inst✝⁶ : NormedSpace 𝕜 V'
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : NormedAddCommGroup W'
inst✝² : NormedSpace 𝕜 W'
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomInvPair σ σ'
L : W →SL[σ] W'
R : V' →SL[σ'] V
f : V → W
z : V'
f' : V →L[𝕜] W
hf : HasFDerivAt f f' (R z)
this : RingHomIsometric σ'
⊢ HasFDerivAt (⇑L ∘ f ∘ ⇑R) (L ∘SL f' ∘SL R) z

Tactic:
rw [hasFDerivAt_iff_isLittleO_nhds_zero] at ⊢ hf

Goal state after:
𝕜 : Type u_1
V : Type u_2
V' : Type u_3
W : Type u_4
W' : Type u_5
inst✝¹⁰ : NontriviallyNormedField 𝕜
σ σ' : 𝕜 →+* 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : NormedAddCommGroup V'
inst✝⁶ : NormedSpace 𝕜 V'
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : NormedAddCommGroup W'
inst✝² : NormedSpace 𝕜 W'
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomInvPair σ σ'
L : W →SL[σ] W'
R : V' →SL[σ'] V
f : V → W
z : V'
f' : V →L[𝕜] W
hf : (fun h ↦ f (R z + h) - f (R z) - f' h) =o[𝓝 0] fun h ↦ h
this : RingHomIsometric σ'
⊢ (fun h ↦ (⇑L ∘ f ∘ ⇑R) (z + h) - (⇑L ∘ f ∘ ⇑R) z - (L ∘SL f' ∘SL R) h) =o[𝓝 0] fun h ↦ h
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
⊢ p.radius / ‖0‖ₑ ≤ (p.compContinuousLinearMap 0).radius

pp: case inr
𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
⊢ p.radius / ‖u‖ₑ ≤ (p.compContinuousLinearMap u).radius

Tactic:
· simp

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
⊢ p.radius / ‖u‖ₑ ≤ (p.compContinuousLinearMap u).radius
Module: Mathlib.Analysis.Analytic.ChangeOrigin

Goal state before:
pp: case refine_2
𝕜 : 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
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
x_mem_ball : x ∈ Metric.eball 0 p.radius
y_mem_ball : y ∈ Metric.eball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ Metric.eball 0 p.radius
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
hsf : Summable f
k : ℕ
this : HasSum (fun n ↦ (p.changeOriginSeries k n) fun x_1 ↦ x) (p.changeOrigin x k)
s : (b : ℕ) × { s // s.card = b }
⊢ ‖(p.changeOriginSeriesTerm k s.fst ↑s.snd ⋯) fun x_1 ↦ x‖₊ ≤ ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst

Tactic:
refine (ContinuousMultilinearMap.le_opNNNorm _ _).trans_eq ?_

Goal state after:
case refine_2
𝕜 : 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
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
x_mem_ball : x ∈ Metric.eball 0 p.radius
y_mem_ball : y ∈ Metric.eball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ Metric.eball 0 p.radius
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
hsf : Summable f
k : ℕ
this : HasSum (fun n ↦ (p.changeOriginSeries k n) fun x_1 ↦ x) (p.changeOrigin x k)
s : (b : ℕ) × { s // s.card = b }
⊢ ‖p.changeOriginSeriesTerm k s.fst ↑s.snd ⋯‖₊ * ∏ i, ‖x‖₊ = ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: case h.zero
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C
⊢ ‖p 0‖ * ↑r ^ 0 ≤ ‖p 0‖ ∨ ‖p 0‖ * ↑r ^ 0 ≤ C * ↑r

pp: case h.succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C
m : ℕ
⊢ ‖p (m + 1)‖ * ↑r ^ (m + 1) ≤ ‖p 0‖ ∨ ‖p (m + 1)‖ * ↑r ^ (m + 1) ≤ C * ↑r

Tactic:
· simp

Goal state after:
case h.succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C
m : ℕ
⊢ ‖p (m + 1)‖ * ↑r ^ (m + 1) ≤ ‖p 0‖ ∨ ‖p (m + 1)‖ * ↑r ^ (m + 1) ≤ C * ↑r
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: case inl
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G✝ : Type wG
G' : Type wG'
inst✝¹⁴ : Fintype ι
inst✝¹³ : Fintype ι'
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁹ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁸ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝⁷ : NormedAddCommGroup G✝
inst✝⁶ : NormedSpace 𝕜 G✝
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : Option ι → G × ((i : ι) → E i)
j : Option ι
x y z : G × ((i : ι) → E i)
i : ι
⊢ (update v (some i) z (some i)).2 i = update (fun i ↦ (v (some i)).2 i) i (z.2 i) i

pp: case inr
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G✝ : Type wG
G' : Type wG'
inst✝¹⁴ : Fintype ι
inst✝¹³ : Fintype ι'
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁹ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁸ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝⁷ : NormedAddCommGroup G✝
inst✝⁶ : NormedSpace 𝕜 G✝
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : Option ι → G × ((i : ι) → E i)
j✝ : Option ι
x y : G × ((i : ι) → E i)
j : ι
z : G × ((i : ι) → E i)
i : ι
hij : i ≠ j
⊢ (update v (some j) z (some i)).2 i = update (fun i ↦ (v (some i)).2 i) j (z.2 j) i

Tactic:
· simp

Goal state after:
case inr
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G✝ : Type wG
G' : Type wG'
inst✝¹⁴ : Fintype ι
inst✝¹³ : Fintype ι'
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁹ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁸ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝⁷ : NormedAddCommGroup G✝
inst✝⁶ : NormedSpace 𝕜 G✝
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : Option ι → G × ((i : ι) → E i)
j✝ : Option ι
x y : G × ((i : ι) → E i)
j : ι
z : G × ((i : ι) → E i)
i : ι
hij : i ≠ j
⊢ (update v (some j) z (some i)).2 i = update (fun i ↦ (v (some i)).2 i) j (z.2 j) i
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: case inl
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G✝ : Type wG
G' : Type wG'
inst✝¹⁴ : Fintype ι
inst✝¹³ : Fintype ι'
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁹ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁸ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝⁷ : NormedAddCommGroup G✝
inst✝⁶ : NormedSpace 𝕜 G✝
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : Option ι → G × ((i : ι) → E i)
j : Option ι
c : 𝕜
x z : G × ((i : ι) → E i)
i : ι
⊢ (update v (some i) z (some i)).2 i = update (fun i ↦ (v (some i)).2 i) i (z.2 i) i

pp: case inr
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G✝ : Type wG
G' : Type wG'
inst✝¹⁴ : Fintype ι
inst✝¹³ : Fintype ι'
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁹ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁸ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝⁷ : NormedAddCommGroup G✝
inst✝⁶ : NormedSpace 𝕜 G✝
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : Option ι → G × ((i : ι) → E i)
j✝ : Option ι
c : 𝕜
x : G × ((i : ι) → E i)
j : ι
z : G × ((i : ι) → E i)
i : ι
hij : i ≠ j
⊢ (update v (some j) z (some i)).2 i = update (fun i ↦ (v (some i)).2 i) j (z.2 j) i

Tactic:
· simp

Goal state after:
case inr
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G✝ : Type wG
G' : Type wG'
inst✝¹⁴ : Fintype ι
inst✝¹³ : Fintype ι'
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁹ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁸ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝⁷ : NormedAddCommGroup G✝
inst✝⁶ : NormedSpace 𝕜 G✝
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : Option ι → G × ((i : ι) → E i)
j✝ : Option ι
c : 𝕜
x : G × ((i : ι) → E i)
j : ι
z : G × ((i : ι) → E i)
i : ι
hij : i ≠ j
⊢ (update v (some j) z (some i)).2 i = update (fun i ↦ (v (some i)).2 i) j (z.2 j) i
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : y ∈ Metric.eball 0 r
m : ℕ
hm : n ≤ m
N : ℕ
hN : N ∉ Finset.range m
⊢ ((p N) fun x ↦ y) = 0

Tactic:
by simp only [Finset.mem_range, not_lt] at hN
                    rw [hf.finite _ (le_trans hm hN), zero_apply]

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

Goal state before:
pp: case e'_5
𝕜 : 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 : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
y : E
hy : y ∈ Metric.eball 0 r
x✝ : ℕ
⊢ ((p x✝) fun x ↦ y) = 0

Tactic:
hp,

Goal state after:
case e'_5
𝕜 : 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 : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
y : E
hy : y ∈ Metric.eball 0 r
x✝ : ℕ
⊢ (0 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
hy : x + y ∈ insert x s
h'y : y ∈ Metric.eball 0 r
⊢ HasSum (fun n ↦ (p n) fun x ↦ y) (g (x + y))

Tactic:
convert h.hasSum hy 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
hy : x + y ∈ insert x s
h'y : y ∈ Metric.eball 0 r
⊢ g (x + y) = f (x + y)
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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (insert x s ∩ Metric.eball x r)
y : E
hy : x + y ∈ insert x s
h'y : y ∈ Metric.eball 0 r
⊢ HasSum (fun n ↦ (p n) fun x ↦ y) (g (x + y))

Tactic:
convert h.hasSum hy 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (insert x s ∩ Metric.eball x r)
y : E
hy : x + y ∈ insert x s
h'y : y ∈ Metric.eball 0 r
⊢ g (x + y) = f (x + y)
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
⊢ ∀ᶠ (y : E) in 𝓝 x, HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (f y)

Tactic:
by
  filter_upwards [Metric.eball_mem_nhds x hf.r_pos] with y using hf.hasSum_sub

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

Goal state before:
pp: case inl
𝕜 : 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')
h'y : 0 ∈ Metric.eball 0 (min r r')
⊢ x + 0 ∈ insert x s

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 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 ∈ insert x s

Tactic:
· simp

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 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 ∈ insert x s
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: case hd
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 0 < ‖c n‖

Tactic:
· refine Ne.lt_of_le (fun hr' ↦ Not.elim ?_ hc) (norm_nonneg _)
      rw [← hr']
      simp [this]

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
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‖ * ↑r' ^ n * (‖y‖ / ↑r') ^ n ≤ C * a ^ n * (‖y‖ / ↑r') ^ n

Tactic:
by gcongr ?_ * _; apply hp

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
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f p s x
n : ℕ
⊢ (fun y ↦ f (x + y) - p.partialSum n y) =O[𝓝[(fun x_1 ↦ x + x_1) ⁻¹' insert x s] 0] fun y ↦ ‖y‖ ^ n

Tactic:
rcases hf with ⟨r, 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
s : Set E
x : E
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ (fun y ↦ f (x + y) - p.partialSum n y) =O[𝓝[(fun x_1 ↦ x + x_1) ⁻¹' insert x s] 0] fun y ↦ ‖y‖ ^ n
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case h₁
𝕜 : 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
x : E
n : ℕ
⊢ Composition.ones n ∉ Finset.univ → p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = 0

Tactic:
· simp

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

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
x : E
⊢ p.comp (id 𝕜 E x) = p

Tactic:
ext1 n
  dsimp [FormalMultilinearSeries.comp]
  rw [Finset.sum_eq_single (Composition.ones n)]
  · show compAlongComposition p (id 𝕜 E x) (Composition.ones n) = p n
    ext v
    rw [compAlongComposition_apply]
    apply p.congr (Composition.ones_length n)
    intros
    rw [applyComposition_ones]
    refine congr_arg v ?_
    rw [Fin.ext_iff, Fin.val_castLE, Fin.val_mk]
  · change
    ∀ b : Composition n,
      b ∈ Finset.univ → b ≠ Composition.ones n → compAlongComposition p (id 𝕜 E x) b = 0
    intro b _ hb
    obtain ⟨k, hk, lt_k⟩ : ∃ (k : ℕ), k ∈ Composition.blocks b ∧ 1 < k :=
      Composition.ne_ones_iff.1 hb
    obtain ⟨i, hi⟩ : ∃ (i : Fin b.blocks.length), b.blocks[i] = k :=
      List.get_of_mem hk
    let j : Fin b.length := ⟨i.val, b.blocks_length ▸ i.prop⟩
    have A : 1 < b.blocksFun j := by convert! lt_k
    ext v
    rw [compAlongComposition_apply, _root_.zero_apply]
    apply ContinuousMultilinearMap.map_coord_zero _ j
    dsimp [applyComposition]
    rw [id_apply_of_one_lt _ _ _ A, _root_.zero_apply]
  · simp

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
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))
y : E × E
hy' : y ∈ Metric.eball (x, x) ↑r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F := fun n ↦ ((p n) fun x_1 ↦ y.1 - x) - (p n) fun x_1 ↦ y.2 - x
⊢ ((p 1) fun x ↦ y.1 - y.2) = (p 1) (Pi.single 0 (y.1 - x - (y.2 - x)))

Tactic:
Subsingleton.pi_single_eq,

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∞
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))
y : E × E
hy' : y ∈ Metric.eball (x, x) ↑r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F := fun n ↦ ((p n) fun x_1 ↦ y.1 - x) - (p n) fun x_1 ↦ y.2 - x
⊢ ((p 1) fun x ↦ y.1 - y.2) = (p 1) fun x_1 ↦ y.1 - x - (y.2 - x)
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case inr.h₁
𝕜 : 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
⊢ Composition.single n n_pos ∉ Finset.univ → (id 𝕜 F ((p 0) v0)).compAlongComposition p (Composition.single n n_pos) = 0

Tactic:
· simp

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 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:
by
  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
  simpa using hf.isBigO_image_sub_image_sub_deriv_principal hr

Goal state after: