internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.finite_of_weight_le
Proof state before:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
this : {f | (weight w) f ≤ n} ⊆ ↑(Finset.image (fun uv => uv.1) fg)
⊢ {f | (weight w) f ≤ n}.Finite
Tactic:
apply Set.Finite.subset _ this
Proof state after:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
this : {f | (weight w) f ≤ n} ⊆ ↑(Finset.image (fun uv => uv.1) fg)
⊢ (↑(Finset.image (fun uv => uv.1) fg)).Finite
Theorem: MvPowerSeries.finite_of_weight_le
Proof state before:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
this : {f | (weight w) f ≤ n} ⊆ ↑(Finset.image (fun uv => uv.1) fg)
⊢ (↑(Finset.image (fun uv => uv.1) fg)).Finite
Tactic:
apply Finset.finite_toSet
Proof state after:
no goals
Theorem: MvPowerSeries.exists_coeff_ne_zero_of_weight_iff_ne_zero
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (∃ n d, (weight w) d = n ∧ (coeff α d) f ≠ 0) ↔ f ≠ 0
Tactic:
refine' not_iff_not.mp _
Proof state after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (¬∃ n d, (weight w) d = n ∧ (coeff α d) f ≠ 0) ↔ ¬f ≠ 0
Theorem: MvPowerSeries.exists_coeff_ne_zero_of_weight_iff_ne_zero
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (¬∃ n d, (weight w) d = n ∧ (coeff α d) f ≠ 0) ↔ ¬f ≠ 0
Tactic:
push_neg
Proof state after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0) ↔ f = 0
Theorem: MvPowerSeries.exists_coeff_ne_zero_of_weight_iff_ne_zero
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0) ↔ f = 0
Tactic:
constructor
Proof state after:
case mp
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0) → f = 0

case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ f = 0 → ∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0
Theorem: MvPowerSeries.exists_coeff_ne_zero_of_weight_iff_ne_zero
Proof state before:
case mp
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0) → f = 0
Tactic:
intro h
Proof state after:
case mp
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0
⊢ f = 0
Theorem: MvPowerSeries.exists_coeff_ne_zero_of_weight_iff_ne_zero
Proof state before:
case mp
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0
⊢ f = 0
Tactic:
ext d
Proof state after:
case mp.h
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) 0
Theorem: MvPowerSeries.exists_coeff_ne_zero_of_weight_iff_ne_zero
Proof state before:
case mp.h
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) 0
Tactic:
exact h _ d rfl
Proof state after:
no goals
Theorem: MvPowerSeries.exists_coeff_ne_zero_of_weight_iff_ne_zero
Proof state before:
case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ f = 0 → ∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0
Tactic:
rintro rfl n d _
Proof state after:
case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
n : ℕ
d : σ →₀ ℕ
_✝ : (weight w) d = n
⊢ (coeff α d) 0 = 0
Theorem: MvPowerSeries.exists_coeff_ne_zero_of_weight_iff_ne_zero
Proof state before:
case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
n : ℕ
d : σ →₀ ℕ
_✝ : (weight w) d = n
⊢ (coeff α d) 0 = 0
Tactic:
exact coeff_zero _
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_zero
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ weightedOrder w 0 = ⊤
Tactic:
rw [weightedOrder, dif_pos rfl]
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_finite_iff_ne_zero
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ ↑(toNat (weightedOrder w f)) = weightedOrder w f ↔ f ≠ 0
Tactic:
simp only [weightedOrder]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)) ↔ f ≠ 0
Theorem: MvPowerSeries.weightedOrder_finite_iff_ne_zero
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)) ↔ f ≠ 0
Tactic:
constructor
Proof state after:
case mp
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)) → f ≠ 0

case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ f ≠ 0 → ↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)
Theorem: MvPowerSeries.weightedOrder_finite_iff_ne_zero
Proof state before:
case mp
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)) → f ≠ 0
Tactic:
split_ifs with h <;> intro H
Proof state after:
case pos
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : f = 0
H : ↑(toNat ⊤) = ⊤
⊢ f ≠ 0

case neg
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ¬f = 0
H : ↑(toNat ↑(Nat.find ⋯)) = ↑(Nat.find ⋯)
⊢ f ≠ 0
Theorem: MvPowerSeries.weightedOrder_finite_iff_ne_zero
Proof state before:
case pos
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : f = 0
H : ↑(toNat ⊤) = ⊤
⊢ f ≠ 0
Tactic:
exfalso
Proof state after:
case pos
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : f = 0
H : ↑(toNat ⊤) = ⊤
⊢ False
Theorem: MvPowerSeries.weightedOrder_finite_iff_ne_zero
Proof state before:
case pos
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : f = 0
H : ↑(toNat ⊤) = ⊤
⊢ False
Tactic:
apply ENat.coe_ne_top _ H
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_finite_iff_ne_zero
Proof state before:
case neg
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ¬f = 0
H : ↑(toNat ↑(Nat.find ⋯)) = ↑(Nat.find ⋯)
⊢ f ≠ 0
Tactic:
exact h
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_finite_iff_ne_zero
Proof state before:
case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ f ≠ 0 → ↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)
Tactic:
intro h
Proof state after:
case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : f ≠ 0
⊢ ↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)
Theorem: MvPowerSeries.weightedOrder_finite_iff_ne_zero
Proof state before:
case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : f ≠ 0
⊢ ↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)
Tactic:
simp only [h, not_false_iff, dif_neg, toNat_coe]
Proof state after:
no goals
Theorem: MvPowerSeries.exists_coeff_ne_zero_of_weightedOrder
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ↑(toNat (weightedOrder w f)) = weightedOrder w f
⊢ ∃ d, ↑((weight w) d) = weightedOrder w f ∧ (coeff α d) f ≠ 0
Tactic:
classical
simp_rw [weightedOrder, dif_neg ((weightedOrder_finite_iff_ne_zero _ f).mp h), Nat.cast_inj]
generalize_proofs h1
exact Nat.find_spec h1
Proof state after:
no goals
Theorem: MvPowerSeries.exists_coeff_ne_zero_of_weightedOrder
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ↑(toNat (weightedOrder w f)) = weightedOrder w f
⊢ ∃ d, ↑((weight w) d) = weightedOrder w f ∧ (coeff α d) f ≠ 0
Tactic:
simp_rw [weightedOrder, dif_neg ((weightedOrder_finite_iff_ne_zero _ f).mp h), Nat.cast_inj]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ↑(toNat (weightedOrder w f)) = weightedOrder w f
⊢ ∃ d, (weight w) d = Nat.find ⋯ ∧ (coeff α d) f ≠ 0
Theorem: MvPowerSeries.exists_coeff_ne_zero_of_weightedOrder
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ↑(toNat (weightedOrder w f)) = weightedOrder w f
⊢ ∃ d, (weight w) d = Nat.find ⋯ ∧ (coeff α d) f ≠ 0
Tactic:
generalize_proofs h1
Proof state after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ↑(toNat (weightedOrder w f)) = weightedOrder w f
h1 : ∃ n d, (weight w) d = n ∧ (coeff α d) f ≠ 0
⊢ ∃ d, (weight w) d = Nat.find h1 ∧ (coeff α d) f ≠ 0
Theorem: MvPowerSeries.exists_coeff_ne_zero_of_weightedOrder
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ↑(toNat (weightedOrder w f)) = weightedOrder w f
h1 : ∃ n d, (weight w) d = n ∧ (coeff α d) f ≠ 0
⊢ ∃ d, (weight w) d = Nat.find h1 ∧ (coeff α d) f ≠ 0
Tactic:
exact Nat.find_spec h1
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_le
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ weightedOrder w f ≤ ↑((weight w) d)
Tactic:
rw [weightedOrder, dif_neg]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑((weight w) d)

case hnc
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ ¬f = 0
Theorem: MvPowerSeries.weightedOrder_le
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑((weight w) d)
Tactic:
simp only [ne_eq, Nat.cast_le, Nat.find_le_iff]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ ∃ m ≤ (weight w) d, ∃ d, (weight w) d = m ∧ ¬(coeff α d) f = 0
Theorem: MvPowerSeries.weightedOrder_le
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ ∃ m ≤ (weight w) d, ∃ d, (weight w) d = m ∧ ¬(coeff α d) f = 0
Tactic:
exact ⟨weight w d, le_rfl, d, rfl, h⟩
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_le
Proof state before:
case hnc
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ ¬f = 0
Tactic:
exact (f.exists_coeff_ne_zero_of_weight_iff_ne_zero w).mp ⟨weight w d, d, rfl, h⟩
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_of_lt_weightedOrder
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w f
⊢ (coeff α d) f = 0
Tactic:
contrapose! h
Proof state after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ weightedOrder w f ≤ ↑((weight w) d)
Theorem: MvPowerSeries.coeff_of_lt_weightedOrder
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ weightedOrder w f ≤ ↑((weight w) d)
Tactic:
exact weightedOrder_le w f h
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_eq_top_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
⊢ weightedOrder w f = ⊤ ↔ f = 0
Tactic:
constructor
Proof state after:
case mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
⊢ weightedOrder w f = ⊤ → f = 0

case mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
⊢ f = 0 → weightedOrder w f = ⊤
Theorem: MvPowerSeries.weightedOrder_eq_top_iff
Proof state before:
case mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
⊢ weightedOrder w f = ⊤ → f = 0
Tactic:
intro h
Proof state after:
case mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
⊢ f = 0
Theorem: MvPowerSeries.weightedOrder_eq_top_iff
Proof state before:
case mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
⊢ f = 0
Tactic:
ext d
Proof state after:
case mp.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) 0
Theorem: MvPowerSeries.weightedOrder_eq_top_iff
Proof state before:
case mp.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) 0
Tactic:
rw [(coeff α d).map_zero, coeff_of_lt_weightedOrder w]
Proof state after:
case mp.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
d : σ →₀ ℕ
⊢ ↑((weight w) d) < weightedOrder w f
Theorem: MvPowerSeries.weightedOrder_eq_top_iff
Proof state before:
case mp.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
d : σ →₀ ℕ
⊢ ↑((weight w) d) < weightedOrder w f
Tactic:
rw [h]
Proof state after:
case mp.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
d : σ →₀ ℕ
⊢ ↑((weight w) d) < ⊤
Theorem: MvPowerSeries.weightedOrder_eq_top_iff
Proof state before:
case mp.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
d : σ →₀ ℕ
⊢ ↑((weight w) d) < ⊤
Tactic:
exact WithTop.coe_lt_top _
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_eq_top_iff
Proof state before:
case mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
⊢ f = 0 → weightedOrder w f = ⊤
Tactic:
rintro rfl
Proof state after:
case mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ weightedOrder w 0 = ⊤
Theorem: MvPowerSeries.weightedOrder_eq_top_iff
Proof state before:
case mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ weightedOrder w 0 = ⊤
Tactic:
exact weightedOrder_zero w
Proof state after:
no goals
Theorem: MvPowerSeries.nat_le_weightedOrder
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
⊢ ↑n ≤ weightedOrder w f
Tactic:
by_contra H
Proof state after:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : ¬↑n ≤ weightedOrder w f
⊢ False
Theorem: MvPowerSeries.nat_le_weightedOrder
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : ¬↑n ≤ weightedOrder w f
⊢ False
Tactic:
rw [not_le] at H
Proof state after:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : weightedOrder w f < ↑n
⊢ False
Theorem: MvPowerSeries.nat_le_weightedOrder
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : weightedOrder w f < ↑n
⊢ False
Tactic:
have : ↑(toNat (f.weightedOrder w)) = f.weightedOrder w := by
  rw [coe_toNat_eq_self] ; exact ne_top_of_lt H
Proof state after:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : weightedOrder w f < ↑n
this : ↑(toNat (weightedOrder w f)) = weightedOrder w f
⊢ False
Theorem: MvPowerSeries.nat_le_weightedOrder
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : weightedOrder w f < ↑n
this : ↑(toNat (weightedOrder w f)) = weightedOrder w f
⊢ False
Tactic:
obtain ⟨d, hd, hfd⟩ := exists_coeff_ne_zero_of_weightedOrder w f this
Proof state after:
case intro.intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : weightedOrder w f < ↑n
this : ↑(toNat (weightedOrder w f)) = weightedOrder w f
d : σ →₀ ℕ
hd : ↑((weight w) d) = weightedOrder w f
hfd : (coeff α d) f ≠ 0
⊢ False
Theorem: MvPowerSeries.nat_le_weightedOrder
Proof state before:
case intro.intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : weightedOrder w f < ↑n
this : ↑(toNat (weightedOrder w f)) = weightedOrder w f
d : σ →₀ ℕ
hd : ↑((weight w) d) = weightedOrder w f
hfd : (coeff α d) f ≠ 0
⊢ False
Tactic:
rw [← hd, Nat.cast_lt] at H
Proof state after:
case intro.intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
this : ↑(toNat (weightedOrder w f)) = weightedOrder w f
d : σ →₀ ℕ
H : (weight w) d < n
hd : ↑((weight w) d) = weightedOrder w f
hfd : (coeff α d) f ≠ 0
⊢ False
Theorem: MvPowerSeries.nat_le_weightedOrder
Proof state before:
case intro.intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
this : ↑(toNat (weightedOrder w f)) = weightedOrder w f
d : σ →₀ ℕ
H : (weight w) d < n
hd : ↑((weight w) d) = weightedOrder w f
hfd : (coeff α d) f ≠ 0
⊢ False
Tactic:
exact hfd (h d H)
Proof state after:
no goals
Theorem: MvPowerSeries.nat_le_weightedOrder
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : weightedOrder w f < ↑n
⊢ ↑(toNat (weightedOrder w f)) = weightedOrder w f
Tactic:
rw [coe_toNat_eq_self]
Proof state after:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : weightedOrder w f < ↑n
⊢ weightedOrder w f ≠ ⊤
Theorem: MvPowerSeries.nat_le_weightedOrder
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : weightedOrder w f < ↑n
⊢ weightedOrder w f ≠ ⊤
Tactic:
exact ne_top_of_lt H
Proof state after:
no goals
Theorem: MvPowerSeries.le_weightedOrder
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ∞
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < n → (coeff α d) f = 0
⊢ n ≤ weightedOrder w f
Tactic:
cases n
Proof state after:
case top
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff α d) f = 0
⊢ ⊤ ≤ weightedOrder w f

case coe
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff α d) f = 0
⊢ ↑a✝ ≤ weightedOrder w f
Theorem: MvPowerSeries.le_weightedOrder
Proof state before:
case top
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff α d) f = 0
⊢ ⊤ ≤ weightedOrder w f
Tactic:
rw [top_le_iff, weightedOrder_eq_top_iff]
Proof state after:
case top
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff α d) f = 0
⊢ f = 0
Theorem: MvPowerSeries.le_weightedOrder
Proof state before:
case top
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff α d) f = 0
⊢ f = 0
Tactic:
ext d
Proof state after:
case top.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff α d) f = 0
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) 0
Theorem: MvPowerSeries.le_weightedOrder
Proof state before:
case top.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff α d) f = 0
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) 0
Tactic:
exact h d (coe_lt_top _)
Proof state after:
no goals
Theorem: MvPowerSeries.le_weightedOrder
Proof state before:
case coe
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff α d) f = 0
⊢ ↑a✝ ≤ weightedOrder w f
Tactic:
apply nat_le_weightedOrder
Proof state after:
case coe.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff α d) f = 0
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < a✝ → (coeff α d) f = 0
Theorem: MvPowerSeries.le_weightedOrder
Proof state before:
case coe.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff α d) f = 0
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < a✝ → (coeff α d) f = 0
Tactic:
simpa only [ENat.some_eq_coe, Nat.cast_lt] using h
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_eq_nat
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
⊢ weightedOrder w f = ↑n ↔
    (∃ d, (weight w) d = n ∧ (coeff α d) f ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Tactic:
rcases eq_or_ne f 0 with (rfl | hf)
Proof state after:
case inl
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
n : ℕ
⊢ weightedOrder w 0 = ↑n ↔
    (∃ d, (weight w) d = n ∧ (coeff α d) 0 ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) 0 = 0

case inr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ weightedOrder w f = ↑n ↔
    (∃ d, (weight w) d = n ∧ (coeff α d) f ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Theorem: MvPowerSeries.weightedOrder_eq_nat
Proof state before:
case inl
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
n : ℕ
⊢ weightedOrder w 0 = ↑n ↔
    (∃ d, (weight w) d = n ∧ (coeff α d) 0 ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) 0 = 0
Tactic:
simp only [weightedOrder_zero, ENat.top_ne_coe, map_zero, ne_eq, not_true, and_false,
  exists_false, implies_true, forall_const, and_true]
Proof state after:
no goals