Theorem: MvPowerSeries.coeff_mul_trunc' (DividedPowers/ForMathlib/RingTheory/MvPowerSeries/Trunc.lean)

State before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ MvPolynomial.coeff m ((trunc' R n) f * (trunc' R n) g) = (coeff R m) (f * g)
Tactic:
classical
simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]
apply Finset.sum_congr rfl
rintro ⟨i, j⟩ hij
simp only [mem_antidiagonal] at hij
rw [← hij] at h
simp only
apply congr_arg₂
rw [coeff_trunc', if_pos (le_trans le_self_add h)]
rw [coeff_trunc', if_pos (le_trans le_add_self h)]
State after:
no goals

State before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ MvPolynomial.coeff m ((trunc' R n) f * (trunc' R n) g) = (coeff R m) (f * g)
Tactic:
simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]
State after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ ∑ x ∈ antidiagonal m, MvPolynomial.coeff x.1 ((trunc' R n) f) * MvPolynomial.coeff x.2 ((trunc' R n) g) =
    ∑ p ∈ antidiagonal m, (coeff R p.1) f * (coeff R p.2) g

State before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ ∑ x ∈ antidiagonal m, MvPolynomial.coeff x.1 ((trunc' R n) f) * MvPolynomial.coeff x.2 ((trunc' R n) g) =
    ∑ p ∈ antidiagonal m, (coeff R p.1) f * (coeff R p.2) g
Tactic:
apply Finset.sum_congr rfl
State after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ ∀ x ∈ antidiagonal m,
    MvPolynomial.coeff x.1 ((trunc' R n) f) * MvPolynomial.coeff x.2 ((trunc' R n) g) =
      (coeff R x.1) f * (coeff R x.2) g

State before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ ∀ x ∈ antidiagonal m,
    MvPolynomial.coeff x.1 ((trunc' R n) f) * MvPolynomial.coeff x.2 ((trunc' R n) g) =
      (coeff R x.1) f * (coeff R x.2) g
Tactic:
rintro ⟨i, j⟩ hij
State after:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g) =
    (coeff R (i, j).1) f * (coeff R (i, j).2) g

State before:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g) =
    (coeff R (i, j).1) f * (coeff R (i, j).2) g
Tactic:
simp only [mem_antidiagonal] at hij
State after:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
i j : σ →₀ ℕ
hij : i + j = m
⊢ MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g) =
    (coeff R (i, j).1) f * (coeff R (i, j).2) g

State before:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
i j : σ →₀ ℕ
hij : i + j = m
⊢ MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g) =
    (coeff R (i, j).1) f * (coeff R (i, j).2) g
Tactic:
rw [← hij] at h
State after:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g) =
    (coeff R (i, j).1) f * (coeff R (i, j).2) g

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

State before:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff i ((trunc' R n) f) * MvPolynomial.coeff j ((trunc' R n) g) = (coeff R i) f * (coeff R j) g
Tactic:
apply congr_arg₂
State after:
case mk.hx
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff i ((trunc' R n) f) = (coeff R i) f

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

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

case mk.hy
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff j ((trunc' R n) g) = (coeff R j) g
Tactic:
rw [coeff_trunc', if_pos (le_trans le_self_add h)]
State after:
case mk.hy
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff j ((trunc' R n) g) = (coeff R j) g

State before:
case mk.hy
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff j ((trunc' R n) g) = (coeff R j) g
Tactic:
rw [coeff_trunc', if_pos (le_trans le_add_self h)]
State after:
no goals