∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) (x y : M),
  AddOpposite.unop ((⇑f ∘ AddOpposite.op) (x + y)) =
    AddOpposite.unop
      { unop' := (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) x + (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) y }