-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem trunc_C_mul_T (n : ℤ) (r : R) : trunc (C r * T n) = ite (0 ≤ n) (monomial n.toNat r) 0

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
⊢ (toFinsuppIso R) ((toFinsuppIso R).symm.toAddMonoidHom ((comapDomain.addMonoidHom ⋯) (Finsupp.single n r))) =
    (toFinsuppIso R) (if 0 ≤ n then (monomial n.toNat) r else 0)

Tactic:
erw [comapDomain.addMonoidHom_apply Int.ofNat_injective]

Result:
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
⊢ comapDomain Int.ofNat (Finsupp.single n r) ⋯ = (toFinsuppIso R) (if 0 ≤ n then (monomial n.toNat) r else 0)

Proof state:
case pos.intro
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ comapDomain Int.ofNat (Finsupp.single (↑n) r) ⋯ = Finsupp.single (↑n).toNat r

Tactic:
apply comapDomain_single

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
⊢ trunc (C r * T n) = if 0 ≤ n then (monomial n.toNat) r else 0

Tactic:
apply (toFinsuppIso R).injective

Result:
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
⊢ (toFinsuppIso R) (trunc (C r * T n)) = (toFinsuppIso R) (if 0 ≤ n then (monomial n.toNat) r else 0)

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
⊢ (toFinsuppIso R) (trunc (C r * T n)) = (toFinsuppIso R) (if 0 ≤ n then (monomial n.toNat) r else 0)

Tactic:
rw [← single_eq_C_mul_T, trunc, AddMonoidHom.coe_comp, Function.comp_apply]

Result:
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
⊢ (toFinsuppIso R) ((toFinsuppIso R).symm.toAddMonoidHom ((comapDomain.addMonoidHom ⋯) (Finsupp.single n r))) =
    (toFinsuppIso R) (if 0 ≤ n then (monomial n.toNat) r else 0)

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
n0 : 0 ≤ n
⊢ comapDomain Int.ofNat (Finsupp.single n r) ⋯ = ((monomial n.toNat) r).toFinsupp

Tactic:
rw [toFinsupp_monomial]

Result:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
n0 : 0 ≤ n
⊢ comapDomain Int.ofNat (Finsupp.single n r) ⋯ = Finsupp.single n.toNat r

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
a : ℕ
this : n ≠ ↑a
⊢ { toFinsupp := comapDomain Int.ofNat (Finsupp.single n r) ⋯ }.coeff a = coeff 0 a

Tactic:
simp only [coeff_ofFinsupp, comapDomain_apply, Int.ofNat_eq_coe, coeff_zero,
  single_eq_of_ne this]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
a : ℕ
⊢ n ≠ ↑a

Tactic:
omega

Result:
no goals

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
a : ℕ
⊢ { toFinsupp := comapDomain Int.ofNat (Finsupp.single n r) ⋯ }.coeff a = coeff 0 a

Tactic:
have : n ≠ a := by omega

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
a : ℕ
this : n ≠ ↑a
⊢ { toFinsupp := comapDomain Int.ofNat (Finsupp.single n r) ⋯ }.coeff a = coeff 0 a

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
⊢ comapDomain Int.ofNat (Finsupp.single n r) ⋯ = toFinsupp 0

Tactic:
rw [toFinsupp_inj]

Result:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
⊢ { toFinsupp := comapDomain Int.ofNat (Finsupp.single n r) ⋯ } = 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
n0 : 0 ≤ n
⊢ comapDomain Int.ofNat (Finsupp.single n r) ⋯ = Finsupp.single n.toNat r

Tactic:
lift n to ℕ using n0

Result:
case pos.intro
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ comapDomain Int.ofNat (Finsupp.single (↑n) r) ⋯ = Finsupp.single (↑n).toNat r

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
⊢ comapDomain Int.ofNat (Finsupp.single n r) ⋯ = (if 0 ≤ n then (monomial n.toNat) r else 0).toFinsupp

Tactic:
split_ifs with n0

Result:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
n0 : 0 ≤ n
⊢ comapDomain Int.ofNat (Finsupp.single n r) ⋯ = ((monomial n.toNat) r).toFinsupp

case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
⊢ comapDomain Int.ofNat (Finsupp.single n r) ⋯ = toFinsupp 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
⊢ { toFinsupp := comapDomain Int.ofNat (Finsupp.single n r) ⋯ } = 0

Tactic:
ext a

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
a : ℕ
⊢ { toFinsupp := comapDomain Int.ofNat (Finsupp.single n r) ⋯ }.coeff a = coeff 0 a

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
⊢ comapDomain Int.ofNat (Finsupp.single n r) ⋯ = (toFinsuppIso R) (if 0 ≤ n then (monomial n.toNat) r else 0)

Tactic:
rw [toFinsuppIso_apply]

Result:
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
⊢ comapDomain Int.ofNat (Finsupp.single n r) ⋯ = (if 0 ≤ n then (monomial n.toNat) r else 0).toFinsupp