no goals
α : Type u_3
α' : Type ?u.52126
β : Type u_1
β' : Type ?u.52132
γ : Type u_2
γ' : Type ?u.52138
δ : Type ?u.52141
δ' : Type ?u.52144
ε : Type ?u.52147
ε' : Type ?u.52150
ζ : Type ?u.52153
ζ' : Type ?u.52156
ν : Type ?u.52159
inst✝⁸ : DecidableEq α'
inst✝⁷ : DecidableEq β'
inst✝⁶ : DecidableEq γ
inst✝⁵ : DecidableEq γ'
inst✝⁴ : DecidableEq δ
inst✝³ : DecidableEq δ'
inst✝² : DecidableEq ε
inst✝¹ : DecidableEq ε'
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Finset α
t t' : Finset β
u u' : Finset γ
a a' : α
b b' : β
c : γ
inst✝ : DecidableEq β
t₁ t₂ : Finset β
hf : Injective (f a)
⊢ image₂ f {a} (t₁ ∩ t₂) = image₂ f {a} t₁ ∩ image₂ f {a} t₂
simp_rw [image₂_singleton_left, image_inter _ _ hf]