[Merged by Bors] - feat(Order/WellFoundedSet): minimal element of a nonempty set exists if < is well founded on the set

Mathlib/Order/WellFounded.lean

@@ -82,6 +82,19 @@ instance (r : β → β → Prop) (f : α → β) [IsWellFounded β r] :
     IsWellFounded α (r.onFun f) where
   wf := IsWellFounded.wf.onFun
 
+theorem subtype_iff {p : α → Prop} :
+    WellFounded (α := Subtype p) (Function.onFun r Subtype.val) ↔
+      WellFounded (fun a b ↦ r a b ∧ p a ∧ p b) := by
+  simp_rw [wellFounded_iff_isEmpty_descending_chain, ← not_iff_not (a := IsEmpty _),
+    not_isEmpty_iff, nonempty_subtype]
+  refine ⟨fun ⟨f, ha⟩ ↦ ⟨(f ·), ?_⟩, fun ⟨f, ha⟩ ↦ ⟨(⟨f ·, ?_⟩), ?_⟩⟩ <;> grind
+
+theorem subtype_iff' {p : α → Prop} {r : Subtype p → Subtype p → Prop} :
+    WellFounded r ↔ WellFounded (fun a b ↦ ∃ ha : p a, ∃ hb : p b, r ⟨a, ha⟩ ⟨b, hb⟩) := by
+  simp_rw [wellFounded_iff_isEmpty_descending_chain, ← not_iff_not (a := IsEmpty _),
+    not_isEmpty_iff, nonempty_subtype]
+  refine ⟨fun ⟨f, ha⟩ ↦ ⟨(f ·), ?_⟩, fun ⟨f, ha⟩ ↦ ⟨(⟨f ·, (ha _).snd.fst⟩), ?_⟩⟩ <;> grind
+
 theorem _root_.Function.Injective.isWellOrder (r : β → β → Prop) {f : α → β} (hf : f.Injective)
     [IsWellOrder β r] : IsWellOrder α (r.onFun f) where
   __ := hf.trichotomous_onFun r

Mathlib/Order/WellFoundedSet.lean

@@ -559,6 +559,14 @@ lemma WellFoundedOn.mapsTo {α β : Type*} {r : α → α → Prop} (f : β →
     t.WellFoundedOn (r on f) := by
   exact InvImage.wf (fun x : t ↦ ⟨f x, h x.prop⟩) hw
 
+@[to_dual]
+theorem WellFoundedOn.exists_minimal {α : Type*} [Preorder α] {s : Set α}
+    (h : s.WellFoundedOn (· < ·)) (nonempty : s.Nonempty) : ∃ a, Minimal (· ∈ s) a := by
+  rw [wellFoundedOn_iff, ← WellFounded.subtype_iff] at h
+  convert WellFoundedLT.exists_minimal ⟨h⟩ Set.univ (@Set.univ_nonempty _ (by simpa))
+  refine ⟨fun ⟨a, ha⟩ ↦ ⟨⟨a, ha.prop⟩, ?_⟩, fun ⟨a, this⟩ ↦ ⟨a, ?_⟩⟩
+  <;> simpa only [mem_univ, minimal_true_subtype]
+
 end WellFoundedOn
 
 section LinearOrder