Theorem: Set.union_subset_of_subset_of_subset (GMLInit/Data/Set/Subset.lean)

State before:
α : Sort u_1
s t u : Set α
⊢ s.Subset u → t.Subset u → (s.union t).Subset u
Tactic:
intro hsu htu x
State after:
α : Sort u_1
s t u : Set α
hsu : s.Subset u
htu : t.Subset u
x : α
⊢ x ∈ s.union t → x ∈ u

State before:
α : Sort u_1
s t u : Set α
hsu : s.Subset u
htu : t.Subset u
x : α
⊢ x ∈ s.union t → x ∈ u
Tactic:
intro
| Or.inl hxs =>
  exact hsu x hxs
| Or.inr hxt =>
  exact htu x hxt
State after:
no goals

State before:
α : Sort u_1
s t u : Set α
hsu : s.Subset u
htu : t.Subset u
x : α
x✝ : x ∈ s.union t
hxs : x ∈ s
⊢ x ∈ u
Tactic:
exact hsu x hxs
State after:
no goals

State before:
α : Sort u_1
s t u : Set α
hsu : s.Subset u
htu : t.Subset u
x : α
x✝ : x ∈ s.union t
hxt : x ∈ t
⊢ x ∈ u
Tactic:
exact htu x hxt
State after:
no goals