Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
⊢ ∃ a b c,
    a ∪ (b ∪ c) = s ∧
      MeasurableSet a ∧
        MeasurableSet b ∧
          MeasurableSet c ∧
            Disjoint a (b ∪ c) ∧
              Disjoint b c ∧ a.Countable ∧ (f '' b).Countable ∧ (∀ x ∈ b, f' x = 0) ∧ (∀ x ∈ c, 0 ≤ f' x) ∧ InjOn f c

Tactic:
by
  let a := {x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x ∈ s | 𝓝[s ∩ Iio x] x = ⊥}
  have a_count : a.Countable :=
    countable_setOfPred_isolated_right_within.union countable_setOfPred_isolated_left_within
  let s₁ := s \ a
  have hs₁ : MeasurableSet s₁ := hs.diff a_count.measurableSet
  let u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
  have hu : Set.Countable u := MonotoneOn.countable_setOfPred_two_preimages (hf.mono sdiff_subset)
  let b := s₁ ∩ f ⁻¹' u
  have hb : MeasurableSet b := by
    have : b = ⋃ z ∈ u, s₁ ∩ f ⁻¹' {z} := by ext; simp [b]
    rw [this]
    apply MeasurableSet.biUnion hu (fun z hz ↦ ?_)
    obtain ⟨v, hv, tv⟩ : ∃ v, OrdConnected v ∧ (s \ a) ∩ f ⁻¹' {z} = (s \ a) ∩ v :=
      ordConnected_singleton.preimage_monotoneOn (hf.mono sdiff_subset)
    exact tv ▸ (hs.diff a_count.measurableSet).inter hv.measurableSet
  let c := s₁ \ b
  have hc : MeasurableSet c := hs₁.diff hb
  refine ⟨a, b, c, ?_, a_count.measurableSet, hb, hc, ?_, ?_, a_count, ?_, ?_, ?_, ?_⟩
  · ext x
    simp only [sdiff_self_inter, inter_union_sdiff, union_sdiff_self, mem_union, mem_ofPred_eq,
      or_iff_right_iff_imp, a, b, s₁, c]
    tauto
  · simpa [b, c, s₁] using disjoint_sdiff_right
  · simpa [c] using disjoint_sdiff_right
  · exact hu.mono (by simp [b])
  · /- We have to show that the derivative is `0` at `x ∈ b`. For that, we use that there is another
    point `p` with `f p = f x`, by definition of `b`. If `p < x`, then `f` is locally constant to
    the left of `x`. As `x` is not isolated to its left (since we are not in the set `a`), it
    follows that `f' x = 0`. The same argument works if `x < p`, using the right neighborhood
    instead. -/
    intro x hx
    obtain ⟨p, ps₁, px, fpx⟩ : ∃ p ∈ s₁, p ≠ x ∧ f p = f x := by
      rcases hx.2 with ⟨p, q, ps₁, qs₁, pq, hp, hq⟩
      rcases eq_or_ne p x with h'p | h'p
      · exact ⟨q, qs₁, (h'p.symm.le.trans_lt pq).ne', hq⟩
      · exact ⟨p, ps₁, h'p, hp⟩
    -- we treat separately the cases `p < x` and `x < p` as we couldn't unify their proofs nicely
    rcases lt_or_gt_of_ne px with px | px
    · have K : HasDerivWithinAt f 0 (s ∩ Ioo p x) x := by
        have E (y) (hy : y ∈ s ∩ Ioo p x) : f y = f x := by
          apply le_antisymm (hf hy.1 hx.1.1 hy.2.2.le)
          rw [← fpx]
          exact hf ps₁.1 hy.1 hy.2.1.le
        have : HasDerivWithinAt (fun y ↦ f x) 0 (s ∩ Ioo p x) x :=
          hasDerivWithinAt_const x (s ∩ Ioo p x) (f x)
        exact this.congr E rfl
      have K' : HasDerivWithinAt f (f' x) (s ∩ Ioo p x) x :=
        (hf' x hx.1.1).mono inter_subset_left
      apply UniqueDiffWithinAt.eq_deriv _ _ K' K
      have J1 : (s ∩ Ioo p x) \ {x} = s ∩ Ioo p x := by simp
      have J2 : 𝓝[s ∩ Ioo p x] x = 𝓝[s ∩ Iio x] x := by
        simp [nhdsWithin_inter, nhdsWithin_Ioo_eq_nhdsLT px]
      rw [uniqueDiffWithinAt_iff_accPt, accPt_principal_iff_nhdsWithin, J1, J2]
      simp only [mem_inter_iff, Set.mem_sdiff, hx.1.1, mem_union, mem_ofPred_eq, true_and, not_or,
        mem_preimage, b, s₁, a] at hx
      exact neBot_iff.2 hx.1.2
    · have K : HasDerivWithinAt f 0 (s ∩ Ioo x p) x := by
        have E (y) (hy : y ∈ s ∩ Ioo x p) : f y = f x := by
          apply le_antisymm _ (hf hx.1.1 hy.1 hy.2.1.le)
          rw [← fpx]
          exact hf hy.1 ps₁.1 hy.2.2.le
        have : HasDerivWithinAt (fun y ↦ f x) 0 (s ∩ Ioo x p) x :=
          hasDerivWithinAt_const x (s ∩ Ioo x p) (f x)
        exact this.congr E rfl
      have K' : HasDerivWithinAt f (f' x) (s ∩ Ioo x p) x :=
        (hf' x hx.1.1).mono inter_subset_left
      apply UniqueDiffWithinAt.eq_deriv _ _ K' K
      have J1 : (s ∩ Ioo x p) \ {x} = (s ∩ Ioo x p) := by simp
      have J2 : 𝓝[s ∩ Ioo x p] x = 𝓝[s ∩ Ioi x] x := by
        simp [nhdsWithin_inter, nhdsWithin_Ioo_eq_nhdsGT px]
      rw [uniqueDiffWithinAt_iff_accPt, accPt_principal_iff_nhdsWithin, J1, J2]
      simp only [mem_inter_iff, Set.mem_sdiff, hx.1.1, mem_union, mem_ofPred_eq, true_and, not_or,
        mem_preimage, b, s₁, a] at hx
      exact neBot_iff.2 hx.1.1
  · /- We have to show that the derivative is nonnegative at points of `c`. As these points are
    not isolated in `s`, this follows from the fact that `f` is monotone on `s`. -/
    intro x hx
    apply (hf' x hx.1.1).nonneg_of_monotoneOn _ hf
    simp only [Set.mem_sdiff, hx.1.1, mem_union, mem_ofPred_eq, true_and, not_or, c, s₁, a, b] at hx
    rw [accPt_principal_iff_nhdsWithin]
    have : (𝓝[s ∩ Iio x] x).NeBot := neBot_iff.2 hx.1.2
    apply this.mono
    apply nhdsWithin_mono
    rintro y ⟨yt, yx : y < x⟩
    exact ⟨yt, by simpa using yx.ne⟩
  · intro x hx y hy hxy
    contrapose! hxy
    wlog H : x < y generalizing x y with h
    · have : y < x := by order
      exact (h hy hx hxy.symm this).symm
    refine fun h ↦ hx.2 ⟨hx.1, ?_⟩
    exact ⟨x, y, hx.1, hy.1, H, rfl, h.symm⟩

Goal state after: