awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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)
inr₇ 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)
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, 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]

Premises used: neg_smul, neg_sub, Real.volume_real_Ioc_of_le, inv_neg, smul_neg, LT.lt.le, MeasureTheory.setAverage_eq, intervalIntegral.integral_of_ge, Set.uIoc_of_ge
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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)
rw₂ rw₃ : (b - a)⁻¹ * ∫ (x : ℝ) in a..b, f x = (b - a)⁻¹ * ∫ (x : ℝ) in a..b, f x
⊢ ⨍ (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]

Premises used: smul_eq_mul, div_eq_inv_mul, interval_average_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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
rw₂ rw₃ : Eq (α := ℝ) (⨍ (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)

Tactic:
rw [interval_average_eq, integral_congr_codiscreteWithin hf, ← interval_average_eq]

Premises used: intervalIntegral.integral_congr_codiscreteWithin, interval_average_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
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 ∈ Ι a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ

Tactic:
exists_eq_setAverage ⟨nonempty_of_measure_ne_zero hμ0, isPreconnected_Ioc⟩
    (hf.mono uIoc_subset_uIcc) (hf.integrableOn_of_subset_isCompact
    isCompact_uIcc measurableSet_uIoc uIoc_subset_uIcc hμfin) hμfin hμ0

Premises used: MeasureTheory.nonempty_of_measure_ne_zero, isCompact_uIcc, ContinuousOn.integrableOn_of_subset_isCompact, Set.uIoc_subset_uIcc, measurableSet_uIoc, isPreconnected_Ioc, And.intro, ContinuousOn.mono, MeasureTheory.exists_eq_setAverage
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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)
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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) μ
hab : a = b
⊢ False

Tactic:
simp [hab] at hμ0
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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) μ
⊢ a ≠ b

Tactic:
have h : a ≠ b := by intro hab; simp [hab] at hμ0
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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
⊢ min a b < x

Tactic:
rcases hx with ⟨h1, h2⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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 < max a b

Tactic:
rcases hx with ⟨h1, h2⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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 : ℝ
h1 : min a b < x
h2 : x < max a b
⊢ x ∈ Ι a b

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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
⊢ s ⊆ Ι a b

Tactic:
have hs' : s ⊆ Ι a b := by intro x hx; rcases hx with ⟨h1, h2⟩; grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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
⊢ s =ᶠ[ae μ] Ι a b

Tactic:
simpa using Ioo_ae_eq_Ioc

Premises used: MeasureTheory.Ioo_ae_eq_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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
⊢ s =ᶠ[ae μ] Ι a b

Tactic:
have hs_ev : s =ᵐ[μ] Ι a b := by simpa using Ioo_ae_eq_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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
rw rw₁ :
  Eq (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) s : ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal)

Tactic:
rw [measure_congr hs_ev]

Premises used: MeasureTheory.measure_congr
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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)

Tactic:
have hμ : μ s = μ (Ι a b) := by rw [measure_congr hs_ev]
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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μ : Eq (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) s : ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal)
rwa rwa₁ rwa₂ rwa₃ : Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (0 : ENNReal)
⊢ Ne (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
rwa [hμ]
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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)

Tactic:
have hμ0' : μ s ≠ 0 := by
    have hμ : μ s = μ (Ι a b) := by rw [measure_congr hs_ev]
    rwa [hμ]
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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)
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 ∂μ
⊢ ∃ 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'

Premises used: Set.uIoo_subset_uIcc_self, MeasureTheory.IntegrableOn.mono_set, MeasureTheory.measure_ne_top_of_subset, ContinuousOn.mono, MeasureTheory.exists_eq_setAverage, isConnected_uIoo
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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 : ℝ
hc : c ∈ uIoo a b
heq : f c = ⨍ (x : ℝ) in uIoo a b, f x ∂μ
rwa rwa₁ rwa₂ rwa₃ : f c = ⨍ (x : ℝ) in s, f x ∂μ
⊢ f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ

Tactic:
rwa [← setAverage_congr hs_ev]

Premises used: MeasureTheory.setAverage_congr
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
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 : ℝ
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:
exact ⟨c, hc, by rwa [← setAverage_congr hs_ev]⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≠ b
hf : ContinuousOn f [[a, b]]
⊢ Ne (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≠ b
hf : ContinuousOn f [[a, b]]
⊢ Ne (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (0 : ENNReal)

Tactic:
simpa using sub_ne_zero.mpr hab.symm

Premises used: Iff.mpr, sub_ne_zero, Ne.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
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)
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)
⊢ ∃ (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

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d η : ℝ
hη : 0 < η
hdb : d ≤ d
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d d → HasDerivAt f (f' x) x
⊢ (∀ (z : ℝ × ℝ),
      Membership.mem (γ := Set (ℝ × ℝ)) ∅ z → (d < z.1 ∧ z.1 < z.2 ∧ z.2 < d) ∧ dist (slope f z.1 z.2) (f' z.1) < η) ∧
    (PairwiseDisjoint (α := Set ℝ) ∅ fun (z : ℝ × ℝ) ↦ Icc z.1 z.2) ∧
      HasSum (fun (z : (↑∅ : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (d - d)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → F
d η : ℝ
hη : 0 < η
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:
exact ⟨∅, by simp⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
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)
hf₁ :
  ∀ x ∈ s,
    ∃ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∃ a ∈ t, HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a = ε ∧ a.1 = 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)

Tactic:
apply Vitali.exists_disjoint_covering_ae' volume s t 6 (Prod.snd - Prod.fst) Prod.fst
      (fun z ↦ Icc z.1 z.2)

Premises used: HSub.hSub, Prod.fst, Set.Icc, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, Prod.snd, Vitali.exists_disjoint_covering_ae'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
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 ∈ t,
    Icc a.1 a.2 ⊆
      Metric.closedBall a.1 (HSub.hSub (α := (self : ℝ × ℝ) → ℝ) (β := (self : ℝ × ℝ) → ℝ) Prod.snd Prod.fst a)

Tactic:
grind [Metric.closedBall, Real.dist_eq, Pi.sub_apply, abs_le']

Premises used: Real.dist_eq, Metric.closedBall, abs_le', Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
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
μB : ENNReal.ofReal (2 * (3 * (A.2 - A.1))) ≤ 6 * ENNReal.ofReal (A.2 - A.1)
⊢ (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:
simp only [Pi.sub_apply, Real.volume_closedBall, ENNReal.coe_ofNat, Real.volume_Icc]

Premises used: Real.volume_closedBall, Real.volume_Icc, ENNReal.coe_ofNat, Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
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
⊢ 6 = ENNReal.ofReal 6

Tactic:
norm_num
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
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
⊢ LE.le (α := ℝ) 0 6

Tactic:
norm_num
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
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
⊢ 0 ≤ 6 * (A.2 - A.1)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
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
μB : 2 * (3 * (A.2 - A.1)) ≤ 6 * (A.2 - A.1)
⊢ ENNReal.ofReal (2 * (3 * (A.2 - A.1))) ≤ 6 * ENNReal.ofReal (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)]

Premises used: ENNReal.ofReal_le_ofReal_iff, ENNReal.ofReal_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
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
linarith : 6 * (A.2 - A.1) < 2 * (3 * (A.2 - A.1)) → 6 * (A.2 - A.1) - 2 * (3 * (A.2 - A.1)) = 0
⊢ 2 * (3 * (A.2 - A.1)) ≤ 6 * (A.2 - A.1)

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
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 ∈ t, (interior (Icc a.1 a.2)).Nonempty

Tactic:
simp +contextual [t]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
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 ∈ t, IsClosed (Icc a.1 a.2)

Tactic:
simp [isClosed_Icc]

Premises used: isClosed_Icc