[Merged by Bors] - refactor(Order/Basic): move Pi & Prop orders to a new file

Mathlib.lean

@@ -5963,6 +5963,7 @@ public import Mathlib.Order.CountableSupClosed
 public import Mathlib.Order.Cover
 public import Mathlib.Order.Defs.LinearOrder
 public import Mathlib.Order.Defs.PartialOrder
+public import Mathlib.Order.Defs.Prop
 public import Mathlib.Order.Defs.Unbundled
 public import Mathlib.Order.DirSupClosed
 public import Mathlib.Order.Directed

Mathlib/Logic/Relation.lean

@@ -9,6 +9,7 @@ public import Mathlib.Logic.Relator
 public import Mathlib.Tactic.Use
 public import Mathlib.Tactic.MkIffOfInductiveProp
 public import Mathlib.Tactic.SimpRw
+public import Mathlib.Order.Defs.Prop
 public import Mathlib.Order.Defs.Unbundled
 public import Batteries.Logic
 public import Batteries.Tactic.Trans
@@ -53,7 +54,7 @@ the bundled version, see `Rel`.
 
 open Function
 
-variable {α β γ δ ε ζ : Sort*}
+variable {α β γ δ ε ζ : Type*}
 
 section NeImp
 
@@ -280,9 +281,8 @@ lemma map_equivalence {r : α → α → Prop} (hr : Equivalence r) (f : α →
   symm := @(hr.stdSymm.map f |>.symm)
   trans := @(hr.isTrans.map hf_ker |>.trans)
 
--- TODO: state this using `≤`, after adjusting imports.
-lemma map_mono {r s : α → β → Prop} {f : α → γ} {g : β → δ} (h : ∀ x y, r x y → s x y) :
-    ∀ x y, Relation.Map r f g x y → Relation.Map s f g x y :=
+lemma map_mono {r s : α → β → Prop} {f : α → γ} {g : β → δ} (h : r ≤ s) :
+    Relation.Map r f g ≤ Relation.Map s f g :=
   fun _ _ ⟨x, y, hxy, hx, hy⟩ => ⟨x, y, h _ _ hxy, hx, hy⟩
 
 lemma le_onFun_map {r : α → α → Prop} (f : α → β) : Subrelation r (Relation.Map r f f on f) := by

Mathlib/Order/Basic.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Data.Subtype
 public import Mathlib.Order.Defs.LinearOrder
+public import Mathlib.Order.Defs.Prop
 public import Mathlib.Order.Notation
 public import Mathlib.Tactic.Spread
 public import Mathlib.Tactic.Convert
@@ -549,15 +550,6 @@ instance Ne.instIsEquiv_compl : IsEquiv α (· ≠ ·)ᶜ := by
 
 /-! ### Order instances on the function space -/
 
-
-instance Pi.hasLe [∀ i, LE (π i)] :
-    LE (∀ i, π i) where le x y := ∀ i, x i ≤ y i
-
-@[to_dual self]
-theorem Pi.le_def [∀ i, LE (π i)] {x y : ∀ i, π i} :
-    x ≤ y ↔ ∀ i, x i ≤ y i :=
-  Iff.rfl
-
 instance Pi.preorder [∀ i, Preorder (π i)] : Preorder (∀ i, π i) where
   __ := (inferInstance : LE (∀ i, π i))
   le_refl := fun a i ↦ le_refl (a i)
@@ -1098,14 +1090,6 @@ end PUnit
 
 section «Prop»
 
-/-- Propositions form a complete Boolean algebra, where the `≤` relation is given by implication. -/
-instance Prop.le : LE Prop :=
-  ⟨(· → ·)⟩
-
-@[simp]
-theorem le_Prop_eq : ((· ≤ ·) : Prop → Prop → Prop) = (· → ·) :=
-  rfl
-
 theorem subrelation_iff_le {r s : α → α → Prop} : Subrelation r s ↔ r ≤ s :=
   Iff.rfl
 

Mathlib/Order/Defs/Prop.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2026 Snir Broshi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Snir Broshi
+-/
+module
+
+import Mathlib.Tactic.ToDual
+
+/-!
+# Order definitions for propositions
+
+This file defines orders on `Pi` and `Prop`.
+-/
+
+public section
+
+instance Pi.hasLe {ι : Type*} {π : ι → Type*} [∀ i, LE (π i)] : LE (∀ i, π i) where
+  le x y := ∀ i, x i ≤ y i
+
+@[to_dual self]
+theorem Pi.le_def {ι : Type*} {π : ι → Type*} [∀ i, LE (π i)] {x y : ∀ i, π i} :
+    x ≤ y ↔ ∀ i, x i ≤ y i :=
+  .rfl
+
+/-- Propositions form a complete Boolean algebra, where the `≤` relation is given by implication. -/
+instance Prop.le : LE Prop :=
+  ⟨(· → ·)⟩
+
+@[simp]
+theorem le_Prop_eq : ((· ≤ ·) : Prop → Prop → Prop) = (· → ·) :=
+  rfl