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

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