α : Type u_1
β : Type u_2
inst✝ : OrderedSemiring β
s : Set α
hs : Set.Subsingleton s
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f j ≤ f j + 1
α : Type u_1
β : Type u_2
inst✝ : OrderedSemiring β
s : Set α
hs : Set.Subsingleton s
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f i ≤ f j + 1
rw [hs hi hj]
no goals
α : Type u_1
β : Type u_2
inst✝ : OrderedSemiring β
s : Set α
hs : Set.Subsingleton s
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f j ≤ f j + 1
exact le_add_of_nonneg_right zero_le_one