case h
α : Type u_3
β : Type ?u.22458
ι : Type ?u.22461
M : Type u_2
N : Type u_1
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g✝ : α → M
a : α
g : M → N
hg : g 1 = 1
x✝ : α
⊢ mulIndicator s (g ∘ f) x✝ = (g ∘ mulIndicator s f) x✝
α : Type u_3
β : Type ?u.22458
ι : Type ?u.22461
M : Type u_2
N : Type u_1
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g✝ : α → M
a : α
g : M → N
hg : g 1 = 1
⊢ mulIndicator s (g ∘ f) = g ∘ mulIndicator s f
funext
case h
α : Type u_3
β : Type ?u.22458
ι : Type ?u.22461
M : Type u_2
N : Type u_1
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g✝ : α → M
a : α
g : M → N
hg : g 1 = 1
x✝ : α
⊢ (if x✝ ∈ s then (g ∘ f) x✝ else 1) = (g ∘ mulIndicator s f) x✝
case h
α : Type u_3
β : Type ?u.22458
ι : Type ?u.22461
M : Type u_2
N : Type u_1
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g✝ : α → M
a : α
g : M → N
hg : g 1 = 1
x✝ : α
⊢ mulIndicator s (g ∘ f) x✝ = (g ∘ mulIndicator s f) x✝
simp only [mulIndicator]
no goals
case h
α : Type u_3
β : Type ?u.22458
ι : Type ?u.22461
M : Type u_2
N : Type u_1
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g✝ : α → M
a : α
g : M → N
hg : g 1 = 1
x✝ : α
⊢ (if x✝ ∈ s then (g ∘ f) x✝ else 1) = (g ∘ mulIndicator s f) x✝
split_ifs <;> simp [*]