-- Mathlib/Analysis/Analytic/CPolynomial.lean
theorem hasFiniteFPowerSeriesOnBall :
    HasFiniteFPowerSeriesOnBall f f.toFormalMultilinearSeries 0 (Fintype.card ι + 1) ⊤ :=
  .mk' (fun _ hm ↦ dif_neg (Nat.succ_le_iff.mp hm).ne) ENNReal.zero_lt_top fun y _ ↦ by
    rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]
    · rw [toFormalMultilinearSeries, dif_pos rfl]; rfl
    · intro m _ ne; rw [toFormalMultilinearSeries, dif_neg ne.symm]; rfl

Proof state:
𝕜 : 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 ∈ EMetric.ball 0 ⊤
⊢ ∀ b ∈ Finset.range (Fintype.card ι + 1), b ≠ Fintype.card ι → ((f.toFormalMultilinearSeries b) fun x => y) = 0

Tactic:
intro m _ ne

Result:
𝕜 : 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 ∈ EMetric.ball 0 ⊤
m : ℕ
a✝ : m ∈ Finset.range (Fintype.card ι + 1)
ne : m ≠ Fintype.card ι
⊢ ((f.toFormalMultilinearSeries m) fun x => y) = 0

Proof state:
𝕜 : 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 ∈ EMetric.ball 0 ⊤
⊢ ((f.toFormalMultilinearSeries (Fintype.card ι)) fun x => y) = f y

Tactic:
rw [toFormalMultilinearSeries, dif_pos rfl]

Result:
𝕜 : 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 ∈ EMetric.ball 0 ⊤
⊢ ((domDomCongr (Fintype.equivFinOfCardEq ⋯) (f.compContinuousLinearMap ContinuousLinearMap.proj)) fun x => y) = f y

Proof state:
𝕜 : 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 ∈ EMetric.ball 0 ⊤
m : ℕ
a✝ : m ∈ Finset.range (Fintype.card ι + 1)
ne : m ≠ Fintype.card ι
⊢ (0 fun x => y) = 0

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : 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 ∈ EMetric.ball 0 ⊤
⊢ (∑ i ∈ Finset.range (Fintype.card ι + 1), (f.toFormalMultilinearSeries i) fun x => y) = f (0 + y)

Tactic:
rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]

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

Proof state:
𝕜 : 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 ∈ EMetric.ball 0 ⊤
m : ℕ
a✝ : m ∈ Finset.range (Fintype.card ι + 1)
ne : m ≠ Fintype.card ι
⊢ ((f.toFormalMultilinearSeries m) fun x => y) = 0

Tactic:
rw [toFormalMultilinearSeries, dif_neg ne.symm]

Result:
𝕜 : 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 ∈ EMetric.ball 0 ⊤
m : ℕ
a✝ : m ∈ Finset.range (Fintype.card ι + 1)
ne : m ≠ Fintype.card ι
⊢ (0 fun x => y) = 0

Proof state:
𝕜 : 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 ∈ EMetric.ball 0 ⊤
⊢ ((domDomCongr (Fintype.equivFinOfCardEq ⋯) (f.compContinuousLinearMap ContinuousLinearMap.proj)) fun x => y) = f y

Tactic:
rfl

Result:
no goals