chore(Order/Defs/Unbundled): deprecate def Reflexive in favor of class Std.Refl (#37278)

Also adds definitional lemmas `std*_def` for the relation classes, and cleans up things nearby, especially in `Logic/Relation.lean`.

Author: SnirBroshi

Mathlib/Algebra/Group/Semiconj/Defs.lean

@@ -99,8 +99,10 @@ theorem one_left (x : M) : SemiconjBy 1 x x :=
 generally, on `MulOneClass` type) is reflexive. -/
 @[to_additive /-- The relation “there exists an element that semiconjugates `a` to `b`” on an
 additive monoid (or, more generally, on an `AddZeroClass` type) is reflexive. -/]
-protected theorem reflexive : Reflexive fun a b : M ↦ ∃ c, SemiconjBy c a b
-  | a => ⟨1, one_left a⟩
+protected theorem refl : Std.Refl fun a b : M ↦ ∃ c, SemiconjBy c a b where
+  refl a := ⟨1, one_left a⟩
+
+@[deprecated (since := "2026-03-27")] protected alias reflexive := SemiconjBy.refl
 
 end MulOneClass
 

Mathlib/CategoryTheory/Abelian/Pseudoelements.lean

@@ -106,8 +106,8 @@ theorem app_hom {P Q : C} (f : P ⟶ Q) (a : Over P) : (app f a).hom = a.hom ≫
 def PseudoEqual (P : C) (f g : Over P) : Prop :=
   ∃ (R : C) (p : R ⟶ f.1) (q : R ⟶ g.1) (_ : Epi p) (_ : Epi q), p ≫ f.hom = q ≫ g.hom
 
-theorem pseudoEqual_refl {P : C} : Reflexive (PseudoEqual P) :=
-  fun f => ⟨f.1, 𝟙 f.1, 𝟙 f.1, inferInstance, inferInstance, by simp⟩
+theorem pseudoEqual_refl {P : C} : Std.Refl (PseudoEqual P) where
+  refl f := ⟨f.1, 𝟙 f.1, 𝟙 f.1, inferInstance, inferInstance, by simp⟩
 
 theorem pseudoEqual_symm {P : C} : Symmetric (PseudoEqual P) :=
   fun _ _ ⟨R, p, q, ep, Eq, comm⟩ => ⟨R, q, p, Eq, ep, comm.symm⟩
@@ -131,7 +131,7 @@ end
 /-- The arrows with codomain `P` equipped with the equivalence relation of being pseudo-equal. -/
 @[instance_reducible]
 def Pseudoelement.setoid (P : C) : Setoid (Over P) :=
-  ⟨_, ⟨pseudoEqual_refl, @pseudoEqual_symm _ _ _, pseudoEqual_trans.trans _ _ _⟩⟩
+  ⟨_, ⟨pseudoEqual_refl.refl, @pseudoEqual_symm _ _ _, pseudoEqual_trans.trans _ _ _⟩⟩
 
 attribute [local instance] Pseudoelement.setoid
 

Mathlib/CategoryTheory/IsConnected.lean

@@ -315,8 +315,7 @@ theorem zigzag_symmetric : Symmetric (@Zigzag J _) :=
   Relation.ReflTransGen.symmetric zag_symmetric
 
 theorem zigzag_equivalence : _root_.Equivalence (@Zigzag J _) :=
-  ⟨Relation.reflexive_reflTransGen, (zigzag_symmetric ·),
-    IsTrans.trans (r := Relation.ReflTransGen _) _ _ _⟩
+  ⟨refl_of <| Relation.ReflTransGen _, (zigzag_symmetric ·), trans_of <| Relation.ReflTransGen _⟩
 
 @[refl] theorem Zigzag.refl (X : J) : Zigzag X X := zigzag_equivalence.refl _
 

Mathlib/Computability/Reduce.lean

@@ -59,11 +59,13 @@ theorem ManyOneReducible.trans {α β γ} [Primcodable α] [Primcodable β] [Pri
     ⟨g ∘ f, c₂.comp c₁,
       fun a => ⟨fun h => by rw [comp_apply, ← h₂, ← h₁]; assumption, fun h => by rwa [h₁, h₂]⟩⟩
 
-theorem reflexive_manyOneReducible {α} [Primcodable α] : Reflexive (@ManyOneReducible α α _ _) :=
-  manyOneReducible_refl
+instance stdRefl_manyOneReducible {α} [Primcodable α] : Std.Refl (@ManyOneReducible α α _ _) where
+  refl := manyOneReducible_refl
 
-theorem isTrans_manyOneReducible {α} [Primcodable α] : IsTrans (α → Prop) ManyOneReducible :=
-  ⟨fun _ _ _ ↦ ManyOneReducible.trans⟩
+@[deprecated (since := "2026-03-27")] alias reflexive_manyOneReducible := stdRefl_manyOneReducible
+
+instance isTrans_manyOneReducible {α} [Primcodable α] : IsTrans (α → Prop) ManyOneReducible where
+  trans _ _ _ := ManyOneReducible.trans
 
 @[deprecated (since := "2026-02-21")] alias transitive_manyOneReducible := isTrans_manyOneReducible
 
@@ -104,11 +106,13 @@ theorem OneOneReducible.of_equiv_symm {α β} [Primcodable α] [Primcodable β]
     (q : β → Prop) (h : Computable e.symm) : q ≤₁ (q ∘ e) := by
   convert OneOneReducible.of_equiv _ h; funext; simp
 
-theorem reflexive_oneOneReducible {α} [Primcodable α] : Reflexive (@OneOneReducible α α _ _) :=
-  oneOneReducible_refl
+instance stdRefl_oneOneReducible {α} [Primcodable α] : Std.Refl (@OneOneReducible α α _ _) where
+  refl := oneOneReducible_refl
+
+@[deprecated (since := "2026-03-27")] alias reflexive_oneOneReducible := stdRefl_oneOneReducible
 
-theorem isTrans_oneOneReducible {α} [Primcodable α] : IsTrans (α → Prop) OneOneReducible :=
-  ⟨fun _ _ _ ↦ OneOneReducible.trans⟩
+instance isTrans_oneOneReducible {α} [Primcodable α] : IsTrans (α → Prop) OneOneReducible where
+  trans _ _ _ := OneOneReducible.trans
 
 @[deprecated (since := "2026-02-21")] alias transitive_oneOneReducible := isTrans_oneOneReducible
 

Mathlib/Data/List/Pairwise.lean

@@ -54,12 +54,12 @@ theorem Pairwise.forall (hR : Symmetric R) (hl : l.Pairwise R) :
 theorem Pairwise.set_pairwise (hl : Pairwise R l) (hr : Symmetric R) : { x | x ∈ l }.Pairwise R :=
   hl.forall hr
 
-theorem pairwise_of_reflexive_of_forall_ne (hr : Reflexive R)
-    (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → R a b) : l.Pairwise R := by
+theorem pairwise_of_reflexive_of_forall_ne [Std.Refl R] (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → R a b) :
+    l.Pairwise R := by
   rw [pairwise_iff_forall_sublist]
   intro a b hab
   if heq : a = b then
-    cases heq; apply hr
+    cases heq; apply refl
   else
     apply h <;> try (apply hab.subset; simp)
     exact heq

Mathlib/Data/Seq/Computation.lean

@@ -880,8 +880,8 @@ theorem lift_eq_iff_equiv (c₁ c₂ : Computation α) : LiftRel (· = ·) c₁
      fun a2 => by let ⟨b, b1, ab⟩ := h2 a2; rwa [← ab]⟩,
     fun e => ⟨fun {a} a1 => ⟨a, (e _).1 a1, rfl⟩, fun {a} a2 => ⟨a, (e _).2 a2, rfl⟩⟩⟩
 
-theorem LiftRel.refl (R : α → α → Prop) (H : Reflexive R) : Reflexive (LiftRel R) := fun _ =>
-  ⟨fun {a} as => ⟨a, as, H a⟩, fun {b} bs => ⟨b, bs, H b⟩⟩
+instance LiftRel.refl (R : α → α → Prop) [Std.Refl R] : Std.Refl (LiftRel R) where
+  refl _ := ⟨fun {a} as => ⟨a, as, refl_of R a⟩, fun {b} bs => ⟨b, bs, refl_of R b⟩⟩
 
 theorem LiftRel.symm (R : α → α → Prop) (H : Symmetric R) : Symmetric (LiftRel R) :=
   fun _ _ ⟨l, r⟩ =>
@@ -892,19 +892,21 @@ theorem LiftRel.symm (R : α → α → Prop) (H : Symmetric R) : Symmetric (Lif
     let ⟨b, b2, ab⟩ := l a1
     ⟨b, b2, H ab⟩⟩
 
-theorem LiftRel.trans (R : α → α → Prop) (H : IsTrans α R) : IsTrans _ (LiftRel R) :=
+instance LiftRel.trans (R : α → α → Prop) [IsTrans α R] : IsTrans _ (LiftRel R) :=
   ⟨fun _ _ _ ⟨l1, r1⟩ ⟨l2, r2⟩ =>
-  ⟨fun {a} a1 =>
-    let ⟨b, b2, ab⟩ := l1 a1
+  ⟨fun {_a} a1 =>
+    let ⟨_b, b2, ab⟩ := l1 a1
     let ⟨c, c3, bc⟩ := l2 b2
-    ⟨c, c3, H.trans a b c ab bc⟩,
-    fun {c} c3 =>
-    let ⟨b, b2, bc⟩ := r2 c3
+    ⟨c, c3, trans_of R ab bc⟩,
+    fun {_c} c3 =>
+    let ⟨_b, b2, bc⟩ := r2 c3
     let ⟨a, a1, ab⟩ := r1 b2
-    ⟨a, a1, H.trans a b c ab bc⟩⟩⟩
+    ⟨a, a1, trans_of R ab bc⟩⟩⟩
 
-theorem LiftRel.equiv (R : α → α → Prop) (H : Equivalence R) : Equivalence (LiftRel R) :=
-  ⟨LiftRel.refl R H.refl, @LiftRel.symm _ R @H.symm, LiftRel.trans R H.isTrans |>.trans _ _ _⟩
+theorem LiftRel.equiv (R : α → α → Prop) (H : Equivalence R) : Equivalence (LiftRel R) where
+  refl := @LiftRel.refl α R H.stdRefl |>.refl
+  symm := @LiftRel.symm α R H.symmetric
+  trans := @LiftRel.trans α R H.isTrans |>.trans _ _ _
 
 theorem LiftRel.imp {R S : α → β → Prop} (H : ∀ {a b}, R a b → S a b) (s t) :
     LiftRel R s t → LiftRel S s t

Mathlib/Data/Sym/Sym2.lean

@@ -620,20 +620,19 @@ lemma diagSet_eq_fromRel_eq : diagSet = fromRel (α := α) eq_equivalence.symmet
 lemma diagSet_compl_eq_fromRel_ne : diagSetᶜ = fromRel (α := α) (r := Ne) (fun _ _ ↦ Ne.symm) := by
   ext ⟨a, b⟩; simp
 
-@[simp] lemma diagSet_subset_fromRel (hr : Symmetric r) : diagSet ⊆ fromRel hr ↔ Reflexive r := by
-  simp [Set.subset_def, Sym2.forall, Reflexive]
+@[simp] lemma diagSet_subset_fromRel (hr : Symmetric r) : diagSet ⊆ fromRel hr ↔ Std.Refl r := by
+  simp [Set.subset_def, Sym2.forall, refl_def]
 
 @[simp] lemma disjoint_diagSet_fromRel (hr : Symmetric r) :
     Disjoint diagSet (fromRel hr) ↔ Std.Irrefl r := by
-  refine .trans ?_ ⟨(⟨·⟩), (·.irrefl)⟩
-  simp [Set.disjoint_left, Sym2.forall]
+  simp [Set.disjoint_left, Sym2.forall, irrefl_def]
 
 @[simp] lemma fromRel_subset_compl_diagSet (hr : Symmetric r) :
     fromRel hr ⊆ diagSetᶜ ↔ Std.Irrefl r := by simp [Set.subset_compl_iff_disjoint_left]
 
 @[deprecated diagSet_subset_fromRel (since := "2025-12-10")]
 theorem reflexive_iff_diagSet_subset_fromRel (sym : Symmetric r) :
-    Reflexive r ↔ diagSet ⊆ fromRel sym := by simp
+    Std.Refl r ↔ diagSet ⊆ fromRel sym := by simp
 
 @[deprecated fromRel_subset_compl_diagSet (since := "2025-12-10")]
 theorem irreflexive_iff_fromRel_subset_diagSet_compl (sym : Symmetric r) :

Mathlib/Data/WSeq/Relation.lean

@@ -104,21 +104,24 @@ theorem LiftRel.swap_lem {R : α → β → Prop} {s1 s2} (h : LiftRel R s1 s2)
 theorem LiftRel.swap (R : α → β → Prop) : swap (LiftRel R) = LiftRel (swap R) :=
   funext fun _ => funext fun _ => propext ⟨LiftRel.swap_lem, LiftRel.swap_lem⟩
 
-theorem LiftRel.refl (R : α → α → Prop) (H : Reflexive R) : Reflexive (LiftRel R) := fun s => by
-  refine ⟨(· = ·), rfl, fun {s t} (h : s = t) => ?_⟩
-  rw [← h]
-  apply Computation.LiftRel.refl
-  intro a
-  rcases a with - | a
-  · simp
-  · cases a
-    simp only [LiftRelO, and_true]
-    apply H
+instance LiftRelO.refl (R : α → α → Prop) [Std.Refl R] : Std.Refl <| LiftRelO R (· = ·) where
+  refl a := by
+    rcases a with - | a
+    · simp
+    · cases a
+      simp only [LiftRelO, and_true]
+      apply refl_of R
+
+instance LiftRel.refl (R : α → α → Prop) [Std.Refl R] : Std.Refl (LiftRel R) where
+  refl s := by
+    refine ⟨(· = ·), rfl, fun {s t} (h : s = t) => ?_⟩
+    rw [← h]
+    apply Computation.LiftRel.refl _ |>.refl
 
 theorem LiftRel.symm (R : α → α → Prop) (H : Symmetric R) : Symmetric (LiftRel R) :=
   fun s1 s2 (h : Function.swap (LiftRel R) s2 s1) => by rwa [LiftRel.swap, H.swap_eq] at h
 
-theorem LiftRel.trans (R : α → α → Prop) (H : IsTrans α R) : IsTrans _ (LiftRel R) := by
+instance LiftRel.trans (R : α → α → Prop) [IsTrans α R] : IsTrans _ (LiftRel R) := by
   refine ⟨fun s t u h1 h2 ↦ ?_⟩
   refine ⟨fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u, ⟨t, h1, h2⟩, fun {s u} h => ?_⟩
   rcases h with ⟨t, h1, h2⟩
@@ -147,10 +150,12 @@ theorem LiftRel.trans (R : α → α → Prop) (H : IsTrans α R) : IsTrans _ (L
     obtain ⟨c, u⟩ := c
     obtain ⟨ab, st⟩ := t1
     obtain ⟨bc, tu⟩ := t2
-    exact ⟨H.trans a b c ab bc, t, st, tu⟩
+    exact ⟨trans_of R ab bc, t, st, tu⟩
 
-theorem LiftRel.equiv (R : α → α → Prop) (H : Equivalence R) : Equivalence (LiftRel R) :=
-  ⟨LiftRel.refl R H.refl, @(LiftRel.symm R @H.symm), LiftRel.trans R H.isTrans |>.trans _ _ _⟩
+theorem LiftRel.equiv (R : α → α → Prop) (H : Equivalence R) : Equivalence (LiftRel R) where
+  refl := @LiftRel.refl α R H.stdRefl |>.refl
+  symm := @LiftRel.symm α R H.symmetric
+  trans := @LiftRel.trans α R H.isTrans |>.trans _ _ _
 
 /-- If two sequences are equivalent, then they have the same values and
   the same computational behavior (i.e. if one loops forever then so does
@@ -163,15 +168,15 @@ def Equiv : WSeq α → WSeq α → Prop :=
 
 @[refl]
 theorem Equiv.refl : ∀ s : WSeq α, s ~ʷ s :=
-  LiftRel.refl (· = ·) Eq.refl
+  LiftRel.refl (· = ·) |>.refl
 
 @[symm]
 theorem Equiv.symm : ∀ {s t : WSeq α}, s ~ʷ t → t ~ʷ s :=
   @(LiftRel.symm (· = ·) (@Eq.symm _))
 
 @[trans]
 theorem Equiv.trans : ∀ {s t u : WSeq α}, s ~ʷ t → t ~ʷ u → s ~ʷ u :=
-  LiftRel.trans (· = ·) inferInstance |>.trans _ _ _
+  LiftRel.trans (· = ·) |>.trans _ _ _
 
 theorem Equiv.equivalence : Equivalence (@Equiv α) :=
   ⟨@Equiv.refl _, @Equiv.symm _, @Equiv.trans _⟩

Mathlib/GroupTheory/FreeGroup/Basic.lean

@@ -323,7 +323,7 @@ theorem Step.sublist (H : Red.Step L₁ L₂) : L₂ <+ L₁ := by
 protected theorem sublist : Red L₁ L₂ → L₂ <+ L₁ :=
   @reflTransGen_of_isTrans_reflexive
     _ (fun a b => b <+ a) _ _ _
-    (fun l => List.Sublist.refl l)
+    ⟨List.Sublist.refl⟩
     ⟨fun _a _b _c hab hbc => List.Sublist.trans hbc hab⟩
     (fun _ _ => Red.Step.sublist)
 
@@ -367,8 +367,9 @@ theorem equivalence_join_red : Equivalence (Join (@Red α)) :=
     | _, _, Or.inr ⟨d, hbd, hcd⟩ => ⟨d, ReflGen.single hbd, ReflTransGen.single hcd⟩
 
 @[to_additive]
-theorem join_red_of_step (h : Red.Step L₁ L₂) : Join Red L₁ L₂ :=
-  join_of_single reflexive_reflTransGen h.to_red
+theorem join_red_of_step (h : Red.Step L₁ L₂) : Join Red L₁ L₂ := by
+  unfold Red
+  exact join_of_single h.to_red
 
 @[to_additive]
 theorem eqvGen_step_iff_join_red : EqvGen Red.Step L₁ L₂ ↔ Join Red L₁ L₂ :=

Mathlib/Logic/Pairwise.lean

@@ -96,10 +96,13 @@ theorem Pairwise.imp (h : s.Pairwise r) (hpq : ∀ ⦃a b : α⦄, r a b → p a
 protected theorem Pairwise.eq (hs : s.Pairwise r) (ha : a ∈ s) (hb : b ∈ s) (h : ¬r a b) : a = b :=
   of_not_not fun hab => h <| hs ha hb hab
 
-theorem _root_.Reflexive.set_pairwise_iff (hr : Reflexive r) :
+theorem _root_.Std.Refl.set_pairwise_iff [Std.Refl r] :
     s.Pairwise r ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → r a b :=
   forall₄_congr fun a _ _ _ => or_iff_not_imp_left.symm.trans <| or_iff_right_of_imp <| Eq.ndrec <|
-    hr a
+    refl a
+
+@[deprecated (since := "2026-03-27")]
+alias _root_.Reflexive.set_pairwise_iff := Std.Refl.set_pairwise_iff
 
 theorem Pairwise.on_injective (hs : s.Pairwise r) (hf : Function.Injective f) (hfs : ∀ x, f x ∈ s) :
     Pairwise (r on f) := fun i j hij => hs (hfs i) (hfs j) (hf.ne hij)