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

State before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
⊢ StronglySummable f ↔ Tendsto (fun i => weightedOrder w (f i)) cofinite (nhds ⊤)
Tactic:
refine' ⟨fun hf => _, of_weightedOrder_tendsto_top w f⟩
State after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ Tendsto (fun i => weightedOrder w (f i)) cofinite (nhds ⊤)

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

State before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ ∀ i < ⊤, ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi i
Tactic:
intro n hn
State after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ∞
hn : n < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi n

State before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ∞
hn : n < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi n
Tactic:
induction n
State after:
case top
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
hn : ⊤ < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ⊤

case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
a✝ : ℕ
hn : ↑a✝ < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑a✝

State before:
case top
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
hn : ⊤ < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ⊤
Tactic:
exfalso
State after:
case top
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
hn : ⊤ < ⊤
⊢ False

State before:
case top
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
hn : ⊤ < ⊤
⊢ False
Tactic:
exact lt_irrefl ⊤ hn
State after:
no goals

State before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
a✝ : ℕ
hn : ↑a✝ < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑a✝
Tactic:
rename_i n
State after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑n

State before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑n
Tactic:
simp only [Set.mem_Ioi, eventually_cofinite, not_lt]
State after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
⊢ {x | weightedOrder w (f x) ≤ ↑n}.Finite

State before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
⊢ {x | weightedOrder w (f x) ≤ ↑n}.Finite
Tactic:
let s := {d : σ →₀ ℕ | (weight w d) ≤ n}
State after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
⊢ {x | weightedOrder w (f x) ≤ ↑n}.Finite

State before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
⊢ {x | weightedOrder w (f x) ≤ ↑n}.Finite
Tactic:
suffices h_ss : {i | (f i).weightedOrder w ≤ some n} ⊆
    ⋃ (d : σ →₀ ℕ) (_ : d ∈ s), {i | coeff α d (f i) ≠ 0} by
  exact ((finite_of_weight_le w hw n).biUnion fun d _ => hf d).subset h_ss
State after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
⊢ {i | weightedOrder w (f i) ≤ some n} ⊆ ⋃ d ∈ s, {i | (coeff α d) (f i) ≠ 0}

State before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
h_ss : {i | weightedOrder w (f i) ≤ some n} ⊆ ⋃ d ∈ s, {i | (coeff α d) (f i) ≠ 0}
⊢ {x | weightedOrder w (f x) ≤ ↑n}.Finite
Tactic:
exact ((finite_of_weight_le w hw n).biUnion fun d _ => hf d).subset h_ss
State after:
no goals

State before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
⊢ {i | weightedOrder w (f i) ≤ some n} ⊆ ⋃ d ∈ s, {i | (coeff α d) (f i) ≠ 0}
Tactic:
intro i hi
State after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : i ∈ {i | weightedOrder w (f i) ≤ some n}
⊢ i ∈ ⋃ d ∈ s, {i | (coeff α d) (f i) ≠ 0}

State before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : i ∈ {i | weightedOrder w (f i) ≤ some n}
⊢ i ∈ ⋃ d ∈ s, {i | (coeff α d) (f i) ≠ 0}
Tactic:
simp only [mem_setOf_eq] at hi
State after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
⊢ i ∈ ⋃ d ∈ s, {i | (coeff α d) (f i) ≠ 0}

State before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
⊢ i ∈ ⋃ d ∈ s, {i | (coeff α d) (f i) ≠ 0}
Tactic:
simp only [mem_setOf_eq, Nat.cast_id, ne_eq, mem_iUnion, mem_setOf_eq, exists_prop]
State after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
⊢ ∃ i_1 ∈ s, ¬(coeff α i_1) (f i) = 0

State before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
⊢ ∃ i_1 ∈ s, ¬(coeff α i_1) (f i) = 0
Tactic:
have heq: (ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i) := by
  rw [ENat.coe_toNat_eq_self]
  exact ne_of_lt (lt_of_le_of_lt hi hn)
State after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
heq : ↑(ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i)
⊢ ∃ i_1 ∈ s, ¬(coeff α i_1) (f i) = 0

State before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
heq : ↑(ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i)
⊢ ∃ i_1 ∈ s, ¬(coeff α i_1) (f i) = 0
Tactic:
obtain ⟨d, hd⟩ := exists_coeff_ne_zero_of_weightedOrder w (f i) heq
State after:
case coe.intro
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
heq : ↑(ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i)
d : σ →₀ ℕ
hd : ↑((weight w) d) = weightedOrder w (f i) ∧ (coeff α d) (f i) ≠ 0
⊢ ∃ i_1 ∈ s, ¬(coeff α i_1) (f i) = 0

State before:
case coe.intro
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
heq : ↑(ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i)
d : σ →₀ ℕ
hd : ↑((weight w) d) = weightedOrder w (f i) ∧ (coeff α d) (f i) ≠ 0
⊢ ∃ i_1 ∈ s, ¬(coeff α i_1) (f i) = 0
Tactic:
refine' ⟨d, _, hd.2⟩
State after:
case coe.intro
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
heq : ↑(ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i)
d : σ →₀ ℕ
hd : ↑((weight w) d) = weightedOrder w (f i) ∧ (coeff α d) (f i) ≠ 0
⊢ d ∈ s

State before:
case coe.intro
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
heq : ↑(ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i)
d : σ →₀ ℕ
hd : ↑((weight w) d) = weightedOrder w (f i) ∧ (coeff α d) (f i) ≠ 0
⊢ d ∈ s
Tactic:
simpa [← hd.1, WithTop.some_eq_coe, Nat.cast_le] using hi
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
⊢ ↑(ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i)
Tactic:
rw [ENat.coe_toNat_eq_self]
State after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
⊢ weightedOrder w (f i) ≠ ⊤

State before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
⊢ weightedOrder w (f i) ≠ ⊤
Tactic:
exact ne_of_lt (lt_of_le_of_lt hi hn)
State after:
no goals