α : Type u_1
β : Type ?u.188858
γ : Type ?u.188861
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝ b : α
x y s t : Finset α
h : x ⊆ y
h' : s ⊆ t
a : α
a_in : a ∈ x ∩ s
⊢ a ∈ y ∩ t
α : Type u_1
β : Type ?u.188858
γ : Type ?u.188861
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a b : α
x y s t : Finset α
h : x ⊆ y
h' : s ⊆ t
⊢ x ∩ s ⊆ y ∩ t
intro a a_in
α : Type u_1
β : Type ?u.188858
γ : Type ?u.188861
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝ b : α
x y s t : Finset α
h : x ⊆ y
h' : s ⊆ t
a : α
a_in : a ∈ x ∧ a ∈ s
⊢ a ∈ y ∧ a ∈ t
α : Type u_1
β : Type ?u.188858
γ : Type ?u.188861
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝ b : α
x y s t : Finset α
h : x ⊆ y
h' : s ⊆ t
a : α
a_in : a ∈ x ∩ s
⊢ a ∈ y ∩ t
rw [Finset.mem_inter] at a_in ⊢
no goals
α : Type u_1
β : Type ?u.188858
γ : Type ?u.188861
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝ b : α
x y s t : Finset α
h : x ⊆ y
h' : s ⊆ t
a : α
a_in : a ∈ x ∧ a ∈ s
⊢ a ∈ y ∧ a ∈ t
exact ⟨h a_in.1, h' a_in.2⟩