case h
α : Type u_1
β : Type ?u.53297
ι : Type ?u.53300
M : Type u_2
N : Type ?u.53306
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
⊢ mulIndicator s (fun a => f a * g a) x✝ = mulIndicator s f x✝ * mulIndicator s g x✝
α : Type u_1
β : Type ?u.53297
ι : Type ?u.53300
M : Type u_2
N : Type ?u.53306
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
⊢ (mulIndicator s fun a => f a * g a) = fun a => mulIndicator s f a * mulIndicator s g a
funext
case h
α : Type u_1
β : Type ?u.53297
ι : Type ?u.53300
M : Type u_2
N : Type ?u.53306
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
⊢ (if x✝ ∈ s then f x✝ * g x✝ else 1) = (if x✝ ∈ s then f x✝ else 1) * if x✝ ∈ s then g x✝ else 1
case h
α : Type u_1
β : Type ?u.53297
ι : Type ?u.53300
M : Type u_2
N : Type ?u.53306
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
⊢ mulIndicator s (fun a => f a * g a) x✝ = mulIndicator s f x✝ * mulIndicator s g x✝
simp only [mulIndicator]
case h.inl
α : Type u_1
β : Type ?u.53297
ι : Type ?u.53300
M : Type u_2
N : Type ?u.53306
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
h✝ : x✝ ∈ s
⊢ f x✝ * g x✝ = f x✝ * g x✝

case h.inr
α : Type u_1
β : Type ?u.53297
ι : Type ?u.53300
M : Type u_2
N : Type ?u.53306
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
h✝ : ¬x✝ ∈ s
⊢ 1 = 1 * 1
case h
α : Type u_1
β : Type ?u.53297
ι : Type ?u.53300
M : Type u_2
N : Type ?u.53306
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
⊢ (if x✝ ∈ s then f x✝ * g x✝ else 1) = (if x✝ ∈ s then f x✝ else 1) * if x✝ ∈ s then g x✝ else 1
split_ifs
no goals
case h.inr
α : Type u_1
β : Type ?u.53297
ι : Type ?u.53300
M : Type u_2
N : Type ?u.53306
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
h✝ : ¬x✝ ∈ s
⊢ 1 = 1 * 1
rw [mul_one]
no goals
case h.inl
α : Type u_1
β : Type ?u.53297
ι : Type ?u.53300
M : Type u_2
N : Type ?u.53306
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
h✝ : x✝ ∈ s
⊢ f x✝ * g x✝ = f x✝ * g x✝
rfl