no goals
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a : R
ha : a ≠ 0
i j : ℕ
⊢ ↑(monomial i) a = ↑(monomial j) a ↔ i = j
rw [← ofFinsupp_single, ← ofFinsupp_single, ofFinsupp.injEq, Finsupp.single_left_inj ha]