feat: add instances for intervals (#5957)

Don't mind at all if anyone would like to push refactors or golfs. My main requirement from this PR is that
```lean
import Mathlib

example : WellFoundedLT { x : ℕ // x ≤ 37 }ᵒᵈ := inferInstance
```
works out of the box.




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Matthew Robert Ballard <matt@mrb.email>
Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jz Pan <acme_pjz@hotmail.com>
Co-authored-by: Thomas Browning <tb65536@uw.edu>
Co-authored-by: Oliver Nash <github@olivernash.org>
Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
Co-authored-by: Matthew Robert Ballard <k.buzzard@imperial.ac.uk>
Co-authored-by: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Co-authored-by: MohanadAhmed <m.a.m.elhassan@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: damiano <adomani@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
Co-authored-by: Rémy Degenne <Remydegenne@gmail.com>
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Mathlib.lean

@@ -1757,6 +1757,7 @@ import Mathlib.Data.Set.Image
 import Mathlib.Data.Set.Intervals.Basic
 import Mathlib.Data.Set.Intervals.Disjoint
 import Mathlib.Data.Set.Intervals.Group
+import Mathlib.Data.Set.Intervals.Image
 import Mathlib.Data.Set.Intervals.Infinite
 import Mathlib.Data.Set.Intervals.Instances
 import Mathlib.Data.Set.Intervals.IsoIoo

Mathlib/Data/PNat/Interval.lean

@@ -19,7 +19,7 @@ intervals as finsets and fintypes.
 open Finset Function PNat
 
 instance : LocallyFiniteOrder ℕ+ :=
-  instLocallyFiniteOrderSubtypePreorder _
+  Subtype.instLocallyFiniteOrder _
 
 namespace PNat
 

Mathlib/Data/Set/Function.lean

@@ -663,6 +663,10 @@ theorem injOn_of_injective (h : Injective f) (s : Set α) : InjOn f s := fun _ _
 alias injOn_of_injective ← _root_.Function.Injective.injOn
 #align function.injective.inj_on Function.Injective.injOn
 
+-- A specialization of `injOn_of_injective` for `Subtype.val`.
+theorem injOn_subtype_val {s : Set { x // p x }} : Set.InjOn Subtype.val s :=
+  Subtype.coe_injective.injOn s
+
 lemma injOn_id (s : Set α) : InjOn id s := injective_id.injOn _
 #align set.inj_on_id Set.injOn_id
 

Mathlib/Data/Set/Intervals/Image.lean

@@ -0,0 +1,137 @@
+/-
+Copyright (c) 2023 Kim Liesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Liesinger
+-/
+import Mathlib.Data.Set.Intervals.Basic
+import Mathlib.Data.Set.Function
+
+/-! ### Lemmas about monotone functions on intervals, and intervals in subtypes.
+-/
+
+variable {f : α → β}
+
+open Set
+
+section
+variable [Preorder α] [Preorder β]
+
+theorem Monotone.mapsTo_Icc (h : Monotone f) :
+    MapsTo f (Icc a b) (Icc (f a) (f b)) :=
+  fun _ _ => by aesop
+
+theorem StrictMono.mapsTo_Ioo (h : StrictMono f) :
+    MapsTo f (Ioo a b) (Ioo (f a) (f b)) :=
+  fun _ _ => by aesop
+
+theorem Monotone.mapsTo_Ici  (h : Monotone f) :
+    MapsTo f (Ici a) (Ici (f a)) :=
+  fun _ _ => by aesop
+
+theorem Monotone.mapsTo_Iic (h : Monotone f) :
+    MapsTo f (Iic a) (Iic (f a)) :=
+  fun _ _ => by aesop
+
+theorem StrictMono.mapsTo_Ioi (h : StrictMono f) :
+    MapsTo f (Ioi a) (Ioi (f a)) :=
+  fun _ _ => by aesop
+
+theorem StrictMono.mapsTo_Iio (h : StrictMono f) :
+    MapsTo f (Iio a) (Iio (f a)) :=
+  fun _ _ => by aesop
+
+end
+
+section
+variable [PartialOrder α] [Preorder β]
+
+theorem StrictMono.mapsTo_Ico (h : StrictMono f) :
+    MapsTo f (Ico a b) (Ico (f a) (f b)) :=
+  -- It makes me sad that `aesop` doesn't do this. There are clearly missing lemmas.
+  fun _ m => ⟨h.monotone m.1, h m.2⟩
+
+theorem StrictMono.mapsTo_Ioc (h : StrictMono f) :
+    MapsTo f (Ioc a b) (Ioc (f a) (f b)) :=
+  fun _ m => ⟨h m.1, h.monotone m.2⟩
+
+end
+
+section
+variable [Preorder α] [Preorder β]
+
+theorem Monotone.image_Icc_subset (h : Monotone f) :
+    f '' Icc a b ⊆ Icc (f a) (f b) :=
+  h.mapsTo_Icc.image_subset
+
+theorem StrictMono.image_Ioo_subset (h : StrictMono f) :
+    f '' Ioo a b ⊆ Ioo (f a) (f b) :=
+  h.mapsTo_Ioo.image_subset
+
+theorem Monotone.image_Ici_subset (h : Monotone f) :
+    f '' Ici a ⊆ Ici (f a) :=
+  h.mapsTo_Ici.image_subset
+
+theorem Monotone.image_Iic_subset (h : Monotone f) :
+    f '' Iic a ⊆ Iic (f a) :=
+  h.mapsTo_Iic.image_subset
+
+theorem StrictMono.image_Ioi_subset (h : StrictMono f) :
+    f '' Ioi a ⊆ Ioi (f a) :=
+  h.mapsTo_Ioi.image_subset
+
+theorem StrictMono.image_Iio_subset (h : StrictMono f) :
+    f '' Iio a ⊆ Iio (f a) :=
+  h.mapsTo_Iio.image_subset
+
+end
+
+section
+variable [PartialOrder α] [Preorder β]
+
+theorem StrictMono.imageIco_subset (h : StrictMono f) :
+    f '' Ico a b ⊆ Ico (f a) (f b) :=
+  h.mapsTo_Ico.image_subset
+
+theorem StrictMono.imageIoc_subset (h : StrictMono f) :
+    f '' Ioc a b ⊆ Ioc (f a) (f b) :=
+  h.mapsTo_Ioc.image_subset
+
+end
+
+namespace Set
+
+variable [Preorder α] {p : α → Prop}
+
+theorem image_subtype_val_Icc_subset (a b : {x // p x}) :
+    Subtype.val '' Icc a b ⊆ Icc a.val b.val :=
+  image_subset_iff.mpr fun _ m => m
+
+theorem image_subtype_val_Ico_subset (a b : {x // p x}) :
+    Subtype.val '' Ico a b ⊆ Ico a.val b.val :=
+  image_subset_iff.mpr fun _ m => m
+
+theorem image_subtype_val_Ioc_subset (a b : {x // p x}) :
+    Subtype.val '' Ioc a b ⊆ Ioc a.val b.val :=
+  image_subset_iff.mpr fun _ m => m
+
+theorem image_subtype_val_Ioo_subset (a b : {x // p x}) :
+    Subtype.val '' Ioo a b ⊆ Ioo a.val b.val :=
+  image_subset_iff.mpr fun _ m => m
+
+theorem image_subtype_val_Iic_subset (a : {x // p x}) :
+    Subtype.val '' Iic a ⊆ Iic a.val :=
+  image_subset_iff.mpr fun _ m => m
+
+theorem image_subtype_val_Iio_subset (a : {x // p x}) :
+    Subtype.val '' Iio a ⊆ Iio a.val :=
+  image_subset_iff.mpr fun _ m => m
+
+theorem image_subtype_val_Ici_subset (a : {x // p x}) :
+    Subtype.val '' Ici a ⊆ Ici a.val :=
+  image_subset_iff.mpr fun _ m => m
+
+theorem image_subtype_val_Ioi_subset (a : {x // p x}) :
+    Subtype.val '' Ioi a ⊆ Ioi a.val :=
+  image_subset_iff.mpr fun _ m => m
+
+end Set

Mathlib/NumberTheory/NumberField/Units.lean

@@ -111,6 +111,7 @@ instance [NumberField K] : Fintype (torsion K) := by
   · rw [← h_ua]
     exact le_of_eq ((eq_iff_eq _ 1).mp ((mem_torsion K).mp h_tors) φ)
 
+set_option synthInstance.maxHeartbeats 30000 in
 /-- The torsion subgroup is cylic. -/
 instance [NumberField K] : IsCyclic (torsion K) := subgroup_units_cyclic _
 

Mathlib/Order/LocallyFinite.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Data.Finset.Preimage
 import Mathlib.Data.Set.Intervals.UnorderedInterval
+import Mathlib.Data.Set.Intervals.Image
 
 #align_import order.locally_finite from "leanprover-community/mathlib"@"1d29de43a5ba4662dd33b5cfeecfc2a27a5a8a29"
 
@@ -1237,7 +1238,8 @@ end OrderIso
 
 variable [Preorder α] (p : α → Prop) [DecidablePred p]
 
-instance [LocallyFiniteOrder α] : LocallyFiniteOrder (Subtype p) where
+instance Subtype.instLocallyFiniteOrder [LocallyFiniteOrder α] :
+    LocallyFiniteOrder (Subtype p) where
   finsetIcc a b := (Icc (a : α) b).subtype p
   finsetIco a b := (Ico (a : α) b).subtype p
   finsetIoc a b := (Ioc (a : α) b).subtype p
@@ -1249,13 +1251,15 @@ instance [LocallyFiniteOrder α] : LocallyFiniteOrder (Subtype p) where
     simp_rw [Finset.mem_subtype, mem_Ioc, Subtype.coe_le_coe, Subtype.coe_lt_coe]
   finset_mem_Ioo a b x := by simp_rw [Finset.mem_subtype, mem_Ioo, Subtype.coe_lt_coe]
 
-instance [LocallyFiniteOrderTop α] : LocallyFiniteOrderTop (Subtype p) where
+instance Subtype.instLocallyFiniteOrderTop [LocallyFiniteOrderTop α] :
+    LocallyFiniteOrderTop (Subtype p) where
   finsetIci a := (Ici (a : α)).subtype p
   finsetIoi a := (Ioi (a : α)).subtype p
   finset_mem_Ici a x := by simp_rw [Finset.mem_subtype, mem_Ici, Subtype.coe_le_coe]
   finset_mem_Ioi a x := by simp_rw [Finset.mem_subtype, mem_Ioi, Subtype.coe_lt_coe]
 
-instance [LocallyFiniteOrderBot α] : LocallyFiniteOrderBot (Subtype p) where
+instance Subtype.instLocallyFiniteOrderBot [LocallyFiniteOrderBot α] :
+    LocallyFiniteOrderBot (Subtype p) where
   finsetIic a := (Iic (a : α)).subtype p
   finsetIio a := (Iio (a : α)).subtype p
   finset_mem_Iic a x := by simp_rw [Finset.mem_subtype, mem_Iic, Subtype.coe_le_coe]
@@ -1391,3 +1395,78 @@ theorem Set.finite_iff_bddBelow_bddAbove [Nonempty α] [Lattice α] [LocallyFini
     fun ⟨⟨a,ha⟩,⟨b,hb⟩⟩ ↦ (Set.finite_Icc a b).subset (fun x hx ↦ ⟨ha hx,hb hx⟩ )⟩
 
 end Finite
+
+/-! We make the instances below low priority
+so when alternative constructions are available they are preferred. -/
+
+instance (priority := low) [Preorder α] [DecidableRel ((· : α) ≤ ·)] [LocallyFiniteOrder α] :
+    LocallyFiniteOrderTop { x : α // x ≤ y } where
+  finsetIoi a := Finset.Ioc a ⟨y, by rfl⟩
+  finsetIci a := Finset.Icc a ⟨y, by rfl⟩
+  finset_mem_Ici a b := by
+    simp only [Finset.mem_Icc, and_iff_left_iff_imp]
+    exact fun _ => b.property
+  finset_mem_Ioi a b := by
+    simp only [Finset.mem_Ioc, and_iff_left_iff_imp]
+    exact fun _ => b.property
+
+instance (priority := low) [Preorder α] [DecidableRel ((· : α) < ·)] [LocallyFiniteOrder α] :
+    LocallyFiniteOrderTop { x : α // x < y } where
+  finsetIoi a := (Finset.Ioo ↑a y).subtype _
+  finsetIci a := (Finset.Ico ↑a y).subtype _
+  finset_mem_Ici a b := by
+    simp only [Finset.mem_subtype, Finset.mem_Ico, Subtype.coe_le_coe, and_iff_left_iff_imp]
+    exact fun _ => b.property
+  finset_mem_Ioi a b := by
+    simp only [Finset.mem_subtype, Finset.mem_Ioo, Subtype.coe_lt_coe, and_iff_left_iff_imp]
+    exact fun _ => b.property
+
+instance (priority := low) [Preorder α] [DecidableRel ((· : α) ≤ ·)] [LocallyFiniteOrder α] :
+    LocallyFiniteOrderBot { x : α // y ≤ x } where
+  finsetIio a := Finset.Ico ⟨y, by rfl⟩ a
+  finsetIic a := Finset.Icc ⟨y, by rfl⟩ a
+  finset_mem_Iic a b := by
+    simp only [Finset.mem_Icc, and_iff_right_iff_imp]
+    exact fun _ => b.property
+  finset_mem_Iio a b := by
+    simp only [Finset.mem_Ico, and_iff_right_iff_imp]
+    exact fun _ => b.property
+
+instance (priority := low) [Preorder α] [DecidableRel ((· : α) < ·)] [LocallyFiniteOrder α] :
+    LocallyFiniteOrderBot { x : α // y < x } where
+  finsetIio a := (Finset.Ioo y ↑a).subtype _
+  finsetIic a := (Finset.Ioc y ↑a).subtype _
+  finset_mem_Iic a b := by
+    simp only [Finset.mem_subtype, Finset.mem_Ioc, Subtype.coe_le_coe, and_iff_right_iff_imp]
+    exact fun _ => b.property
+  finset_mem_Iio a b := by
+    simp only [Finset.mem_subtype, Finset.mem_Ioo, Subtype.coe_lt_coe, and_iff_right_iff_imp]
+    exact fun _ => b.property
+
+instance [Preorder α] [LocallyFiniteOrderBot α] : Finite { x : α // x ≤ y } := by
+  apply Set.Finite.to_subtype
+  convert (Finset.Iic y).finite_toSet using 1
+  ext
+  simp
+  rfl
+
+instance [Preorder α] [LocallyFiniteOrderBot α] : Finite { x : α // x < y } := by
+  apply Set.Finite.to_subtype
+  convert (Finset.Iio y).finite_toSet using 1
+  ext
+  simp
+  rfl
+
+instance [Preorder α] [LocallyFiniteOrderTop α] : Finite { x : α // y ≤ x } := by
+  apply Set.Finite.to_subtype
+  convert (Finset.Ici y).finite_toSet using 1
+  ext
+  simp
+  rfl
+
+instance [Preorder α] [LocallyFiniteOrderTop α] : Finite { x : α // y < x } := by
+  apply Set.Finite.to_subtype
+  convert (Finset.Ioi y).finite_toSet using 1
+  ext
+  simp
+  rfl