R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
⊢ ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
have : Function.Injective Int.ofNat := fun x y h => Int.ofNat_inj.mp h
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ ↑(toFinsuppIso R) (↑trunc (↑C r * T n)) = ↑(toFinsuppIso R) (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0)
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
apply (toFinsuppIso R).injective
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ ↑(toFinsuppIso R)
      (↑(RingEquiv.toAddMonoidHom (RingEquiv.symm (toFinsuppIso R)))
        (↑(comapDomain.addMonoidHom trunc.proof_1) (Finsupp.single n r))) =
    ↑(toFinsuppIso R) (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0)
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ ↑(toFinsuppIso R) (↑trunc (↑C r * T n)) = ↑(toFinsuppIso R) (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0)
rw [← single_eq_C_mul_T, trunc, AddMonoidHom.coe_comp, Function.comp_apply]
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    ↑(toFinsuppIso R) (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0)
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ ↑(toFinsuppIso R)
      (↑(RingEquiv.toAddMonoidHom (RingEquiv.symm (toFinsuppIso R)))
        (↑(comapDomain.addMonoidHom trunc.proof_1) (Finsupp.single n r))) =
    ↑(toFinsuppIso R) (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0)
erw [comapDomain.addMonoidHom_apply this]
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    ↑(toFinsuppIso R) (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0)
rw [toFinsuppIso_apply]
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : 0 ≤ n
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp

case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
by_cases n0 : 0 ≤ n
case pos.intro
R : Type u_1
inst✝ : Semiring R
r : R
this : Function.Injective Int.ofNat
n : ℕ
⊢ comapDomain Int.ofNat (Finsupp.single (↑n) r)
      (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single (↑n) r).support)) =
    (if 0 ≤ ↑n then ↑(monomial (Int.toNat ↑n)) r else 0).toFinsupp
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : 0 ≤ n
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
lift n to ℕ using n0
case pos.intro
R : Type u_1
inst✝ : Semiring R
r : R
this : Function.Injective Int.ofNat
n : ℕ
⊢ Finsupp.single n r = (if 0 ≤ ↑n then ↑(monomial (Int.toNat ↑n)) r else 0).toFinsupp
case pos.intro
R : Type u_1
inst✝ : Semiring R
r : R
this : Function.Injective Int.ofNat
n : ℕ
⊢ comapDomain Int.ofNat (Finsupp.single (↑n) r)
      (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single (↑n) r).support)) =
    (if 0 ≤ ↑n then ↑(monomial (Int.toNat ↑n)) r else 0).toFinsupp
erw [comapDomain_single]
no goals
case pos.intro
R : Type u_1
inst✝ : Semiring R
r : R
this : Function.Injective Int.ofNat
n : ℕ
⊢ Finsupp.single n r = (if 0 ≤ ↑n then ↑(monomial (Int.toNat ↑n)) r else 0).toFinsupp
simp only [Nat.cast_nonneg, Int.toNat_ofNat, ite_true, toFinsupp_monomial]
case neg.intro
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
lift -n to ℕ using (neg_pos.mpr (not_le.mp n0)).le with m
case neg.intro
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
⊢ {
      toFinsupp :=
        comapDomain Int.ofNat (Finsupp.single n r)
          (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) } =
    0
case neg.intro
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
rw [toFinsupp_inj, if_neg n0]
case neg.intro.a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
a : ℕ
⊢ coeff
      {
        toFinsupp :=
          comapDomain Int.ofNat (Finsupp.single n r)
            (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) }
      a =
    coeff 0 a
case neg.intro
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
⊢ {
      toFinsupp :=
        comapDomain Int.ofNat (Finsupp.single n r)
          (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) } =
    0
ext a
case neg.intro.a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this✝ : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
a : ℕ
this : n ≠ ↑a
⊢ coeff
      {
        toFinsupp :=
          comapDomain Int.ofNat (Finsupp.single n r)
            (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) }
      a =
    coeff 0 a
case neg.intro.a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
a : ℕ
⊢ coeff
      {
        toFinsupp :=
          comapDomain Int.ofNat (Finsupp.single n r)
            (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) }
      a =
    coeff 0 a
have := ((not_le.mp n0).trans_le (Int.ofNat_zero_le a)).ne
no goals
case neg.intro.a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this✝ : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
a : ℕ
this : n ≠ ↑a
⊢ coeff
      {
        toFinsupp :=
          comapDomain Int.ofNat (Finsupp.single n r)
            (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) }
      a =
    coeff 0 a
simp only [coeff_ofFinsupp, comapDomain_apply, Int.ofNat_eq_coe, coeff_zero,
  single_eq_of_ne this]