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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
f : F [×c.length]→L[𝕜] G
v : Fin n → E
⊢ (‖f‖ * ∏ i, ‖p (c.blocksFun i)‖) * ∏ i, ∏ j, ‖(v ∘ ⇑(c.embedding i)) j‖ =
    (‖f‖ * ∏ i, ‖p (c.blocksFun i)‖) * ∏ a, ∏ s, ‖v (c.blocksFinEquiv ⟨a, s⟩)‖

Tactic:
]

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
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
f : F [×c.length]→L[𝕜] G
v : Fin n → E
⊢ (‖f‖ * ∏ i, ‖p (c.blocksFun i)‖) * ∏ i, ∏ j, ‖(v ∘ ⇑(c.embedding i)) j‖ =
    (‖f‖ * ∏ i, ‖p (c.blocksFun i)‖) * ∏ a, ∏ s, ‖v (c.blocksFinEquiv ⟨a, s⟩)‖
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
n : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
⊢ ↑‖q.compAlongComposition p c‖₊ ≤ ↑(‖q c.length‖₊ * ∏ i, ‖p (c.blocksFun i)‖₊)

Tactic:
]

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
n : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
⊢ ↑‖q.compAlongComposition p c‖₊ ≤ ↑(‖q c.length‖₊ * ∏ i, ‖p (c.blocksFun i)‖₊)
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
⊢ y ∈ Metric.eball (x, x) r

Tactic:
]

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
⊢ y ∈ Metric.eball (x, x) r
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
N : ℕ
hN : max n m ≤ N
⊢ 0 = 0

Tactic:
]

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
n : ℕ
⊢ p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = p n

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 : ℕ
⊢ ∀ b ∈ Finset.univ, b ≠ Composition.ones n → p.compAlongComposition (id 𝕜 E x) b = 0

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:
]

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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
⊢ p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = p n

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 : ℕ
⊢ ∀ b ∈ Finset.univ, b ≠ Composition.ones n → p.compAlongComposition (id 𝕜 E x) b = 0

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
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
n : ℕ
v : Fin n → E
⊢ (p (Composition.ones n).length) ((id 𝕜 E x).applyComposition (Composition.ones n) v) = (p n) v

Tactic:
]

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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : Fin n → E
⊢ (p (Composition.ones n).length) ((id 𝕜 E x).applyComposition (Composition.ones n) v) = (p n) v
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 : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f pf x n r
m : ℕ
hm : n ≤ m
⊢ 0 = 0

Tactic:
]

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
n : ℕ
v : Fin n → E
i✝ : ℕ
him✝ : i✝ < (Composition.ones n).length
hin✝ : i✝ < n
⊢ (fun v i ↦ (id 𝕜 E x 1) fun x ↦ v (Fin.castLE ⋯ i)) v ⟨i✝, him✝⟩ = v ⟨i✝, hin✝⟩

Tactic:
]

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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : Fin n → E
i✝ : ℕ
him✝ : i✝ < (Composition.ones n).length
hin✝ : i✝ < n
⊢ (fun v i ↦ (id 𝕜 E x 1) fun x ↦ v (Fin.castLE ⋯ i)) v ⟨i✝, him✝⟩ = v ⟨i✝, hin✝⟩
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
n : ℕ
v : Fin n → E
i✝ : ℕ
him✝ : i✝ < (Composition.ones n).length
hin✝ : i✝ < n
⊢ i✝ = i✝

Tactic:
]

Goal state after:
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 ∞
⊢ ((f.toFormalMultilinearSeries (Fintype.card ι)) fun x ↦ y) = f y

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 ∞
⊢ ∀ b ∈ Finset.range (Fintype.card ι + 1), b ≠ Fintype.card ι → ((f.toFormalMultilinearSeries b) fun x ↦ y) = 0

Tactic:
]

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 ∞
⊢ ((f.toFormalMultilinearSeries (Fintype.card ι)) fun x ↦ y) = f y

𝕜 : 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 ∞
⊢ ∀ b ∈ Finset.range (Fintype.card ι + 1), b ≠ Fintype.card ι → ((f.toFormalMultilinearSeries b) fun x ↦ y) = 0
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 ∞
⊢ ((domDomCongr (Fintype.equivFinOfCardEq ⋯) (f.compContinuousLinearMap ContinuousLinearMap.proj)) fun x ↦ y) = f y

Tactic:
]

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 ∞
⊢ ((domDomCongr (Fintype.equivFinOfCardEq ⋯) (f.compContinuousLinearMap ContinuousLinearMap.proj)) fun x ↦ y) = f y
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 : ℕ
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : b.blocks[i] = k
j : Fin b.length := ⟨↑i, ⋯⟩
A : 1 < b.blocksFun j
v : Fin n → E
⊢ (p b.length) ((id 𝕜 E x).applyComposition b v) = 0

Tactic:
]

Goal state after:
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 : ℕ
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : b.blocks[i] = k
j : Fin b.length := ⟨↑i, ⋯⟩
A : 1 < b.blocksFun j
v : Fin n → E
⊢ (p b.length) ((id 𝕜 E x).applyComposition b v) = 0
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 : ℕ
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : b.blocks[i] = k
j : Fin b.length := ⟨↑i, ⋯⟩
A : 1 < b.blocksFun j
v : Fin n → E
⊢ 0 = 0

Tactic:
]

Goal state after:
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)
ne : m ≠ Fintype.card ι
⊢ (0 fun x ↦ y) = 0

Tactic:
]

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 ι
⊢ (0 fun x ↦ y) = 0
Module: Mathlib.Analysis.Analytic.Composition

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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
⊢ (id 𝕜 F ((p 0) v0)).compAlongComposition p (Composition.single n n_pos) = p n

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
⊢ ∀ b ∈ Finset.univ, b ≠ Composition.single n n_pos → (id 𝕜 F ((p 0) v0)).compAlongComposition p b = 0

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:
]

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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
⊢ (id 𝕜 F ((p 0) v0)).compAlongComposition p (Composition.single n n_pos) = p n

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
⊢ ∀ b ∈ Finset.univ, b ≠ Composition.single n n_pos → (id 𝕜 F ((p 0) v0)).compAlongComposition p b = 0

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
Module: Mathlib.Analysis.Analytic.Composition

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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : Fin n → E
⊢ p.applyComposition (Composition.single n n_pos) v ⟨0, ⋯⟩ = (p n) v

Tactic:
]

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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : Fin n → E
⊢ p.applyComposition (Composition.single n n_pos) v ⟨0, ⋯⟩ = (p n) v
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 ∞
⊢ ((f.toFormalMultilinearSeriesOfMultilinear (Fintype.card (Option ι))) fun x ↦ y) = (f y.1) y.2

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 ∞
⊢ ∀ b ∈ Finset.range (Fintype.card (Option ι) + 1),
    b ≠ Fintype.card (Option ι) → ((f.toFormalMultilinearSeriesOfMultilinear b) fun x ↦ y) = 0

Tactic:
]

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 ∞
⊢ ((f.toFormalMultilinearSeriesOfMultilinear (Fintype.card (Option ι))) fun x ↦ y) = (f y.1) y.2

𝕜 : 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 ∞
⊢ ∀ b ∈ Finset.range (Fintype.card (Option ι) + 1),
    b ≠ Fintype.card (Option ι) → ((f.toFormalMultilinearSeriesOfMultilinear b) 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
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 ↦ y.1 - y.2

Tactic:
]

Goal state after:
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 ∞
⊢ ((ContinuousMultilinearMap.domDomCongr (Fintype.equivFinOfCardEq ⋯) f.continuousMultilinearMapOption) fun x ↦ y) =
    (f y.1) y.2

Tactic:
]

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 ∞
⊢ ((ContinuousMultilinearMap.domDomCongr (Fintype.equivFinOfCardEq ⋯) f.continuousMultilinearMapOption) fun x ↦ y) =
    (f y.1) y.2
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
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.single n n_pos
A : 1 < b.length
v : Fin n → E
⊢ 0 = 0

Tactic:
]

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 - (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
hA : HasSum (fun n ↦ A (n + 2)) (f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2)
⊢ ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L y

Tactic:
]

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 - (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
hA : HasSum (fun n ↦ A (n + 2)) (f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2)
⊢ ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L y