-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s,
      p < q →
        ∃ (u : Set α) (v : Set α),
          MeasurableSet u ∧
            MeasurableSet v ∧
              {x : α | f x < p} ⊆ u ∧
                {x : α | q < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
haveI haveI₁ haveI₂ : ∀ (this : Encodable (↑s : Type u_2)), AEMeasurable f μ
haveI₃ :
  ∀ (this : Encodable (↑s : Type u_2))
    (h' :
      ∀ (p q : β),
        ∃ (u : Set α) (v : Set α),
          MeasurableSet u ∧
            MeasurableSet v ∧
              {x : α | f x < p} ⊆ u ∧
                {x : α | q < f x} ⊆ v ∧
                  (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞))),
    AEMeasurable f μ
haveI₄ haveI₅ :
  ∀ (this : Encodable (↑s : Type u_2)) (u v : (p q : β) → Set α)
    (huv :
      ∀ (p q : β),
        MeasurableSet (u p q) ∧
          MeasurableSet (v p q) ∧
            {x : α | f x < p} ⊆ u p q ∧
              {x : α | q < f x} ⊆ v p q ∧
                (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u p q ∩ v p q) : ℝ≥0∞) (0 : ℝ≥0∞))),
    AEMeasurable f μ
haveI₆ haveI₇ :
  ∀ (this : Encodable (↑s : Type u_2)) (u v : (p q : β) → Set α)
    (huv :
      ∀ (p q : β),
        MeasurableSet (u p q) ∧
          MeasurableSet (v p q) ∧
            {x : α | f x < p} ⊆ u p q ∧
              {x : α | q < f x} ⊆ v p q ∧
                (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u p q ∩ v p q) : ℝ≥0∞) (0 : ℝ≥0∞))),
    let u' : β → Set α := fun (p : β) ↦ ⋂ q ∈ s ∩ Ioi p, u p q;
    ∀ (u'_meas : ∀ (i : β), MeasurableSet (u' i)), AEMeasurable f μ
haveI₈ haveI₉ :
  ∀ (this : Encodable (↑s : Type u_2)) (u v : (p q : β) → Set α)
    (huv :
      ∀ (p q : β),
        MeasurableSet (u p q) ∧
          MeasurableSet (v p q) ∧
            {x : α | f x < p} ⊆ u p q ∧
              {x : α | q < f x} ⊆ v p q ∧
                (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u p q ∩ v p q) : ℝ≥0∞) (0 : ℝ≥0∞))),
    let u' : β → Set α := fun (p : β) ↦ ⋂ q ∈ s ∩ Ioi p, u p q;
    ∀ (u'_meas : ∀ (i : β), MeasurableSet (u' i)),
      let f' : α → β := fun (x : α) ↦
        ⨅ (i : (↑s : Type u_2)),
          (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x;
      ∀ (f'_meas : Measurable f'), AEMeasurable f μ
haveI₁₀ :
  ∀ (this : Encodable (↑s : Type u_2)) (u v : (p q : β) → Set α)
    (huv :
      ∀ (p q : β),
        MeasurableSet (u p q) ∧
          MeasurableSet (v p q) ∧
            {x : α | f x < p} ⊆ u p q ∧
              {x : α | q < f x} ⊆ v p q ∧
                (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u p q ∩ v p q) : ℝ≥0∞) (0 : ℝ≥0∞))),
    let u' : β → Set α := fun (p : β) ↦ ⋂ q ∈ s ∩ Ioi p, u p q;
    ∀ (u'_meas : ∀ (i : β), MeasurableSet (u' i)),
      let f' : α → β := fun (x : α) ↦
        ⨅ (i : (↑s : Type u_2)),
          (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x;
      ∀ (f'_meas : Measurable f'),
        let t : Set α :=
          ⋃ (p : (↑s : Type u_2)), ⋃ (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)), u' (↑p : β) ∩ v (↑p : β) (↑q : β);
        ∀ (μt : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)), AEMeasurable f μ
haveI₁₁ :
  ∀ (this : Encodable (↑s : Type u_2)) (u v : (p q : β) → Set α)
    (huv :
      ∀ (p q : β),
        MeasurableSet (u p q) ∧
          MeasurableSet (v p q) ∧
            {x : α | f x < p} ⊆ u p q ∧
              {x : α | q < f x} ⊆ v p q ∧
                (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u p q ∩ v p q) : ℝ≥0∞) (0 : ℝ≥0∞))),
    let u' : β → Set α := fun (p : β) ↦ ⋂ q ∈ s ∩ Ioi p, u p q;
    ∀ (u'_meas : ∀ (i : β), MeasurableSet (u' i)),
      let f' : α → β := fun (x : α) ↦
        ⨅ (i : (↑s : Type u_2)),
          (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x;
      ∀ (f'_meas : Measurable f'),
        let t : Set α :=
          ⋃ (p : (↑s : Type u_2)), ⋃ (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)), u' (↑p : β) ∩ v (↑p : β) (↑q : β);
        ∀ (μt : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)) (ff' : ∀ᵐ (x : α) ∂μ, f x = f' x),
          AEMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
classical
  haveI : Encodable s := s_count.toEncodable
  have h' : ∀ p q, ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧
      { x | f x < p } ⊆ u ∧ { x | q < f x } ⊆ v ∧ (p ∈ s → q ∈ s → p < q → μ (u ∩ v) = 0) := by
    intro p q
    by_cases H : p ∈ s ∧ q ∈ s ∧ p < q
    · rcases h p H.1 q H.2.1 H.2.2 with ⟨u, v, hu, hv, h'u, h'v, hμ⟩
      exact ⟨u, v, hu, hv, h'u, h'v, fun _ _ _ => hμ⟩
    · refine
        ⟨univ, univ, MeasurableSet.univ, MeasurableSet.univ, subset_univ _, subset_univ _,
          fun ps qs pq => ?_⟩
      exact (H ⟨ps, qs, pq⟩).elim
  choose! u v huv using h'
  let u' : β → Set α := fun p => ⋂ q ∈ s ∩ Ioi p, u p q
  have u'_meas : ∀ i, MeasurableSet (u' i) := by
    intro i
    exact MeasurableSet.biInter (s_count.mono inter_subset_left) fun b _ => (huv i b).1
  let f' : α → β := fun x => ⨅ i : s, piecewise (u' i) (fun _ => (i : β)) (fun _ => (⊤ : β)) x
  have f'_meas : Measurable f' := by fun_prop (disch := simp_all)
  let t := ⋃ (p : s) (q : ↥(s ∩ Ioi p)), u' p ∩ v p q
  have μt : μ t ≤ 0 :=
    calc
      μ t ≤ ∑' (p : s) (q : ↥(s ∩ Ioi p)), μ (u' p ∩ v p q) := by
        refine (measure_iUnion_le _).trans ?_
        refine ENNReal.tsum_le_tsum fun p => ?_
        haveI := (s_count.mono (s.inter_subset_left (t := Ioi ↑p))).to_subtype
        apply measure_iUnion_le
      _ ≤ ∑' (p : s) (q : ↥(s ∩ Ioi p)), μ (u p q ∩ v p q) := by
        gcongr with p q
        exact biInter_subset_of_mem q.2
      _ = ∑' (p : s) (_ : ↥(s ∩ Ioi p)), (0 : ℝ≥0∞) := by grind
      _ = 0 := by simp only [tsum_zero]
  have ff' : ∀ᵐ x ∂μ, f x = f' x := by
    have : ∀ᵐ x ∂μ, x ∉ t := by
      have : μ t = 0 := le_antisymm μt bot_le
      change μ _ = 0
      convert! this
      ext y
      simp only [mem_setOf_eq, mem_compl_iff, not_notMem]
    filter_upwards [this] with x hx
    apply (iInf_eq_of_forall_ge_of_forall_gt_exists_lt _ _).symm
    · intro i
      by_cases H : x ∈ u' i
      swap
      · simp only [H, le_top, not_false_iff, piecewise_eq_of_notMem]
      simp only [H, piecewise_eq_of_mem]
      contrapose! hx
      obtain ⟨r, ⟨xr, rq⟩, rs⟩ : ∃ r, r ∈ Ioo (i : β) (f x) ∩ s :=
        dense_iff_inter_open.1 s_dense (Ioo i (f x)) isOpen_Ioo (nonempty_Ioo.2 hx)
      have A : x ∈ v i r := (huv i r).2.2.2.1 rq
      refine mem_iUnion.2 ⟨i, ?_⟩
      refine mem_iUnion.2 ⟨⟨r, ⟨rs, xr⟩⟩, ?_⟩
      exact ⟨H, A⟩
    · intro q hq
      obtain ⟨r, ⟨xr, rq⟩, rs⟩ : ∃ r, r ∈ Ioo (f x) q ∩ s :=
        dense_iff_inter_open.1 s_dense (Ioo (f x) q) isOpen_Ioo (nonempty_Ioo.2 hq)
      refine ⟨⟨r, rs⟩, ?_⟩
      have A : x ∈ u' r := mem_biInter fun i _ => (huv r i).2.2.1 xr
      simp only [A, rq, piecewise_eq_of_mem]
  exact ⟨f', f'_meas, ff'⟩