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

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