internlm/Lean-Github huggingface dataset:
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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]
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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]
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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]
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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]
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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]
Proof state after:
no goals
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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
Proof state after:
no goals
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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⟩
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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 ⊢
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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]
Proof state after:
no goals
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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]
Proof state after:
no goals