Theorem: MvPowerSeries.coeff_mul_of_lt_weightedOrder (DividedPowers/ForMathlib/MvPowerSeries/Order.lean)

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]
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

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
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

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
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

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) _
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

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)
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)

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
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)

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']
State after:
no goals