α : Type u_2
β : Type u_1
γ : Type ?u.507429
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s' : Finset β
⊢ (∀ ⦃x : β⦄, (∃ a, a ∈ s ∧ x ∈ t a) → x ∈ s') ↔ ∀ (x : α), x ∈ s → ∀ ⦃x_1 : β⦄, x_1 ∈ t x → x_1 ∈ s'
α : Type u_2
β : Type u_1
γ : Type ?u.507429
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s' : Finset β
⊢ Finset.biUnion s t ⊆ s' ↔ ∀ (x : α), x ∈ s → t x ⊆ s'
simp only [subset_iff, mem_biUnion]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.507429
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s' : Finset β
⊢ (∀ ⦃x : β⦄, (∃ a, a ∈ s ∧ x ∈ t a) → x ∈ s') ↔ ∀ (x : α), x ∈ s → ∀ ⦃x_1 : β⦄, x_1 ∈ t x → x_1 ∈ s'
exact ⟨fun H a ha b hb => H ⟨a, ha, hb⟩, fun H b ⟨a, ha, hb⟩ => H a ha hb⟩