Apply suggestions

Author: IvanRenison

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

@@ -521,7 +521,7 @@ lemma csInf_eq_iff (hs : s.Nonempty) (n : α) :
   · intro rfl
     exact ⟨csInf_mem hs, fun _ ↦ csInf_le (OrderBot.bddBelow s)⟩
   · intro ⟨hn, hle⟩
-    apply le_antisymm (csInf_le (OrderBot.bddBelow s) hn) (le_csInf hs hle)
+    exact le_antisymm (csInf_le (OrderBot.bddBelow s) hn) (le_csInf hs hle)
 
 theorem MonotoneOn.map_csInf {β : Type*} [ConditionallyCompleteLattice β] {f : α → β}
     (hf : MonotoneOn f s) (hs : s.Nonempty) : f (sInf s) = sInf (f '' s) :=

Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

@@ -427,8 +427,11 @@ theorem ciInf_mem [Nonempty ι] (f : ι → α) : iInf f ∈ range f :=
 lemma ciInf_eq_iff [Nonempty ι] (f : ι → α) (n : α) :
     ⨅ i, (f i) = n ↔ (∃ i, f i = n) ∧ ∀ i, n ≤ f i := by
   have : OrderBot α := WellFoundedLT.toOrderBot α
-  refine ⟨(· ▸ ⟨ciInf_mem f, ciInf_le (OrderBot.bddBelow ..)⟩), fun ⟨⟨i, hi⟩, h⟩ ↦ ?_⟩
-  exact le_antisymm (hi ▸ ciInf_le (OrderBot.bddBelow ..) _) (le_ciInf h)
+  constructor
+  · rintro rfl
+    exact ⟨ciInf_mem f, ciInf_le (OrderBot.bddBelow ..)⟩
+  · rintro ⟨⟨i, rfl⟩, h⟩
+    exact le_antisymm (ciInf_le (OrderBot.bddBelow ..) _) (le_ciInf h)
 
 end ConditionallyCompleteLinearOrder