awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
this : ∀ (z : (↑u : Type)) (hz : z ∈ s), g z ≤ r / (b - d) * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
grw : ∑ i ∈ s, r / (b - d) * ((↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1) ≤ r
⊢ ∑ z ∈ s, g z ≤ r

Tactic:
grw [Finset.sum_le_sum this]

Premises used: Finset.sum_le_sum
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
this : ∀ (z : (↑u : Type)) (hz : z ∈ s), g z ≤ r / (b - d) * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
rw : r / (b - d) * ∑ i ∈ s, ((↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1) ≤ r
⊢ ∑ i ∈ s, r / (b - d) * ((↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1) ≤ r

Tactic:
rw [← Finset.mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
this : ∀ (z : (↑u : Type)) (hz : z ∈ s), g z ≤ r / (b - d) * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
⊢ ∀ i ∉ s, 0 ≤ (↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
this : ∀ (z : (↑u : Type)) (hz : z ∈ s), g z ≤ r / (b - d) * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
⊢ ∑ z ∈ s, ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) ≤ b - d

Tactic:
have : ∑ z ∈ s, (z.val.2 - z.val.1) ≤ b - d :=
      hu₃.tsum_eq ▸ Summable.sum_le_tsum _ (by grind) hu₃.summable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
this_1 : ∀ (z : (↑u : Type)) (hz : z ∈ s), g z ≤ r / (b - d) * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
this : ∑ z ∈ s, ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) ≤ b - d
grw : r / (b - d) * (b - d) ≤ r
⊢ r / (b - d) * ∑ i ∈ s, ((↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1) ≤ r

Tactic:
grw [this]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
this_1 : ∀ (z : (↑u : Type)) (hz : z ∈ s), g z ≤ r / (b - d) * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
this : ∑ z ∈ s, ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) ≤ b - d
field_simp : LE.le (α := ℝ) 1 1
⊢ r / (b - d) * (b - d) ≤ r

Tactic:
field_simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
this_1 : ∀ (z : (↑u : Type)) (hz : z ∈ s), g z ≤ r / (b - d) * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
this : ∑ z ∈ s, ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) ≤ b - d
⊢ LE.le (α := ℝ) 1 1

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
⊢ ∀ (s : Finset (↑u : Type)), ∑ z ∈ s, g z ≤ r

Tactic:
have g_finsum_bound (s : Finset u) : ∑ z ∈ s, g z ≤ r := by
    have (z : u) (hz : z ∈ s) : g z ≤ r / (b - d) * (z.val.2 - z.val.1) := by
      have slope_bound := hu₁ z (by simp) |>.right |>.le
      have : 0 < z.val.2 - z.val.1 := by linarith [hu₁ z (by simp)]
      grw [← slope_bound]
      simp only [dist_eq_norm, slope, vsub_eq_sub, sub_zero, ge_iff_le, g, mul_comm]
      nth_rw 1 [← Real.norm_of_nonneg this.le]
      simp only [norm_smul, Real.norm_eq_abs, norm_inv]
      field_simp
      rw [norm_sub_rev]
    grw [Finset.sum_le_sum this]
    rw [← Finset.mul_sum]
    have : ∑ z ∈ s, (z.val.2 - z.val.1) ≤ b - d :=
      hu₃.tsum_eq ▸ Summable.sum_le_tsum _ (by grind) hu₃.summable
    grw [this]
    field_simp
    grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
g_finsum_bound : ∀ (s : Finset (↑u : Type)), ∑ z ∈ s, g z ≤ r
⊢ HasSum g (∑' (b : (↑u : Type)), g b)

Tactic:
have hu₄ := summable_of_sum_le g_nonneg g_finsum_bound |>.hasSum
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
g_finsum_bound : ∀ (s : Finset (↑u : Type)), ∑ z ∈ s, g z ≤ r
hu₄ : HasSum g (∑' (b : (↑u : Type)), g b)
⊢ ∑' (x : (↑u : Type)), g x ≤ r

Tactic:
have g_sum_bound := Real.tsum_le_of_sum_le g_nonneg g_finsum_bound
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
g_finsum_bound : ∀ (s : Finset (↑u : Type)), ∑ z ∈ s, g z ≤ r
hu₄ : HasSum g (∑' (b : (↑u : Type)), g b)
g_sum_bound : ∑' (x : (↑u : Type)), g x ≤ r
⊢ uIcc d b ⊆ uIcc a b

Tactic:
grind [uIcc_of_le]

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
g_finsum_bound : ∀ (s : Finset (↑u : Type)), ∑ z ∈ s, g z ≤ r
hu₄ : HasSum g (∑' (b : (↑u : Type)), g b)
g_sum_bound : ∑' (x : (↑u : Type)), g x ≤ r
⊢ dist (f d) (f b) ≤ ∑' (b : (↑u : Type)), g b

Tactic:
have := (hf.mono (by grind [uIcc_of_le])).dist_le_of_pairwiseDisjoint_hasSum hd.right
    (fun s hs ↦ hu₁ s hs |>.left) hu₂ hu₃ hu₄
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
g_finsum_bound : ∀ (s : Finset (↑u : Type)), ∑ z ∈ s, g z ≤ r
hu₄ : HasSum g (∑' (b : (↑u : Type)), g b)
g_sum_bound : ∑' (x : (↑u : Type)), g x ≤ r
this : dist (f d) (f b) ≤ ∑' (b : (↑u : Type)), g b
linarith :
  r < dist (f d) (f b) →
    ∑' (x : (↑u : Type)), g x - r + (dist (f d) (f b) - ∑' (b : (↑u : Type)), g b) + (r - dist (f d) (f b)) = 0
⊢ dist (f d) (f b) ≤ r

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
⊢ a ∈ uIcc a b

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b

Tactic:
have f_deriv_integral_ac :=
    hf.intervalIntegrable_deriv.absolutelyContinuousOnInterval_intervalIntegral
    (c := a) (by simp)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
⊢ AbsolutelyContinuousOnInterval g a b

Tactic:
have g_ac : AbsolutelyContinuousOnInterval g a b := hf.sub (f_deriv_integral_ac)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
h :
  ∀ (x : ℝ) (hx₁ : x ∈ uIcc a b → DifferentiableAt ℝ f x)
    (hx₂ : x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, deriv f t) (deriv f x) x)
    (hx₃ : x ∈ uIcc a b), HasDerivAt g 0 x
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x

Tactic:
filter_upwards [hf.ae_differentiableAt, hf.intervalIntegrable_deriv.ae_hasDerivAt_integral]
      with x hx₁ hx₂ hx₃

Premises used: AbsolutelyContinuousOnInterval.ae_differentiableAt, IntervalIntegrable.ae_hasDerivAt_integral, AbsolutelyContinuousOnInterval.intervalIntegrable_deriv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableAt ℝ f x
hx₂ : x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, deriv f t) (deriv f x) x
hx₃ : x ∈ uIcc a b
⊢ a ∈ uIcc a b

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableAt ℝ f x
hx₂ : x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, deriv f t) (deriv f x) x
hx₃ : x ∈ uIcc a b
h : 0 = deriv f x - deriv f x
⊢ HasDerivAt g 0 x

Tactic:
convert! (hx₁ hx₃).hasDerivAt.sub (hx₂ hx₃ a (by simp))

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableAt ℝ f x
hx₂ : x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, deriv f t) (deriv f x) x
hx₃ : x ∈ uIcc a b
⊢ 0 = deriv f x - deriv f x

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x

Tactic:
have g_ae_deriv_zero : ∀ᵐ x, x ∈ uIcc a b → HasDerivAt g 0 x := by
    filter_upwards [hf.ae_differentiableAt, hf.intervalIntegrable_deriv.ae_hasDerivAt_integral]
      with x hx₁ hx₂ hx₃
    convert! (hx₁ hx₃).hasDerivAt.sub (hx₂ hx₃ a (by simp))
    abel
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
g_ae_deriv_zero : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x
obtain : ∀ (C : ℝ) (hC : ∀ x ∈ uIcc a b, g x = C), ∫ (x : ℝ) in a..b, deriv f x = f b - f a
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
obtain ⟨C, hC⟩ := g_ac.const_of_ae_hasDerivAt_zero g_ae_deriv_zero

Premises used: AbsolutelyContinuousOnInterval.const_of_ae_hasDerivAt_zero
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
g_ae_deriv_zero : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x
C : ℝ
hC : ∀ x ∈ uIcc a b, g x = C
⊢ f a = g a

Tactic:
simp [g]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
g_ae_deriv_zero : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x
C : ℝ
hC : ∀ x ∈ uIcc a b, g x = C
⊢ f a = g a

Tactic:
have : f a = g a := by simp [g]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
g_ae_deriv_zero : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x
C : ℝ
hC : ∀ x ∈ uIcc a b, g x = C
this : f a = g a
⊢ a ∈ uIcc a b

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
g_ae_deriv_zero : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x
C : ℝ
hC : ∀ x ∈ uIcc a b, g x = C
this : f a = g a
⊢ g a = C

Tactic:
have := hC a (by simp)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
g_ae_deriv_zero : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x
C : ℝ
hC : ∀ x ∈ uIcc a b, g x = C
this_1 : f a = g a
this : g a = C
⊢ b ∈ uIcc a b

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
g_ae_deriv_zero : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x
C : ℝ
hC : ∀ x ∈ uIcc a b, g x = C
this_1 : f a = g a
this : g a = C
⊢ g b = C

Tactic:
have := hC b (by simp)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
g_ae_deriv_zero : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x
C : ℝ
hC : ∀ x ∈ uIcc a b, g x = C
this_1 : f a = g a
this_2 : g a = C
this : g b = C
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
rw :
  Eq (α := ℝ) (∫ (x : ℝ) in a..b, deriv f x * g x + f x * deriv g x)
    (∫ (x : ℝ) in a..b, deriv (fun (i : ℝ) ↦ f i * g i) x)
⊢ ∫ (x : ℝ) in a..b, deriv f x * g x + f x * deriv g x = f b * g b - f a * g a

Tactic:
rw [← (hf.fun_mul hg).integral_deriv_eq_sub]

Premises used: AbsolutelyContinuousOnInterval.integral_deriv_eq_sub, AbsolutelyContinuousOnInterval.fun_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
h : ∀ᵐ (x : ℝ), x ∈ uIoc a b → deriv f x * g x + f x * deriv g x = deriv (fun (i : ℝ) ↦ f i * g i) x
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, deriv f x * g x + f x * deriv g x)
    (∫ (x : ℝ) in a..b, deriv (fun (i : ℝ) ↦ f i * g i) x)

Tactic:
apply intervalIntegral.integral_congr_ae

Premises used: intervalIntegral.integral_congr_ae