α : Type u_1
β : Type ?u.128368
ι : Type ?u.128371
M : Type u_2
N : Type ?u.128377
inst✝ : MulZeroOneClass M
s t : Set α
x✝ : α
⊢ indicator (s ∩ t) 1 x✝ = indicator (s ∩ t) (fun x => 1) x✝
α : Type u_1
β : Type ?u.128368
ι : Type ?u.128371
M : Type u_2
N : Type ?u.128377
inst✝ : MulZeroOneClass M
s t : Set α
x✝ : α
⊢ indicator (s ∩ t) 1 x✝ = (indicator s 1 * indicator t 1) x✝
simp only [← inter_indicator_mul, Pi.mul_apply, Pi.one_apply, one_mul]
no goals
α : Type u_1
β : Type ?u.128368
ι : Type ?u.128371
M : Type u_2
N : Type ?u.128377
inst✝ : MulZeroOneClass M
s t : Set α
x✝ : α
⊢ indicator (s ∩ t) 1 x✝ = indicator (s ∩ t) (fun x => 1) x✝
congr