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

theorem lt_add_iff_lt_left_or_exists_lt {α : Type u_1} [LinearOrder α] {a b c : α} [Add α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] : a < b + c ↔ a < b ∨ ∃ d < c, a = b + d

theorem forall_lt_add_iff_lt_left {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [Add α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] : (∀ a < b + c, P a) ↔ (∀ a < b, P a) ∧ ∀ d < c, P (b + d)

theorem exists_lt_add_iff_lt_left {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [Add α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] : (∃ a < b + c, P a) ↔ (∃ a < b, P a) ∨ ∃ d < c, P (b + d)

theorem le_add_iff_lt_left_or_exists_le {α : Type u_1} [LinearOrder α] {a b c : α} [Add α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] : a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d

theorem forall_le_add_iff_le_left {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [Add α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] : (∀ a ≤ b + c, P a) ↔ (∀ a < b, P a) ∧ ∀ d ≤ c, P (b + d)

theorem exists_le_add_iff_le_left {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [Add α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] : (∃ a ≤ b + c, P a) ↔ (∃ a < b, P a) ∨ ∃ d ≤ c, P (b + d)

theorem lt_add_iff_lt_right_or_exists_lt {α : Type u_1} [LinearOrder α] {a b c : α} [AddCommMagma α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] : a < b + c ↔ a < c ∨ ∃ d < b, a = d + c

theorem forall_lt_add_iff_lt_right {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [AddCommMagma α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] : (∀ a < b + c, P a) ↔ (∀ a < c, P a) ∧ ∀ d < b, P (d + c)

theorem exists_lt_add_iff_lt_right {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [AddCommMagma α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] : (∃ a < b + c, P a) ↔ (∃ a < c, P a) ∨ ∃ d < b, P (d + c)

theorem le_add_iff_lt_right_or_exists_le {α : Type u_1} [LinearOrder α] {a b c : α} [AddCommMagma α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] : a ≤ b + c ↔ a < c ∨ ∃ d ≤ b, a = d + c

theorem forall_le_add_iff_le_right {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [AddCommMagma α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] : (∀ a ≤ b + c, P a) ↔ (∀ a < c, P a) ∧ ∀ d ≤ b, P (d + c)

theorem exists_le_add_iff_le_right {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [AddCommMagma α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] : (∃ a ≤ b + c, P a) ↔ (∃ a < c, P a) ∨ ∃ d ≤ b, P (d + c)