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 : p < x
E : ∀ (y : ℝ) (hy : y ∈ s ∩ Ioo p x), f y = f x
this : HasDerivWithinAt (F := ℝ) (fun (y : ℝ) ↦ f x) 0 (s ∩ Ioo p x) x
⊢ HasDerivWithinAt f 0 (s ∩ Ioo p x) x

Tactic:
this.congr E rfl

Premises used: HasDerivWithinAt.congr, 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 ∈ 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
this : HasDerivWithinAt (F := ℝ) (fun (y : ℝ) ↦ f x) 0 (s ∩ Ioo p x) x
⊢ HasDerivWithinAt f 0 (s ∩ Ioo p x) x

Tactic:
exact this.congr E rfl

Premises used: HasDerivWithinAt.congr, 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 ∈ b
p : ℝ
ps₁ : p ∈ s₁
px_1 : p ≠ x
fpx : f p = f x
px : p < x
⊢ HasDerivWithinAt f 0 (s ∩ Ioo p x) x

Tactic:
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
-- 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
K : HasDerivWithinAt f 0 (s ∩ Ioo p x) x
⊢ HasDerivWithinAt f (f' x) (s ∩ Ioo p x) x

Tactic:
have K' : HasDerivWithinAt f (f' x) (s ∩ Ioo p x) x :=
        (hf' x hx.1.1).mono inter_subset_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
K : HasDerivWithinAt f 0 (s ∩ Ioo p x) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo p x) x
apply : UniqueDiffWithinAt ℝ (s ∩ Ioo p x) x
⊢ f' x = 0

Tactic:
apply UniqueDiffWithinAt.eq_deriv _ _ K' K

Premises used: UniqueDiffWithinAt.eq_deriv
-- 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
K : HasDerivWithinAt f 0 (s ∩ Ioo p x) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo p x) x
⊢ (s ∩ Ioo p x) \ {x} = s ∩ Ioo p x

Tactic:
simp
-- 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
K : HasDerivWithinAt f 0 (s ∩ Ioo p x) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo p x) x
⊢ (s ∩ Ioo p x) \ {x} = s ∩ Ioo p x

Tactic:
have J1 : (s ∩ Ioo p x) \ {x} = s ∩ Ioo p x := by simp
-- 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
K : HasDerivWithinAt f 0 (s ∩ Ioo p x) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo p x) x
J1 : (s ∩ Ioo p x) \ {x} = s ∩ Ioo p x
⊢ 𝓝[s ∩ Ioo p x] x = 𝓝[s ∩ Iio x] x

Tactic:
simp [nhdsWithin_inter, nhdsWithin_Ioo_eq_nhdsLT px]

Premises used: nhdsWithin_Ioo_eq_nhdsLT, nhdsWithin_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
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
K : HasDerivWithinAt f 0 (s ∩ Ioo p x) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo p x) x
J1 : (s ∩ Ioo p x) \ {x} = s ∩ Ioo p x
⊢ 𝓝[s ∩ Ioo p x] x = 𝓝[s ∩ Iio x] x

Tactic:
have J2 : 𝓝[s ∩ Ioo p x] x = 𝓝[s ∩ Iio x] x := by
        simp [nhdsWithin_inter, nhdsWithin_Ioo_eq_nhdsLT px]
-- 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
K : HasDerivWithinAt f 0 (s ∩ Ioo p x) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo p x) x
J1 : (s ∩ Ioo p x) \ {x} = s ∩ Ioo p x
J2 : 𝓝[s ∩ Ioo p x] x = 𝓝[s ∩ Iio x] x
rw : (𝓝[s ∩ Iio x] x).NeBot
⊢ UniqueDiffWithinAt ℝ (s ∩ Ioo p x) x

Tactic:
rw [uniqueDiffWithinAt_iff_accPt, accPt_principal_iff_nhdsWithin, J1, J2]

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

Tactic:
neBot_iff.2 hx.1.2

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

Tactic:
exact neBot_iff.2 hx.1.2

Premises used: Iff.mpr, Filter.neBot_iff, 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 : x < p
y : ℝ
hy : y ∈ s ∩ Ioo x p
rw : f y ≤ f p
⊢ f y ≤ f x

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 : x < p
y : ℝ
hy : y ∈ s ∩ Ioo x p
⊢ f y ≤ f p

Tactic:
hf hy.1 ps₁.1 hy.2.2.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 : x < p
y : ℝ
hy : y ∈ s ∩ Ioo x p
⊢ f y ≤ f p

Tactic:
exact hf hy.1 ps₁.1 hy.2.2.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 : x < p
⊢ ∀ (y : ℝ) (hy : y ∈ s ∩ Ioo x p), f y = f x

Tactic:
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
-- 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
E : ∀ (y : ℝ) (hy : y ∈ s ∩ Ioo x p), f y = f x
⊢ HasDerivWithinAt (F := ℝ) (fun (y : ℝ) ↦ f x) 0 (s ∩ Ioo x p) x

Tactic:
have : HasDerivWithinAt (fun y ↦ f x) 0 (s ∩ Ioo x p) x :=
          hasDerivWithinAt_const x (s ∩ Ioo x p) (f 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 : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px_1 : p ≠ x
fpx : f p = f x
px : x < p
E : ∀ (y : ℝ) (hy : y ∈ s ∩ Ioo x p), f y = f x
this : HasDerivWithinAt (F := ℝ) (fun (y : ℝ) ↦ f x) 0 (s ∩ Ioo x p) x
⊢ HasDerivWithinAt f 0 (s ∩ Ioo x p) x

Tactic:
this.congr E rfl

Premises used: HasDerivWithinAt.congr, 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 ∈ b
p : ℝ
ps₁ : p ∈ s₁
px_1 : p ≠ x
fpx : f p = f x
px : x < p
E : ∀ (y : ℝ) (hy : y ∈ s ∩ Ioo x p), f y = f x
this : HasDerivWithinAt (F := ℝ) (fun (y : ℝ) ↦ f x) 0 (s ∩ Ioo x p) x
⊢ HasDerivWithinAt f 0 (s ∩ Ioo x p) x

Tactic:
exact this.congr E rfl

Premises used: HasDerivWithinAt.congr, 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 ∈ b
p : ℝ
ps₁ : p ∈ s₁
px_1 : p ≠ x
fpx : f p = f x
px : x < p
⊢ HasDerivWithinAt f 0 (s ∩ Ioo x p) x

Tactic:
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
-- 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
⊢ HasDerivWithinAt f (f' x) (s ∩ Ioo x p) x

Tactic:
have K' : HasDerivWithinAt f (f' x) (s ∩ Ioo x p) x :=
        (hf' x hx.1.1).mono inter_subset_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 : x < p
K : HasDerivWithinAt f 0 (s ∩ Ioo x p) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo x p) x
apply : UniqueDiffWithinAt ℝ (s ∩ Ioo x p) x
⊢ f' x = 0

Tactic:
apply UniqueDiffWithinAt.eq_deriv _ _ K' K

Premises used: UniqueDiffWithinAt.eq_deriv
-- 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
⊢ (s ∩ Ioo x p) \ {x} = s ∩ Ioo x p

Tactic:
simp
-- 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
⊢ (s ∩ Ioo x p) \ {x} = s ∩ Ioo x p

Tactic:
have J1 : (s ∩ Ioo x p) \ {x} = (s ∩ Ioo x p) := by simp
-- 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
⊢ 𝓝[s ∩ Ioo x p] x = 𝓝[s ∩ Ioi x] x

Tactic:
simp [nhdsWithin_inter, nhdsWithin_Ioo_eq_nhdsGT px]

Premises used: nhdsWithin_inter, nhdsWithin_Ioo_eq_nhdsGT
-- 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
⊢ 𝓝[s ∩ Ioo x p] x = 𝓝[s ∩ Ioi x] x

Tactic:
have J2 : 𝓝[s ∩ Ioo x p] x = 𝓝[s ∩ Ioi x] x := by
        simp [nhdsWithin_inter, nhdsWithin_Ioo_eq_nhdsGT px]
-- 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
rw : (𝓝[s ∩ Ioi x] x).NeBot
⊢ UniqueDiffWithinAt ℝ (s ∩ Ioo x p) x

Tactic:
rw [uniqueDiffWithinAt_iff_accPt, accPt_principal_iff_nhdsWithin, J1, J2]

Premises used: uniqueDiffWithinAt_iff_accPt, accPt_principal_iff_nhdsWithin