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