case pos
α : Type u_1
β : Type ?u.2284
ι : Type ?u.2287
M : Type u_2
N : Type ?u.2293
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a✝ : α
s : Set α
f : α → M
a : α
h : a ∈ s
⊢ mulIndicator s f a = 1 ∨ mulIndicator s f a = f a

case neg
α : Type u_1
β : Type ?u.2284
ι : Type ?u.2287
M : Type u_2
N : Type ?u.2293
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a✝ : α
s : Set α
f : α → M
a : α
h : ¬a ∈ s
⊢ mulIndicator s f a = 1 ∨ mulIndicator s f a = f a
α : Type u_1
β : Type ?u.2284
ι : Type ?u.2287
M : Type u_2
N : Type ?u.2293
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a✝ : α
s : Set α
f : α → M
a : α
⊢ mulIndicator s f a = 1 ∨ mulIndicator s f a = f a
by_cases h : a ∈ s
no goals
case pos
α : Type u_1
β : Type ?u.2284
ι : Type ?u.2287
M : Type u_2
N : Type ?u.2293
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a✝ : α
s : Set α
f : α → M
a : α
h : a ∈ s
⊢ mulIndicator s f a = 1 ∨ mulIndicator s f a = f a
exact Or.inr (mulIndicator_of_mem h f)
no goals
case neg
α : Type u_1
β : Type ?u.2284
ι : Type ?u.2287
M : Type u_2
N : Type ?u.2293
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a✝ : α
s : Set α
f : α → M
a : α
h : ¬a ∈ s
⊢ mulIndicator s f a = 1 ∨ mulIndicator s f a = f a
exact Or.inl (mulIndicator_of_not_mem h f)