internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.weightedOrder_eq_nat
Proof state before:
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
Tactic:
simp only [weightedOrder, dif_neg hf, ne_eq, Nat.cast_inj, Nat.find_eq_iff]
Proof state after:
case inr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ ((∃ d, (weight w) d = n ∧ ¬(coeff α d) f = 0) ∧ ∀ n_1 < n, ¬∃ d, (weight w) d = n_1 ∧ ¬(coeff α d) f = 0) ↔
    (∃ 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 inr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ ((∃ d, (weight w) d = n ∧ ¬(coeff α d) f = 0) ∧ ∀ n_1 < n, ¬∃ d, (weight w) d = n_1 ∧ ¬(coeff α d) f = 0) ↔
    (∃ d, (weight w) d = n ∧ ¬(coeff α d) f = 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Tactic:
apply and_congr_right'
Proof state after:
case inr.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ (∀ n_1 < n, ¬∃ d, (weight w) d = n_1 ∧ ¬(coeff α d) f = 0) ↔ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Theorem: MvPowerSeries.weightedOrder_eq_nat
Proof state before:
case inr.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ (∀ n_1 < n, ¬∃ d, (weight w) d = n_1 ∧ ¬(coeff α d) f = 0) ↔ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Tactic:
simp only [not_exists, not_and, Classical.not_not, imp_forall_iff]
Proof state after:
case inr.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ (∀ (n_1 : ℕ) (x : σ →₀ ℕ), n_1 < n → (weight w) x = n_1 → (coeff α x) f = 0) ↔
    ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Theorem: MvPowerSeries.weightedOrder_eq_nat
Proof state before:
case inr.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ (∀ (n_1 : ℕ) (x : σ →₀ ℕ), n_1 < n → (weight w) x = n_1 → (coeff α x) f = 0) ↔
    ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Tactic:
rw [forall_swap]
Proof state after:
case inr.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ (∀ (y : σ →₀ ℕ), ∀ x < n, (weight w) y = x → (coeff α y) f = 0) ↔ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Theorem: MvPowerSeries.weightedOrder_eq_nat
Proof state before:
case inr.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ (∀ (y : σ →₀ ℕ), ∀ x < n, (weight w) y = x → (coeff α y) f = 0) ↔ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Tactic:
apply forall_congr'
Proof state after:
case inr.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ ∀ (a : σ →₀ ℕ), (∀ x < n, (weight w) a = x → (coeff α a) f = 0) ↔ (weight w) a < n → (coeff α a) f = 0
Theorem: MvPowerSeries.weightedOrder_eq_nat
Proof state before:
case inr.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ ∀ (a : σ →₀ ℕ), (∀ x < n, (weight w) a = x → (coeff α a) f = 0) ↔ (weight w) a < n → (coeff α a) f = 0
Tactic:
intro d
Proof state after:
case inr.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
⊢ (∀ x < n, (weight w) d = x → (coeff α d) f = 0) ↔ (weight w) d < n → (coeff α d) f = 0
Theorem: MvPowerSeries.weightedOrder_eq_nat
Proof state before:
case inr.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
⊢ (∀ x < n, (weight w) d = x → (coeff α d) f = 0) ↔ (weight w) d < n → (coeff α d) f = 0
Tactic:
constructor
Proof state after:
case inr.h.h.mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
⊢ (∀ x < n, (weight w) d = x → (coeff α d) f = 0) → (weight w) d < n → (coeff α d) f = 0

case inr.h.h.mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
⊢ ((weight w) d < n → (coeff α d) f = 0) → ∀ x < n, (weight w) d = x → (coeff α d) f = 0
Theorem: MvPowerSeries.weightedOrder_eq_nat
Proof state before:
case inr.h.h.mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
⊢ (∀ x < n, (weight w) d = x → (coeff α d) f = 0) → (weight w) d < n → (coeff α d) f = 0
Tactic:
intro h hd
Proof state after:
case inr.h.h.mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
h : ∀ x < n, (weight w) d = x → (coeff α d) f = 0
hd : (weight w) d < n
⊢ (coeff α d) f = 0
Theorem: MvPowerSeries.weightedOrder_eq_nat
Proof state before:
case inr.h.h.mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
h : ∀ x < n, (weight w) d = x → (coeff α d) f = 0
hd : (weight w) d < n
⊢ (coeff α d) f = 0
Tactic:
exact h (weight w d) hd rfl
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_eq_nat
Proof state before:
case inr.h.h.mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
⊢ ((weight w) d < n → (coeff α d) f = 0) → ∀ x < n, (weight w) d = x → (coeff α d) f = 0
Tactic:
intro h m hm hd
Proof state after:
case inr.h.h.mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
h : (weight w) d < n → (coeff α d) f = 0
m : ℕ
hm : m < n
hd : (weight w) d = m
⊢ (coeff α d) f = 0
Theorem: MvPowerSeries.weightedOrder_eq_nat
Proof state before:
case inr.h.h.mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
h : (weight w) d < n → (coeff α d) f = 0
m : ℕ
hm : m < n
hd : (weight w) d = m
⊢ (coeff α d) f = 0
Tactic:
rw [← hd] at hm
Proof state after:
case inr.h.h.mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
h : (weight w) d < n → (coeff α d) f = 0
m : ℕ
hm : (weight w) d < n
hd : (weight w) d = m
⊢ (coeff α d) f = 0
Theorem: MvPowerSeries.weightedOrder_eq_nat
Proof state before:
case inr.h.h.mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
h : (weight w) d < n → (coeff α d) f = 0
m : ℕ
hm : (weight w) d < n
hd : (weight w) d = m
⊢ (coeff α d) f = 0
Tactic:
exact h hm
Proof state after:
no goals
Theorem: MvPowerSeries.le_weightedOrder_add
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
⊢ min (weightedOrder w f) (weightedOrder w g) ≤ weightedOrder w (f + g)
Tactic:
refine' le_weightedOrder w _
Proof state after:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
⊢ ∀ (d : σ →₀ ℕ), ↑((weight w) d) < min (weightedOrder w f) (weightedOrder w g) → (coeff α d) (f + g) = 0
Theorem: MvPowerSeries.le_weightedOrder_add
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
⊢ ∀ (d : σ →₀ ℕ), ↑((weight w) d) < min (weightedOrder w f) (weightedOrder w g) → (coeff α d) (f + g) = 0
Tactic:
simp (config := { contextual := true }) only [coeff_of_lt_weightedOrder w, lt_min_iff, map_add,
  add_zero, eq_self_iff_true, imp_true_iff]
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) = weightedOrder w f
Tactic:
obtain ⟨n, hn⟩ := ne_top_iff_exists.mp (ne_top_of_lt H)
Proof state after:
case intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
⊢ weightedOrder w (f + g) = weightedOrder w f
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux
Proof state before:
case intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
⊢ weightedOrder w (f + g) = weightedOrder w f
Tactic:
erw [← hn, weightedOrder_eq_nat]
Proof state after:
case intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
⊢ (∃ d, (weight w) d = n ∧ (coeff α d) (f + g) ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) (f + g) = 0
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux
Proof state before:
case intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
⊢ (∃ d, (weight w) d = n ∧ (coeff α d) (f + g) ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) (f + g) = 0
Tactic:
obtain ⟨d, hd, hd'⟩ := ((weightedOrder_eq_nat w).mp hn.symm).1
Proof state after:
case intro.intro.intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (∃ d, (weight w) d = n ∧ (coeff α d) (f + g) ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) (f + g) = 0
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux
Proof state before:
case intro.intro.intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (∃ d, (weight w) d = n ∧ (coeff α d) (f + g) ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) (f + g) = 0
Tactic:
constructor
Proof state after:
case intro.intro.intro.left
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ ∃ d, (weight w) d = n ∧ (coeff α d) (f + g) ≠ 0

case intro.intro.intro.right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) (f + g) = 0
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux
Proof state before:
case intro.intro.intro.left
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ ∃ d, (weight w) d = n ∧ (coeff α d) (f + g) ≠ 0
Tactic:
use d
Proof state after:
case h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (weight w) d = n ∧ (coeff α d) (f + g) ≠ 0
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux
Proof state before:
case h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (weight w) d = n ∧ (coeff α d) (f + g) ≠ 0
Tactic:
use hd
Proof state after:
case right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (coeff α d) (f + g) ≠ 0
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux
Proof state before:
case right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (coeff α d) (f + g) ≠ 0
Tactic:
rw [← hn, ← hd] at H
Proof state after:
case right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (coeff α d) (f + g) ≠ 0
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux
Proof state before:
case right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (coeff α d) (f + g) ≠ 0
Tactic:
rw [(coeff _ _).map_add, coeff_of_lt_weightedOrder w g H, add_zero]
Proof state after:
case right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (coeff α d) f ≠ 0
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux
Proof state before:
case right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (coeff α d) f ≠ 0
Tactic:
exact hd'
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux
Proof state before:
case intro.intro.intro.right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) (f + g) = 0
Tactic:
intro b hb
Proof state after:
case intro.intro.intro.right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ (coeff α b) (f + g) = 0
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux
Proof state before:
case intro.intro.intro.right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ (coeff α b) (f + g) = 0
Tactic:
suffices ↑(weight w b) < weightedOrder w f by
  rw [(coeff _ _).map_add, coeff_of_lt_weightedOrder w f this,
    coeff_of_lt_weightedOrder w g (lt_trans this H), add_zero]
Proof state after:
case intro.intro.intro.right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ ↑((weight w) b) < weightedOrder w f
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux
Proof state before:
case intro.intro.intro.right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ ↑((weight w) b) < weightedOrder w f
Tactic:
rw [← hn, ENat.some_eq_coe, Nat.cast_lt]
Proof state after:
case intro.intro.intro.right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ (weight w) b < n
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux
Proof state before:
case intro.intro.intro.right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ (weight w) b < n
Tactic:
exact hb
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
b : σ →₀ ℕ
hb : (weight w) b < n
this : ↑((weight w) b) < weightedOrder w f
⊢ (coeff α b) (f + g) = 0
Tactic:
rw [(coeff _ _).map_add, coeff_of_lt_weightedOrder w f this,
  coeff_of_lt_weightedOrder w g (lt_trans this H), add_zero]
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_eq
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
⊢ weightedOrder w (f + g) = weightedOrder w f ⊓ weightedOrder w g
Tactic:
refine' le_antisymm _ (le_weightedOrder_add w _ _)
Proof state after:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_eq
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g
Tactic:
by_cases H₁ : f.weightedOrder w < g.weightedOrder w
Proof state after:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g

case neg
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_eq
Proof state before:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g
Tactic:
simp only [le_inf_iff, weightedOrder_add_of_weightedOrder_lt.aux w H₁]
Proof state after:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w f ≤ weightedOrder w f ∧ weightedOrder w f ≤ weightedOrder w g
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_eq
Proof state before:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w f ≤ weightedOrder w f ∧ weightedOrder w f ≤ weightedOrder w g
Tactic:
exact ⟨le_rfl, le_of_lt H₁⟩
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_eq
Proof state before:
case neg
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g
Tactic:
by_cases H₂ : g.weightedOrder w < f.weightedOrder w
Proof state after:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
H₂ : weightedOrder w g < weightedOrder w f
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g

case neg
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
H₂ : ¬weightedOrder w g < weightedOrder w f
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_eq
Proof state before:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
H₂ : weightedOrder w g < weightedOrder w f
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g
Tactic:
simp only [add_comm f g, le_inf_iff, weightedOrder_add_of_weightedOrder_lt.aux w H₂]
Proof state after:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
H₂ : weightedOrder w g < weightedOrder w f
⊢ weightedOrder w g ≤ weightedOrder w f ∧ weightedOrder w g ≤ weightedOrder w g
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_eq
Proof state before:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
H₂ : weightedOrder w g < weightedOrder w f
⊢ weightedOrder w g ≤ weightedOrder w f ∧ weightedOrder w g ≤ weightedOrder w g
Tactic:
exact ⟨le_of_lt H₂, le_rfl⟩
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_eq
Proof state before:
case neg
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
H₂ : ¬weightedOrder w g < weightedOrder w f
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g
Tactic:
exact absurd (le_antisymm (not_lt.1 H₂) (not_lt.1 H₁)) h
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_mul_ge
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
⊢ weightedOrder w f + weightedOrder w g ≤ weightedOrder w (f * g)
Tactic:
apply le_weightedOrder
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
⊢ ∀ (d : σ →₀ ℕ), ↑((weight w) d) < weightedOrder w f + weightedOrder w g → (coeff α d) (f * g) = 0
Theorem: MvPowerSeries.weightedOrder_mul_ge
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
⊢ ∀ (d : σ →₀ ℕ), ↑((weight w) d) < weightedOrder w f + weightedOrder w g → (coeff α d) (f * g) = 0
Tactic:
intro d hd
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
⊢ (coeff α d) (f * g) = 0
Theorem: MvPowerSeries.weightedOrder_mul_ge
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
⊢ (coeff α d) (f * g) = 0
Tactic:
rw [coeff_mul, Finset.sum_eq_zero]
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
⊢ ∀ x ∈ Finset.antidiagonal d, (coeff α x.1) f * (coeff α x.2) g = 0