-- Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
theorem coeff_mul_of_add_lexOrder {φ ψ : MvPowerSeries σ R}
    {p q : σ →₀ ℕ} (hp : lexOrder φ = toLex p) (hq : lexOrder ψ = toLex q) :
    coeff R (p + q) (φ * ψ) = coeff R p φ * coeff R q ψ

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : ¬toLex u < toLex p
⊢ (coeff R u) φ * (coeff R v) ψ = 0

Tactic:
rw [coeff_eq_zero_of_lt_lexOrder (d := v), mul_zero]

Result:
case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : ¬toLex u < toLex p
⊢ ↑(toLex v) < ψ.lexOrder

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : ¬toLex u < toLex p
⊢ ↑(toLex v) < ψ.lexOrder

Tactic:
simp only [hq, WithTop.coe_lt_coe, ← not_le]

Result:
case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : ¬toLex u < toLex p
⊢ ¬↑(toLex q) ≤ ↑(toLex v)

Proof state:
case h₁
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
⊢ (p, q) ∉ Finset.antidiagonal (p + q) → (coeff R (p, q).1) φ * (coeff R (p, q).2) ψ = 0

Tactic:
intro h

Result:
case h₁
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
h : (p, q) ∉ Finset.antidiagonal (p + q)
⊢ (coeff R (p, q).1) φ * (coeff R (p, q).2) ψ = 0

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : toLex p ≤ toLex u
hv : toLex q ≤ toLex v
⊢ (u, v) = (p, q)

Tactic:
simp only [Prod.mk.injEq]

Result:
case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : toLex p ≤ toLex u
hv : toLex q ≤ toLex v
⊢ u = p ∧ v = q

Proof state:
case h₁
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
h : (p, q) ∉ Finset.antidiagonal (p + q)
⊢ (coeff R (p, q).1) φ * (coeff R (p, q).2) ψ = 0

Tactic:
simp only [Finset.mem_antidiagonal, not_true_eq_false] at h

Result:
no goals

Proof state:
case neg.left.a
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : toLex p ≤ toLex u
hv : toLex q ≤ toLex v
⊢ ¬toLex p < toLex u

Tactic:
intro hu'

Result:
case neg.left.a
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : toLex p ≤ toLex u
hv : toLex q ≤ toLex v
hu' : toLex p < toLex u
⊢ False

Proof state:
case neg.right.a
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : toLex p ≤ toLex u
hv : toLex q ≤ toLex v
⊢ ¬toLex q < toLex v

Tactic:
intro hv'

Result:
case neg.right.a
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : toLex p ≤ toLex u
hv : toLex q ≤ toLex v
hv' : toLex q < toLex v
⊢ False

Proof state:
case neg.left.a
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : toLex p ≤ toLex u
hv : toLex q ≤ toLex v
hu' : toLex p < toLex u
⊢ False

Tactic:
exact not_le.mpr (add_lt_add_of_lt_of_le hu' hv) (le_of_eq h)

Result:
no goals

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : toLex u < toLex p
⊢ (coeff R u) φ * (coeff R v) ψ = 0

Tactic:
rw [coeff_eq_zero_of_lt_lexOrder (R := R) (d := u), zero_mul]

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : toLex u < toLex p
⊢ ↑(toLex u) < φ.lexOrder

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
⊢ (coeff R (p + q)) (φ * ψ) = (coeff R p) φ * (coeff R q) ψ

Tactic:
rw [coeff_mul]

Result:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
⊢ ∑ p ∈ Finset.antidiagonal (p + q), (coeff R p.1) φ * (coeff R p.2) ψ = (coeff R p) φ * (coeff R q) ψ

Proof state:
case neg.left
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : toLex p ≤ toLex u
hv : toLex q ≤ toLex v
⊢ u = p

Tactic:
apply toLex.injective

Result:
case neg.left.a
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : toLex p ≤ toLex u
hv : toLex q ≤ toLex v
⊢ toLex u = toLex p

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : toLex p ≤ toLex u
hv : ↑(toLex q) ≤ ↑(toLex v)
⊢ False

Tactic:
simp only [WithTop.coe_le_coe] at hv

Result:
case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
hu : toLex p ≤ toLex u
hv : toLex q ≤ toLex v
⊢ False