chore(order/bounds): golf (#5401)

Author: urkud

src/order/bounds.lean

@@ -635,13 +635,29 @@ section linear_order
 variables [linear_order α] {s : set α} {a b : α}
 
 lemma lt_is_lub_iff (h : is_lub s a) : b < a ↔ ∃ c ∈ s, b < c :=
-by haveI := classical.dec;
-   simpa [upper_bounds, not_ball] using
-   not_congr (@is_lub_le_iff _ _ _ _ b h)
+by simp only [← not_le, is_lub_le_iff h, mem_upper_bounds, not_forall]
 
 lemma is_glb_lt_iff (h : is_glb s a) : a < b ↔ ∃ c ∈ s, c < b :=
 @lt_is_lub_iff (order_dual α) _ _ _ _ h
 
+lemma is_lub.exists_between (h : is_lub s a) (hb : b < a) :
+  ∃ c ∈ s, b < c ∧ c ≤ a :=
+let ⟨c, hcs, hbc⟩ := (lt_is_lub_iff h).1 hb in ⟨c, hcs, hbc, h.1 hcs⟩
+
+lemma is_lub.exists_between' (h : is_lub s a) (h' : a ∉ s) (hb : b < a) :
+  ∃ c ∈ s, b < c ∧ c < a :=
+let ⟨c, hcs, hbc, hca⟩ := h.exists_between hb
+in ⟨c, hcs, hbc, hca.lt_of_ne $ λ hac, h' $ hac ▸ hcs⟩
+
+lemma is_glb.exists_between (h : is_glb s a) (hb : a < b) :
+  ∃ c ∈ s, a ≤ c ∧ c < b :=
+let ⟨c, hcs, hbc⟩ := (is_glb_lt_iff h).1 hb in ⟨c, hcs, h.1 hcs, hbc⟩
+
+lemma is_glb.exists_between' (h : is_glb s a) (h' : a ∉ s) (hb : a < b) :
+  ∃ c ∈ s, a < c ∧ c < b :=
+let ⟨c, hcs, hac, hcb⟩ := h.exists_between hb
+in ⟨c, hcs, hac.lt_of_ne $ λ hac, h' $ hac.symm ▸ hcs, hcb⟩
+
 end linear_order
 
 /-!
@@ -650,52 +666,22 @@ end linear_order
 
 section linear_ordered_add_comm_group
 
-variables [linear_ordered_add_comm_group α] {s : set α} {a ε : α} (h₃ : 0 < ε)
-include h₃
+variables [linear_ordered_add_comm_group α] {s : set α} {a ε : α}
 
-lemma is_glb.exists_between_self_add (h₁ : is_glb s a) : ∃ b, b ∈ s ∧ a ≤ b ∧ b < a + ε :=
-begin
-  have h' : a + ε ∉ lower_bounds s,
-  { set A := a + ε,
-    have : a < A := by { simp [A, h₃] },
-    intros hA,
-    exact lt_irrefl a (lt_of_lt_of_le this (h₁.2 hA)) },
-  obtain ⟨b, hb, hb'⟩ : ∃ b ∈ s, b < a + ε, by simpa [lower_bounds] using h',
-  exact ⟨b, hb, h₁.1 hb, hb'⟩
-end
+lemma is_glb.exists_between_self_add (h : is_glb s a) (hε : 0 < ε) :
+  ∃ b ∈ s, a ≤ b ∧ b < a + ε :=
+h.exists_between $ lt_add_of_pos_right _ hε
 
-lemma is_glb.exists_between_self_add' (h₁ : is_glb s a) (h₂ : a ∉ s) :
-  ∃ b, b ∈ s ∧ a < b ∧ b < a + ε :=
-begin
-  rcases h₁.exists_between_self_add h₃ with ⟨b, b_in, hb₁, hb₂⟩,
-  have h₅ : a ≠ b,
-  { intros contra,
-    apply h₂,
-    rwa ← contra at b_in },
-  exact ⟨b, b_in, lt_of_le_of_ne (h₁.1 b_in) h₅, hb₂⟩
-end
+lemma is_glb.exists_between_self_add' (h : is_glb s a) (h₂ : a ∉ s) (hε : 0 < ε) :
+  ∃ b ∈ s, a < b ∧ b < a + ε :=
+h.exists_between' h₂ $ lt_add_of_pos_right _ hε
 
-lemma is_lub.exists_between_sub_self  (h₁ : is_lub s a) : ∃ b, b ∈ s ∧ a - ε < b ∧ b ≤ a :=
-begin
-  have h' : a - ε ∉ upper_bounds s,
-  { set A := a - ε,
-    have : A < a := sub_lt_self a h₃,
-    intros hA,
-    exact lt_irrefl a (lt_of_le_of_lt (h₁.2 hA) this) },
-  obtain ⟨b, hb, hb'⟩ : ∃ (x : α), x ∈ s ∧ a - ε < x, by simpa [upper_bounds] using h',
-  exact ⟨b, hb, hb', h₁.1 hb⟩
-end
+lemma is_lub.exists_between_sub_self  (h : is_lub s a) (hε : 0 < ε) : ∃ b ∈ s, a - ε < b ∧ b ≤ a :=
+h.exists_between $ sub_lt_self _ hε
 
-lemma is_lub.exists_between_sub_self' (h₁ : is_lub s a) (h₂ : a ∉ s) :
-  ∃ b, b ∈ s ∧ a - ε < b ∧ b < a :=
-begin
-  rcases h₁.exists_between_sub_self h₃ with ⟨b, b_in, hb₁, hb₂⟩,
-  have h₅ : a ≠ b,
-  { intros contra,
-    apply h₂,
-    rwa ← contra at b_in },
-  exact ⟨b, b_in, hb₁, lt_of_le_of_ne (h₁.1 b_in) h₅.symm⟩
-end
+lemma is_lub.exists_between_sub_self' (h : is_lub s a) (h₂ : a ∉ s) (hε : 0 < ε) :
+  ∃ b ∈ s, a - ε < b ∧ b < a :=
+h.exists_between' h₂ $ sub_lt_self _ hε
 
 end linear_ordered_add_comm_group
 

src/topology/instances/real.lean

@@ -351,9 +351,9 @@ begin
   { intros H,
     exact H' a ⟨H, ha.1⟩ },
   obtain ⟨g₂, g₂_in, g₂_pos, g₂_lt⟩ : ∃ g₂ : ℝ, g₂ ∈ G ∧ 0 < g₂ ∧ g₂ < ε,
-  { obtain ⟨b, hb, hb', hb''⟩ := ha.exists_between_self_add' ε_pos a_notin,
-    obtain ⟨c, hc, hc', hc''⟩ := ha.exists_between_self_add' (by linarith : 0 < b - a) a_notin,
-    refine ⟨b - c, add_subgroup.sub_mem G hb.1 hc.1, _, _⟩ ;
+  { obtain ⟨b, hb, hb', hb''⟩ := ha.exists_between_self_add' a_notin ε_pos,
+    obtain ⟨c, hc, hc', hc''⟩ := ha.exists_between_self_add' a_notin (sub_pos.2 hb'),
+    refine ⟨b - c, G.sub_mem hb.1 hc.1, _, _⟩ ;
     linarith },
   refine ⟨floor (x/g₂) * g₂, _, _⟩,
   { exact add_subgroup.int_mul_mem _ g₂_in },