awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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}
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)
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
⊢ Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)

Tactic:
rw [measure_eq_zero_iff_ae_notMem] at hu₄ ⊢

Premises used: MeasureTheory.measure_eq_zero_iff_ae_notMem
-- 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}
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)
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
⊢ ∀ᵐ (a : ℝ), a ∉ Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2

Tactic:
filter_upwards [hf, hu₄] with x hx₁ hx₂
-- 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}
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)
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:
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}
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)

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
-- 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}
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
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
simp : ∀ (i : ℝ × ℝ) (i_1 : i ∈ u), Icc i.1 i.2 ⊆ Ioo d b
⊢ ⋃ z ∈ u, Icc z.1 z.2 ⊆ Ioo d b

Tactic:
simp only [iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff
-- 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}
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
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
⊢ ∀ (i : ℝ × ℝ) (i_1 : i ∈ u), Icc i.1 i.2 ⊆ Ioo d b

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}
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
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
h : Eq (α := Set ℝ) (⋃ (z : (↑u : Type)), Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) (⋃ z ∈ u, Icc z.1 z.2)
⊢ (volume : (a : Set ℝ) → ENNReal) (⋃ (z : (↑u : Type)), Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) = ENNReal.ofReal (b - d)

Tactic:
convert!
      Real.volume_Ioo ▸
        measure_eq_measure_of_null_diff (by simp only [iUnion_subset_iff]; grind) hu₄ using 2
-- 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}
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
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
⊢ Eq (α := Set ℝ) (⋃ (z : (↑u : Type)), Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) (⋃ z ∈ u, Icc z.1 z.2)

Tactic:
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}
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
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
⊢ (volume : (a : Set ℝ) → ENNReal) (⋃ (z : (↑u : Type)), Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) = ENNReal.ofReal (b - d)

Tactic:
have vol_sum : volume (⋃ z : u, Icc z.val.1 z.val.2) = ENNReal.ofReal (b - d) := by
    convert!
      Real.volume_Ioo ▸
        measure_eq_measure_of_null_diff (by simp only [iUnion_subset_iff]; grind) hu₄ using 2
    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}
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
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
vol_sum :
  (volume : (a : Set ℝ) → ENNReal) (⋃ (z : (↑u : Type)), Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) = ENNReal.ofReal (b - d)
⊢ ∀ (i : (↑u : Type)), MeasurableSet (Icc (↑i : ℝ × ℝ).1 (↑i : ℝ × ℝ).2)

Tactic:
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}
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
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
vol_sum :
  (volume : (a : Set ℝ) → ENNReal) (⋃ (z : (↑u : Type)), Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) = ENNReal.ofReal (b - d)
⊢ ∑' (i : (↑u : Type)), (volume : (a : Set ℝ) → ENNReal) (Icc (↑i : ℝ × ℝ).1 (↑i : ℝ × ℝ).2) = ENNReal.ofReal (b - d)

Tactic:
rw [measure_iUnion this (by simp)] at vol_sum

Premises used: MeasureTheory.measure_iUnion
-- 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}
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
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
vol_sum :
  ∑' (i : (↑u : Type)), (volume : (a : Set ℝ) → ENNReal) (Icc (↑i : ℝ × ℝ).1 (↑i : ℝ × ℝ).2) = ENNReal.ofReal (b - d)
⊢ ∑' (i : (↑u : Type)), ENNReal.ofReal ((↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1) = ENNReal.ofReal (b - d)

Tactic:
simp_rw [Real.volume_Icc] at vol_sum

Premises used: Real.volume_Icc
-- 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}
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
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
vol_sum : ∑' (i : (↑u : Type)), ENNReal.ofReal ((↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1) = ENNReal.ofReal (b - d)
⊢ ENNReal.toReal (∑' (i : (↑u : Type)), ENNReal.ofReal ((↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1)) =
    (ENNReal.ofReal (b - d)).toReal

Tactic:
apply_fun fun x ↦ x.toReal at vol_sum
-- 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}
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
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
vol_sum :
  ENNReal.toReal (∑' (i : (↑u : Type)), ENNReal.ofReal ((↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1)) =
    (ENNReal.ofReal (b - d)).toReal
⊢ ∀ (a : (↑u : Type)), ENNReal.ofReal ((↑a : ℝ × ℝ).2 - (↑a : ℝ × ℝ).1) ≠ ⊤

Tactic:
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}
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
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
vol_sum :
  ∑' (a : (↑u : Type)), (ENNReal.ofReal ((↑a : ℝ × ℝ).2 - (↑a : ℝ × ℝ).1)).toReal = (ENNReal.ofReal (b - d)).toReal
linarith : b - d < 0 → d - b + (b - d - 0) = 0
⊢ 0 ≤ b - d

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}
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
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
vol_sum : ∑' (a : (↑u : Type)), (ENNReal.ofReal ((↑a : ℝ × ℝ).2 - (↑a : ℝ × ℝ).1)).toReal = b - d
⊢ Summable (α := ℝ) fun (a : (↑u : Type)) ↦ (ENNReal.ofReal ((↑a : ℝ × ℝ).2 - (↑a : ℝ × ℝ).1)).toReal

Tactic:
grind [tsum_def]

Premises used: tsum_def
-- 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}
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
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
vol_sum :
  ENNReal.toReal (∑' (i : (↑u : Type)), ENNReal.ofReal ((↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1)) =
    (ENNReal.ofReal (b - d)).toReal
⊢ HasSum (fun (a : (↑u : Type)) ↦ (ENNReal.ofReal ((↑a : ℝ × ℝ).2 - (↑a : ℝ × ℝ).1)).toReal) (b - d)

Tactic:
rw [ENNReal.tsum_toReal_eq (by simp), ENNReal.toReal_ofReal (by linarith),
      ← Summable.hasSum_iff (by grind [tsum_def])] at vol_sum

Premises used: ENNReal.toReal_ofReal, Summable.hasSum_iff, ENNReal.tsum_toReal_eq
-- 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}
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
this_1 : Countable (↑u : Type)
this :
  Pairwise (α := (↑u : Type)) (onFun (β := Set ℝ) Disjoint fun (z : (↑u : Type)) ↦ Icc (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2)
hu₄ : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) : ENNReal) (0 : ENNReal)
vol_sum : HasSum (fun (a : (↑u : Type)) ↦ (ENNReal.ofReal ((↑a : ℝ × ℝ).2 - (↑a : ℝ × ℝ).1)).toReal) (b - d)
⊢ HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)

Tactic:
grind [ENNReal.toReal_ofReal]

Premises used: ENNReal.toReal_ofReal
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, d < z.1 ∧ z.1 < z.2 ∧ z.2 < b
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
hu₄ : HasSum (fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)) y
u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦ Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s
s : Finset (↑u : Type)
⊢ ∀ ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, d < z.1 ∧ z.1 < z.2 ∧ z.2 < b
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
hu₄ : HasSum (fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)) y
u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦ Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s
⊢ ∀ (s : Finset (↑u : Type)) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b

Tactic:
replace hu₁ (s : Finset u) : ∀ ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b := by
    grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
hu₄ : HasSum (fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)) y
u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦ Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s
hu₁ : ∀ (s : Finset (↑u : Type)) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
s : Finset (↑u : Type)
⊢ (↑(u_coe s) : Set (ℝ × ℝ)) ⊆ u

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
hu₄ : HasSum (fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)) y
u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦ Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s
hu₁ : ∀ (s : Finset (↑u : Type)) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
⊢ ∀ (s : Finset (↑u : Type)), (↑(u_coe s) : Set (ℝ × ℝ)).PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2

Tactic:
replace hu₂ (s : Finset u) : (SetLike.coe (u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2 :=
    hu₂.subset (by grind)