-- Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
theorem lexOrder_mul [NoZeroDivisors R] (φ ψ : MvPowerSeries σ R) :
    lexOrder (φ * ψ) = lexOrder φ + lexOrder ψ

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

Tactic:
apply lexOrder_le_of_coeff_ne_zero (d := p + q)

Result:
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
hψ : ¬ψ = 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
q : σ →₀ ℕ
hq : ψ.lexOrder = ↑(toLex q)
⊢ (coeff R (p + q)) (φ * ψ) ≠ 0

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
hψ : ¬ψ = 0
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
rcases exists_finsupp_eq_lexOrder_of_ne_zero hφ with ⟨p, hp⟩

Result:
case neg.intro
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
hψ : ¬ψ = 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Proof state:
case neg.intro.intro
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
hψ : ¬ψ = 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
q : σ →₀ ℕ
hq : ψ.lexOrder = ↑(toLex q)
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
apply le_antisymm _ (lexOrder_mul_ge φ ψ)

Result:
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
hψ : ¬ψ = 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
q : σ →₀ ℕ
hq : ψ.lexOrder = ↑(toLex q)
⊢ (φ * ψ).lexOrder ≤ φ.lexOrder + ψ.lexOrder

Proof state:
case neg.intro
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
hψ : ¬ψ = 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
rcases exists_finsupp_eq_lexOrder_of_ne_zero hψ with ⟨q, hq⟩

Result:
case neg.intro.intro
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
hψ : ¬ψ = 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
q : σ →₀ ℕ
hq : ψ.lexOrder = ↑(toLex q)
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

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

Tactic:
rw [hp, hq]

Result:
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
hψ : ¬ψ = 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
q : σ →₀ ℕ
hq : ψ.lexOrder = ↑(toLex q)
⊢ (φ * ψ).lexOrder ≤ ↑(toLex p) + ↑(toLex q)

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ = 0
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
simp only [hφ, zero_mul, lexOrder_zero, top_add]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
hψ : ¬ψ = 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
q : σ →₀ ℕ
hq : ψ.lexOrder = ↑(toLex q)
⊢ (coeff R p) φ ≠ 0 ∧ (coeff R q) ψ ≠ 0

Tactic:
exact ⟨coeff_ne_zero_of_lexOrder hp.symm, coeff_ne_zero_of_lexOrder hq.symm⟩

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
by_cases hφ : φ = 0

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ = 0
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

case neg
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
by_cases hψ : ψ = 0

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
hψ : ψ = 0
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

case neg
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
hψ : ¬ψ = 0
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

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

Tactic:
rw [coeff_mul_of_add_lexOrder hp hq, mul_ne_zero_iff]

Result:
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
hψ : ¬ψ = 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
q : σ →₀ ℕ
hq : ψ.lexOrder = ↑(toLex q)
⊢ (coeff R p) φ ≠ 0 ∧ (coeff R q) ψ ≠ 0

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : ¬φ = 0
hψ : ψ = 0
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
simp only [hψ, mul_zero, lexOrder_zero, add_top]

Result:
no goals