Extra lemmas about canonically ordered monoids

@[simp]

theorem Finset.sup_eq_zero {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [LinearOrder α] [OrderBot α] [CanonicallyOrderedAdd α] {s : Finset ι} {f : ι → α} : s.sup f = 0 ↔ ∀ i ∈ s, f i = 0

@[simp]

theorem Finset.sup'_eq_zero {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [LinearOrder α] [OrderBot α] [CanonicallyOrderedAdd α] {s : Finset ι} {f : ι → α} (hs : s.Nonempty) : s.sup' hs f = 0 ↔ ∀ i ∈ s, f i = 0

theorem Set.range_add_eq_image_Ici {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {β : Type u_2} {f : α → β} {k : α} : (range fun (x : α) => f (x + k)) = f '' Ici k