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
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.splitWrtComposition b).flatten

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n : ℕ
a : Composition n
b : Composition a.length
i✝ : Fin (a.gather b).length
i : ℕ
hi : i ∈ (a.blocks.splitWrtComposition b)[↑i✝]
⊢ i ∈ (a.blocks.splitWrtComposition b).flatten
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
⊢ b.blocks[↑i] = b.blocks[↑i]

Tactic:
]

Goal state after:
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:
]

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
⊢ ↑r ≤ p.radius ∧ ↑r ≤ q.radius
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
j : Fin (b.blocksFun i)
⊢ a.blocks[b.sizeUpTo ↑⟨↑i, ⋯⟩ + ↑⟨↑j, ⋯⟩] = a.blocksFun ((b.embedding i) j)

Tactic:
]

Goal state after:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
j : Fin (b.blocksFun i)
⊢ a.blocks[b.sizeUpTo ↑⟨↑i, ⋯⟩ + ↑⟨↑j, ⋯⟩] = a.blocksFun ((b.embedding i) j)
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
j : Fin (b.blocksFun i)
⊢ (a.sigmaCompositionAux b ⟨↑i, ⋯⟩).blocksFun ⟨↑j, ⋯⟩ = a.blocksFun ((b.embedding i) j)

Tactic:
unfold sigmaCompositionAux
  rw [blocksFun, get_eq_getElem, getElem_of_eq (getElem_splitWrtComposition _ _ _ _),
    getElem_drop, getElem_take]; rfl

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : TopologicalSpace E
F : Type u_3
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
f : E →L[𝕜] F
x : E
s : Set E
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : T2Space F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 (⇑f) x = f

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : TopologicalSpace E
F : Type u_3
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
f : E →L[𝕜] F
x : E
s : Set E
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : T2Space F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 (⇑f) x = f
Module: Mathlib.Analysis.Calculus.FDeriv.Linear

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 : IsBoundedLinearMap 𝕜 f
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 f x = toContinuousLinearMap f h

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : IsBoundedLinearMap 𝕜 f
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 f x = toContinuousLinearMap f h
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case a.left
𝕜 : 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
n : ℕ
⊢ ‖p n‖ * ‖↑r ^ n‖ ≤ ‖p.prod q n‖ * ‖↑r ^ n‖

Tactic:
]

Goal state after:
case a.left
𝕜 : 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
n : ℕ
⊢ ‖p n‖ * ‖↑r ^ n‖ ≤ ‖p.prod q n‖ * ‖↑r ^ n‖
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case zero.succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
⊢ (take (take (i + 1) b.blocks).sum a.blocks).sum =
    (take (take i b.blocks).sum a.blocks).sum + (List.map sum (a.blocks.splitWrtComposition b))[i]

Tactic:
]

Goal state after:
case zero.succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
⊢ (take (take (i + 1) b.blocks).sum a.blocks).sum =
    (take (take i b.blocks).sum a.blocks).sum + (List.map sum (a.blocks.splitWrtComposition b))[i]
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case e_x
𝕜 : 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))
B :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n.1 n.2, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (f (x + y)))
C : Tendsto (fun n ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a) fun _b ↦ y)) atTop (𝓝 (f (x + y)))
fst✝ n : ℕ
hn : 1 ≤ n
⊢ (((p 0) fun x ↦ 0) + ∑ a ∈ Ico 1 (fst✝, n).2, (p a) fun _b ↦ y) =
    ((p 0) fun x ↦ y) + ∑ k ∈ Ico (0 + 1) n, (p k) fun x ↦ y

Tactic:
]

Goal state after:
case e_x
𝕜 : 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))
B :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n.1 n.2, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (f (x + y)))
C : Tendsto (fun n ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a) fun _b ↦ y)) atTop (𝓝 (f (x + y)))
fst✝ n : ℕ
hn : 1 ≤ n
⊢ (((p 0) fun x ↦ 0) + ∑ a ∈ Ico 1 (fst✝, n).2, (p a) fun _b ↦ y) =
    ((p 0) fun x ↦ y) + ∑ k ∈ Ico (0 + 1) n, (p k) fun x ↦ y
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case a.left
𝕜 : 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
n : ℕ
⊢ ‖p n‖ ≤ max ‖p n‖ ‖q n‖

Tactic:
]

Goal state after:
case a.left
𝕜 : 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
n : ℕ
⊢ ‖p n‖ ≤ max ‖p n‖ ‖q n‖
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 : F → G
f : E → F
x : E
s : Set E
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
v : E
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ (fderivWithin 𝕜 g t (f x)) ((fderivWithin 𝕜 f s x) v) = (fderivWithin 𝕜 g t (f x)) ((fderivWithin 𝕜 f s x) v)

Tactic:
]

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

Goal state before:
pp: n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
⊢ take (take i b.blocks).sum a.blocks = take (take i b.blocks).sum a.blocks

pp: n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
⊢ (take i b.blocks).sum ≤ (take (i + 1) b.blocks).sum

Tactic:
]

Goal state after:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
⊢ (take i b.blocks).sum ≤ (take (i + 1) b.blocks).sum
Module: Mathlib.Analysis.Calculus.FDeriv.Comp

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') L

Tactic:
]

Goal state after:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') L
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case a.right
𝕜 : 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
n : ℕ
⊢ ‖q n‖ * ‖↑r ^ n‖ ≤ ‖p.prod q n‖ * ‖↑r ^ n‖

Tactic:
]

Goal state after:
case a.right
𝕜 : 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
n : ℕ
⊢ ‖q n‖ * ‖↑r ^ n‖ ≤ ‖p.prod q n‖ * ‖↑r ^ n‖
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case a.right
𝕜 : 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
n : ℕ
⊢ ‖q n‖ ≤ max ‖p n‖ ‖q n‖

Tactic:
]

Goal state after:
case a.right
𝕜 : 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
n : ℕ
⊢ ‖q n‖ ≤ max ‖p n‖ ‖q n‖
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case zero.succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
this : take (take i b.blocks).sum a.blocks = take (take i b.blocks).sum (take (take (i + 1) b.blocks).sum a.blocks)
⊢ (take (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks)).sum +
      (drop (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks)).sum =
    (take (take i b.blocks).sum
          (take (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks) ++
            drop (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks))).sum +
      (drop (b.sizeUpTo i) (take (b.sizeUpTo (i + 1)) a.blocks)).sum

Tactic:
]

Goal state after:
case zero.succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
this : take (take i b.blocks).sum a.blocks = take (take i b.blocks).sum (take (take (i + 1) b.blocks).sum a.blocks)
⊢ (take (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks)).sum +
      (drop (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks)).sum =
    (take (take i b.blocks).sum
          (take (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks) ++
            drop (take i b.blocks).sum (take (take i.succ b.blocks).sum a.blocks))).sum +
      (drop (b.sizeUpTo i) (take (b.sizeUpTo (i + 1)) a.blocks)).sum
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case zero.succ.e_a.e_xs
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
this : take (take i b.blocks).sum a.blocks = take (take i b.blocks).sum (take (take (i + 1) b.blocks).sum a.blocks)
⊢ take (take i.succ b.blocks).sum a.blocks = take (take i.succ b.blocks).sum a.blocks

Tactic:
]

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

Goal state before:
pp: n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
hi : i < b.length
j : ℕ
IHj :
  j < b.blocksFun ⟨i, hi⟩ →
    a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j
hj : j + 1 < b.blocksFun ⟨i, hi⟩
A : j < b.blocksFun ⟨i, hi⟩
⊢ (a.sigmaCompositionAux b ⟨i, ⋯⟩).length = (a.sigmaCompositionAux b ⟨↑⟨i, hi⟩, ⋯⟩).length

Tactic:
]

Goal state after:
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.radius ∧ ↑r < q.radius
⊢ ↑r ≤ (p.prod q).radius

Tactic:
]

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.radius ∧ ↑r < q.radius
⊢ ↑r ≤ (p.prod q).radius
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
hi : i < b.length
j : ℕ
IHj :
  j < b.blocksFun ⟨i, hi⟩ →
    a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j
hj : j + 1 < b.blocksFun ⟨i, hi⟩
A : j < b.blocksFun ⟨i, hi⟩
B : j < (a.sigmaCompositionAux b ⟨i, ⋯⟩).length
C : b.sizeUpTo i + j < b.sizeUpTo (i + 1)
D : b.sizeUpTo i + j < a.length
this : b.sizeUpTo i + j.succ = (b.sizeUpTo i + j).succ
⊢ (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j + a.blocks[b.sizeUpTo i + j] =
    (a.gather b).sizeUpTo i + ((a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j + (a.sigmaCompositionAux b ⟨i, ⋯⟩).blocks[j])

Tactic:
]

Goal state after:
case succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
hi : i < b.length
j : ℕ
IHj :
  j < b.blocksFun ⟨i, hi⟩ →
    a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j
hj : j + 1 < b.blocksFun ⟨i, hi⟩
A : j < b.blocksFun ⟨i, hi⟩
B : j < (a.sigmaCompositionAux b ⟨i, ⋯⟩).length
C : b.sizeUpTo i + j < b.sizeUpTo (i + 1)
D : b.sizeUpTo i + j < a.length
this : b.sizeUpTo i + j.succ = (b.sizeUpTo i + j).succ
⊢ (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j + a.blocks[b.sizeUpTo i + j] =
    (a.gather b).sizeUpTo i + ((a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j + (a.sigmaCompositionAux b ⟨i, ⋯⟩).blocks[j])
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)))
⊢ Tendsto (fun n ↦ p.partialSum n y) atTop (𝓝 (f (x + y))) →
    f (x + y) - f x ∈ Metric.eball 0 q.radius → HasSum (fun n ↦ (q n) fun x_1 ↦ f (x + y) - f x) (g (f (x + y)))

Tactic:
h'y

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
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)))
⊢ f (x + y) - f x ∈ Metric.eball 0 q.radius → HasSum (fun n ↦ (q n) fun x_1 ↦ f (x + y) - f x) (g (f (x + y)))
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.radius ∧ ↑r < q.radius
this : (fun x ↦ ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x ↦ 1
n : ℕ
⊢ ‖p.prod q n‖ * ‖↑r ^ n‖ ≤ ‖‖p n‖ + ‖q n‖‖ * ‖↑r ^ n‖

Tactic:
]

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.radius ∧ ↑r < q.radius
this : (fun x ↦ ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x ↦ 1
n : ℕ
⊢ ‖p.prod q n‖ * ‖↑r ^ n‖ ≤ ‖‖p n‖ + ‖q n‖‖ * ‖↑r ^ n‖