chore(algebra/order,data/set/intervals): a few more trivial lemmas (#…

…4611)

* a few more lemmas for `has_le.le` and `has_lt.lt` namespaces;
* a few lemmas about intersections of intervals;
* fix section header in `topology/algebra/module`.

src/algebra/order.lean

@@ -63,15 +63,29 @@ lemma lt_iff_ne [partial_order α] {x y : α} (h : x ≤ y) : x < y ↔ x ≠ y
 lemma le_iff_eq [partial_order α] {x y : α} (h : x ≤ y) : y ≤ x ↔ y = x :=
 ⟨λ h', h'.antisymm h, eq.le⟩
 
+lemma lt_or_le [linear_order α] {a b : α} (h : a ≤ b) (c : α) : a < c ∨ c ≤ b :=
+(lt_or_ge a c).imp id $ λ hc, le_trans hc h
+
+lemma le_or_lt [linear_order α] {a b : α} (h : a ≤ b) (c : α) : a ≤ c ∨ c < b :=
+(le_or_gt a c).imp id $ λ hc, lt_of_lt_of_le hc h
+
+lemma le_or_le [linear_order α] {a b : α} (h : a ≤ b) (c : α) : a ≤ c ∨ c ≤ b :=
+(h.le_or_lt c).elim or.inl (λ h, or.inr $ le_of_lt h)
+
 end has_le.le
 
-namespace has_lt
-namespace lt
+namespace has_lt.lt
+
 @[nolint ge_or_gt] -- see Note [nolint_ge]
 protected lemma gt [has_lt α] {x y : α} (h : x < y) : y > x := h
 protected lemma false [preorder α] {x : α} : x < x → false := lt_irrefl x
-end lt
-end has_lt
+
+lemma ne' [preorder α] {x y : α} (h : x < y) : y ≠ x := h.ne.symm
+
+lemma lt_or_lt [linear_order α] {x y : α} (h : x < y) (z : α) : x < z ∨ z < y :=
+(lt_or_ge z y).elim or.inr (λ hz, or.inl $ h.trans_le hz)
+
+end has_lt.lt
 
 namespace ge
 @[nolint ge_or_gt] -- see Note [nolint_ge]
@@ -134,12 +148,6 @@ lemma le_or_lt [linear_order α] : ∀ a b : α, a ≤ b ∨ b < a := le_or_gt
 lemma ne.lt_or_lt [linear_order α] {a b : α} (h : a ≠ b) : a < b ∨ b < a :=
 lt_or_gt_of_ne h
 
-lemma has_le.le.lt_or_le [linear_order α] {a b : α} (h : a ≤ b) (c : α) : a < c ∨ c ≤ b :=
-(lt_or_le a c).imp id $ λ hc, hc.trans h
-
-lemma has_le.le.le_or_lt [linear_order α] {a b : α} (h : a ≤ b) (c : α) : a ≤ c ∨ c < b :=
-(le_or_lt a c).imp id $ λ hc, hc.trans_le h
-
 lemma not_lt_iff_eq_or_lt [linear_order α] {a b : α} : ¬ a < b ↔ a = b ∨ b < a :=
 not_lt.trans $ le_iff_eq_or_lt.trans $ or_congr eq_comm iff.rfl
 

src/data/set/intervals/basic.lean

@@ -804,6 +804,20 @@ end lattice
 section decidable_linear_order
 variables {α : Type u} [decidable_linear_order α] {a a₁ a₂ b b₁ b₂ c d : α}
 
+lemma Ioc_inter_Ioo_of_left_lt (h : b₁ < b₂) : Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioc (max a₁ a₂) b₁ :=
+ext $ λ x, by simp [and_assoc, @and.left_comm (x ≤ _),
+  and_iff_left_iff_imp.2 (λ h', lt_of_le_of_lt h' h)]
+
+lemma Ioc_inter_Ioo_of_right_le (h : b₂ ≤ b₁) : Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (max a₁ a₂) b₂ :=
+ext $ λ x, by simp [and_assoc, @and.left_comm (x ≤ _),
+  and_iff_right_iff_imp.2 (λ h', (le_trans (le_of_lt h') h))]
+
+lemma Ioo_inter_Ioc_of_left_le (h : b₁ ≤ b₂) : Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioo (max a₁ a₂) b₁ :=
+by rw [inter_comm, Ioc_inter_Ioo_of_right_le h, max_comm]
+
+lemma Ioo_inter_Ioc_of_right_lt (h : b₂ < b₁) : Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (max a₁ a₂) b₂ :=
+by rw [inter_comm, Ioc_inter_Ioo_of_left_lt h, max_comm]
+
 @[simp] lemma Ico_diff_Iio : Ico a b \ Iio c = Ico (max a c) b :=
 ext $ by simp [Ico, Iio, iff_def, max_le_iff] {contextual:=tt}
 

src/topology/algebra/module.lean

@@ -191,7 +191,9 @@ notation M ` ≃L[`:50 R `] ` M₂ := continuous_linear_equiv R M M₂
 namespace continuous_linear_map
 
 section semiring
-/- Properties that hold for non-necessarily commutative semirings. -/
+/-!
+### Properties that hold for non-necessarily commutative semirings.
+-/
 
 variables
 {R : Type*} [semiring R]