[GOAL]
R✝ : Type u_1
S : Type u_2
A✝ : Type u_3
B : Type u_4
inst✝¹² : CommSemiring R✝
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R✝ S
inst✝⁷ : Algebra R✝ A✝
inst✝⁶ : Algebra R✝ B
inst✝⁵ : Algebra S A✝
inst✝⁴ : SMulCommClass R✝ S A✝
inst✝³ : IsScalarTower R✝ S A✝
R : Type ?u.2035
A : Type ?u.2038
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
x : A
⊢ ↑(RingHom.toOpposite (algebraMap R A)
            (_ :
              ∀ (x y : R),
                ↑(algebraMap R ((fun x => A) x)) x * ↑(algebraMap R A) y =
                  ↑(algebraMap R A) y * ↑(algebraMap R ((fun x => A) x)) x))
        r *
      op x =
    op x *
      ↑(RingHom.toOpposite (algebraMap R A)
            (_ :
              ∀ (x y : R),
                ↑(algebraMap R ((fun x => A) x)) x * ↑(algebraMap R A) y =
                  ↑(algebraMap R A) y * ↑(algebraMap R ((fun x => A) x)) x))
        r
[PROOFSTEP]
simp only [RingHom.toOpposite_apply, Function.comp_apply, ← op_mul, Algebra.commutes]
[GOAL]
R✝ : Type u_1
S : Type u_2
A✝ : Type u_3
B : Type u_4
inst✝¹² : CommSemiring R✝
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R✝ S
inst✝⁷ : Algebra R✝ A✝
inst✝⁶ : Algebra R✝ B
inst✝⁵ : Algebra S A✝
inst✝⁴ : SMulCommClass R✝ S A✝
inst✝³ : IsScalarTower R✝ S A✝
R : Type ?u.2035
A : Type ?u.2038
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
c : R
x : (fun x => Aᵐᵒᵖ) c
⊢ unop (c • x) =
    unop
      (↑(RingHom.toOpposite (algebraMap R A)
              (_ :
                ∀ (x y : R),
                  ↑(algebraMap R ((fun x => A) x)) x * ↑(algebraMap R A) y =
                    ↑(algebraMap R A) y * ↑(algebraMap R ((fun x => A) x)) x))
          c *
        x)
[PROOFSTEP]
simp only [unop_smul, RingHom.toOpposite_apply, Function.comp_apply, unop_mul, op_mul, Algebra.smul_def,
  Algebra.commutes, op_unop, unop_op]
