-- 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 p ≤ toLex u
hv : toLex q ≤ toLex v
⊢ u = p ∧ v = q

Tactic:
constructor

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

case neg.right
σ : 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
⊢ v = q

Proof state:
case h₀.mk
σ : 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) ∈ Finset.antidiagonal (p + q)
h' : (u, v) ≠ (p, q)
⊢ (coeff R (u, v).1) φ * (coeff R (u, v).2) ψ = 0

Tactic:
simp only [Finset.mem_antidiagonal] at h

Result:
case h₀.mk
σ : 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
⊢ (coeff R (u, v).1) φ * (coeff R (u, v).2) ψ = 0

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)
⊢ ∑ p ∈ Finset.antidiagonal (p + q), (coeff R p.1) φ * (coeff R p.2) ψ = (coeff R p) φ * (coeff R q) ψ

Tactic:
apply Finset.sum_eq_single (⟨p, q⟩ : (σ →₀ ℕ) × (σ →₀ ℕ))

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)
⊢ ∀ b ∈ Finset.antidiagonal (p + q), b ≠ (p, q) → (coeff R b.1) φ * (coeff R b.2) ψ = 0

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

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
⊢ ↑(toLex u) < φ.lexOrder

Tactic:
simp only [hp, WithTop.coe_lt_coe, hu]

Result:
no goals