English
Equivalent formulation of the previous fact: u = s ⊎ t iff u^{toLeft} = s and u^{toRight} = t.
Русский
Эквивалентная формулировка предыдущего факта: u = s ⊎ t, если и только если u^{toLeft} = s и u^{toRight} = t.
LaTeX
$$u = s \uplus t \iff u^{\mathrm{toLeft}} = s \land u^{\mathrm{toRight}} = t$$
Lean4
theorem eq_disjSum_iff : u = s.disjSum t ↔ u.toLeft = s ∧ u.toRight = t :=
⟨fun h => by simp [h], fun h => by simp [← h, toLeft_disjSum_toRight]⟩