case pos
α : Type u_1
β : Type ?u.151856
ι : Type ?u.151859
M : Type u_2
N : Type ?u.151865
inst✝¹ : One M
s t : Set α
f g : α → M
a : α
y : M
inst✝ : LE M
hfg : a ∈ s → f a ≤ y
hg : ¬a ∈ s → 1 ≤ y
ha : a ∈ s
⊢ mulIndicator s f a ≤ y

case neg
α : Type u_1
β : Type ?u.151856
ι : Type ?u.151859
M : Type u_2
N : Type ?u.151865
inst✝¹ : One M
s t : Set α
f g : α → M
a : α
y : M
inst✝ : LE M
hfg : a ∈ s → f a ≤ y
hg : ¬a ∈ s → 1 ≤ y
ha : ¬a ∈ s
⊢ mulIndicator s f a ≤ y
α : Type u_1
β : Type ?u.151856
ι : Type ?u.151859
M : Type u_2
N : Type ?u.151865
inst✝¹ : One M
s t : Set α
f g : α → M
a : α
y : M
inst✝ : LE M
hfg : a ∈ s → f a ≤ y
hg : ¬a ∈ s → 1 ≤ y
⊢ mulIndicator s f a ≤ y
by_cases ha : a ∈ s
no goals
case pos
α : Type u_1
β : Type ?u.151856
ι : Type ?u.151859
M : Type u_2
N : Type ?u.151865
inst✝¹ : One M
s t : Set α
f g : α → M
a : α
y : M
inst✝ : LE M
hfg : a ∈ s → f a ≤ y
hg : ¬a ∈ s → 1 ≤ y
ha : a ∈ s
⊢ mulIndicator s f a ≤ y
simpa [ha] using hfg ha
no goals
case neg
α : Type u_1
β : Type ?u.151856
ι : Type ?u.151859
M : Type u_2
N : Type ?u.151865
inst✝¹ : One M
s t : Set α
f g : α → M
a : α
y : M
inst✝ : LE M
hfg : a ∈ s → f a ≤ y
hg : ¬a ∈ s → 1 ≤ y
ha : ¬a ∈ s
⊢ mulIndicator s f a ≤ y
simpa [ha] using hg ha