awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
⊢ (𝓝[s \ {x}] x).NeBot
have apply : 𝓝[s ∩ Iio x] x ≤ 𝓝[s \ {x}] x
Tactic: apply this.mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
⊢ 𝓝[s ∩ Iio x] x ≤ 𝓝[s \ {x}] x
have h : s ∩ Iio x ⊆ s \ {x}
Tactic: apply nhdsWithin_mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
⊢ x = y
have refine_7 : ∀ (hxy : x ≠ y), f x ≠ f y
Tactic: contrapose! hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
⊢ f x ≠ f y
have 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
Tactic: wlog H : x < y generalizing x y with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
⊢ f x ≠ f y
have wlog : ∀ ⦃x : ℝ⦄ (hx : x ∈ c) ⦃y : ℝ⦄ (hy : y ∈ c) (hxy : x ≠ y) (H : x < y), f x ≠ f y
Tactic: wlog H : x < y generalizing x y with h
Cleared hypotheses: x, hx, y, hy, hxy
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
have order : ¬y < x → False
Tactic: order
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
⊢ y < x
have order₄ : x ≤ y → False
Tactic: order
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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
⊢ f x ≠ f y
have this : y < x
Tactic: have : y < x := by order
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
have refine : ∀ (h : f x = f y), x ∈ f ⁻¹' u
Tactic: refine fun h ↦ hx.2 ⟨hx.1, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x)
have 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)
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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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)
have this : ∫⁻ (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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 s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
have rw : ∫⁻ (a : ℝ) in b ∪ c, ENNReal.ofReal (f' a) * u (f a) ∂volume = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
Tactic: rw [← h_union, lintegral_union (hb.union hc) h_disj, this, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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
⊢ ∫⁻ (a : ℝ) in b ∪ c, ENNReal.ofReal (f' a) * u (f a) ∂volume = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
have this₁ : ∫⁻ (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])
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
⊢ ∫⁻ (a : ℝ) in b ∪ c, ENNReal.ofReal (f' a) * u (f a) ∂volume = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
have 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)
Tactic: rw [lintegral_union hc h_disj', this, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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)
⊢ ∫⁻ (a : ℝ) in b ∪ c, ENNReal.ofReal (f' a) * u (f a) ∂volume = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
have rw₁ : 0 + ∫⁻ (a : ℝ) in 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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)
⊢ ∫⁻ (a : ℝ) in b ∪ c, ENNReal.ofReal (f' a) * u (f a) ∂volume = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
have rw₂ : ∫⁻ (a : ℝ) in 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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 f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x)
have I : ∫⁻ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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)
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
have h : f '' s =ᶠ[ae (F := Measure ℝ) volume] f '' c
Tactic: apply setLIntegral_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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)
⊢ f '' s =ᶠ[ae (F := Measure ℝ) volume] f '' c
have h : f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' c
Tactic: rw [← h_union, image_union, image_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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)
⊢ f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' b ∪ f '' c
have refine : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (f '' a) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine union_ae_eq_right_of_ae_eq_empty (ae_eq_empty.mpr ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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)
⊢ f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' c
have A : f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' b ∪ f '' c
Tactic: have A : (f '' a ∪ (f '' b ∪ f '' c) : Set ℝ) =ᵐ[volume] (f '' b ∪ f '' c : Set ℝ) := by
      refine union_ae_eq_right_of_ae_eq_empty (ae_eq_empty.mpr ?_)
      exact (a_count.image _).measure_zero _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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)
A : f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' b ∪ f '' c
⊢ f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' c
have B : f '' b ∪ f '' c =ᶠ[ae (F := Measure ℝ) volume] f '' c
Tactic: have B : (f '' b ∪ f '' c : Set ℝ) =ᵐ[volume] f '' c :=
      union_ae_eq_right_of_ae_eq_empty (ae_eq_empty.mpr (fb_count.measure_zero _))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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)
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x)
have J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
Tactic: have J : ∫⁻ x in f '' s, u x = ∫⁻ x in f '' c, u x := by
    apply setLIntegral_congr
    rw [← h_union, image_union, image_union]
    have A : (f '' a ∪ (f '' b ∪ f '' c) : Set ℝ) =ᵐ[volume] (f '' b ∪ f '' c : Set ℝ) := by
      refine union_ae_eq_right_of_ae_eq_empty (ae_eq_empty.mpr ?_)
      exact (a_count.image _).measure_zero _
    have B : (f '' b ∪ f '' c : Set ℝ) =ᵐ[volume] f '' c :=
      union_ae_eq_right_of_ae_eq_empty (ae_eq_empty.mpr (fb_count.measure_zero _))
    exact A.trans B
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x)
have rw : ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
Tactic: rw [I, J]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
⊢ c ⊆ s
have rw : c ⊆ a ∪ (b ∪ c)
Tactic: rw [← h_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
⊢ ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
have c_s : c ⊆ s
Tactic: have c_s : c ⊆ s := by rw [← h_union]; exact subset_union_right.trans subset_union_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
⊢ ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
have hf'₁ : ∀ (x : ℝ) (hx : x ∈ c), HasFDerivWithinAt f (F' x) c x
Tactic: have hf' (x : ℝ) (hx : x ∈ c) : HasFDerivWithinAt f (F' x) c x :=
    (hf' x (c_s hx)).hasFDerivWithinAt.mono c_s