Theorem: MvPowerSeries.StronglySummable.of_weightedOrder_tendsto_top (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Basic.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
hf : Tendsto (fun i => weightedOrder w (f i)) cofinite (nhds ⊤)
⊢ StronglySummable f
Tactic:
intro d
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
hf : Tendsto (fun i => weightedOrder w (f i)) cofinite (nhds ⊤)
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)).Finite

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
hf : Tendsto (fun i => weightedOrder w (f i)) cofinite (nhds ⊤)
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)).Finite
Tactic:
rw [HasBasis.tendsto_right_iff nhds_top_basis] at hf
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
hf : ∀ i < ⊤, ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi i
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)).Finite

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
hf : ∀ i < ⊤, ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi i
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)).Finite
Tactic:
specialize hf (weight w d : ℕ∞) (WithTop.coe_lt_top _)
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
⊢ (support fun i => (coeff α d) (f i)).Finite

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
⊢ (support fun i => (coeff α d) (f i)).Finite
Tactic:
refine' hf.subset _
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
⊢ (support fun i => (coeff α d) (f i)) ⊆ {x | (fun x => weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)) x}ᶜ

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
⊢ (support fun i => (coeff α d) (f i)) ⊆ {x | (fun x => weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)) x}ᶜ
Tactic:
intro i  h' h
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
i : ι
h' : i ∈ support fun i => (coeff α d) (f i)
h : i ∈ {x | (fun x => weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)) x}
⊢ False

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
i : ι
h' : i ∈ support fun i => (coeff α d) (f i)
h : i ∈ {x | (fun x => weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)) x}
⊢ False
Tactic:
apply h'
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
i : ι
h' : i ∈ support fun i => (coeff α d) (f i)
h : i ∈ {x | (fun x => weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)) x}
⊢ (fun i => (coeff α d) (f i)) i = 0

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
i : ι
h' : i ∈ support fun i => (coeff α d) (f i)
h : i ∈ {x | (fun x => weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)) x}
⊢ (fun i => (coeff α d) (f i)) i = 0
Tactic:
exact coeff_of_lt_weightedOrder w _ h
State after:
no goals