no goals
α : Type u_1
β : Type ?u.58114
ι : Type ?u.58117
M : Type u_2
N : Type ?u.58123
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g : α → M
a✝ : α
s : Set α
f : α → M
a : α
ha : a ∈ s
⊢ mulIndicator (sᶜ) f a * mulIndicator s f a = f a
simp [ha]
no goals
α : Type u_1
β : Type ?u.58114
ι : Type ?u.58117
M : Type u_2
N : Type ?u.58123
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g : α → M
a✝ : α
s : Set α
f : α → M
a : α
ha : ¬a ∈ s
⊢ mulIndicator (sᶜ) f a * mulIndicator s f a = f a
simp [ha]