From d719abc7d36140758a11fb9b4c27651689083829 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Fri, 26 Jan 2024 10:40:14 -0800
Subject: [PATCH 1/3] chore(Probability/Kernel/CondCdf): mv some theorems

---
 Mathlib/Logic/Encodable/Basic.lean      | 10 ++++++++++
 Mathlib/Probability/Kernel/CondCdf.lean | 16 +---------------
 2 files changed, 11 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Logic/Encodable/Basic.lean b/Mathlib/Logic/Encodable/Basic.lean
index 62579a65debf8..2c4d67ab73263 100644
--- a/Mathlib/Logic/Encodable/Basic.lean
+++ b/Mathlib/Logic/Encodable/Basic.lean
@@ -665,6 +665,16 @@ theorem le_sequence (a : α) : f a ≤ f (hf.sequence f (encode a + 1)) :=
   hf.rel_sequence a
 #align directed.le_sequence Directed.le_sequence
 
+variable (hf : Directed (· ≥ ·) f)
+
+theorem sequence_anti : Antitone (f ∘ hf.sequence f) :=
+  antitone_nat_of_succ_le <| hf.sequence_mono_nat
+#align directed.sequence_anti Directed.sequence_anti
+
+theorem sequence_le (a : α) : f (hf.sequence f (Encodable.encode a + 1)) ≤ f a :=
+  hf.rel_sequence a
+#align directed.sequence_le Directed.sequence_le
+
 end Directed
 
 section Quotient
diff --git a/Mathlib/Probability/Kernel/CondCdf.lean b/Mathlib/Probability/Kernel/CondCdf.lean
index 2d223aba3e6ac..6e4ae2bbe3bd2 100644
--- a/Mathlib/Probability/Kernel/CondCdf.lean
+++ b/Mathlib/Probability/Kernel/CondCdf.lean
@@ -6,6 +6,7 @@ Authors: Rémy Degenne
 import Mathlib.MeasureTheory.Measure.Stieltjes
 import Mathlib.MeasureTheory.Decomposition.RadonNikodym
 import Mathlib.MeasureTheory.Constructions.Prod.Basic
+import Mathlib.Logic.Encodable.Basic
 
 #align_import probability.kernel.cond_cdf from "leanprover-community/mathlib"@"3b88f4005dc2e28d42f974cc1ce838f0dafb39b8"
 
@@ -51,21 +52,6 @@ section AuxLemmasToBeMoved
 
 variable {α β ι : Type*}
 
-namespace Directed
-
--- todo after the port: move this to logic.encodable.basic near sequence_mono
-variable [Encodable α] [Inhabited α] [Preorder β] {f : α → β} (hf : Directed (· ≥ ·) f)
-
-theorem sequence_anti : Antitone (f ∘ hf.sequence f) :=
-  antitone_nat_of_succ_le <| hf.sequence_mono_nat
-#align directed.sequence_anti Directed.sequence_anti
-
-theorem sequence_le (a : α) : f (hf.sequence f (Encodable.encode a + 1)) ≤ f a :=
-  hf.rel_sequence a
-#align directed.sequence_le Directed.sequence_le
-
-end Directed
-
 -- todo: move to data/set/lattice next to prod_sUnion or prod_sInter
 theorem prod_iInter {s : Set α} {t : ι → Set β} [hι : Nonempty ι] :
     (s ×ˢ ⋂ i, t i) = ⋂ i, s ×ˢ t i := by

From 9f27b534912016be076716da60c0bb02b549de1b Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Fri, 26 Jan 2024 10:48:47 -0800
Subject: [PATCH 2/3] Update Mathlib/Probability/Kernel/CondCdf.lean

---
 Mathlib/Probability/Kernel/CondCdf.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Probability/Kernel/CondCdf.lean b/Mathlib/Probability/Kernel/CondCdf.lean
index 6e4ae2bbe3bd2..e060ba82a1cda 100644
--- a/Mathlib/Probability/Kernel/CondCdf.lean
+++ b/Mathlib/Probability/Kernel/CondCdf.lean
@@ -3,10 +3,10 @@ Copyright (c) 2023 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
+import Mathlib.Logic.Encodable.Basic
 import Mathlib.MeasureTheory.Measure.Stieltjes
 import Mathlib.MeasureTheory.Decomposition.RadonNikodym
 import Mathlib.MeasureTheory.Constructions.Prod.Basic
-import Mathlib.Logic.Encodable.Basic
 
 #align_import probability.kernel.cond_cdf from "leanprover-community/mathlib"@"3b88f4005dc2e28d42f974cc1ce838f0dafb39b8"
 

From 5d5226ce5a30d2f6072da4640e6251473b554274 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sat, 27 Jan 2024 10:09:56 -0800
Subject: [PATCH 3/3] add sections

---
 Mathlib/Logic/Encodable/Basic.lean | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Logic/Encodable/Basic.lean b/Mathlib/Logic/Encodable/Basic.lean
index 2c4d67ab73263..283c750ab734a 100644
--- a/Mathlib/Logic/Encodable/Basic.lean
+++ b/Mathlib/Logic/Encodable/Basic.lean
@@ -655,7 +655,11 @@ theorem rel_sequence {r : β → β → Prop} {f : α → β} (hf : Directed r f
   exact (Classical.choose_spec (hf _ a)).2
 #align directed.rel_sequence Directed.rel_sequence
 
-variable [Preorder β] {f : α → β} (hf : Directed (· ≤ ·) f)
+variable [Preorder β] {f : α → β}
+
+section
+
+variable (hf : Directed (· ≤ ·) f)
 
 theorem sequence_mono : Monotone (f ∘ hf.sequence f) :=
   monotone_nat_of_le_succ <| hf.sequence_mono_nat
@@ -665,6 +669,10 @@ theorem le_sequence (a : α) : f a ≤ f (hf.sequence f (encode a + 1)) :=
   hf.rel_sequence a
 #align directed.le_sequence Directed.le_sequence
 
+end
+
+section
+
 variable (hf : Directed (· ≥ ·) f)
 
 theorem sequence_anti : Antitone (f ∘ hf.sequence f) :=
@@ -675,6 +683,8 @@ theorem sequence_le (a : α) : f (hf.sequence f (Encodable.encode a + 1)) ≤ f
   hf.rel_sequence a
 #align directed.sequence_le Directed.sequence_le
 
+end
+
 end Directed
 
 section Quotient