Theorem: union_elem_uplus (Pdl/Discon.lean)

State before:
XS YS : Finset (Finset Formula)
X Y : Finset Formula
⊢ X ∈ XS → Y ∈ YS → X ∪ Y ∈ XS⊎YS
Tactic:
intro X_in Y_in
State after:
XS YS : Finset (Finset Formula)
X Y : Finset Formula
X_in : X ∈ XS
Y_in : Y ∈ YS
⊢ X ∪ Y ∈ XS⊎YS

State before:
XS YS : Finset (Finset Formula)
X Y : Finset Formula
X_in : X ∈ XS
Y_in : Y ∈ YS
⊢ X ∪ Y ∈ XS⊎YS
Tactic:
simp
State after:
XS YS : Finset (Finset Formula)
X Y : Finset Formula
X_in : X ∈ XS
Y_in : Y ∈ YS
⊢ ∃ a ∈ XS, ∃ a_1 ∈ YS, X ∪ Y = a ∪ a_1

State before:
XS YS : Finset (Finset Formula)
X Y : Finset Formula
X_in : X ∈ XS
Y_in : Y ∈ YS
⊢ ∃ a ∈ XS, ∃ a_1 ∈ YS, X ∪ Y = a ∪ a_1
Tactic:
exact ⟨X, X_in, Y, Y_in, rfl⟩
State after:
no goals