α : Type u_2
β✝ : Type ?u.165616
ι : Type ?u.165619
M : Type ?u.165622
N : Type ?u.165625
β : Type u_1
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
⊢ indicator s f x ≤ indicator {x | 0 ≤ f x} f x
α : Type u_2
β✝ : Type ?u.165616
ι : Type ?u.165619
M : Type ?u.165622
N : Type ?u.165625
β : Type u_1
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
⊢ indicator s f ≤ indicator {x | 0 ≤ f x} f
intro x
α : Type u_2
β✝ : Type ?u.165616
ι : Type ?u.165619
M : Type ?u.165622
N : Type ?u.165625
β : Type u_1
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
⊢ (if x ∈ s then f x else 0) ≤ if x ∈ {x | 0 ≤ f x} then f x else 0
α : Type u_2
β✝ : Type ?u.165616
ι : Type ?u.165619
M : Type ?u.165622
N : Type ?u.165625
β : Type u_1
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
⊢ indicator s f x ≤ indicator {x | 0 ≤ f x} f x
simp_rw [indicator_apply]
case inl.inl
α : Type u_2
β✝ : Type ?u.165616
ι : Type ?u.165619
M : Type ?u.165622
N : Type ?u.165625
β : Type u_1
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
h_1 : x ∈ s
h_2 : x ∈ {x | 0 ≤ f x}
⊢ f x ≤ f x

case inl.inr
α : Type u_2
β✝ : Type ?u.165616
ι : Type ?u.165619
M : Type ?u.165622
N : Type ?u.165625
β : Type u_1
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
h_1 : x ∈ s
h_2 : ¬x ∈ {x | 0 ≤ f x}
⊢ f x ≤ 0

case inr.inl
α : Type u_2
β✝ : Type ?u.165616
ι : Type ?u.165619
M : Type ?u.165622
N : Type ?u.165625
β : Type u_1
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
h_1 : ¬x ∈ s
h_3 : x ∈ {x | 0 ≤ f x}
⊢ 0 ≤ f x

case inr.inr
α : Type u_2
β✝ : Type ?u.165616
ι : Type ?u.165619
M : Type ?u.165622
N : Type ?u.165625
β : Type u_1
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
h_1 : ¬x ∈ s
h_3 : ¬x ∈ {x | 0 ≤ f x}
⊢ 0 ≤ 0
α : Type u_2
β✝ : Type ?u.165616
ι : Type ?u.165619
M : Type ?u.165622
N : Type ?u.165625
β : Type u_1
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
⊢ (if x ∈ s then f x else 0) ≤ if x ∈ {x | 0 ≤ f x} then f x else 0
split_ifs with h_1 h_2 h_3
no goals
case inl.inl
α : Type u_2
β✝ : Type ?u.165616
ι : Type ?u.165619
M : Type ?u.165622
N : Type ?u.165625
β : Type u_1
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
h_1 : x ∈ s
h_2 : x ∈ {x | 0 ≤ f x}
⊢ f x ≤ f x
exact le_rfl
no goals
case inl.inr
α : Type u_2
β✝ : Type ?u.165616
ι : Type ?u.165619
M : Type ?u.165622
N : Type ?u.165625
β : Type u_1
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
h_1 : x ∈ s
h_2 : ¬x ∈ {x | 0 ≤ f x}
⊢ f x ≤ 0
exact (not_le.mp h_2).le
no goals
case inr.inl
α : Type u_2
β✝ : Type ?u.165616
ι : Type ?u.165619
M : Type ?u.165622
N : Type ?u.165625
β : Type u_1
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
h_1 : ¬x ∈ s
h_3 : x ∈ {x | 0 ≤ f x}
⊢ 0 ≤ f x
exact h_3
no goals
case inr.inr
α : Type u_2
β✝ : Type ?u.165616
ι : Type ?u.165619
M : Type ?u.165622
N : Type ?u.165625
β : Type u_1
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
h_1 : ¬x ∈ s
h_3 : ¬x ∈ {x | 0 ≤ f x}
⊢ 0 ≤ 0
exact le_rfl