no goals
α : Type u_2
β : Type u_1
γ : Type ?u.508302
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
a : α
⊢ Finset.biUnion {a} t = t a
classical rw [← insert_emptyc_eq, biUnion_insert, biUnion_empty, union_empty]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.508302
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
a : α
⊢ Finset.biUnion {a} t = t a
rw [← insert_emptyc_eq, biUnion_insert, biUnion_empty, union_empty]