-- Mathlib/RingTheory/MvPowerSeries/Trunc.lean
theorem coeff_mul_eq_coeff_trunc'_mul_trunc' (n : σ →₀ ℕ)
    (f g : MvPowerSeries σ R) {m : σ →₀ ℕ} (h : m ≤ n) :
    coeff R m (f * g) = ((trunc' R n f) * (trunc' R n g)).coeff m

Proof state:
case mk.hy
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ (coeff R j) g = MvPolynomial.coeff j ((trunc' R n) g)

Tactic:
rw [coeff_trunc', if_pos (le_trans le_add_self h)]

Result:
no goals

Proof state:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ (coeff R i) f * (coeff R j) g = MvPolynomial.coeff i ((trunc' R n) f) * MvPolynomial.coeff j ((trunc' R n) g)

Tactic:
apply congr_arg₂

Result:
case mk.hx
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ (coeff R i) f = MvPolynomial.coeff i ((trunc' R n) f)

case mk.hy
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ (coeff R j) g = MvPolynomial.coeff j ((trunc' R n) g)

Proof state:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ (coeff R (i, j).1) f * (coeff R (i, j).2) g =
    MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g)

Tactic:
simp only

Result:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ (coeff R i) f * (coeff R j) g = MvPolynomial.coeff i ((trunc' R n) f) * MvPolynomial.coeff j ((trunc' R n) g)

Proof state:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ (coeff R (i, j).1) f * (coeff R (i, j).2) g =
    MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g)

Tactic:
simp only [mem_antidiagonal] at hij

Result:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
i j : σ →₀ ℕ
hij : i + j = m
⊢ (coeff R (i, j).1) f * (coeff R (i, j).2) g =
    MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ ∀ x ∈ antidiagonal m,
    (coeff R x.1) f * (coeff R x.2) g =
      MvPolynomial.coeff x.1 ((trunc' R n) f) * MvPolynomial.coeff x.2 ((trunc' R n) g)

Tactic:
rintro ⟨i, j⟩ hij

Result:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ (coeff R (i, j).1) f * (coeff R (i, j).2) g =
    MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ (coeff R m) (f * g) = MvPolynomial.coeff m ((trunc' R n) f * (trunc' R n) g)

Tactic:
simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ ∑ p ∈ antidiagonal m, (coeff R p.1) f * (coeff R p.2) g =
    ∑ x ∈ antidiagonal m, MvPolynomial.coeff x.1 ((trunc' R n) f) * MvPolynomial.coeff x.2 ((trunc' R n) g)

Proof state:
case mk.hx
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ (coeff R i) f = MvPolynomial.coeff i ((trunc' R n) f)

Tactic:
rw [coeff_trunc', if_pos (le_trans le_self_add h)]

Result:
no goals

Proof state:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
i j : σ →₀ ℕ
hij : i + j = m
⊢ (coeff R (i, j).1) f * (coeff R (i, j).2) g =
    MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g)

Tactic:
rw [← hij] at h

Result:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ (coeff R (i, j).1) f * (coeff R (i, j).2) g =
    MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ ∑ p ∈ antidiagonal m, (coeff R p.1) f * (coeff R p.2) g =
    ∑ x ∈ antidiagonal m, MvPolynomial.coeff x.1 ((trunc' R n) f) * MvPolynomial.coeff x.2 ((trunc' R n) g)

Tactic:
apply Finset.sum_congr rfl

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ ∀ x ∈ antidiagonal m,
    (coeff R x.1) f * (coeff R x.2) g =
      MvPolynomial.coeff x.1 ((trunc' R n) f) * MvPolynomial.coeff x.2 ((trunc' R n) g)