no goals
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝¹ : Finset α
t✝ : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq γ
f : α → β
s✝ : Finset α
t : β → Finset γ
this : DecidableEq α
a : α
s : Finset α
x✝ : ¬a ∈ s
ih : Finset.biUnion (image f s) t = Finset.biUnion s fun a => t (f a)
⊢ Finset.biUnion (image f (insert a s)) t = Finset.biUnion (insert a s) fun a => t (f a)
simp only [image_insert, biUnion_insert, ih]