R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ Finset.max (↑C a * T n).support = ↑n
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ degree (↑C a * T n) = ↑n
rw [degree]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
this : (↑C a * T n).support = {n}
⊢ Finset.max (↑C a * T n).support = ↑n
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ Finset.max (↑C a * T n).support = ↑n
have : Finsupp.support (C a * T n) = {n} := by
  refine' support_eq_singleton.mpr _
  rw [← single_eq_C_mul_T]
  simp only [single_eq_same, a0, Ne.def, not_false_iff, eq_self_iff_true, and_self_iff]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
this : (↑C a * T n).support = {n}
⊢ Finset.max {n} = ↑n
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
this : (↑C a * T n).support = {n}
⊢ Finset.max (↑C a * T n).support = ↑n
rw [this]
no goals
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
this : (↑C a * T n).support = {n}
⊢ Finset.max {n} = ↑n
exact Finset.max_singleton
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ ↑(↑C a * T n) n ≠ 0 ∧ ↑C a * T n = Finsupp.single n (↑(↑C a * T n) n)
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ (↑C a * T n).support = {n}
refine' support_eq_singleton.mpr _
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ ↑(Finsupp.single n a) n ≠ 0 ∧ Finsupp.single n a = Finsupp.single n (↑(Finsupp.single n a) n)
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ ↑(↑C a * T n) n ≠ 0 ∧ ↑C a * T n = Finsupp.single n (↑(↑C a * T n) n)
rw [← single_eq_C_mul_T]
no goals
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ ↑(Finsupp.single n a) n ≠ 0 ∧ Finsupp.single n a = Finsupp.single n (↑(Finsupp.single n a) n)
simp only [single_eq_same, a0, Ne.def, not_false_iff, eq_self_iff_true, and_self_iff]