α : Type u_2
β : Type u_1
γ : Type ?u.518185
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t✝ t₁ t₂ t : α → Finset β
h : s₁ ⊆ s₂
x : β
⊢ x ∈ Finset.biUnion s₁ t → x ∈ Finset.biUnion s₂ t
α : Type u_2
β : Type u_1
γ : Type ?u.518185
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t✝ t₁ t₂ t : α → Finset β
h : s₁ ⊆ s₂
⊢ Finset.biUnion s₁ t ⊆ Finset.biUnion s₂ t
intro x
α : Type u_2
β : Type u_1
γ : Type ?u.518185
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t✝ t₁ t₂ t : α → Finset β
h : s₁ ⊆ s₂
x : β
⊢ (∃ a, a ∈ s₁ ∧ x ∈ t a) → ∃ a, a ∈ s₂ ∧ x ∈ t a
α : Type u_2
β : Type u_1
γ : Type ?u.518185
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t✝ t₁ t₂ t : α → Finset β
h : s₁ ⊆ s₂
x : β
⊢ x ∈ Finset.biUnion s₁ t → x ∈ Finset.biUnion s₂ t
simp only [and_imp, mem_biUnion, exists_prop]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.518185
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t✝ t₁ t₂ t : α → Finset β
h : s₁ ⊆ s₂
x : β
⊢ (∃ a, a ∈ s₁ ∧ x ∈ t a) → ∃ a, a ∈ s₂ ∧ x ∈ t a
exact Exists.imp fun a ha => ⟨h ha.1, ha.2⟩