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

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

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

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

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

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

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

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

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

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

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

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

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

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