∀ {ι : Type u_1} (A₁ : ι → Type u_2) [inst : (i : ι) → Semiring (A₁ i)] (x y : ((i : ι) → A₁ i)ᵐᵒᵖ),
  (RingEquiv.piMulOpposite A₁).toFun (x * y) =
    (RingEquiv.piMulOpposite A₁).toFun x * (RingEquiv.piMulOpposite A₁).toFun y