case a
α : Type u_1
β : Type u_2
γ : Type ?u.509507
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
x : β
⊢ x ∈ Finset.biUnion s f ∩ t ↔ x ∈ Finset.biUnion s fun x => f x ∩ t
α : Type u_1
β : Type u_2
γ : Type ?u.509507
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Finset.biUnion s f ∩ t = Finset.biUnion s fun x => f x ∩ t
ext x
case a
α : Type u_1
β : Type u_2
γ : Type ?u.509507
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
x : β
⊢ (∃ a, a ∈ s ∧ x ∈ f a) ∧ x ∈ t ↔ ∃ a, a ∈ s ∧ x ∈ f a ∧ x ∈ t
case a
α : Type u_1
β : Type u_2
γ : Type ?u.509507
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
x : β
⊢ x ∈ Finset.biUnion s f ∩ t ↔ x ∈ Finset.biUnion s fun x => f x ∩ t
simp only [mem_biUnion, mem_inter]
no goals
case a
α : Type u_1
β : Type u_2
γ : Type ?u.509507
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
x : β
⊢ (∃ a, a ∈ s ∧ x ∈ f a) ∧ x ∈ t ↔ ∃ a, a ∈ s ∧ x ∈ f a ∧ x ∈ t
tauto