refactor(order/bounds): general cleanup (#14127)

Apart from golfing, this PR does the following:

Add the following theorems (which are immediate from the non-self counterparts):
- `monotone_on.mem_upper_bounds_image_self`
- `monotone_on.mem_lower_bounds_image_self`
- `antitone_on.mem_upper_bounds_image_self`
- `antitone_on.mem_lower_bounds_image_self`

Remove the following theorems (as they're just `mem_X_bounds_image` under unnecessarily stronger assumptions):

- `monotone_on.is_lub_image_le`
- `monotone_on.le_is_glb_image`
- `antitone_on.is_lub_image_le`
- `antitone_on.le_is_glb_image`
- `monotone.is_lub_image_le`
- `monotone.le_is_glb_image`
- `antitone.is_lub_image_le`
- `antitone.le_is_glb_image`

Remove a redundant argument `s ⊆ t` from the following (the old theorems follow immediately from the new ones and `monotone_on.mono`):

- `monotone_on.map_is_greatest`
- `monotone_on.map_is_least`
- `antitone_on.map_is_greatest`
- `antitone_on.map_is_least`

Author: vihdzp

src/order/bounds.lean

@@ -310,8 +310,7 @@ lemma is_lub.union [semilattice_sup γ] {a b : γ} {s t : set γ}
   (hs : is_lub s a) (ht : is_lub t b) :
   is_lub (s ∪ t) (a ⊔ b) :=
 ⟨λ c h, h.cases_on (λ h, le_sup_of_le_left $ hs.left h) (λ h, le_sup_of_le_right $ ht.left h),
-  assume c hc, sup_le
-    (hs.right $ assume d hd, hc $ or.inl hd) (ht.right $ assume d hd, hc $ or.inr hd)⟩
+  λ c hc, sup_le (hs.right $ λ d hd, hc $ or.inl hd) (ht.right $ λ d hd, hc $ or.inr hd)⟩
 
 /-- If `a` is the greatest lower bound of `s` and `b` is the greatest lower bound of `t`,
 then `a ⊓ b` is the greatest lower bound of `s ∪ t`. -/
@@ -622,9 +621,7 @@ lemma is_lub_empty [preorder γ] [order_bot γ] : is_lub ∅ (⊥:γ) := @is_glb
 
 lemma is_lub.nonempty [no_min_order α] (hs : is_lub s a) : s.nonempty :=
 let ⟨a', ha'⟩ := exists_lt a in
-ne_empty_iff_nonempty.1 $ assume h,
-have a ≤ a', from hs.right $ by simp only [h, upper_bounds_empty],
-not_le_of_lt ha' this
+ne_empty_iff_nonempty.1 $ λ h, not_le_of_lt ha' $ hs.right $ by simp only [h, upper_bounds_empty]
 
 lemma is_glb.nonempty [no_max_order α] (hs : is_glb s a) : s.nonempty := hs.dual.nonempty
 
@@ -682,11 +679,11 @@ by rw [insert_eq, lower_bounds_union, lower_bounds_singleton]
 
 /-- When there is a global maximum, every set is bounded above. -/
 @[simp] protected lemma order_top.bdd_above [preorder γ] [order_top γ] (s : set γ) : bdd_above s :=
-⟨⊤, assume a ha, order_top.le_top a⟩
+⟨⊤, λ a ha, order_top.le_top a⟩
 
 /-- When there is a global minimum, every set is bounded below. -/
 @[simp] protected lemma order_bot.bdd_below [preorder γ] [order_bot γ] (s : set γ) : bdd_below s :=
-⟨⊥, assume a ha, order_bot.bot_le a⟩
+⟨⊥, λ a ha, order_bot.bot_le a⟩
 
 /-!
 #### Pair
@@ -750,13 +747,13 @@ lemma is_least.unique (Ha : is_least s a) (Hb : is_least s b) : a = b :=
 le_antisymm (Ha.right Hb.left) (Hb.right Ha.left)
 
 lemma is_least.is_least_iff_eq (Ha : is_least s a) : is_least s b ↔ a = b :=
-iff.intro Ha.unique (assume h, h ▸ Ha)
+iff.intro Ha.unique (λ h, h ▸ Ha)
 
 lemma is_greatest.unique (Ha : is_greatest s a) (Hb : is_greatest s b) : a = b :=
 le_antisymm (Hb.right Ha.left) (Ha.right Hb.left)
 
 lemma is_greatest.is_greatest_iff_eq (Ha : is_greatest s a) : is_greatest s b ↔ a = b :=
-iff.intro Ha.unique (assume h, h ▸ Ha)
+iff.intro Ha.unique (λ h, h ▸ Ha)
 
 lemma is_lub.unique (Ha : is_lub s a) (Hb : is_lub s b) : a = b :=
 Ha.unique Hb
@@ -839,17 +836,23 @@ namespace monotone_on
 
 variables [preorder α] [preorder β] {f : α → β} {s t : set α}
   (Hf : monotone_on f t) {a : α} (Hst : s ⊆ t)
-include Hf Hst
+include Hf
 
 lemma mem_upper_bounds_image (Has : a ∈ upper_bounds s) (Hat : a ∈ t) :
   f a ∈ upper_bounds (f '' s) :=
-ball_image_of_ball (assume x H,  Hf (Hst H) Hat (Has H))
+ball_image_of_ball (λ x H, Hf (Hst H) Hat (Has H))
+
+lemma mem_upper_bounds_image_self : a ∈ upper_bounds t → a ∈ t → f a ∈ upper_bounds (f '' t) :=
+Hf.mem_upper_bounds_image subset_rfl
 
 lemma mem_lower_bounds_image (Has : a ∈ lower_bounds s) (Hat : a ∈ t) :
   f a ∈ lower_bounds (f '' s) :=
-ball_image_of_ball (assume x H,  Hf Hat (Hst H) (Has H))
+ball_image_of_ball (λ x H, Hf Hat (Hst H) (Has H))
+
+lemma mem_lower_bounds_image_self : a ∈ lower_bounds t → a ∈ t → f a ∈ lower_bounds (f '' t) :=
+Hf.mem_lower_bounds_image subset_rfl
 
-lemma image_upper_bounds_subset_upper_bounds_image :
+lemma image_upper_bounds_subset_upper_bounds_image (Hst : s ⊆ t) :
   f '' (upper_bounds s ∩ t) ⊆ upper_bounds (f '' s) :=
 by { rintro _ ⟨a, ha, rfl⟩, exact Hf.mem_upper_bounds_image Hst ha.1 ha.2 }
 
@@ -868,36 +871,32 @@ lemma map_bdd_below : (lower_bounds s ∩ t).nonempty → bdd_below (f '' s) :=
 λ ⟨C, hs, ht⟩, ⟨f C, Hf.mem_lower_bounds_image Hst hs ht⟩
 
 /-- A monotone map sends a least element of a set to a least element of its image. -/
-lemma map_is_least (Ha : is_least s a) : is_least (f '' s) (f a) :=
-⟨mem_image_of_mem _ Ha.1, Hf.mem_lower_bounds_image Hst Ha.2 (Hst Ha.1)⟩
+lemma map_is_least (Ha : is_least t a) : is_least (f '' t) (f a) :=
+⟨mem_image_of_mem _ Ha.1, Hf.mem_lower_bounds_image_self Ha.2 Ha.1⟩
 
 /-- A monotone map sends a greatest element of a set to a greatest element of its image. -/
-lemma map_is_greatest (Ha : is_greatest s a) : is_greatest (f '' s) (f a) :=
-⟨mem_image_of_mem _ Ha.1, Hf.mem_upper_bounds_image Hst Ha.2 (Hst Ha.1)⟩
-
-lemma is_lub_image_le (Ha : is_lub s a) (Hat : a ∈ t) {b : β} (Hb : is_lub (f '' s) b) :
-  b ≤ f a :=
-Hb.2 (Hf.mem_upper_bounds_image Hst Ha.1 Hat)
-
-lemma le_is_glb_image (Ha : is_glb s a) (Hat : a ∈ t) {b : β} (Hb : is_glb (f '' s) b) :
-  f a ≤ b :=
-Hb.2 (Hf.mem_lower_bounds_image Hst Ha.1 Hat)
+lemma map_is_greatest (Ha : is_greatest t a) : is_greatest (f '' t) (f a) :=
+⟨mem_image_of_mem _ Ha.1, Hf.mem_upper_bounds_image_self Ha.2 Ha.1⟩
 
 end monotone_on
 
 namespace antitone_on
 
 variables [preorder α] [preorder β] {f : α → β} {s t : set α}
   (Hf : antitone_on f t) {a : α} (Hst : s ⊆ t)
-include Hf Hst
+include Hf
 
-lemma mem_upper_bounds_image (Has : a ∈ lower_bounds s) (Hat : a ∈ t) :
-  f a ∈ upper_bounds (f '' s) :=
-Hf.dual_right.mem_lower_bounds_image Hst Has Hat
+lemma mem_upper_bounds_image (Has : a ∈ lower_bounds s) : a ∈ t → f a ∈ upper_bounds (f '' s) :=
+Hf.dual_right.mem_lower_bounds_image Hst Has
 
-lemma mem_lower_bounds_image (Has : a ∈ upper_bounds s) (Hat : a ∈ t) :
-  f a ∈ lower_bounds (f '' s) :=
-Hf.dual_right.mem_upper_bounds_image Hst Has Hat
+lemma mem_upper_bounds_image_self : a ∈ lower_bounds t → a ∈ t → f a ∈ upper_bounds (f '' t) :=
+Hf.dual_right.mem_lower_bounds_image_self
+
+lemma mem_lower_bounds_image : a ∈ upper_bounds s → a ∈ t → f a ∈ lower_bounds (f '' s) :=
+Hf.dual_right.mem_upper_bounds_image Hst
+
+lemma mem_lower_bounds_image_self : a ∈ upper_bounds t → a ∈ t → f a ∈ lower_bounds (f '' t) :=
+Hf.dual_right.mem_upper_bounds_image_self
 
 lemma image_lower_bounds_subset_upper_bounds_image :
   f '' (lower_bounds s ∩ t) ⊆ upper_bounds (f '' s) :=
@@ -916,51 +915,39 @@ lemma map_bdd_below : (lower_bounds s ∩ t).nonempty → bdd_above (f '' s) :=
 Hf.dual_right.map_bdd_below Hst
 
 /-- An antitone map sends a greatest element of a set to a least element of its image. -/
-lemma map_is_greatest (Ha : is_greatest s a) : is_least (f '' s) (f a) :=
-Hf.dual_right.map_is_greatest Hst Ha
+lemma map_is_greatest : is_greatest t a → is_least (f '' t) (f a) :=
+Hf.dual_right.map_is_greatest
 
 /-- An antitone map sends a least element of a set to a greatest element of its image. -/
-lemma map_is_least (Ha : is_least s a) : is_greatest (f '' s) (f a) :=
-Hf.dual_right.map_is_least Hst Ha
-
-lemma is_lub_image_le (Ha : is_glb s a) (Hat : a ∈ t) {b : β} (Hb : is_lub (f '' s) b) : b ≤ f a :=
-Hf.dual_left.is_lub_image_le Hst Ha Hat Hb
-
-lemma le_is_glb_image (Ha : is_lub s a) (Hat : a ∈ t) {b : β} (Hb : is_glb (f '' s) b) : f a ≤ b :=
-Hf.dual_left.le_is_glb_image Hst Ha Hat Hb
+lemma map_is_least : is_least t a → is_greatest (f '' t) (f a) :=
+Hf.dual_right.map_is_least
 
 end antitone_on
 
 namespace monotone
 
 variables [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {a : α} {s : set α}
+include Hf
 
-lemma mem_upper_bounds_image (Ha : a ∈ upper_bounds s) :
-  f a ∈ upper_bounds (f '' s) :=
-ball_image_of_ball (assume x H, Hf (Ha ‹x ∈ s›))
+lemma mem_upper_bounds_image (Ha : a ∈ upper_bounds s) : f a ∈ upper_bounds (f '' s) :=
+ball_image_of_ball (λ x H, Hf (Ha H))
 
-lemma mem_lower_bounds_image (Ha : a ∈ lower_bounds s) :
-  f a ∈ lower_bounds (f '' s) :=
-ball_image_of_ball (assume x H, Hf (Ha ‹x ∈ s›))
+lemma mem_lower_bounds_image (Ha : a ∈ lower_bounds s) : f a ∈ lower_bounds (f '' s) :=
+ball_image_of_ball (λ x H, Hf (Ha H))
 
-lemma image_upper_bounds_subset_upper_bounds_image (hf : monotone f) :
-  f '' upper_bounds s ⊆ upper_bounds (f '' s) :=
-begin
-  rintro _ ⟨a, ha, rfl⟩,
-  exact hf.mem_upper_bounds_image ha,
-end
+lemma image_upper_bounds_subset_upper_bounds_image : f '' upper_bounds s ⊆ upper_bounds (f '' s) :=
+by { rintro _ ⟨a, ha, rfl⟩, exact Hf.mem_upper_bounds_image ha }
 
-lemma image_lower_bounds_subset_lower_bounds_image (hf : monotone f) :
-  f '' lower_bounds s ⊆ lower_bounds (f '' s) :=
-hf.dual.image_upper_bounds_subset_upper_bounds_image
+lemma image_lower_bounds_subset_lower_bounds_image : f '' lower_bounds s ⊆ lower_bounds (f '' s) :=
+Hf.dual.image_upper_bounds_subset_upper_bounds_image
 
 /-- The image under a monotone function of a set which is bounded above is bounded above. -/
-lemma map_bdd_above (hf : monotone f) : bdd_above s → bdd_above (f '' s)
-| ⟨C, hC⟩ := ⟨f C, hf.mem_upper_bounds_image hC⟩
+lemma map_bdd_above : bdd_above s → bdd_above (f '' s)
+| ⟨C, hC⟩ := ⟨f C, Hf.mem_upper_bounds_image hC⟩
 
 /-- The image under a monotone function of a set which is bounded below is bounded below. -/
-lemma map_bdd_below (hf : monotone f) : bdd_below s → bdd_below (f '' s)
-| ⟨C, hC⟩ := ⟨f C, hf.mem_lower_bounds_image hC⟩
+lemma map_bdd_below : bdd_below s → bdd_below (f '' s)
+| ⟨C, hC⟩ := ⟨f C, Hf.mem_lower_bounds_image hC⟩
 
 /-- A monotone map sends a least element of a set to a least element of its image. -/
 lemma map_is_least (Ha : is_least s a) : is_least (f '' s) (f a) :=
@@ -970,56 +957,38 @@ lemma map_is_least (Ha : is_least s a) : is_least (f '' s) (f a) :=
 lemma map_is_greatest (Ha : is_greatest s a) : is_greatest (f '' s) (f a) :=
 ⟨mem_image_of_mem _ Ha.1, Hf.mem_upper_bounds_image Ha.2⟩
 
-lemma is_lub_image_le (Ha : is_lub s a) {b : β} (Hb : is_lub (f '' s) b) :
-  b ≤ f a :=
-Hb.2 (Hf.mem_upper_bounds_image Ha.1)
-
-lemma le_is_glb_image (Ha : is_glb s a) {b : β} (Hb : is_glb (f '' s) b) :
-  f a ≤ b :=
-Hb.2 (Hf.mem_lower_bounds_image Ha.1)
-
 end monotone
 
 namespace antitone
 variables [preorder α] [preorder β] {f : α → β} (hf : antitone f) {a : α} {s : set α}
 
-lemma mem_upper_bounds_image (ha : a ∈ lower_bounds s) :
-  f a ∈ upper_bounds (f '' s) :=
-hf.dual_right.mem_lower_bounds_image ha
+lemma mem_upper_bounds_image : a ∈ lower_bounds s → f a ∈ upper_bounds (f '' s) :=
+hf.dual_right.mem_lower_bounds_image
 
-lemma mem_lower_bounds_image (ha : a ∈ upper_bounds s) :
-  f a ∈ lower_bounds (f '' s) :=
-hf.dual_right.mem_upper_bounds_image ha
+lemma mem_lower_bounds_image : a ∈ upper_bounds s → f a ∈ lower_bounds (f '' s) :=
+hf.dual_right.mem_upper_bounds_image
 
-lemma image_lower_bounds_subset_upper_bounds_image (hf : antitone f) :
-  f '' lower_bounds s ⊆ upper_bounds (f '' s) :=
+lemma image_lower_bounds_subset_upper_bounds_image : f '' lower_bounds s ⊆ upper_bounds (f '' s) :=
 hf.dual_right.image_lower_bounds_subset_lower_bounds_image
 
-lemma image_upper_bounds_subset_lower_bounds_image (hf : antitone f) :
-  f '' upper_bounds s ⊆ lower_bounds (f '' s) :=
+lemma image_upper_bounds_subset_lower_bounds_image : f '' upper_bounds s ⊆ lower_bounds (f '' s) :=
 hf.dual_right.image_upper_bounds_subset_upper_bounds_image
 
 /-- The image under an antitone function of a set which is bounded above is bounded below. -/
-lemma map_bdd_above (hf : antitone f) : bdd_above s → bdd_below (f '' s) :=
+lemma map_bdd_above : bdd_above s → bdd_below (f '' s) :=
 hf.dual_right.map_bdd_above
 
 /-- The image under an antitone function of a set which is bounded below is bounded above. -/
-lemma map_bdd_below (hf : antitone f) : bdd_below s → bdd_above (f '' s) :=
+lemma map_bdd_below : bdd_below s → bdd_above (f '' s) :=
 hf.dual_right.map_bdd_below
 
 /-- An antitone map sends a greatest element of a set to a least element of its image. -/
-lemma map_is_greatest (ha : is_greatest s a) : is_least (f '' s) (f a) :=
-hf.dual_right.map_is_greatest ha
+lemma map_is_greatest : is_greatest s a → is_least (f '' s) (f a) :=
+hf.dual_right.map_is_greatest
 
 /-- An antitone map sends a least element of a set to a greatest element of its image. -/
-lemma map_is_least (ha : is_least s a) : is_greatest (f '' s) (f a) :=
-hf.dual_right.map_is_least ha
-
-lemma is_lub_image_le (ha : is_glb s a) {b : β} (hb : is_lub (f '' s) b) : b ≤ f a :=
-hf.dual_left.is_lub_image_le ha hb
-
-lemma le_is_glb_image (ha : is_lub s a) {b : β} (hb : is_glb (f '' s) b) : f a ≤ b :=
-hf.dual_left.le_is_glb_image ha hb
+lemma map_is_least : is_least s a → is_greatest (f '' s) (f a) :=
+hf.dual_right.map_is_least
 
 end antitone
 

src/order/galois_connection.lean

@@ -522,8 +522,8 @@ def lift_complete_lattice [complete_lattice α] (gi : galois_insertion l u) : co
 { Sup := λ s, l (Sup (u '' s)),
   Sup_le := λ s, (gi.is_lub_of_u_image (is_lub_Sup _)).2,
   le_Sup := λ s, (gi.is_lub_of_u_image (is_lub_Sup _)).1,
-  Inf := λ s, gi.choice (Inf (u '' s)) $ gi.gc.monotone_u.le_is_glb_image
-    (gi.is_glb_of_u_image $ is_glb_Inf _) (is_glb_Inf _),
+  Inf := λ s, gi.choice (Inf (u '' s)) $ (is_glb_Inf _).2 $ gi.gc.monotone_u.mem_lower_bounds_image
+    (gi.is_glb_of_u_image $ is_glb_Inf _).1,
   Inf_le := λ s, by { rw gi.choice_eq, exact (gi.is_glb_of_u_image (is_glb_Inf _)).1 },
   le_Inf := λ s, by { rw gi.choice_eq, exact (gi.is_glb_of_u_image (is_glb_Inf _)).2 },
   .. gi.lift_bounded_order,