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

State before:
α : Sort u_1
s t u : Set α
⊢ u.Subset s → u.Subset t → u.Subset (s.inter t)
Tactic:
intro hus hut x hxu
State after:
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ s.inter t

State before:
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ s.inter t
Tactic:
constructor
State after:
case left
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ s

case right
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ t

State before:
case left
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ s
Tactic:
exact hus x hxu
State after:
no goals

State before:
case right
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ t
Tactic:
exact hut x hxu
State after:
no goals