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

State before:
X Y : Type u_1
x : X
y : Y
⊢ { fst := x, snd := y }.snd = y
Tactic:
simp
State after:
no goals