[Merged by Bors] - refactor: redefine Subrel in terms of α → Prop instead of Set α

Mathlib/Order/InitialSeg.lean

@@ -215,7 +215,7 @@ theorem eq_or_principal [IsWellOrder β s] (f : r ≼i s) :
     cases hy (Set.mem_range_self z)
 
 /-- Restrict the codomain of an initial segment -/
-def codRestrict (p : Set β) (f : r ≼i s) (H : ∀ a, f a ∈ p) : r ≼i Subrel s p :=
+def codRestrict (p : Set β) (f : r ≼i s) (H : ∀ a, f a ∈ p) : r ≼i Subrel s (· ∈ p) :=
   ⟨RelEmbedding.codRestrict p f H, fun a ⟨b, m⟩ h =>
     let ⟨a', e⟩ := f.mem_range_of_rel h
     ⟨a', by subst e; rfl⟩⟩
@@ -462,34 +462,31 @@ theorem top_rel_top {r : α → α → Prop} {s : β → β → Prop} {t : γ 
 alias topLTTop := top_rel_top
 
 /-- Any element of a well order yields a principal segment. -/
--- The explicit typing is required in order for `simp` to work properly.
 @[simps!]
-def ofElement {α : Type*} (r : α → α → Prop) (a : α) :
-    @PrincipalSeg { b // r b a } α (Subrel r { b | r b a }) r :=
+def ofElement {α : Type*} (r : α → α → Prop) (a : α) : (Subrel r (r · a)) ≺i r :=
   ⟨Subrel.relEmbedding _ _, a, fun _ => ⟨fun ⟨⟨_, h⟩, rfl⟩ => h, fun h => ⟨⟨_, h⟩, rfl⟩⟩⟩
 
 @[simp]
 theorem ofElement_apply {α : Type*} (r : α → α → Prop) (a : α) (b) : ofElement r a b = b.1 :=
   rfl
 
 /-- For any principal segment `r ≺i s`, there is a `Subrel` of `s` order isomorphic to `r`. -/
--- The explicit typing is required in order for `simp` to work properly.
 @[simps! symm_apply]
-noncomputable def subrelIso (f : r ≺i s) :
-    @RelIso { b // s b f.top } α (Subrel s { b | s b f.top }) r :=
+noncomputable def subrelIso (f : r ≺i s) : (Subrel s (s · f.top)) ≃r r :=
   RelIso.symm ⟨(Equiv.ofInjective f f.injective).trans
     (Equiv.setCongr (funext fun _ ↦ propext f.mem_range_iff_rel)), f.map_rel_iff⟩
 
 @[simp]
-theorem apply_subrelIso (f : r ≺i s) (b : {b | s b f.top}) : f (f.subrelIso b) = b :=
+theorem apply_subrelIso (f : r ≺i s) (b : {b // s b f.top}) : f (f.subrelIso b) = b :=
   Equiv.apply_ofInjective_symm f.injective _
 
 @[simp]
 theorem subrelIso_apply (f : r ≺i s) (a : α) : f.subrelIso ⟨f a, f.lt_top a⟩ = a :=
   Equiv.ofInjective_symm_apply f.injective _
 
 /-- Restrict the codomain of a principal segment -/
-def codRestrict (p : Set β) (f : r ≺i s) (H : ∀ a, f a ∈ p) (H₂ : f.top ∈ p) : r ≺i Subrel s p :=
+def codRestrict (p : Set β) (f : r ≺i s) (H : ∀ a, f a ∈ p) (H₂ : f.top ∈ p) :
+    r ≺i Subrel s (· ∈ p) :=
   ⟨RelEmbedding.codRestrict p f H, ⟨f.top, H₂⟩, fun ⟨_, _⟩ => by simp [← f.mem_range_iff_rel]⟩
 
 @[simp]

Mathlib/Order/RelIso/Set.lean

@@ -45,66 +45,61 @@ theorem range_eq (e : r ≃r s) : Set.range e = Set.univ :=
 
 end RelIso
 
-/-- `Subrel r p` is the inherited relation on a subset. -/
-def Subrel (r : α → α → Prop) (p : Set α) : p → p → Prop :=
-  (Subtype.val : p → α) ⁻¹'o r
+/-- `Subrel r p` is the inherited relation on a subtype.
+
+We could also consider a Set.Subrel r s variant for dot notation, but this ends up interacting
+poorly with `simpNF`. -/
+def Subrel (r : α → α → Prop) (p : α → Prop) : Subtype p → Subtype p → Prop :=
+  Subtype.val ⁻¹'o r
 
 @[simp]
-theorem subrel_val (r : α → α → Prop) (p : Set α) {a b} : Subrel r p a b ↔ r a.1 b.1 :=
+theorem subrel_val (r : α → α → Prop) (p : α → Prop) {a b} : Subrel r p a b ↔ r a.1 b.1 :=
   Iff.rfl
 
 namespace Subrel
 
 /-- The relation embedding from the inherited relation on a subset. -/
-protected def relEmbedding (r : α → α → Prop) (p : Set α) : Subrel r p ↪r r :=
+protected def relEmbedding (r : α → α → Prop) (p : α → Prop) : Subrel r p ↪r r :=
   ⟨Embedding.subtype _, Iff.rfl⟩
 
 @[simp]
 theorem relEmbedding_apply (r : α → α → Prop) (p a) : Subrel.relEmbedding r p a = a.1 :=
   rfl
 
-/-- A set inclusion as a relation embedding. -/
-protected def inclusionEmbedding (r : α → α → Prop) {p q : Set α} (h : p ⊆ q) :
-    Subrel r p ↪r Subrel r q where
+/-- `Set.inclusion` as a relation embedding. -/
+protected def inclusionEmbedding (r : α → α → Prop) {s t : Set α} (h : s ⊆ t) :
+    Subrel r (· ∈ s) ↪r Subrel r (· ∈ t) where
   toFun := Set.inclusion h
   inj' _ _ h := (Set.inclusion_inj _).mp h
   map_rel_iff' := Iff.rfl
 
 @[simp]
-theorem coe_inclusionEmbedding (r : α → α → Prop) {p q : Set α} (h : p ⊆ q) :
-    (Subrel.inclusionEmbedding r h : p → q) = Set.inclusion h :=
+theorem coe_inclusionEmbedding (r : α → α → Prop) {s t : Set α} (h : s ⊆ t) :
+    (Subrel.inclusionEmbedding r h : s → t) = Set.inclusion h :=
   rfl
 
-instance (r : α → α → Prop) [IsWellOrder α r] (p : Set α) : IsWellOrder p (Subrel r p) :=
+instance (r : α → α → Prop) [IsWellOrder α r] (p : α → Prop) : IsWellOrder _ (Subrel r p) :=
   RelEmbedding.isWellOrder (Subrel.relEmbedding r p)
 
--- TODO: this instance is needed as `simp` automatically simplifies `↑{a // p a}` as `{a | p a}`.
---
--- Should `Subrel` be redefined in terms of `p : α → Prop` instead of `p : Set α` to avoid
--- this issue?
-instance (r : α → α → Prop) (p : α → Prop) [IsWellOrder α r] :
-    IsWellOrder {a // p a} (Subrel r {a | p a}) :=
-  instIsWellOrderElem _ _
-
-instance (r : α → α → Prop) [IsRefl α r] (p : Set α) : IsRefl p (Subrel r p) :=
+instance (r : α → α → Prop) [IsRefl α r] (p : α → Prop) : IsRefl _ (Subrel r p) :=
   ⟨fun x => @IsRefl.refl α r _ x⟩
 
-instance (r : α → α → Prop) [IsSymm α r] (p : Set α) : IsSymm p (Subrel r p) :=
+instance (r : α → α → Prop) [IsSymm α r] (p : α → Prop) : IsSymm _ (Subrel r p) :=
   ⟨fun x y => @IsSymm.symm α r _ x y⟩
 
-instance (r : α → α → Prop) [IsAsymm α r] (p : Set α) : IsAsymm p (Subrel r p) :=
+instance (r : α → α → Prop) [IsAsymm α r] (p : α → Prop) : IsAsymm _ (Subrel r p) :=
   ⟨fun x y => @IsAsymm.asymm α r _ x y⟩
 
-instance (r : α → α → Prop) [IsTrans α r] (p : Set α) : IsTrans p (Subrel r p) :=
+instance (r : α → α → Prop) [IsTrans α r] (p : α → Prop) : IsTrans _ (Subrel r p) :=
   ⟨fun x y z => @IsTrans.trans α r _ x y z⟩
 
-instance (r : α → α → Prop) [IsIrrefl α r] (p : Set α) : IsIrrefl p (Subrel r p) :=
+instance (r : α → α → Prop) [IsIrrefl α r] (p : α → Prop) : IsIrrefl _ (Subrel r p) :=
   ⟨fun x => @IsIrrefl.irrefl α r _ x⟩
 
 end Subrel
 
 /-- Restrict the codomain of a relation embedding. -/
-def RelEmbedding.codRestrict (p : Set β) (f : r ↪r s) (H : ∀ a, f a ∈ p) : r ↪r Subrel s p :=
+def RelEmbedding.codRestrict (p : Set β) (f : r ↪r s) (H : ∀ a, f a ∈ p) : r ↪r Subrel s (· ∈ p) :=
   ⟨f.toEmbedding.codRestrict p H, f.map_rel_iff'⟩
 
 @[simp]
@@ -123,12 +118,12 @@ theorem RelIso.preimage_eq_image_symm (e : r ≃r s) (t : Set β) : e ⁻¹' t =
 end image
 
 theorem Acc.of_subrel {r : α → α → Prop} [IsTrans α r] {b : α} (a : { a // r a b })
-    (h : Acc (Subrel r { a | r a b }) a) : Acc r a.1 :=
+    (h : Acc (Subrel r (r · b)) a) : Acc r a.1 :=
   h.recOn fun a _ IH ↦ ⟨_, fun _ hb ↦ IH ⟨_, _root_.trans hb a.2⟩ hb⟩
 
 /-- A relation `r` is well-founded iff every downward-interval `{ a | r a b }` of it is
 well-founded. -/
 theorem wellFounded_iff_wellFounded_subrel {r : α → α → Prop} [IsTrans α r] :
-    WellFounded r ↔ ∀ b, WellFounded (Subrel r { a | r a b }) where
+    WellFounded r ↔ ∀ b, WellFounded (Subrel r (r · b)) where
   mp h _ := InvImage.wf Subtype.val h
   mpr h := ⟨fun a ↦ ⟨_, fun b hr ↦ ((h a).apply _).of_subrel ⟨b, hr⟩⟩⟩

Mathlib/SetTheory/Cardinal/Cofinality.lean

@@ -157,7 +157,7 @@ theorem cof_eq (r : α → α → Prop) [IsWellOrder α r] : ∃ S, Unbounded r
   csInf_mem (Order.cof_nonempty (swap rᶜ))
 
 theorem ord_cof_eq (r : α → α → Prop) [IsWellOrder α r] :
-    ∃ S, Unbounded r S ∧ type (Subrel r S) = (cof (type r)).ord := by
+    ∃ S, Unbounded r S ∧ type (Subrel r (· ∈ S)) = (cof (type r)).ord := by
   let ⟨S, hS, e⟩ := cof_eq r
   let ⟨s, _, e'⟩ := Cardinal.ord_eq S
   let T : Set α := { a | ∃ aS : a ∈ S, ∀ b : S, s b ⟨_, aS⟩ → r b a }
@@ -570,7 +570,7 @@ theorem exists_fundamental_sequence (a : Ordinal.{u}) :
   rcases exists_lsub_cof a with ⟨ι, f, hf, hι⟩
   rcases ord_eq ι with ⟨r, wo, hr⟩
   haveI := wo
-  let r' := Subrel r { i | ∀ j, r j i → f j < f i }
+  let r' := Subrel r fun i ↦ ∀ j, r j i → f j < f i
   let hrr' : r' ↪r r := Subrel.relEmbedding _ _
   haveI := hrr'.isWellOrder
   refine

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -435,7 +435,7 @@ theorem typein.principalSeg_coe (r : α → α → Prop) [IsWellOrder α r] :
 
 @[simp]
 theorem type_subrel (r : α → α → Prop) [IsWellOrder α r] (a : α) :
-    type (Subrel r { b | r b a }) = typein r a :=
+    type (Subrel r (r · a)) = typein r a :=
   rfl
 
 @[simp]
@@ -513,6 +513,7 @@ theorem enum_le_enum (r : α → α → Prop) [IsWellOrder α r] {o₁ o₂ : Ii
     ¬r (enum r o₁) (enum r o₂) ↔ o₂ ≤ o₁ := by
   rw [enum_lt_enum (r := r), not_lt]
 
+-- TODO: generalize to other well-orders
 @[simp]
 theorem enum_le_enum' (a : Ordinal) {o₁ o₂ : Iio (type (· < ·))} :
     enum (· < ·) o₁ ≤ enum (α := a.toType) (· < ·) o₂ ↔ o₁ ≤ o₂ := by

Mathlib/SetTheory/ZFC/Ordinal.lean

@@ -118,13 +118,13 @@ theorem subset_of_mem (h : x.IsOrdinal) : y ∈ x → y ⊆ x :=
 theorem mem_trans (h : z.IsOrdinal) : x ∈ y → y ∈ z → x ∈ z :=
   h.isTransitive.mem_trans
 
-protected theorem isTrans (h : x.IsOrdinal) : IsTrans x.toSet (Subrel (· ∈ ·) _) :=
+protected theorem isTrans (h : x.IsOrdinal) : IsTrans _ (Subrel (· ∈ ·) (· ∈ x)) :=
   ⟨fun _ _ c hab hbc => h.mem_trans' hab hbc c.2⟩
 
 /-- The simplified form of transitivity used within `IsOrdinal` yields an equivalent definition to
 the standard one. -/
 theorem _root_.ZFSet.isOrdinal_iff_isTrans :
-    x.IsOrdinal ↔ x.IsTransitive ∧ IsTrans x.toSet (Subrel (· ∈ ·) _) where
+    x.IsOrdinal ↔ x.IsTransitive ∧ IsTrans _ (Subrel (· ∈ ·) (· ∈ x)) where
   mp h := ⟨h.isTransitive, h.isTrans⟩
   mpr := by
     rintro ⟨h₁, ⟨h₂⟩⟩
@@ -134,8 +134,7 @@ theorem _root_.ZFSet.isOrdinal_iff_isTrans :
 
 protected theorem mem (hx : x.IsOrdinal) (hy : y ∈ x) : y.IsOrdinal :=
   have := hx.isTrans
-  let f : Subrel (· ∈ ·) y.toSet ↪r Subrel (· ∈ ·) x.toSet :=
-    Subrel.inclusionEmbedding (· ∈ ·) (hx.subset_of_mem hy)
+  let f : _ ↪r Subrel (· ∈ ·) (· ∈ x) := Subrel.inclusionEmbedding (· ∈ ·) (hx.subset_of_mem hy)
   isOrdinal_iff_isTrans.2 ⟨fun _ hz _ ha ↦ hx.mem_trans' ha hz hy, f.isTrans⟩
 
 /-- An ordinal is a transitive set of transitive sets. -/
@@ -203,30 +202,30 @@ theorem mem_trichotomous (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ∈ y ∨ x =
   rw [eq_comm, ← subset_iff_eq_or_mem hy hx]
   exact mem_or_subset hx hy
 
-protected theorem isTrichotomous (h : x.IsOrdinal) : IsTrichotomous x.toSet (Subrel (· ∈ ·) _) :=
+protected theorem isTrichotomous (h : x.IsOrdinal) : IsTrichotomous _ (Subrel (· ∈ ·) (· ∈ x)) :=
   ⟨fun ⟨a, ha⟩ ⟨b, hb⟩ ↦ by simpa using mem_trichotomous (h.mem ha) (h.mem hb)⟩
 
 /-- An ordinal is a transitive set, trichotomous under membership. -/
 theorem _root_.ZFSet.isOrdinal_iff_isTrichotomous :
-    x.IsOrdinal ↔ x.IsTransitive ∧ IsTrichotomous x.toSet (Subrel (· ∈ ·) _) where
+    x.IsOrdinal ↔ x.IsTransitive ∧ IsTrichotomous _ (Subrel (· ∈ ·) (· ∈ x)) where
   mp h := ⟨h.isTransitive, h.isTrichotomous⟩
   mpr := by
     rintro ⟨h₁, h₂⟩
     rw [isOrdinal_iff_isTrans]
     refine ⟨h₁, ⟨@fun y z w hyz hzw ↦ ?_⟩⟩
-    obtain hyw | rfl | hwy := trichotomous_of (Subrel (· ∈ ·) _) y w
+    obtain hyw | rfl | hwy := trichotomous_of (Subrel (· ∈ ·) (· ∈ x)) y w
     · exact hyw
     · cases asymm hyz hzw
     · cases mem_wf.asymmetric₃ _ _ _ hyz hzw hwy
 
-protected theorem isWellOrder (h : x.IsOrdinal) : IsWellOrder x.toSet (Subrel (· ∈ ·) _) where
+protected theorem isWellOrder (h : x.IsOrdinal) : IsWellOrder _ (Subrel (· ∈ ·) (· ∈ x)) where
   wf := (Subrel.relEmbedding _ _).wellFounded mem_wf
   trans := h.isTrans.1
   trichotomous := h.isTrichotomous.1
 
 /-- An ordinal is a transitive set, well-ordered under membership. -/
 theorem _root_.ZFSet.isOrdinal_iff_isWellOrder : x.IsOrdinal ↔
-    x.IsTransitive ∧ IsWellOrder x.toSet (Subrel (· ∈ ·) _) := by
+    x.IsTransitive ∧ IsWellOrder _ (Subrel (· ∈ ·) (· ∈ x)) := by
   use fun h ↦ ⟨h.isTransitive, h.isWellOrder⟩
   rintro ⟨h₁, h₂⟩
   refine isOrdinal_iff_isTrans.2 ⟨h₁, ?_⟩