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

State before:
X Y : Type u_1
inst✝¹ : Sub X
inst✝ : Sub 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