[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ ↑(opRingEquiv R) (op (↑(monomial n) r)) = ↑(monomial n) (op r)
[PROOFSTEP]
simp only [opRingEquiv, RingEquiv.coe_trans, Function.comp_apply, AddMonoidAlgebra.opRingEquiv_apply,
  RingEquiv.op_apply_apply, toFinsuppIso_apply, unop_op, toFinsupp_monomial, Finsupp.mapRange_single,
  toFinsuppIso_symm_apply, ofFinsupp_single]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ ↑(opRingEquiv R) (op (↑C r * X ^ n)) = ↑C (op r) * X ^ n
[PROOFSTEP]
simp only [X_pow_mul, op_mul, op_pow, map_mul, map_pow, opRingEquiv_op_X, opRingEquiv_op_C]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : Rᵐᵒᵖ
⊢ ↑(opRingEquiv R) (↑(RingEquiv.symm (opRingEquiv R)) (↑(monomial n) r)) =
    ↑(opRingEquiv R) (op (↑(monomial n) (unop r)))
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : Rᵐᵒᵖ
n : ℕ
⊢ ↑(RingEquiv.symm (opRingEquiv R)) (↑C r * X ^ n) = op (↑C (unop r) * X ^ n)
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, opRingEquiv_symm_monomial, C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
n : ℕ
⊢ coeff (↑(opRingEquiv R) p) n = op (coeff (unop p) n)
[PROOFSTEP]
induction' p using MulOpposite.rec' with p
[GOAL]
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)
[PROOFSTEP]
cases p
[GOAL]
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)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ support (↑(opRingEquiv R) p) = support (unop p)
[PROOFSTEP]
induction' p using MulOpposite.rec' with p
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ support (↑(opRingEquiv R) (op p)) = support (unop (op p))
[PROOFSTEP]
cases p
[GOAL]
case h.ofFinsupp
R : Type u_1
inst✝ : Semiring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (↑(opRingEquiv R) (op { toFinsupp := toFinsupp✝ })) = support (unop (op { toFinsupp := toFinsupp✝ }))
[PROOFSTEP]
exact Finsupp.support_mapRange_of_injective (map_zero _) _ op_injective
[GOAL]
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ natDegree (↑(opRingEquiv R) p) = natDegree (unop p)
[PROOFSTEP]
by_cases p0 : p = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : p = 0
⊢ natDegree (↑(opRingEquiv R) p) = natDegree (unop p)
[PROOFSTEP]
simp only [p0, _root_.map_zero, natDegree_zero, unop_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : ¬p = 0
⊢ natDegree (↑(opRingEquiv R) p) = natDegree (unop p)
[PROOFSTEP]
simp only [p0, natDegree_eq_support_max', Ne.def, AddEquivClass.map_eq_zero_iff, not_false_iff, support_opRingEquiv,
  unop_eq_zero_iff]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ leadingCoeff (↑(opRingEquiv R) p) = op (leadingCoeff (unop p))
[PROOFSTEP]
rw [leadingCoeff, coeff_opRingEquiv, natDegree_opRingEquiv, leadingCoeff]
