Disjoint union left

theorem disjoint_union_left {s₁ s₂ t : S} : (s₁ ∪ s₂) ## t ↔ s₁ ## t ∧ s₂ ## t := by  simp only [Disjoint.disjoint]  constructor  · intro h; constructor    · exact fun x ⟨hx1, hx2⟩ => h x ⟨(mem_union.mpr (.inl hx1)), hx2⟩    · exact fun x ⟨hx1, hx2⟩ => h x ⟨(mem_union.mpr (.inr hx1)), hx2⟩  · intro ⟨h1, h2⟩ x ⟨hx1, hx2⟩    rw [mem_union] at hx1    cases hx1 with    | inl hx1 => exact h1 x ⟨hx1, hx2⟩    | inr hx1 => exact h2 x ⟨hx1, hx2⟩