case h
R : Type u_1
inst✝ : Semiring R
n : ℕ
p : R[X]
⊢ coeff (↑(opRingEquiv R) (op p)) n = op (coeff (unop (op p)) n)
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
n : ℕ
⊢ coeff (↑(opRingEquiv R) p) n = op (coeff (unop p) n)
induction' p using MulOpposite.rec' with p
case h.ofFinsupp
R : Type u_1
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (↑(opRingEquiv R) (op { toFinsupp := toFinsupp✝ })) n = op (coeff (unop (op { toFinsupp := toFinsupp✝ })) n)
case h
R : Type u_1
inst✝ : Semiring R
n : ℕ
p : R[X]
⊢ coeff (↑(opRingEquiv R) (op p)) n = op (coeff (unop (op p)) n)
cases p
no goals
case h.ofFinsupp
R : Type u_1
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (↑(opRingEquiv R) (op { toFinsupp := toFinsupp✝ })) n = op (coeff (unop (op { toFinsupp := toFinsupp✝ })) n)
rfl