awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
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)
⊢ r / (b - d) * ∑ i ∈ s, ((↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1) ≤ r
have this₁ : ∑ 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
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
⊢ r / (b - d) * ∑ i ∈ s, ((↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1) ≤ r
have grw : r / (b - d) * (b - d) ≤ r
Tactic: grw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
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
⊢ r / (b - d) * (b - d) ≤ r
have field_simp : LE.le (α := ℝ) 1 1
Tactic: field_simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
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
⊢ dist (f d) (f b) ≤ r
have g_finsum_bound : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
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
⊢ dist (f d) (f b) ≤ r
have hu₄ : HasSum g (∑' (b : (↑u : Type)), g b)
Tactic: have hu₄ := summable_of_sum_le g_nonneg g_finsum_bound |>.hasSum
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
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)
⊢ dist (f d) (f b) ≤ r
have g_sum_bound : ∑' (x : (↑u : Type)), g x ≤ r
Tactic: have g_sum_bound := Real.tsum_le_of_sum_le g_nonneg g_finsum_bound
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
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) ≤ r
have this : 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₄
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
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
⊢ dist (f d) (f b) ≤ r
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
have f_deriv_integral_ac : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
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
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
have g_ac : AbsolutelyContinuousOnInterval g a b
Tactic: have g_ac : AbsolutelyContinuousOnInterval g a b := hf.sub (f_deriv_integral_ac)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
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
have 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
Tactic: filter_upwards [hf.ae_differentiableAt, hf.intervalIntegrable_deriv.ae_hasDerivAt_integral]
      with x hx₁ hx₂ hx₃
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
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
⊢ HasDerivAt g 0 x
have h : 0 = deriv f x - deriv f x
Tactic: convert! (hx₁ hx₃).hasDerivAt.sub (hx₂ hx₃ a (by simp))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
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 : ℝ) in a..b, deriv f x = f b - f a
have g_ae_deriv_zero : ∀ᵐ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
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
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
have obtain : ∀ (C : ℝ) (hC : ∀ x ∈ uIcc a b, g x = C), ∫ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
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
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
have this : f a = g a
Tactic: have : f a = g a := by simp [g]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
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
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
have this₁ : g a = C
Tactic: have := hC a (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
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
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
have this₁ : g b = C
Tactic: have := hC b (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ ∫ (x : ℝ) in a..b, deriv f x * g x + f x * deriv g x = f b * g b - f a * g a
have 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)
Tactic: rw [← (hf.fun_mul hg).integral_deriv_eq_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ 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)
have h : ∀ᵐ (x : ℝ), x ∈ uIoc a b → deriv f x * g x + f x * deriv g x = deriv (fun (i : ℝ) ↦ f i * g i) x
Tactic: apply intervalIntegral.integral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc a b → deriv f x * g x + f x * deriv g x = deriv (fun (i : ℝ) ↦ f i * g i) x
have h : ∀ (x : ℝ) (hx₁ : x ∈ uIcc a b → DifferentiableAt ℝ f x) (hx₂ : x ∈ uIcc a b → DifferentiableAt ℝ g x)
  (hx₃ : x ∈ uIoc a b), deriv f x * g x + f x * deriv g x = deriv (fun (i : ℝ) ↦ f i * g i) x
Tactic: filter_upwards [hf.ae_differentiableAt, hg.ae_differentiableAt] with x hx₁ hx₂ hx₃
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableAt ℝ f x
hx₂ : x ∈ uIcc a b → DifferentiableAt ℝ g x
hx₃ : x ∈ uIoc a b
⊢ deriv f x * g x + f x * deriv g x = deriv (fun (i : ℝ) ↦ f i * g i) x
have hx₄ : x ∈ uIcc a b
Tactic: have hx₄ : x ∈ uIcc a b := by grind [uIcc, uIoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableAt ℝ f x
hx₂ : x ∈ uIcc a b → DifferentiableAt ℝ g x
hx₃ : x ∈ uIoc a b
hx₄ : x ∈ uIcc a b
⊢ deriv f x * g x + f x * deriv g x = deriv (fun (i : ℝ) ↦ f i * g i) x
have hx₅ : HasDerivAt (f * g) (deriv f x * g x + f x * deriv g x) x
Tactic: have hx₅ := (hx₁ hx₄).hasDerivAt.mul (hx₂ hx₄).hasDerivAt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ ∫ (x : ℝ) in a..b, f x * deriv g x = f b * g b - f a * g a - ∫ (x : ℝ) in a..b, deriv f x * g x
have rw : Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x * deriv g x)
  (∫ (x : ℝ) in a..b, deriv f x * g x + f x * deriv g x - deriv f x * g x)
Tactic: rw [← AbsolutelyContinuousOnInterval.integral_deriv_mul_eq_sub hf hg,
      ← intervalIntegral.integral_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
rw :
  Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x * deriv g x)
    (∫ (x : ℝ) in a..b, deriv f x * g x + f x * deriv g x - deriv f x * g x)
⊢ ∫ (x : ℝ) in a..b, f x * deriv g x = f b * g b - f a * g a - ∫ (x : ℝ) in a..b, deriv f x * g x
have hf₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ deriv f x * g x + f x * deriv g x) volume a b
Tactic: rw [← AbsolutelyContinuousOnInterval.integral_deriv_mul_eq_sub hf hg,
      ← intervalIntegral.integral_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
rw :
  Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x * deriv g x)
    (∫ (x : ℝ) in a..b, deriv f x * g x + f x * deriv g x - deriv f x * g x)
hf₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ deriv f x * g x + f x * deriv g x) volume a b
⊢ ∫ (x : ℝ) in a..b, f x * deriv g x = f b * g b - f a * g a - ∫ (x : ℝ) in a..b, deriv f x * g x
have hg₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ deriv f x * g x) volume a b
Tactic: rw [← AbsolutelyContinuousOnInterval.integral_deriv_mul_eq_sub hf hg,
      ← intervalIntegral.integral_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ι a b) μ
have rw : IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b ∪ Ioc b a) μ
Tactic: rw [uIoc_eq_union, integrableOn_union, IntervalIntegrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
rw : IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b ∪ Ioc b a) μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ι a b) μ
have rw₁ : IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b) μ ∧ IntegrableOn f (Ioc b a) μ
Tactic: rw [uIoc_eq_union, integrableOn_union, IntervalIntegrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
rw : IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b ∪ Ioc b a) μ
rw₁ : IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b) μ ∧ IntegrableOn f (Ioc b a) μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ι a b) μ
have rw₂ : IntegrableOn f (Ioc a b) μ ∧ IntegrableOn f (Ioc b a) μ ↔ IntegrableOn f (Ioc a b) μ ∧ IntegrableOn f (Ioc b a) μ
Tactic: rw [uIoc_eq_union, integrableOn_union, IntervalIntegrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
g : ℝ → ε
h : f =ᶠ[ae (μ.restrict (Ι a b))] g
⊢ IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b
have rw : IntegrableOn f (Ι a b) μ ↔ IntervalIntegrable g μ a b
Tactic: rw [intervalIntegrable_iff, integrableOn_congr_fun_ae h, intervalIntegrable_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
g : ℝ → ε
h : f =ᶠ[ae (μ.restrict (Ι a b))] g
rw : IntegrableOn f (Ι a b) μ ↔ IntervalIntegrable g μ a b
⊢ IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b
have rw₁ : IntegrableOn g (Ι a b) μ ↔ IntervalIntegrable g μ a b
Tactic: rw [intervalIntegrable_iff, integrableOn_congr_fun_ae h, intervalIntegrable_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
g : ℝ → ε
h : f =ᶠ[ae (μ.restrict (Ι a b))] g
rw : IntegrableOn f (Ι a b) μ ↔ IntervalIntegrable g μ a b
rw₁ : IntegrableOn g (Ι a b) μ ↔ IntervalIntegrable g μ a b
⊢ IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b
have rw₂ : IntegrableOn g (Ι a b) μ ↔ IntegrableOn g (Ι a b) μ
Tactic: rw [intervalIntegrable_iff, integrableOn_congr_fun_ae h, intervalIntegrable_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b) μ
have rw : IntegrableOn f (Ι a b) μ ↔ IntegrableOn f (Ioc a b) μ
Tactic: rw [intervalIntegrable_iff, uIoc_of_le hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
rw : IntegrableOn f (Ι a b) μ ↔ IntegrableOn f (Ioc a b) μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b) μ
have rw₁ : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioc a b) μ
Tactic: rw [intervalIntegrable_iff, uIoc_of_le hab]