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
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 : x < p
K : HasDerivWithinAt f 0 (s ∩ Ioo x p) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo x p) x
J1 : (s ∩ Ioo x p) \ {x} = s ∩ Ioo x p
J2 : 𝓝[s ∩ Ioo x p] x = 𝓝[s ∩ Ioi x] x
⊢ (¬𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬𝓝[s ∩ Iio x] x = ⊥) ∧ f x ∈ u

Tactic:
simp only [mem_inter_iff, mem_diff, hx.1.1, mem_union, mem_setOf_eq, true_and, not_or,
        mem_preimage, b, s₁, a] at hx

Premises used: Set.mem_union, Set.mem_inter_iff, Set.mem_setOf_eq, not_or, And.left, Set.mem_diff, Set.mem_preimage, true_and
-- 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 p : ℝ
ps₁ : p ∈ s₁
px_1 : p ≠ x
fpx : f p = f x
px : x < p
K : HasDerivWithinAt f 0 (s ∩ Ioo x p) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo x p) x
J1 : (s ∩ Ioo x p) \ {x} = s ∩ Ioo x p
J2 : 𝓝[s ∩ Ioo x p] x = 𝓝[s ∩ Ioi x] x
hx : (¬𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬𝓝[s ∩ Iio x] x = ⊥) ∧ f x ∈ u
⊢ (𝓝[s ∩ Ioi x] x).NeBot

Tactic:
neBot_iff.2 hx.1.1

Premises used: Iff.mpr, Filter.neBot_iff, 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 p : ℝ
ps₁ : p ∈ s₁
px_1 : p ≠ x
fpx : f p = f x
px : x < p
K : HasDerivWithinAt f 0 (s ∩ Ioo x p) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo x p) x
J1 : (s ∩ Ioo x p) \ {x} = s ∩ Ioo x p
J2 : 𝓝[s ∩ Ioo x p] x = 𝓝[s ∩ Ioi x] x
hx : (¬𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬𝓝[s ∩ Iio x] x = ⊥) ∧ f x ∈ u
⊢ (𝓝[s ∩ Ioi x] x).NeBot

Tactic:
exact neBot_iff.2 hx.1.1

Premises used: Iff.mpr, Filter.neBot_iff, 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 ∈ c
apply : AccPt x (𝓟 s)
⊢ 0 ≤ f' x

Tactic:
apply (hf' x hx.1.1).nonneg_of_monotoneOn _ hf

Premises used: HasDerivWithinAt.nonneg_of_monotoneOn, 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 ∈ c
⊢ (¬𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬𝓝[s ∩ Iio x] x = ⊥) ∧
    x ∉ s \ ({x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}) ∩ f ⁻¹' u

Tactic:
simp only [mem_diff, hx.1.1, mem_union, mem_setOf_eq, true_and, not_or, c, s₁, a, b] at hx

Premises used: Set.mem_union, Set.mem_setOf_eq, not_or, And.left, Set.mem_diff, true_and
-- 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 :
  (¬𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬𝓝[s ∩ Iio x] x = ⊥) ∧
    x ∉ s \ ({x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}) ∩ f ⁻¹' u
rw : (𝓝[s \ {x}] x).NeBot
⊢ AccPt x (𝓟 s)

Tactic:
rw [accPt_principal_iff_nhdsWithin]

Premises used: accPt_principal_iff_nhdsWithin
-- 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 :
  (¬𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬𝓝[s ∩ Iio x] x = ⊥) ∧
    x ∉ s \ ({x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}) ∩ f ⁻¹' u
⊢ (𝓝[s ∩ Iio x] x).NeBot

Tactic:
have : (𝓝[s ∩ Iio x] x).NeBot := neBot_iff.2 hx.1.2
-- 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 :
  (¬𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬𝓝[s ∩ Iio x] x = ⊥) ∧
    x ∉ s \ ({x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}) ∩ f ⁻¹' u
this : (𝓝[s ∩ Iio x] x).NeBot
apply : 𝓝[s ∩ Iio x] x ≤ 𝓝[s \ {x}] x
⊢ (𝓝[s \ {x}] x).NeBot

Tactic:
apply this.mono

Premises used: Filter.NeBot.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 :
  (¬𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬𝓝[s ∩ Iio x] x = ⊥) ∧
    x ∉ s \ ({x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}) ∩ f ⁻¹' u
this : (𝓝[s ∩ Iio x] x).NeBot
h : s ∩ Iio x ⊆ s \ {x}
⊢ 𝓝[s ∩ Iio x] x ≤ 𝓝[s \ {x}] x

Tactic:
apply nhdsWithin_mono

Premises used: nhdsWithin_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 :
  (¬𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬𝓝[s ∩ Iio x] x = ⊥) ∧
    x ∉ s \ ({x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}) ∩ f ⁻¹' u
this : (𝓝[s ∩ Iio x] x).NeBot
y : ℝ
yt : y ∈ s
yx : y < x
⊢ y ∉ {x}

Tactic:
simpa using yx.ne

Premises used: LT.lt.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 :
  (¬𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬𝓝[s ∩ Iio x] x = ⊥) ∧
    x ∉ s \ ({x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}) ∩ f ⁻¹' u
this : (𝓝[s ∩ Iio x] x).NeBot
y : ℝ
yt : y ∈ s
yx : y < x
⊢ y ∈ s \ {x}

Tactic:
exact ⟨yt, by simpa using yx.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 ∈ c
y : ℝ
hy : y ∈ c
hxy : f x = f y
refine_7 : ∀ (hxy : x ≠ y), f x ≠ f y
⊢ x = y

Tactic:
contrapose! hxy
-- 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 ∈ c
y : ℝ
hy : y ∈ c
hxy : x ≠ y
refine_7 :
  ∀ (h : ∀ ⦃x : ℝ⦄ (hx : x ∈ c) ⦃y : ℝ⦄ (hy : y ∈ c) (hxy : x ≠ y) (H : x < y), f x ≠ f y) (H : ¬x < y), f x ≠ f y
wlog : ∀ ⦃x : ℝ⦄ (hx : x ∈ c) ⦃y : ℝ⦄ (hy : y ∈ c) (hxy : x ≠ y) (H : x < y), f x ≠ f y
⊢ f x ≠ f y

Tactic:
wlog H : x < y generalizing x y with h
-- 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 ∈ c
y : ℝ
hy : y ∈ c
hxy : x ≠ y
h : ∀ ⦃x : ℝ⦄ (hx : x ∈ c) ⦃y : ℝ⦄ (hy : y ∈ c) (hxy : x ≠ y) (H : x < y), f x ≠ f y
H : ¬x < y
order order₁ order₂ order₃ : ¬y < x → False
order₄ order₅ order₆ order₇ order₈ order₉ order₁₀ order₁₁ : x ≤ y → False
⊢ y < x

Tactic:
order
-- 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 ∈ c
y : ℝ
hy : y ∈ c
hxy : x ≠ y
h : ∀ ⦃x : ℝ⦄ (hx : x ∈ c) ⦃y : ℝ⦄ (hy : y ∈ c) (hxy : x ≠ y) (H : x < y), f x ≠ f y
H : ¬x < y
⊢ y < x

Tactic:
have : y < x := by order
-- 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 ∈ c
y : ℝ
hy : y ∈ c
hxy : x ≠ y
h : ∀ ⦃x : ℝ⦄ (hx : x ∈ c) ⦃y : ℝ⦄ (hy : y ∈ c) (hxy : x ≠ y) (H : x < y), f x ≠ f y
H : ¬x < y
this : y < x
⊢ f x ≠ f y

Tactic:
(h hy hx hxy.symm this).symm

Premises used: Ne.symm
-- 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 ∈ c
y : ℝ
hy : y ∈ c
hxy : x ≠ y
h : ∀ ⦃x : ℝ⦄ (hx : x ∈ c) ⦃y : ℝ⦄ (hy : y ∈ c) (hxy : x ≠ y) (H : x < y), f x ≠ f y
H : ¬x < y
this : y < x
⊢ f x ≠ f y

Tactic:
exact (h hy hx hxy.symm this).symm

Premises used: Ne.symm
-- 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 ∈ c
y : ℝ
hy : y ∈ c
hxy : x ≠ y
H : x < y
⊢ f x ≠ f y

Tactic:
fun h ↦ hx.2 ⟨hx.1, ?_⟩

Premises used: And.right, And.left, And.intro, Not
-- 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 ∈ c
y : ℝ
hy : y ∈ c
hxy : x ≠ y
H : x < y
refine : ∀ (h : f x = f y), x ∈ f ⁻¹' u
⊢ f x ≠ f y

Tactic:
refine fun h ↦ hx.2 ⟨hx.1, ?_⟩

Premises used: And.right, And.left, And.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 ∈ c
y : ℝ
hy : y ∈ c
hxy : x ≠ y
H : x < y
h : f x = f y
⊢ x ∈ f ⁻¹' u

Tactic:
⟨x, y, hx.1, hy.1, H, rfl, h.symm⟩

Premises used: Set.Mem, setOf, Set.preimage, And.left, And.intro, Exists.intro, Eq.symm, rfl
-- 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 ∈ c
y : ℝ
hy : y ∈ c
hxy : x ≠ y
H : x < y
h : f x = f y
⊢ x ∈ f ⁻¹' u

Tactic:
exact ⟨x, y, hx.1, hy.1, H, rfl, h.symm⟩
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
rcases :
  ∀ (a b c : Set ℝ) (h_union : a ∪ (b ∪ c) = s) (ha : MeasurableSet a) (hb : MeasurableSet b) (hc : MeasurableSet c)
    (h_disj : Disjoint a (b ∪ c)) (h_disj' : Disjoint b c) (a_count : a.Countable) (fb_count : (f '' b).Countable)
    (deriv_b : ∀ x ∈ b, f' x = 0) (deriv_c : ∀ x ∈ c, 0 ≤ f' x) (inj_c : InjOn f c),
    ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x)
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x)

Tactic:
rcases exists_decomposition_of_monotoneOn_hasDerivWithinAt hs hf hf' with
    ⟨a, b, c, h_union, ha, hb, hc, h_disj, h_disj', a_count, fb_count, deriv_b, deriv_c, inj_c⟩

Premises used: MeasureTheory.exists_decomposition_of_monotoneOn_hasDerivWithinAt
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
⊢ ∫⁻ (x : ℝ) in a, ENNReal.ofReal (f' x) * u (f x) = 0

Tactic:
have : ∫⁻ x in a, ENNReal.ofReal (f' x) * u (f x) = 0 :=
      setLIntegral_measure_zero a _ (a_count.measure_zero volume)
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
this : ∫⁻ (x : ℝ) in a, ENNReal.ofReal (f' x) * u (f x) = 0
rw : ∫⁻ (a : ℝ) in b ∪ c, ENNReal.ofReal (f' a) * u (f a) ∂volume = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
⊢ ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)

Tactic:
rw [← h_union, lintegral_union (hb.union hc) h_disj, this, zero_add]

Premises used: MeasureTheory.lintegral_union, zero_add, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
this : ∫⁻ (x : ℝ) in a, ENNReal.ofReal (f' x) * u (f x) = 0
x : ℝ
hx : x ∈ b
⊢ ENNReal.ofReal (f' x) * u (f x) = 0 x

Tactic:
simp [deriv_b x hx]
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
this : ∫⁻ (x : ℝ) in a, ENNReal.ofReal (f' x) * u (f x) = 0
⊢ ∫⁻ (x : ℝ) in b, ENNReal.ofReal (f' x) * u (f x) = 0

Tactic:
have : ∫⁻ x in b, ENNReal.ofReal (f' x) * u (f x) = 0 :=
      setLIntegral_eq_zero hb (fun x hx ↦ by simp [deriv_b x hx])
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
this_1 : ∫⁻ (x : ℝ) in a, ENNReal.ofReal (f' x) * u (f x) = 0
this : ∫⁻ (x : ℝ) in b, ENNReal.ofReal (f' x) * u (f x) = 0
rw :
  ∫⁻ (a : ℝ) in b, ENNReal.ofReal (f' a) * u (f a) ∂volume + ∫⁻ (a : ℝ) in c, ENNReal.ofReal (f' a) * u (f a) ∂volume =
    ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
rw₁ : 0 + ∫⁻ (a : ℝ) in c, ENNReal.ofReal (f' a) * u (f a) ∂volume = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
rw₂ rw₃ : ∫⁻ (a : ℝ) in c, ENNReal.ofReal (f' a) * u (f a) ∂volume = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
⊢ ∫⁻ (a : ℝ) in b ∪ c, ENNReal.ofReal (f' a) * u (f a) ∂volume = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)

Tactic:
rw [lintegral_union hc h_disj', this, zero_add]

Premises used: MeasureTheory.lintegral_union, zero_add
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
⊢ ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)

Tactic:
have I : ∫⁻ x in s, ENNReal.ofReal (f' x) * u (f x)
      = ∫⁻ x in c, ENNReal.ofReal (f' x) * u (f x) := by
    have : ∫⁻ x in a, ENNReal.ofReal (f' x) * u (f x) = 0 :=
      setLIntegral_measure_zero a _ (a_count.measure_zero volume)
    rw [← h_union, lintegral_union (hb.union hc) h_disj, this, zero_add]
    have : ∫⁻ x in b, ENNReal.ofReal (f' x) * u (f x) = 0 :=
      setLIntegral_eq_zero hb (fun x hx ↦ by simp [deriv_b x hx])
    rw [lintegral_union hc h_disj', this, zero_add]
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
h : f '' s =ᶠ[ae (F := Measure ℝ) volume] f '' c
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x

Tactic:
apply setLIntegral_congr

Premises used: MeasureTheory.setLIntegral_congr
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
h : f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' c
⊢ f '' s =ᶠ[ae (F := Measure ℝ) volume] f '' c

Tactic:
rw [← h_union, image_union, image_union]

Premises used: Set.image_union