Theorem: AnalyticAt.monomial_mul_orderAt (Ray/Analytic/Analytic.lean)

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : AnalyticAt 𝕜 f c
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
⊢ orderAt (fun z => (z - c) ^ n • f z) c = n + orderAt f c
Tactic:
rcases fa with ⟨p, fp⟩
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
⊢ orderAt (fun z => (z - c) ^ n • f z) c = n + orderAt f c

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
⊢ orderAt (fun z => (z - c) ^ n • f z) c = n + orderAt f c
Tactic:
have pnz : p ≠ 0 := by
  contrapose fnz; simp only [ne_eq, not_not] at fnz
  simpa only [HasFPowerSeriesAt.locally_zero_iff fp, Filter.not_frequently, not_not]
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
⊢ orderAt (fun z => (z - c) ^ n • f z) c = n + orderAt f c

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
⊢ orderAt (fun z => (z - c) ^ n • f z) c = n + orderAt f c
Tactic:
have pe : ∃ i, p i ≠ 0 := by rw [Function.ne_iff] at pnz; exact pnz
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
⊢ orderAt (fun z => (z - c) ^ n • f z) c = n + orderAt f c

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
⊢ orderAt (fun z => (z - c) ^ n • f z) c = n + orderAt f c
Tactic:
have pne : ∃ i, (p.unshiftIter n) i ≠ 0 := by
  rcases pe with ⟨i, pi⟩; use n + i
  simp only [FormalMultilinearSeries.ne_zero_iff_coeff_ne_zero] at pi ⊢
  simpa only [p.unshiftIter_coeff, add_lt_iff_neg_left, add_tsub_cancel_left]
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
⊢ orderAt (fun z => (z - c) ^ n • f z) c = n + orderAt f c

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
⊢ orderAt (fun z => (z - c) ^ n • f z) c = n + orderAt f c
Tactic:
have fq : HasFPowerSeriesAt (fun z ↦ (z - c) ^ n • f z) (p.unshiftIter n) c := fp.unshiftIter
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
⊢ orderAt (fun z => (z - c) ^ n • f z) c = n + orderAt f c

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
⊢ orderAt (fun z => (z - c) ^ n • f z) c = n + orderAt f c
Tactic:
rw [fp.orderAt_unique, fq.orderAt_unique]
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
⊢ (p.unshiftIter n).order = n + p.order

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
⊢ (p.unshiftIter n).order = n + p.order
Tactic:
rw [FormalMultilinearSeries.order_eq_find pe, FormalMultilinearSeries.order_eq_find pne]
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
⊢ Nat.find pne = n + Nat.find pe

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
⊢ Nat.find pne = n + Nat.find pe
Tactic:
rw [Nat.find_eq_iff]
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
⊢ p.unshiftIter n (n + Nat.find pe) ≠ 0 ∧ ∀ n_1 < n + Nat.find pe, ¬p.unshiftIter n n_1 ≠ 0

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
⊢ p.unshiftIter n (n + Nat.find pe) ≠ 0 ∧ ∀ n_1 < n + Nat.find pe, ¬p.unshiftIter n n_1 ≠ 0
Tactic:
constructor
State after:
case intro.left
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
⊢ p.unshiftIter n (n + Nat.find pe) ≠ 0

case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
⊢ ∀ n_1 < n + Nat.find pe, ¬p.unshiftIter n n_1 ≠ 0

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
⊢ p ≠ 0
Tactic:
contrapose fnz
State after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
fnz : ¬p ≠ 0
⊢ ¬∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
fnz : ¬p ≠ 0
⊢ ¬∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
Tactic:
simp only [ne_eq, not_not] at fnz
State after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
fnz : p = 0
⊢ ¬∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
fnz : p = 0
⊢ ¬∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
Tactic:
simpa only [HasFPowerSeriesAt.locally_zero_iff fp, Filter.not_frequently, not_not]
State after:
no goals

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
⊢ ∃ i, p i ≠ 0
Tactic:
rw [Function.ne_iff] at pnz
State after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : ∃ a, p a ≠ 0 a
⊢ ∃ i, p i ≠ 0

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : ∃ a, p a ≠ 0 a
⊢ ∃ i, p i ≠ 0
Tactic:
exact pnz
State after:
no goals

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
⊢ ∃ i, p.unshiftIter n i ≠ 0
Tactic:
rcases pe with ⟨i, pi⟩
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
i : ℕ
pi : p i ≠ 0
⊢ ∃ i, p.unshiftIter n i ≠ 0

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
i : ℕ
pi : p i ≠ 0
⊢ ∃ i, p.unshiftIter n i ≠ 0
Tactic:
use n + i
State after:
case h
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
i : ℕ
pi : p i ≠ 0
⊢ p.unshiftIter n (n + i) ≠ 0

State before:
case h
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
i : ℕ
pi : p i ≠ 0
⊢ p.unshiftIter n (n + i) ≠ 0
Tactic:
simp only [FormalMultilinearSeries.ne_zero_iff_coeff_ne_zero] at pi ⊢
State after:
case h
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
i : ℕ
pi : p.coeff i ≠ 0
⊢ (p.unshiftIter n).coeff (n + i) ≠ 0

State before:
case h
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
i : ℕ
pi : p.coeff i ≠ 0
⊢ (p.unshiftIter n).coeff (n + i) ≠ 0
Tactic:
simpa only [p.unshiftIter_coeff, add_lt_iff_neg_left, add_tsub_cancel_left]
State after:
no goals

State before:
case intro.left
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
⊢ p.unshiftIter n (n + Nat.find pe) ≠ 0
Tactic:
have s := Nat.find_spec pe
State after:
case intro.left
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
s : p (Nat.find pe) ≠ 0
⊢ p.unshiftIter n (n + Nat.find pe) ≠ 0

State before:
case intro.left
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
s : p (Nat.find pe) ≠ 0
⊢ p.unshiftIter n (n + Nat.find pe) ≠ 0
Tactic:
simp only [← p.coeff_eq_zero, Ne] at s
State after:
case intro.left
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
s : ¬p.coeff (Nat.find ⋯) = 0
⊢ p.unshiftIter n (n + Nat.find pe) ≠ 0

State before:
case intro.left
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
s : ¬p.coeff (Nat.find ⋯) = 0
⊢ p.unshiftIter n (n + Nat.find pe) ≠ 0
Tactic:
simp only [p.unshiftIter_coeff, ←FormalMultilinearSeries.coeff_eq_zero, s, Ne,
  add_lt_iff_neg_left, not_lt_zero', add_tsub_cancel_left, if_false, not_false_iff, true_and,
  not_not]
State after:
no goals

State before:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
⊢ ∀ n_1 < n + Nat.find pe, ¬p.unshiftIter n n_1 ≠ 0
Tactic:
intro m mp
State after:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mp : m < n + Nat.find pe
⊢ ¬p.unshiftIter n m ≠ 0

State before:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mp : m < n + Nat.find pe
⊢ ¬p.unshiftIter n m ≠ 0
Tactic:
simp [← FormalMultilinearSeries.coeff_eq_zero, p.unshiftIter_coeff]
State after:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mp : m < n + Nat.find pe
⊢ n ≤ m → p.coeff (m - n) = 0

State before:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mp : m < n + Nat.find pe
⊢ n ≤ m → p.coeff (m - n) = 0
Tactic:
intro mn
State after:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mp : m < n + Nat.find pe
mn : n ≤ m
⊢ p.coeff (m - n) = 0

State before:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mp : m < n + Nat.find pe
mn : n ≤ m
⊢ p.coeff (m - n) = 0
Tactic:
generalize ha : m - n = a
State after:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mp : m < n + Nat.find pe
mn : n ≤ m
a : ℕ
ha : m - n = a
⊢ p.coeff a = 0

State before:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mp : m < n + Nat.find pe
mn : n ≤ m
a : ℕ
ha : m - n = a
⊢ p.coeff a = 0
Tactic:
have hm : m = n + a := by rw [← ha, add_comm, Nat.sub_add_cancel mn]
State after:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mp : m < n + Nat.find pe
mn : n ≤ m
a : ℕ
ha : m - n = a
hm : m = n + a
⊢ p.coeff a = 0

State before:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mp : m < n + Nat.find pe
mn : n ≤ m
a : ℕ
ha : m - n = a
hm : m = n + a
⊢ p.coeff a = 0
Tactic:
simp only [hm, add_lt_add_iff_left, Nat.lt_find_iff, not_not] at mp
State after:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mn : n ≤ m
a : ℕ
ha : m - n = a
hm : m = n + a
mp : ∀ m ≤ a, p m = 0
⊢ p.coeff a = 0

State before:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mn : n ≤ m
a : ℕ
ha : m - n = a
hm : m = n + a
mp : ∀ m ≤ a, p m = 0
⊢ p.coeff a = 0
Tactic:
specialize mp a (le_refl _)
State after:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mn : n ≤ m
a : ℕ
ha : m - n = a
hm : m = n + a
mp : p a = 0
⊢ p.coeff a = 0

State before:
case intro.right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mn : n ≤ m
a : ℕ
ha : m - n = a
hm : m = n + a
mp : p a = 0
⊢ p.coeff a = 0
Tactic:
rwa [FormalMultilinearSeries.coeff_eq_zero]
State after:
no goals

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
pnz : p ≠ 0
pe : ∃ i, p i ≠ 0
pne : ∃ i, p.unshiftIter n i ≠ 0
fq : HasFPowerSeriesAt (fun z => (z - c) ^ n • f z) (p.unshiftIter n) c
m : ℕ
mp : m < n + Nat.find pe
mn : n ≤ m
a : ℕ
ha : m - n = a
⊢ m = n + a
Tactic:
rw [← ha, add_comm, Nat.sub_add_cancel mn]
State after:
no goals