alignments from lean 3 init.data.prod

ink

@[simp]

theorem Prod.mk.eta {α : Type u} {β : Type v} {p : α × β} : (p.fst, p.snd) = p