no goals
α : Type u_1
β : Type u_2
ι : Type ?u.22119
M : Type u_3
N : Type ?u.22125
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f : β → M
g : α → β
hg : Injective g
x : α
⊢ mulIndicator (g '' s) f (g x) = mulIndicator s (f ∘ g) x
rw [← mulIndicator_comp_right, preimage_image_eq _ hg]