-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem le_order_mul (φ ψ : R⟦X⟧) : order φ + order ψ ≤ order (φ * ψ)

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : ¬↑i < φ.order
hj : ↑j < ψ.order
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Tactic:
rw [coeff_of_lt_order j hj, mul_zero]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : ↑i < φ.order
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Tactic:
rw [coeff_of_lt_order i hi, zero_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
⊢ φ.order + ψ.order ≤ (φ * ψ).order

Tactic:
apply le_order

Result:
case h
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
⊢ ∀ (i : ℕ), ↑i < φ.order + ψ.order → (coeff R i) (φ * ψ) = 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : ¬↑i < φ.order
hj : ¬↑j < ψ.order
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Tactic:
rw [not_lt] at hi hj

Result:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : ¬↑i < φ.order
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Tactic:
by_cases hj : ↑j < order ψ

Result:
case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : ¬↑i < φ.order
hj : ↑j < ψ.order
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : ¬↑i < φ.order
hj : ¬↑j < ψ.order
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ False

Tactic:
apply ne_of_lt (lt_of_lt_of_le hn <| add_le_add hi hj)

Result:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ ↑n = ↑i + ↑j

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
⊢ ∀ x ∈ antidiagonal n, (coeff R x.1) φ * (coeff R x.2) ψ = 0

Tactic:
rintro ⟨i, j⟩ hij

Result:
case h.mk
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
⊢ (coeff R n) (φ * ψ) = 0

Tactic:
rw [coeff_mul, Finset.sum_eq_zero]

Result:
case h
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
⊢ ∀ x ∈ antidiagonal n, (coeff R x.1) φ * (coeff R x.2) ψ = 0

Proof state:
case h.mk
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Tactic:
by_cases hi : ↑i < order φ

Result:
case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : ↑i < φ.order
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : ¬↑i < φ.order
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Tactic:
exfalso

Result:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ False

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
⊢ ∀ (i : ℕ), ↑i < φ.order + ψ.order → (coeff R i) (φ * ψ) = 0

Tactic:
intro n hn

Result:
case h
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
⊢ (coeff R n) (φ * ψ) = 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Tactic:
rw [mem_antidiagonal] at hij

Result:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ ↑n = ↑i + ↑j

Tactic:
rw [← Nat.cast_add, hij]

Result:
no goals