Theorem: MProd.neg_mk (SciLean/Core/Monads/MProd.lean)

State before:
X Y : Type u_1
inst✝¹ : Neg X
inst✝ : Neg Y
x : X
y : Y
⊢ -{ fst := x, snd := y } = { fst := -x, snd := -y }
Tactic:
rfl
State after:
no goals