awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
inr :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₁ :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc b a))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₂ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₃ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹
      (-@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
inr₄ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    -HSMul.hSMul (β := E) (b - a)⁻¹
        (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
inr₅ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (-(b - a)⁻¹)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
inr₆ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (-(b - a))⁻¹
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
have inr₇ : HSMul.hSMul (β := E) (a - b)⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
  HSMul.hSMul (β := E) (a - b)⁻¹
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
Tactic: rw [setAverage_eq, uIoc_of_ge h.le, Real.volume_real_Ioc_of_le h.le, integral_of_ge h.le,
      smul_neg, ← neg_smul, ← inv_neg, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
⊢ ⨍ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..b, f x) / (b - a)
have rw : HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x) = (∫ (x : ℝ) in a..b, f x) / (b - a)
Tactic: rw [interval_average_eq, smul_eq_mul, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
rw : HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x) = (∫ (x : ℝ) in a..b, f x) / (b - a)
⊢ ⨍ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..b, f x) / (b - a)
have rw₁ : (b - a)⁻¹ * ∫ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..b, f x) / (b - a)
Tactic: rw [interval_average_eq, smul_eq_mul, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
rw : HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x) = (∫ (x : ℝ) in a..b, f x) / (b - a)
rw₁ : (b - a)⁻¹ * ∫ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..b, f x) / (b - a)
⊢ ⨍ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..b, f x) / (b - a)
have rw₂ : (b - a)⁻¹ * ∫ (x : ℝ) in a..b, f x = (b - a)⁻¹ * ∫ (x : ℝ) in a..b, f x
Tactic: rw [interval_average_eq, smul_eq_mul, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
a b : ℝ
f₁ f₂ : ℝ → ℝ
hf : f₁ =ᶠ[Filter.codiscreteWithin (Ι a b)] f₂
⊢ Eq (α := ℝ) (⨍ (x : ℝ) in a..b, f₁ x) (⨍ (x : ℝ) in a..b, f₂ x)
have rw : HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f₁ x) = ⨍ (x : ℝ) in a..b, f₂ x
Tactic: rw [interval_average_eq, integral_congr_codiscreteWithin hf, ← interval_average_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
a b : ℝ
f₁ f₂ : ℝ → ℝ
hf : f₁ =ᶠ[Filter.codiscreteWithin (Ι a b)] f₂
rw : HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f₁ x) = ⨍ (x : ℝ) in a..b, f₂ x
⊢ Eq (α := ℝ) (⨍ (x : ℝ) in a..b, f₁ x) (⨍ (x : ℝ) in a..b, f₂ x)
have rw₁ : HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f₂ x) = ⨍ (x : ℝ) in a..b, f₂ x
Tactic: rw [interval_average_eq, integral_congr_codiscreteWithin hf, ← interval_average_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
a b : ℝ
f₁ f₂ : ℝ → ℝ
hf : f₁ =ᶠ[Filter.codiscreteWithin (Ι a b)] f₂
rw : HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f₁ x) = ⨍ (x : ℝ) in a..b, f₂ x
rw₁ : HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f₂ x) = ⨍ (x : ℝ) in a..b, f₂ x
⊢ Eq (α := ℝ) (⨍ (x : ℝ) in a..b, f₁ x) (⨍ (x : ℝ) in a..b, f₂ x)
have rw₂ : Eq (α := ℝ) (⨍ (x : ℝ) in a..b, f₂ x) (⨍ (x : ℝ) in a..b, f₂ x)
Tactic: rw [interval_average_eq, integral_congr_codiscreteWithin hf, ← interval_average_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst : NoAtoms μ
hf : ContinuousOn f [[a, b]]
hμfin : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
hμ0 : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (0 : ENNReal)
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ
have hint : IntegrableOn f (Ι a b) μ
Tactic: have hint : IntegrableOn f (Ι a b) μ := hf.integrableOn_of_subset_isCompact
    isCompact_uIcc measurableSet_uIoc uIoc_subset_uIcc hμfin
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst : NoAtoms μ
hf : ContinuousOn f [[a, b]]
hμfin : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
hμ0 : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (0 : ENNReal)
hint : IntegrableOn f (Ι a b) μ
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ
have h : a ≠ b
Tactic: have h : a ≠ b := by intro hab; simp [hab] at hμ0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst : NoAtoms μ
hf : ContinuousOn f [[a, b]]
hμfin : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
hμ0 : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (0 : ENNReal)
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
x : ℝ
hx : x ∈ s
⊢ x ∈ Ι a b
have h1 : min a b < x
Tactic: rcases hx with ⟨h1, h2⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst : NoAtoms μ
hf : ContinuousOn f [[a, b]]
hμfin : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
hμ0 : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (0 : ENNReal)
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
x : ℝ
hx : x ∈ s
h1 : min a b < x
⊢ x ∈ Ι a b
have h2 : x < max a b
Tactic: rcases hx with ⟨h1, h2⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst : NoAtoms μ
hf : ContinuousOn f [[a, b]]
hμfin : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
hμ0 : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (0 : ENNReal)
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ
have hs' : s ⊆ Ι a b
Tactic: have hs' : s ⊆ Ι a b := by intro x hx; rcases hx with ⟨h1, h2⟩; grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst : NoAtoms μ
hf : ContinuousOn f [[a, b]]
hμfin : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
hμ0 : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (0 : ENNReal)
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ
have hs_ev : s =ᶠ[ae μ] Ι a b
Tactic: have hs_ev : s =ᵐ[μ] Ι a b := by simpa using Ioo_ae_eq_Ioc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst : NoAtoms μ
hf : ContinuousOn f [[a, b]]
hμfin : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
hμ0 : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (0 : ENNReal)
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᶠ[ae μ] Ι a b
⊢ Eq (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) s : ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal)
have rw : Eq (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal)
Tactic: rw [measure_congr hs_ev]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst : NoAtoms μ
hf : ContinuousOn f [[a, b]]
hμfin : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
hμ0 : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (0 : ENNReal)
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᶠ[ae μ] Ι a b
⊢ Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) s : ENNReal) (0 : ENNReal)
have hμ : Eq (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) s : ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal)
Tactic: have hμ : μ s = μ (Ι a b) := by rw [measure_congr hs_ev]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst : NoAtoms μ
hf : ContinuousOn f [[a, b]]
hμfin : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
hμ0 : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (0 : ENNReal)
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᶠ[ae μ] Ι a b
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ
have hμ0' : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) s : ENNReal) (0 : ENNReal)
Tactic: have hμ0' : μ s ≠ 0 := by
    have hμ : μ s = μ (Ι a b) := by rw [measure_congr hs_ev]
    rwa [hμ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst : NoAtoms μ
hf : ContinuousOn f [[a, b]]
hμfin : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
hμ0 : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (0 : ENNReal)
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᶠ[ae μ] Ι a b
hμ0' : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ
have obtain : ∀ (c : ℝ) (hc : c ∈ uIoo a b) (heq : f c = ⨍ (x : ℝ) in uIoo a b, f x ∂μ),
  ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ
Tactic: obtain ⟨c, hc, heq⟩ := exists_eq_setAverage (isConnected_uIoo h) (hf.mono uIoo_subset_uIcc_self)
    (hint.mono_set hs') (measure_ne_top_of_subset hs' hμfin) hμ0'
-- 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 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
⊢ ∃ (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 inl : ∀ (hdb : d ≤ d) (hf : ∀ᵐ (x : ℝ), x ∈ Ioo d d → HasDerivAt f (f' x) x),
  ∃ (u : Set (ℝ × ℝ)),
    (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < d) ∧ 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) (d - d)
Tactic: rcases hdb.eq_or_lt with rfl | hdb
Cleared hypotheses: b, hdb, hf
-- 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 : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
inl :
  ∀ (hdb : d ≤ d) (hf : ∀ᵐ (x : ℝ), x ∈ Ioo d d → HasDerivAt f (f' x) x),
    ∃ (u : Set (ℝ × ℝ)),
      (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < d) ∧ 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) (d - d)
⊢ ∃ (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 : ∀ (hdb : d < b),
  ∃ (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: rcases hdb.eq_or_lt with rfl | hdb
-- 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 ⊆ t,
    u.Countable ∧
      (u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2) ∧
        Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (s \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
have hB : ∀ a ∈ t,
  Icc a.1 a.2 ⊆
    Metric.closedBall a.1 (HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a)
Tactic: apply Vitali.exists_disjoint_covering_ae' volume s t 6 (Prod.snd - Prod.fst) Prod.fst
      (fun z ↦ Icc z.1 z.2)
-- 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}
hB :
  ∀ a ∈ t,
    Icc a.1 a.2 ⊆
      Metric.closedBall a.1 (HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a)
⊢ ∃ u ⊆ t,
    u.Countable ∧
      (u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2) ∧
        Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (s \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
have μB : ∀ a ∈ t,
  (volume : (a : Set ℝ) → ENNReal)
      (Metric.closedBall a.1 (3 * HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a)) ≤
    HMul.hMul (β := ENNReal) (↑6 : ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Icc a.1 a.2) : ENNReal)
Tactic: apply Vitali.exists_disjoint_covering_ae' volume s t 6 (Prod.snd - Prod.fst) Prod.fst
      (fun z ↦ Icc z.1 z.2)
-- 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}
hB :
  ∀ a ∈ t,
    Icc a.1 a.2 ⊆
      Metric.closedBall a.1 (HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a)
μB :
  ∀ a ∈ t,
    (volume : (a : Set ℝ) → ENNReal)
        (Metric.closedBall a.1
          (3 * HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a)) ≤
      HMul.hMul (β := ENNReal) (↑6 : ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Icc a.1 a.2) : ENNReal)
⊢ ∃ u ⊆ t,
    u.Countable ∧
      (u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2) ∧
        Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (s \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
have ht : ∀ a ∈ t, (interior (Icc a.1 a.2)).Nonempty
Tactic: apply Vitali.exists_disjoint_covering_ae' volume s t 6 (Prod.snd - Prod.fst) Prod.fst
      (fun z ↦ Icc z.1 z.2)
-- 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}
hB :
  ∀ a ∈ t,
    Icc a.1 a.2 ⊆
      Metric.closedBall a.1 (HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a)
μB :
  ∀ a ∈ t,
    (volume : (a : Set ℝ) → ENNReal)
        (Metric.closedBall a.1
          (3 * HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a)) ≤
      HMul.hMul (β := ENNReal) (↑6 : ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Icc a.1 a.2) : ENNReal)
ht : ∀ a ∈ t, (interior (Icc a.1 a.2)).Nonempty
⊢ ∃ u ⊆ t,
    u.Countable ∧
      (u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2) ∧
        Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (s \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
have h't : ∀ a ∈ t, IsClosed (Icc a.1 a.2)
Tactic: apply Vitali.exists_disjoint_covering_ae' volume s t 6 (Prod.snd - Prod.fst) Prod.fst
      (fun z ↦ Icc z.1 z.2)
-- 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}
hB :
  ∀ a ∈ t,
    Icc a.1 a.2 ⊆
      Metric.closedBall a.1 (HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a)
μB :
  ∀ a ∈ t,
    (volume : (a : Set ℝ) → ENNReal)
        (Metric.closedBall a.1
          (3 * HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a)) ≤
      HMul.hMul (β := ENNReal) (↑6 : ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Icc a.1 a.2) : ENNReal)
ht : ∀ a ∈ t, (interior (Icc a.1 a.2)).Nonempty
h't : ∀ a ∈ t, IsClosed (Icc a.1 a.2)
⊢ ∃ u ⊆ t,
    u.Countable ∧
      (u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2) ∧
        Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (s \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
have hf₁ : ∀ x ∈ s,
  ∃ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∃ a ∈ t, HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a = ε ∧ a.1 = x
Tactic: apply Vitali.exists_disjoint_covering_ae' volume s t 6 (Prod.snd - Prod.fst) Prod.fst
      (fun z ↦ Icc z.1 z.2)
-- 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}
A : ℝ × ℝ
hA : A ∈ t
⊢ (volume : (a : Set ℝ) → ENNReal)
      (Metric.closedBall A.1 (3 * HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst A)) ≤
    HMul.hMul (β := ENNReal) (↑6 : ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Icc A.1 A.2) : ENNReal)
have μB : ENNReal.ofReal (2 * (3 * (A.2 - A.1))) ≤ 6 * ENNReal.ofReal (A.2 - A.1)
Tactic: simp only [Pi.sub_apply, Real.volume_closedBall, ENNReal.coe_ofNat, Real.volume_Icc]
-- 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}
A : ℝ × ℝ
hA : A ∈ t
⊢ ENNReal.ofReal (2 * (3 * (A.2 - A.1))) ≤ 6 * ENNReal.ofReal (A.2 - A.1)
have μB : 2 * (3 * (A.2 - A.1)) ≤ 6 * (A.2 - A.1)
Tactic: rw [show 6 = ENNReal.ofReal 6 by norm_num, ← ENNReal.ofReal_mul (by norm_num),
          ENNReal.ofReal_le_ofReal_iff (by grind)]
-- 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}
A : ℝ × ℝ
hA : A ∈ t
⊢ 2 * (3 * (A.2 - A.1)) ≤ 6 * (A.2 - A.1)
have linarith : 6 * (A.2 - A.1) < 2 * (3 * (A.2 - A.1)) → 6 * (A.2 - A.1) - 2 * (3 * (A.2 - A.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
⊢ ∃ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∃ a ∈ t, HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a = ε ∧ a.1 = x
have hf₁ : ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
  ∃ a ∈ t, HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a = x_1 ∧ a.1 = x
Tactic: apply Eventually.frequently
-- 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
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    ∃ a ∈ t, HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a = x_1 ∧ a.1 = x
have this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
Tactic: have := hasDerivAt_iff_tendsto_slope.mp hx.right