no goals
α : Type u_1
β : Type ?u.35667
ι : Type ?u.35670
M : Type u_2
N : Type ?u.35676
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s : Set α
f : α → M
t : Set M
ht : ¬1 ∈ t
⊢ mulIndicator s f ⁻¹' t = f ⁻¹' t ∩ s
simp [mulIndicator_preimage, Pi.one_def, Set.preimage_const_of_not_mem ht]