awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
x : ℝ
⊢ x ∈ b ↔ Membership.mem (γ := Set ℝ) (⋃ z ∈ u, s₁ ∩ f ⁻¹' {z}) x

Tactic:
simp [b]
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
⊢ b = ⋃ z ∈ u, s₁ ∩ f ⁻¹' {z}

Tactic:
have : b = ⋃ z ∈ u, s₁ ∩ f ⁻¹' {z} := by ext; simp [b]
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
this : b = ⋃ z ∈ u, s₁ ∩ f ⁻¹' {z}
rw : MeasurableSet (α := ℝ) (⋃ z ∈ u, s₁ ∩ f ⁻¹' {z})
⊢ MeasurableSet b

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
this : b = ⋃ z ∈ u, s₁ ∩ f ⁻¹' {z}
apply : ∀ (z : ℝ) (hz : z ∈ u), MeasurableSet (s₁ ∩ f ⁻¹' {z})
⊢ MeasurableSet (α := ℝ) (⋃ z ∈ u, s₁ ∩ f ⁻¹' {z})

Tactic:
apply MeasurableSet.biUnion hu (fun z hz ↦ ?_)

Premises used: MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
this : b = ⋃ z ∈ u, s₁ ∩ f ⁻¹' {z}
z : ℝ
hz : z ∈ u
⊢ ∃ (v : Set ℝ), v.OrdConnected ∧ s \ a ∩ f ⁻¹' {z} = s \ a ∩ v

Tactic:
ordConnected_singleton.preimage_monotoneOn (hf.mono diff_subset)

Premises used: Set.diff_subset, Set.ordConnected_singleton, Set.OrdConnected.preimage_monotoneOn, MonotoneOn.mono
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
this : b = ⋃ z ∈ u, s₁ ∩ f ⁻¹' {z}
z : ℝ
hz : z ∈ u
obtain : ∀ (v : Set ℝ) (hv : v.OrdConnected) (tv : s \ a ∩ f ⁻¹' {z} = s \ a ∩ v), MeasurableSet (s₁ ∩ f ⁻¹' {z})
⊢ MeasurableSet (s₁ ∩ f ⁻¹' {z})

Tactic:
obtain ⟨v, hv, tv⟩ : ∃ v, OrdConnected v ∧ (s \ a) ∩ f ⁻¹' {z} = (s \ a) ∩ v :=
      ordConnected_singleton.preimage_monotoneOn (hf.mono diff_subset)

Premises used: Set.diff_subset, SDiff.sdiff, Set.ordConnected_singleton, Set.OrdConnected.preimage_monotoneOn, MonotoneOn.mono
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
this : b = ⋃ z ∈ u, s₁ ∩ f ⁻¹' {z}
z : ℝ
hz : z ∈ u
v : Set ℝ
hv : v.OrdConnected
tv : s \ a ∩ f ⁻¹' {z} = s \ a ∩ v
⊢ MeasurableSet (s₁ ∩ f ⁻¹' {z})

Tactic:
tv ▸ (hs.diff a_count.measurableSet).inter hv.measurableSet

Premises used: MeasurableSet.diff, Set.OrdConnected.measurableSet, Set.Countable.measurableSet, Eq.rec, Eq.symm, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
this : b = ⋃ z ∈ u, s₁ ∩ f ⁻¹' {z}
z : ℝ
hz : z ∈ u
v : Set ℝ
hv : v.OrdConnected
tv : s \ a ∩ f ⁻¹' {z} = s \ a ∩ v
⊢ MeasurableSet (s₁ ∩ f ⁻¹' {z})

Tactic:
exact tv ▸ (hs.diff a_count.measurableSet).inter hv.measurableSet
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
⊢ MeasurableSet b

Tactic:
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 diff_subset)
    exact tv ▸ (hs.diff a_count.measurableSet).inter hv.measurableSet
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
⊢ MeasurableSet c

Tactic:
have hc : MeasurableSet c := hs₁.diff hb
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
⊢ ∃ (a : Set ℝ) (b : Set ℝ) (c : Set ℝ),
    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:
⟨a, b, c, ?_, a_count.measurableSet, hb, hc, ?_, ?_, a_count, ?_, ?_, ?_, ?_⟩

Premises used: Set.Countable.measurableSet, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
refine_1 : a ∪ (b ∪ c) = s
refine_2 : Disjoint a (b ∪ c)
refine_3 : Disjoint b c
refine_4 : (f '' b).Countable
refine_5 : ∀ x ∈ b, f' x = 0
refine_6 : ∀ x ∈ c, 0 ≤ f' x
refine_7 : InjOn f c
⊢ ∃ (a : Set ℝ) (b : Set ℝ) (c : Set ℝ),
    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:
refine ⟨a, b, c, ?_, a_count.measurableSet, hb, hc, ?_, ?_, a_count, ?_, ?_, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
refine_1 : ∀ (x : ℝ), x ∈ a ∪ (b ∪ c) ↔ x ∈ s
⊢ a ∪ (b ∪ c) = s

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
refine_1 : x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∨ x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥ → x ∈ s
⊢ x ∈ a ∪ (b ∪ c) ↔ x ∈ s

Tactic:
simp only [diff_self_inter, inter_union_diff, union_diff_self, mem_union, mem_setOf_eq,
      or_iff_right_iff_imp, a, b, s₁, c]

Premises used: Set.mem_union, Set.diff_self_inter, Set.mem_setOf_eq, or_iff_right_iff_imp, Set.inter_union_diff, Set.union_diff_self
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
refine_1 : x ∈ s → 𝓝[s ∩ Ioi x] x = ⊥ → x ∈ s
refine_1₁ : x ∈ s → 𝓝[s ∩ Iio x] x = ⊥ → x ∈ s
refine_1₂ : x ∈ s → 𝓝[s ∩ Ioi x] x = ⊥ → x ∈ s
refine_1₃ : x ∈ s → 𝓝[s ∩ Iio x] x = ⊥ → x ∈ s
refine_1₄ : x ∈ s → 𝓝[s ∩ Ioi x] x = ⊥ → x ∈ s
refine_1₅ : x ∈ s → 𝓝[s ∩ Iio x] x = ⊥ → x ∈ s
⊢ x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∨ x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥ → x ∈ s

Tactic:
tauto
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
⊢ Disjoint a (b ∪ c)

Tactic:
simpa [b, c, s₁] using disjoint_sdiff_right

Premises used: Set.disjoint_sdiff_right
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
⊢ Disjoint b c

Tactic:
simpa [c] using disjoint_sdiff_right

Premises used: Set.disjoint_sdiff_right
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
⊢ f '' b ⊆ u

Tactic:
simp [b]
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
⊢ (f '' b).Countable

Tactic:
exact hu.mono (by simp [b])

Premises used: Set.Countable.mono
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
rcases :
  ∀ (p q : ℝ) (ps₁ : p ∈ s₁) (qs₁ : q ∈ s₁) (pq : p < q) (hp : f p = f x) (hq : f q = f x), ∃ p ∈ s₁, p ≠ x ∧ f p = f x
⊢ ∃ p ∈ s₁, p ≠ x ∧ f p = f x

Tactic:
rcases hx.2 with ⟨p, q, ps₁, qs₁, pq, hp, hq⟩

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p q : ℝ
ps₁ : p ∈ s₁
qs₁ : q ∈ s₁
pq : p < q
hp : f p = f x
hq : f q = f x
inl : ∀ (h'p : p = x), ∃ p ∈ s₁, p ≠ x ∧ f p = f x
inr : ∀ (h'p : p ≠ x), ∃ p ∈ s₁, p ≠ x ∧ f p = f x
⊢ ∃ p ∈ s₁, p ≠ x ∧ f p = f x

Tactic:
rcases eq_or_ne p x with h'p | h'p

Premises used: eq_or_ne
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p q : ℝ
ps₁ : p ∈ s₁
qs₁ : q ∈ s₁
pq : p < q
hp : f p = f x
hq : f q = f x
h'p : p = x
⊢ ∃ p ∈ s₁, p ≠ x ∧ f p = f x

Tactic:
⟨q, qs₁, (h'p.symm.le.trans_lt pq).ne', hq⟩

Premises used: Eq.le, LT.lt.ne', And.intro, Exists.intro, Eq.symm, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p q : ℝ
ps₁ : p ∈ s₁
qs₁ : q ∈ s₁
pq : p < q
hp : f p = f x
hq : f q = f x
h'p : p = x
⊢ ∃ p ∈ s₁, p ≠ x ∧ f p = f x

Tactic:
exact ⟨q, qs₁, (h'p.symm.le.trans_lt pq).ne', hq⟩
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p q : ℝ
ps₁ : p ∈ s₁
qs₁ : q ∈ s₁
pq : p < q
hp : f p = f x
hq : f q = f x
h'p : p ≠ x
⊢ ∃ p ∈ s₁, p ≠ x ∧ f p = f x

Tactic:
⟨p, ps₁, h'p, hp⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p q : ℝ
ps₁ : p ∈ s₁
qs₁ : q ∈ s₁
pq : p < q
hp : f p = f x
hq : f q = f x
h'p : p ≠ x
⊢ ∃ p ∈ s₁, p ≠ x ∧ f p = f x

Tactic:
exact ⟨p, ps₁, h'p, hp⟩
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
refine_5 : ∀ (p : ℝ) (ps₁ : p ∈ s₁) (px : p ≠ x) (fpx : f p = f x), f' x = 0
⊢ f' x = 0

Tactic:
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⟩
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px : p ≠ x
fpx : f p = f x
refine_5 : ∀ (px : p < x), f' x = 0
refine_5₁ : ∀ (px : x < p), f' x = 0
⊢ f' x = 0

Tactic:
rcases lt_or_gt_of_ne px with px | px

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px_1 : p ≠ x
fpx : f p = f x
px : p < x
y : ℝ
hy : y ∈ s ∩ Ioo p x
apply : f x ≤ f y
⊢ f y = f x

Tactic:
apply le_antisymm (hf hy.1 hx.1.1 hy.2.2.le)

Premises used: LT.lt.le, le_antisymm, And.right, And.left
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px_1 : p ≠ x
fpx : f p = f x
px : p < x
y : ℝ
hy : y ∈ s ∩ Ioo p x
rw : f p ≤ f y
⊢ f x ≤ f y

Tactic:
rw [← fpx]
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px_1 : p ≠ x
fpx : f p = f x
px : p < x
y : ℝ
hy : y ∈ s ∩ Ioo p x
⊢ f p ≤ f y

Tactic:
hf ps₁.1 hy.1 hy.2.1.le

Premises used: LT.lt.le, And.right, And.left
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px_1 : p ≠ x
fpx : f p = f x
px : p < x
y : ℝ
hy : y ∈ s ∩ Ioo p x
⊢ f p ≤ f y

Tactic:
exact hf ps₁.1 hy.1 hy.2.1.le

Premises used: LT.lt.le, And.right, And.left
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px_1 : p ≠ x
fpx : f p = f x
px : p < x
⊢ ∀ (y : ℝ) (hy : y ∈ s ∩ Ioo p x), f y = f x

Tactic:
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
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px_1 : p ≠ x
fpx : f p = f x
px : p < x
E : ∀ (y : ℝ) (hy : y ∈ s ∩ Ioo p x), f y = f x
⊢ HasDerivWithinAt (F := ℝ) (fun (y : ℝ) ↦ f x) 0 (s ∩ Ioo p x) x

Tactic:
have : HasDerivWithinAt (fun y ↦ f x) 0 (s ∩ Ioo p x) x :=
          hasDerivWithinAt_const x (s ∩ Ioo p x) (f x)