chore(order/conditionally_complete_lattice): golf three proofs (#16064)

src/analysis/inner_product_space/rayleigh.lean

@@ -77,12 +77,12 @@ end
 lemma supr_rayleigh_eq_supr_rayleigh_sphere {r : ℝ} (hr : 0 < r) :
   (⨆ x : {x : E // x ≠ 0}, rayleigh_quotient x) = ⨆ x : sphere (0:E) r, rayleigh_quotient x :=
 show (⨆ x : ({0} : set E)ᶜ, rayleigh_quotient x) = _,
-by simp only [@csupr_set _ _ _ _ rayleigh_quotient, T.image_rayleigh_eq_image_rayleigh_sphere hr]
+by simp only [←@Sup_image' _ _ _ _ rayleigh_quotient, T.image_rayleigh_eq_image_rayleigh_sphere hr]
 
 lemma infi_rayleigh_eq_infi_rayleigh_sphere {r : ℝ} (hr : 0 < r) :
   (⨅ x : {x : E // x ≠ 0}, rayleigh_quotient x) = ⨅ x : sphere (0:E) r, rayleigh_quotient x :=
 show (⨅ x : ({0} : set E)ᶜ, rayleigh_quotient x) = _,
-by simp only [@cinfi_set _ _ _ _ rayleigh_quotient, T.image_rayleigh_eq_image_rayleigh_sphere hr]
+by simp only [←@Inf_image' _ _ _ _ rayleigh_quotient, T.image_rayleigh_eq_image_rayleigh_sphere hr]
 
 end continuous_linear_map
 

src/order/conditionally_complete_lattice.lean

@@ -556,17 +556,6 @@ by haveI := unique_prop hp; exact supr_unique
 @[simp] lemma cinfi_pos {p : Prop} {f : p → α} (hp : p) : (⨅ h : p, f h) = f hp :=
 @csupr_pos αᵒᵈ _ _ _ hp
 
-lemma csupr_set {s : set β} {f : β → α} : (⨆ x : s, f x) = Sup (f '' s) :=
-begin
-  rw supr,
-  congr,
-  ext,
-  rw [mem_image, mem_range, set_coe.exists],
-  simp_rw [subtype.coe_mk, exists_prop],
-end
-
-lemma cinfi_set {s : set β} {f : β → α} : (⨅ x : s, f x) = Inf (f '' s) := @csupr_set αᵒᵈ _ _ _ _
-
 /--Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b`
 is larger than `f i` for all `i`, and that this is not the case of any `w<b`.
 See `supr_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/
@@ -931,7 +920,7 @@ eq.symm $ is_lub.csupr_set_eq (gc.is_lub_l_image $ is_lub_cSup hne hbdd) hne
 
 lemma l_cSup' (gc : galois_connection l u) {s : set α} (hne : s.nonempty) (hbdd : bdd_above s) :
   l (Sup s) = Sup (l '' s) :=
-by rw [gc.l_cSup hne hbdd, csupr_set]
+by rw [gc.l_cSup hne hbdd, Sup_image']
 
 lemma l_csupr (gc : galois_connection l u) {f : ι → α}
   (hf : bdd_above (range f)) :
@@ -1182,19 +1171,17 @@ noncomputable instance with_top.with_bot.complete_linear_order {α : Type*}
 lemma with_top.supr_coe_eq_top {ι : Sort*} {α : Type*} [conditionally_complete_linear_order_bot α]
   (f : ι → α) : (⨆ x, (f x : with_top α)) = ⊤ ↔ ¬ bdd_above (set.range f) :=
 begin
-  refine ⟨_, λ hf, _⟩,
-  { rw [supr_eq_top, not_bdd_above_iff],
-    intros hf r,
-    rcases hf r (with_top.coe_lt_top r) with ⟨i, hi⟩,
+  rw [supr_eq_top, not_bdd_above_iff],
+  refine ⟨λ hf r, _, λ hf a ha, _⟩,
+  { rcases hf r (with_top.coe_lt_top r) with ⟨i, hi⟩,
     exact ⟨f i, ⟨i, rfl⟩, with_top.coe_lt_coe.mp hi⟩ },
-  { refine (supr_eq_top _).mpr (λ a ha, _),
-    rcases not_bdd_above_iff.mp hf (a.untop ha.ne) with ⟨-, ⟨i, rfl⟩, hi⟩,
+  { rcases hf (a.untop ha.ne) with ⟨-, ⟨i, rfl⟩, hi⟩,
     exact ⟨i, by simpa only [with_top.coe_untop _ ha.ne] using with_top.coe_lt_coe.mpr hi⟩ },
 end
 
 lemma with_top.supr_coe_lt_top {ι : Sort*} {α : Type*} [conditionally_complete_linear_order_bot α]
   (f : ι → α) : (⨆ x, (f x : with_top α)) < ⊤ ↔ bdd_above (set.range f) :=
-by simpa only [not_not, lt_top_iff_ne_top] using not_iff_not.mpr (with_top.supr_coe_eq_top f)
+lt_top_iff_ne_top.trans $ (with_top.supr_coe_eq_top f).not.trans not_not
 
 end with_top_bot