[Merged by Bors] - feat(Data/ENat): add lemma ENat.iInf_eq_coe_iff

Mathlib/Data/ENat/Lattice.lean

@@ -57,6 +57,18 @@ lemma coe_iSup : BddAbove (range f) → ↑(⨆ i, f i) = ⨆ i, (f i : ℕ∞)
 lemma iInf_eq_top_of_isEmpty [IsEmpty ι] : ⨅ i, (f i : ℕ∞) = ⊤ :=
   iInf_coe_eq_top.mpr ‹_›
 
+lemma iInf_coe_eq_nat_iff {n : ℕ} : ⨅ i, (f i : ℕ∞) = n ↔ (∃ i, f i = n) ∧ ∀ i, n ≤ f i := by
+  by_cases! hι : IsEmpty ι
+  · simp
+  norm_cast
+  apply iInf_eq_iff
+
+lemma iInf_eq_nat_iff {f : ι → ℕ∞} {n : ℕ} :
+    ⨅ i, f i = n ↔ (∃ i, f i = n) ∧ ∀ i, n ≤ f i := by
+  by_cases! hι : IsEmpty ι
+  · simp [iInf_of_isEmpty]
+  apply iInf_eq_iff
+
 lemma iInf_toNat : (⨅ i, (f i : ℕ∞)).toNat = ⨅ i, f i := by
   cases isEmpty_or_nonempty ι
   · simp

Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

@@ -472,6 +472,12 @@ variable [WellFoundedLT α]
 theorem ciInf_mem [Nonempty ι] (f : ι → α) : iInf f ∈ range f :=
   csInf_mem (range_nonempty f)
 
+lemma iInf_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)
+
 end ConditionallyCompleteLinearOrder
 
 /-!