α : Type u_1
β : Type u_2
γ : Type ?u.118066
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ image (↑f) (erase s a) = erase (image (↑f) s) (↑f a)
α : Type u_1
β : Type u_2
γ : Type ?u.118066
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ map f (erase s a) = erase (map f s) (↑f a)
simp_rw [map_eq_image]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.118066
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ image (↑f) (erase s a) = erase (image (↑f) s) (↑f a)
exact s.image_erase f.2 a