feat: minimal elements exist in well-founded orders (#24766)

From Toric

Author: YaelDillies

Mathlib/Order/Minimal.lean

@@ -216,6 +216,37 @@ theorem not_maximal_iff_exists_gt (hx : P x) : ¬ Maximal P x ↔ ∃ y, x < y 
 
 alias ⟨exists_gt_of_not_maximal, _⟩ := not_maximal_iff_exists_gt
 
+section WellFoundedLT
+variable [WellFoundedLT α]
+
+lemma exists_minimalFor_of_wellFoundedLT (P : ι → Prop) (f : ι → α) (hP : ∃ i, P i) :
+    ∃ i, MinimalFor P f i := by
+  simpa [not_lt_iff_le_imp_le, InvImage] using (instIsWellFoundedInvImage (· < ·) f).wf.has_min _ hP
+
+lemma exists_minimal_of_wellFoundedLT (P : α → Prop) (hP : ∃ a, P a) : ∃ a, Minimal P a :=
+  exists_minimalFor_of_wellFoundedLT P id hP
+
+lemma exists_minimal_le_of_wellFoundedLT (P : α → Prop) (a : α) (ha : P a) :
+    ∃ b ≤ a, Minimal P b := by
+  obtain ⟨b, ⟨hba, hb⟩, hbmin⟩ :=
+    exists_minimal_of_wellFoundedLT (fun b ↦ b ≤ a ∧ P b) ⟨a, le_rfl, ha⟩
+  exact ⟨b, hba, hb, fun c hc hcb ↦ hbmin ⟨hcb.trans hba, hc⟩ hcb⟩
+
+end WellFoundedLT
+
+section WellFoundedGT
+variable [WellFoundedGT α]
+
+lemma exists_maximalFor_of_wellFoundedGT (P : ι → Prop) (f : ι → α) (hP : ∃ i, P i) :
+    ∃ i, MaximalFor P f i := exists_minimalFor_of_wellFoundedLT (α := αᵒᵈ) P f hP
+
+lemma exists_maximal_of_wellFoundedGT (P : α → Prop) (hP : ∃ a, P a) : ∃ a, Maximal P a :=
+  exists_minimal_of_wellFoundedLT (α := αᵒᵈ) P hP
+
+lemma exists_maximal_ge_of_wellFoundedGT (P : α → Prop) (a : α) (ha : P a) :
+    ∃ b, a ≤ b ∧ Maximal P b := exists_minimal_le_of_wellFoundedLT (α := αᵒᵈ) P a ha
+
+end WellFoundedGT
 end Preorder
 
 section PartialOrder