internlm/Lean-Github huggingface dataset:
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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]
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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]
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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 _)
Proof 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
Theorem: AnalyticAt.monomial_mul_orderAt
Proof 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]
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
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]
Proof state after:
no goals
Theorem: AnalyticAt.monomial_mul_leadingCoeff
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 : 𝕜
fa : AnalyticAt 𝕜 f c
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
⊢ leadingCoeff (fun z => (z - c) ^ n • f z) c = leadingCoeff f c
Tactic:
simp [leadingCoeff, fa.monomial_mul_orderAt fnz n]
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 : 𝕜
fa : AnalyticAt 𝕜 f c
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
⊢ (Function.swap dslope c)^[n + orderAt f c] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[orderAt f c] f c
Theorem: AnalyticAt.monomial_mul_leadingCoeff
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 : 𝕜
fa : AnalyticAt 𝕜 f c
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n : ℕ
⊢ (Function.swap dslope c)^[n + orderAt f c] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[orderAt f c] f c
Tactic:
generalize orderAt f c = a
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 : 𝕜
fa : AnalyticAt 𝕜 f c
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n a : ℕ
⊢ (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
Theorem: AnalyticAt.monomial_mul_leadingCoeff
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 : 𝕜
fa : AnalyticAt 𝕜 f c
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
n a : ℕ
⊢ (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
Tactic:
induction' n with n h
Proof state after:
case zero
𝕜 : 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
a : ℕ
⊢ (Function.swap dslope c)^[0 + a] (fun z => (z - c) ^ 0 • f z) c = (Function.swap dslope c)^[a] f c

case succ
𝕜 : 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
a n : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
⊢ (Function.swap dslope c)^[n + 1 + a] (fun z => (z - c) ^ (n + 1) • f z) c = (Function.swap dslope c)^[a] f c
Theorem: AnalyticAt.monomial_mul_leadingCoeff
Proof state before:
case zero
𝕜 : 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
a : ℕ
⊢ (Function.swap dslope c)^[0 + a] (fun z => (z - c) ^ 0 • f z) c = (Function.swap dslope c)^[a] f c
Tactic:
simp only [zero_add, pow_zero, one_smul, Nat.zero_eq]
Proof state after:
no goals
Theorem: AnalyticAt.monomial_mul_leadingCoeff
Proof state before:
case succ
𝕜 : 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
a n : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
⊢ (Function.swap dslope c)^[n + 1 + a] (fun z => (z - c) ^ (n + 1) • f z) c = (Function.swap dslope c)^[a] f c
Tactic:
simp [pow_succ', ← smul_smul, Nat.succ_add]
Proof state after:
case succ
𝕜 : 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
a n : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • (z - c) ^ n • f z) c =
    (Function.swap dslope c)^[a] f c
Theorem: AnalyticAt.monomial_mul_leadingCoeff
Proof state before:
case succ
𝕜 : 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
a n : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • (z - c) ^ n • f z) c =
    (Function.swap dslope c)^[a] f c
Tactic:
generalize hg : (fun z ↦ (z - c) ^ n • f z) = g
Proof state after:
case succ
𝕜 : 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
a n : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • (z - c) ^ n • f z) c =
    (Function.swap dslope c)^[a] f c
Theorem: AnalyticAt.monomial_mul_leadingCoeff
Proof state before:
case succ
𝕜 : 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
a n : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • (z - c) ^ n • f z) c =
    (Function.swap dslope c)^[a] f c
Tactic:
have hg' : ∀ z, (z - c) ^ n • f z = g z := by
  rw [←hg]; simp only [eq_self_iff_true, forall_const]
Proof state after:
case succ
𝕜 : 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
a n : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
hg' : ∀ (z : 𝕜), (z - c) ^ n • f z = g z
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • (z - c) ^ n • f z) c =
    (Function.swap dslope c)^[a] f c