internlm/Lean-Github huggingface dataset:
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
⊢ ∀ x ∈ Finset.antidiagonal d, (coeff α x.1) f * (coeff α x.2) g = 0
Tactic:
rintro ⟨i, j⟩ hij
Proof state after:
case h.mk
σ : 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
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0
Theorem: MvPowerSeries.weightedOrder_mul_ge
Proof state before:
case h.mk
σ : 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
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0
Tactic:
by_cases hi : ↑(weight w i) < f.weightedOrder w
Proof state after:
case pos
σ : 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
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : ↑((weight w) i) < weightedOrder w f
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0

case neg
σ : 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
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : ¬↑((weight w) i) < weightedOrder w f
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0
Theorem: MvPowerSeries.weightedOrder_mul_ge
Proof state before:
case pos
σ : 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
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : ↑((weight w) i) < weightedOrder w f
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0
Tactic:
rw [coeff_of_lt_weightedOrder w f hi, MulZeroClass.zero_mul]
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_mul_ge
Proof state before:
case neg
σ : 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
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : ¬↑((weight w) i) < weightedOrder w f
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0
Tactic:
by_cases hj : ↑(weight w j) < g.weightedOrder w
Proof state after:
case pos
σ : 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
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : ¬↑((weight w) i) < weightedOrder w f
hj : ↑((weight w) j) < weightedOrder w g
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0

case neg
σ : 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
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : ¬↑((weight w) i) < weightedOrder w f
hj : ¬↑((weight w) j) < weightedOrder w g
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0
Theorem: MvPowerSeries.weightedOrder_mul_ge
Proof state before:
case pos
σ : 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
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : ¬↑((weight w) i) < weightedOrder w f
hj : ↑((weight w) j) < weightedOrder w g
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0
Tactic:
rw [coeff_of_lt_weightedOrder w g hj, MulZeroClass.mul_zero]
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_mul_ge
Proof state before:
case neg
σ : 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
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : ¬↑((weight w) i) < weightedOrder w f
hj : ¬↑((weight w) j) < weightedOrder w g
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0
Tactic:
rw [not_lt] at hi hj
Proof state after:
case neg
σ : 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
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : weightedOrder w f ≤ ↑((weight w) i)
hj : weightedOrder w g ≤ ↑((weight w) j)
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0
Theorem: MvPowerSeries.weightedOrder_mul_ge
Proof state before:
case neg
σ : 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
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : weightedOrder w f ≤ ↑((weight w) i)
hj : weightedOrder w g ≤ ↑((weight w) j)
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0
Tactic:
simp only [Finset.mem_antidiagonal] at hij
Proof state after:
case neg
σ : 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
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ ↑((weight w) i)
hj : weightedOrder w g ≤ ↑((weight w) j)
hij : i + j = d
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0
Theorem: MvPowerSeries.weightedOrder_mul_ge
Proof state before:
case neg
σ : 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
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ ↑((weight w) i)
hj : weightedOrder w g ≤ ↑((weight w) j)
hij : i + j = d
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0
Tactic:
exfalso
Proof state after:
case neg
σ : 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
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ ↑((weight w) i)
hj : weightedOrder w g ≤ ↑((weight w) j)
hij : i + j = d
⊢ False
Theorem: MvPowerSeries.weightedOrder_mul_ge
Proof state before:
case neg
σ : 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
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ ↑((weight w) i)
hj : weightedOrder w g ≤ ↑((weight w) j)
hij : i + j = d
⊢ False
Tactic:
apply ne_of_lt (lt_of_lt_of_le hd <| add_le_add hi hj)
Proof state after:
case neg
σ : 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
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ ↑((weight w) i)
hj : weightedOrder w g ≤ ↑((weight w) j)
hij : i + j = d
⊢ ↑((weight w) d) = ↑((weight w) i) + ↑((weight w) j)
Theorem: MvPowerSeries.weightedOrder_mul_ge
Proof state before:
case neg
σ : 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
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ ↑((weight w) i)
hj : weightedOrder w g ≤ ↑((weight w) j)
hij : i + j = d
⊢ ↑((weight w) d) = ↑((weight w) i) + ↑((weight w) j)
Tactic:
rw [← hij, map_add, Nat.cast_add]
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_monomial
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
⊢ weightedOrder w ((monomial α d) a) = if a = 0 then ⊤ else ↑((weight w) d)
Tactic:
split_ifs with h
Proof state after:
case pos
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : a = 0
⊢ weightedOrder w ((monomial α d) a) = ⊤

case neg
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ weightedOrder w ((monomial α d) a) = ↑((weight w) d)
Theorem: MvPowerSeries.weightedOrder_monomial
Proof state before:
case pos
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : a = 0
⊢ weightedOrder w ((monomial α d) a) = ⊤
Tactic:
rw [h, weightedOrder_eq_top_iff, LinearMap.map_zero]
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_monomial
Proof state before:
case neg
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ weightedOrder w ((monomial α d) a) = ↑((weight w) d)
Tactic:
rw [weightedOrder_eq_nat]
Proof state after:
case neg
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (∃ d_1, (weight w) d_1 = (weight w) d ∧ (coeff α d_1) ((monomial α d) a) ≠ 0) ∧
    ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff α d_1) ((monomial α d) a) = 0
Theorem: MvPowerSeries.weightedOrder_monomial
Proof state before:
case neg
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (∃ d_1, (weight w) d_1 = (weight w) d ∧ (coeff α d_1) ((monomial α d) a) ≠ 0) ∧
    ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff α d_1) ((monomial α d) a) = 0
Tactic:
constructor
Proof state after:
case neg.left
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∃ d_1, (weight w) d_1 = (weight w) d ∧ (coeff α d_1) ((monomial α d) a) ≠ 0

case neg.right
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff α d_1) ((monomial α d) a) = 0
Theorem: MvPowerSeries.weightedOrder_monomial
Proof state before:
case neg.left
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∃ d_1, (weight w) d_1 = (weight w) d ∧ (coeff α d_1) ((monomial α d) a) ≠ 0
Tactic:
use d
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (weight w) d = (weight w) d ∧ (coeff α d) ((monomial α d) a) ≠ 0
Theorem: MvPowerSeries.weightedOrder_monomial
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (weight w) d = (weight w) d ∧ (coeff α d) ((monomial α d) a) ≠ 0
Tactic:
simp only [coeff_monomial_same, eq_self_iff_true, ne_eq, true_and_iff]
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ¬a = 0
Theorem: MvPowerSeries.weightedOrder_monomial
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ¬a = 0
Tactic:
exact h
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_monomial
Proof state before:
case neg.right
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff α d_1) ((monomial α d) a) = 0
Tactic:
intro b hb
Proof state after:
case neg.right
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ (coeff α b) ((monomial α d) a) = 0
Theorem: MvPowerSeries.weightedOrder_monomial
Proof state before:
case neg.right
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ (coeff α b) ((monomial α d) a) = 0
Tactic:
rw [coeff_monomial, if_neg]
Proof state after:
case neg.right.hnc
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ ¬b = d
Theorem: MvPowerSeries.weightedOrder_monomial
Proof state before:
case neg.right.hnc
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ ¬b = d
Tactic:
intro h
Proof state after:
case neg.right.hnc
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h✝ : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
h : b = d
⊢ False
Theorem: MvPowerSeries.weightedOrder_monomial
Proof state before:
case neg.right.hnc
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h✝ : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
h : b = d
⊢ False
Tactic:
simp only [h, lt_self_iff_false] at hb
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_monomial_of_ne_zero
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
h : a ≠ 0
⊢ weightedOrder w ((monomial α d) a) = ↑((weight w) d)
Tactic:
classical
rw [weightedOrder_monomial, if_neg h]
Proof state after:
no goals
Theorem: MvPowerSeries.weightedOrder_monomial_of_ne_zero
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
h : a ≠ 0
⊢ weightedOrder w ((monomial α d) a) = ↑((weight w) d)
Tactic:
rw [weightedOrder_monomial, if_neg h]
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_mul_of_lt_weightedOrder
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ (coeff α d) (f * g) = 0
Tactic:
rw [coeff_mul]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ ∑ p ∈ Finset.antidiagonal d, (coeff α p.1) f * (coeff α p.2) g = 0
Theorem: MvPowerSeries.coeff_mul_of_lt_weightedOrder
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ ∑ p ∈ Finset.antidiagonal d, (coeff α p.1) f * (coeff α p.2) g = 0
Tactic:
apply 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 : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ ∀ x ∈ Finset.antidiagonal d, (coeff α x.1) f * (coeff α x.2) g = 0
Theorem: MvPowerSeries.coeff_mul_of_lt_weightedOrder
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ ∀ x ∈ Finset.antidiagonal d, (coeff α x.1) f * (coeff α x.2) g = 0
Tactic:
rintro ⟨i, j⟩ hij
Proof state after:
case h.mk
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0
Theorem: MvPowerSeries.coeff_mul_of_lt_weightedOrder
Proof state before:
case h.mk
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
⊢ (coeff α (i, j).1) f * (coeff α (i, j).2) g = 0
Tactic:
refine' mul_eq_zero_of_right (coeff α i f) _
Proof state after:
case h.mk
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
⊢ (coeff α (i, j).2) g = 0
Theorem: MvPowerSeries.coeff_mul_of_lt_weightedOrder
Proof state before:
case h.mk
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
⊢ (coeff α (i, j).2) g = 0
Tactic:
refine' coeff_of_lt_weightedOrder w g (lt_of_le_of_lt _ h)
Proof state after:
case h.mk
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
⊢ ↑((weight w) (i, j).2) ≤ ↑((weight w) d)
Theorem: MvPowerSeries.coeff_mul_of_lt_weightedOrder
Proof state before:
case h.mk
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
⊢ ↑((weight w) (i, j).2) ≤ ↑((weight w) d)
Tactic:
simp only [Finset.mem_antidiagonal] at hij
Proof state after:
case h.mk
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
i j : σ →₀ ℕ
hij : i + j = d
⊢ ↑((weight w) (i, j).2) ≤ ↑((weight w) d)
Theorem: MvPowerSeries.coeff_mul_of_lt_weightedOrder
Proof state before:
case h.mk
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : DecidableEq σ
f g : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
i j : σ →₀ ℕ
hij : i + j = d
⊢ ↑((weight w) (i, j).2) ≤ ↑((weight w) d)
Tactic:
simp only [Nat.cast_le, coe_le_coe, ← hij, map_add, le_add_iff_nonneg_left, zero_le']
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_mul_one_sub_of_lt_weightedOrder
Proof state before:
σ : Type u_1
α✝ : Type ?u.58468
inst✝² : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
inst✝¹ : DecidableEq σ
α : Type u_2
inst✝ : CommRing α
f g : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ (coeff α d) (f * (1 - g)) = (coeff α d) f
Tactic:
simp only [coeff_mul_of_lt_weightedOrder w f h, mul_sub, mul_one, _root_.map_sub, sub_zero]
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_mul_prod_one_sub_of_lt_weightedOrder
Proof state before:
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
⊢ (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f
Tactic:
refine' Finset.induction_on s _ _
Proof state after:
case refine'_1
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
⊢ (∀ i ∈ ∅, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ ∅, (1 - g i)) = (coeff α d) f

case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f) →
        (∀ i ∈ insert a s, ↑((weight w) d) < weightedOrder w (g i)) →
          (coeff α d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff α d) f
Theorem: MvPowerSeries.coeff_mul_prod_one_sub_of_lt_weightedOrder
Proof state before:
case refine'_1
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
⊢ (∀ i ∈ ∅, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ ∅, (1 - g i)) = (coeff α d) f
Tactic:
simp only [imp_true_iff, Finset.prod_empty, mul_one, eq_self_iff_true]
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_mul_prod_one_sub_of_lt_weightedOrder
Proof state before:
case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f) →
        (∀ i ∈ insert a s, ↑((weight w) d) < weightedOrder w (g i)) →
          (coeff α d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff α d) f
Tactic:
intro a s ha ih t
Proof state after:
case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s✝ : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f
t : ∀ i ∈ insert a s, ↑((weight w) d) < weightedOrder w (g i)
⊢ (coeff α d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff α d) f
Theorem: MvPowerSeries.coeff_mul_prod_one_sub_of_lt_weightedOrder
Proof state before:
case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s✝ : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f
t : ∀ i ∈ insert a s, ↑((weight w) d) < weightedOrder w (g i)
⊢ (coeff α d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff α d) f
Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at t
Proof state after:
case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s✝ : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f
t : ↑((weight w) d) < weightedOrder w (g a) ∧ ∀ a ∈ s, ↑((weight w) d) < weightedOrder w (g a)
⊢ (coeff α d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff α d) f