awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    ∃ a ∈ t, HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a = x_1 ∧ a.1 = x
have hf₁ : ∀ (δ : ℝ) (hδ₁ : δ > 0)
  (hδ₂ : ∀ ⦃x_1 : ℝ⦄, Membership.mem (γ := Set ℝ) {x}ᶜ x_1 → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η),
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    ∃ a ∈ t, HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a = x_1 ∧ a.1 = x
Tactic: obtain ⟨δ, hδ₁, hδ₂⟩ := (Metric.tendsto_nhdsWithin_nhds).mp
        (hasDerivAt_iff_tendsto_slope.mp hx.right) η hη
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, Membership.mem (γ := Set ℝ) {x}ᶜ x_1 → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
α : ℝ
hα : 0 < α
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
have rw : ∃ (t : Set ℝ), (∀ y ∈ t, Membership.mem (γ := Set ℝ) (Ioi 0) y → y < α) ∧ IsOpen t ∧ 0 ∈ t
Tactic: rw [eventually_nhdsWithin_iff, eventually_nhds_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, Membership.mem (γ := Set ℝ) {x}ᶜ x_1 → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    ∃ a ∈ t, HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a = x_1 ∧ a.1 = x
have evn_bound : ∀ {α : ℝ} (hα : 0 < α), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
Tactic: have evn_bound {α : ℝ} (hα : 0 < α) : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α := by
        rw [eventually_nhdsWithin_iff, eventually_nhds_iff]
        exact ⟨Ioo (-α) α, by grind, isOpen_Ioo, by grind⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, Membership.mem (γ := Set ℝ) {x}ᶜ x_1 → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ} (hα : 0 < α), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    ∃ a ∈ t, HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a = x_1 ∧ a.1 = x
have evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
Tactic: have evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε :=
        eventually_mem_of_tendsto_nhdsWithin (fun _ a ↦ a)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, Membership.mem (γ := Set ℝ) {x}ᶜ x_1 → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ} (hα : 0 < α), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    ∃ a ∈ t, HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a = x_1 ∧ a.1 = x
have h : ∀ (ε : ℝ) (hε₁ : 0 < ε) (hε₂ : ε < η) (hε₃ : ε < δ) (hε₄ : ε < (b - x) / 2),
  ∃ a ∈ t, HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a = ε ∧ a.1 = x
Tactic: filter_upwards [evn_pos, evn_bound hη, evn_bound hδ₁,
                      evn_bound (α := (b - x) / 2) (by simp [hx.left.right])]
        with ε hε₁ hε₂ hε₃ hε₄
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, Membership.mem (γ := Set ℝ) {x}ᶜ x_1 → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ} (hα : 0 < α), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
ε : ℝ
hε₁ : 0 < ε
hε₂ : ε < η
hε₃ : ε < δ
hε₄ : ε < (b - x) / 2
⊢ (x, x + ε).1 < (x, x + ε).2
have linarith : (x, x + ε).2 ≤ (x, x + ε).1 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, Membership.mem (γ := Set ℝ) {x}ᶜ x_1 → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ} (hα : 0 < α), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
ε : ℝ
hε₁ : 0 < ε
hε₂ : ε < η
hε₃ : ε < δ
hε₄ : ε < (b - x) / 2
linarith : (x, x + ε).2 ≤ (x, x + ε).1 → 2 / 2 = 1
⊢ (x, x + ε).1 < (x, x + ε).2
have linarith₁ : (x, x + ε).2 ≤ (x, x + ε).1 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, Membership.mem (γ := Set ℝ) {x}ᶜ x_1 → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ} (hα : 0 < α), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
ε : ℝ
hε₁ : 0 < ε
hε₂ : ε < η
hε₃ : ε < δ
hε₄ : ε < (b - x) / 2
linarith : (x, x + ε).2 ≤ (x, x + ε).1 → 2 / 2 = 1
linarith₁ : (x, x + ε).2 ≤ (x, x + ε).1 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ (x, x + ε).1 < (x, x + ε).2
have linarith₂ : (x, x + ε).2 ≤ (x, x + ε).1 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, Membership.mem (γ := Set ℝ) {x}ᶜ x_1 → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ} (hα : 0 < α), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
ε : ℝ
hε₁ : 0 < ε
hε₂ : ε < η
hε₃ : ε < δ
hε₄ : ε < (b - x) / 2
linarith : (x, x + ε).2 ≤ (x, x + ε).1 → 2 / 2 = 1
linarith₁ : (x, x + ε).2 ≤ (x, x + ε).1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (x, x + ε).2 ≤ (x, x + ε).1 → GT.gt (α := ℝ) 2 0
⊢ (x, x + ε).1 < (x, x + ε).2
have linarith₃ : (x, x + ε).2 ≤ (x, x + ε).1 → 0 - ε + ((x, x + ε).2 - (x, x + ε).1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, Membership.mem (γ := Set ℝ) {x}ᶜ x_1 → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ} (hα : 0 < α), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
ε : ℝ
hε₁ : 0 < ε
hε₂ : ε < η
hε₃ : ε < δ
hε₄ : ε < (b - x) / 2
⊢ (x, x + ε).2 < b
have linarith : b ≤ (x, x + ε).2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, Membership.mem (γ := Set ℝ) {x}ᶜ x_1 → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ} (hα : 0 < α), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
ε : ℝ
hε₁ : 0 < ε
hε₂ : ε < η
hε₃ : ε < δ
hε₄ : ε < (b - x) / 2
linarith : b ≤ (x, x + ε).2 → 2 / 2 = 1
⊢ (x, x + ε).2 < b
have linarith₁ : b ≤ (x, x + ε).2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, Membership.mem (γ := Set ℝ) {x}ᶜ x_1 → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ} (hα : 0 < α), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
ε : ℝ
hε₁ : 0 < ε
hε₂ : ε < η
hε₃ : ε < δ
hε₄ : ε < (b - x) / 2
linarith : b ≤ (x, x + ε).2 → 2 / 2 = 1
linarith₁ : b ≤ (x, x + ε).2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ (x, x + ε).2 < b
have linarith₂ : b ≤ (x, x + ε).2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, Membership.mem (γ := Set ℝ) {x}ᶜ x_1 → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ} (hα : 0 < α), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
ε : ℝ
hε₁ : 0 < ε
hε₂ : ε < η
hε₃ : ε < δ
hε₄ : ε < (b - x) / 2
linarith : b ≤ (x, x + ε).2 → 2 / 2 = 1
linarith₁ : b ≤ (x, x + ε).2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : b ≤ (x, x + ε).2 → GT.gt (α := ℝ) 2 0
⊢ (x, x + ε).2 < b
have linarith₃ : b ≤ (x, x + ε).2 → 0 - ε + (2 * ε - (1 * b - 1 * x)) + (b - (x, x + ε).2) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, Membership.mem (γ := Set ℝ) {x}ᶜ x_1 → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ} (hα : 0 < α), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
ε : ℝ
hε₁ : 0 < ε
hε₂ : ε < η
hε₃ : ε < δ
hε₄ : ε < (b - x) / 2
⊢ ∃ a ∈ t, HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a = ε ∧ a.1 = x
have h : dist (slope f (x, x + ε).1 (x, x + ε).2) (f' (x, x + ε).1) < η
Tactic: refine ⟨(x, x + ε), ⟨⟨hx.1.1, by linarith, by linarith⟩, ?_⟩, by simp, rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
⊢ ∃ (u : Set (ℝ × ℝ)),
    (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η) ∧
      (u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2) ∧
        HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
have inr : ∀ (u : Set (ℝ × ℝ)) (hu₁ : u ⊆ t) (hu₂ : u.Countable)
  (hu₃ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2)
  (hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (s \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)),
  ∃ (u : Set (ℝ × ℝ)),
    (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η) ∧
      (u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2) ∧
        HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
Tactic: obtain ⟨u, ⟨hu₁, hu₂, hu₃, hu₄⟩⟩ : ∃ u ⊆ t, u.Countable ∧
      u.PairwiseDisjoint (fun z ↦ Icc z.1 z.2) ∧ volume (s \ ⋃ z ∈ u, Icc z.1 z.2) = 0 := by
    apply Vitali.exists_disjoint_covering_ae' volume s t 6 (Prod.snd - Prod.fst) Prod.fst
      (fun z ↦ Icc z.1 z.2)
    · grind [Metric.closedBall, Real.dist_eq, Pi.sub_apply, abs_le']
    · intro A hA
      simp only [Pi.sub_apply, Real.volume_closedBall, ENNReal.coe_ofNat, Real.volume_Icc]
      rw [show 6 = ENNReal.ofReal 6 by norm_num, ← ENNReal.ofReal_mul (by norm_num),
          ENNReal.ofReal_le_ofReal_iff (by grind)]
      linarith
    · simp +contextual [t]
    · simp [isClosed_Icc]
    · intro x hx
      apply Eventually.frequently
      have := hasDerivAt_iff_tendsto_slope.mp hx.right
      obtain ⟨δ, hδ₁, hδ₂⟩ := (Metric.tendsto_nhdsWithin_nhds).mp
        (hasDerivAt_iff_tendsto_slope.mp hx.right) η hη
      have evn_bound {α : ℝ} (hα : 0 < α) : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α := by
        rw [eventually_nhdsWithin_iff, eventually_nhds_iff]
        exact ⟨Ioo (-α) α, by grind, isOpen_Ioo, by grind⟩
      have evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε :=
        eventually_mem_of_tendsto_nhdsWithin (fun _ a ↦ a)
      filter_upwards [evn_pos, evn_bound hη, evn_bound hδ₁,
                      evn_bound (α := (b - x) / 2) (by simp [hx.left.right])]
        with ε hε₁ hε₂ hε₃ hε₄
      refine ⟨(x, x + ε), ⟨⟨hx.1.1, by linarith, by linarith⟩, ?_⟩, by simp, rfl⟩
      exact hδ₂ (by grind) (by simp [abs_eq_self.mpr hε₁.le, hε₃])
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
u : Set (ℝ × ℝ)
hu₁ : ∀ x ∈ u, (d < x.1 ∧ x.1 < x.2 ∧ x.2 < b) ∧ dist (slope f x.1 x.2) (f' x.1) < η
hu₂ : u.Countable
hu₃ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (s \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
⊢ ∃ (u : Set (ℝ × ℝ)),
    (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η) ∧
      (u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2) ∧
        HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
have inr : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
Tactic: refine ⟨u, ⟨hu₁, hu₃, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
u : Set (ℝ × ℝ)
hu₁ : ∀ x ∈ u, (d < x.1 ∧ x.1 < x.2 ∧ x.2 < b) ∧ dist (slope f x.1 x.2) (f' x.1) < η
hu₂ : u.Countable
hu₃ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (s \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
⊢ HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
have this : Countable (↑u : Type)
Tactic: have : Countable u := by simp [hu₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
u : Set (ℝ × ℝ)
hu₁ : ∀ x ∈ u, (d < x.1 ∧ x.1 < x.2 ∧ x.2 < b) ∧ dist (slope f x.1 x.2) (f' x.1) < η
hu₂ : u.Countable
hu₃ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (s \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
this : Countable (↑u : Type)
⊢ HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
have this₁ : Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
Tactic: have : Pairwise (Disjoint on fun (z : u) ↦ Icc z.val.1 z.val.2) :=
    fun z₁ z₂ hz₁z₂ ↦ hu₃ z₁.prop z₂.prop (Subtype.coe_ne_coe.mpr hz₁z₂)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
u : Set (ℝ × ℝ)
hu₁ : ∀ x ∈ u, (d < x.1 ∧ x.1 < x.2 ∧ x.2 < b) ∧ dist (slope f x.1 x.2) (f' x.1) < η
hu₂ : u.Countable
hu₃ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (s \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
⊢ Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
have rw : ∀ (hu₄ : ∀ᵐ (a : ℝ), a ∉ s \ ⋃ z ∈ u, Icc z.1 z.2) (this : Countable (↑u : Type))
  (this :
    Pairwise (α := (↑u : Type))
      (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)),
  ∀ᵐ (a : ℝ), a ∉ Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2
Tactic: rw [measure_eq_zero_iff_ae_notMem] at hu₄ ⊢
Cleared hypotheses: hu₄, this_1, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
u : Set (ℝ × ℝ)
hu₁ : ∀ x ∈ u, (d < x.1 ∧ x.1 < x.2 ∧ x.2 < b) ∧ dist (slope f x.1 x.2) (f' x.1) < η
hu₂ : u.Countable
hu₃ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₄ : ∀ᵐ (a : ℝ), a ∉ s \ ⋃ z ∈ u, Icc z.1 z.2
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
⊢ ∀ᵐ (a : ℝ), a ∉ Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2
have h : ∀ (x : ℝ) (hx₁ : x ∈ Ioo d b → HasDerivAt f (f' x) x) (hx₂ : x ∉ s \ ⋃ z ∈ u, Icc z.1 z.2),
  x ∉ Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2
Tactic: filter_upwards [hf, hu₄] with x hx₁ hx₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb_1 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z : ℝ × ℝ | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x : ℝ | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
u : Set (ℝ × ℝ)
hu₁ : ∀ x ∈ u, (d < x.1 ∧ x.1 < x.2 ∧ x.2 < b) ∧ dist (slope f x.1 x.2) (f' x.1) < η
hu₂ : u.Countable
hu₃ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (s \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
⊢ HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
have hu₅ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
Tactic: replace hu₄ : volume (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) = 0 := by
    rw [measure_eq_zero_iff_ae_notMem] at hu₄ ⊢
    filter_upwards [hf, hu₄] with x hx₁ hx₂
    grind
Cleared hypotheses: hu₄