awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hint : IntervalIntegrable f' volume a b
hab : a ≤ b
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a
have hcont₁ : ContinuousOn f (Icc a b)
Tactic: simp only [uIcc_of_le, min_eq_left, max_eq_right, hab] at hcont hderiv hint
Cleared hypotheses: hcont, hderiv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hint : IntervalIntegrable f' volume a b
hab : a ≤ b
hcont₁ : ContinuousOn f (Icc a b)
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a
have hderiv₁ : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
Tactic: simp only [uIcc_of_le, min_eq_left, max_eq_right, hab] at hcont hderiv hint
Cleared hypotheses: hcont, hderiv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hint : IntervalIntegrable f' volume a b
hab : b ≤ a
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a
have hcont₁ : ContinuousOn f (Icc b a)
Tactic: simp only [uIcc_of_ge, min_eq_right, max_eq_left, hab] at hcont hderiv
Cleared hypotheses: hcont, hderiv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hint : IntervalIntegrable f' volume a b
hab : b ≤ a
hcont₁ : ContinuousOn f (Icc b a)
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a
have hderiv₁ : ∀ x ∈ Ioo b a, HasDerivWithinAt f (f' x) (Ioi x) x
Tactic: simp only [uIcc_of_ge, min_eq_right, max_eq_left, hab] at hcont hderiv
Cleared hypotheses: hcont, hderiv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hint : IntervalIntegrable f' volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ x ∈ Ioo b a, HasDerivWithinAt f (f' x) (Ioi x) x
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a
have inr : -∫ (x : ℝ) in b..a, f' x = f b - f a
Tactic: rw [integral_symm, integral_eq_sub_of_hasDeriv_right_of_le hab hcont hderiv hint.symm, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hint : IntervalIntegrable f' volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ x ∈ Ioo b a, HasDerivWithinAt f (f' x) (Ioi x) x
inr : -∫ (x : ℝ) in b..a, f' x = f b - f a
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a
have inr₁ : -(f a - f b) = f b - f a
Tactic: rw [integral_symm, integral_eq_sub_of_hasDeriv_right_of_le hab hcont hderiv hint.symm, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hint : IntervalIntegrable f' volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ x ∈ Ioo b a, HasDerivWithinAt f (f' x) (Ioi x) x
inr : -∫ (x : ℝ) in b..a, f' x = f b - f a
inr₁ : -(f a - f b) = f b - f a
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a
have inr₂ : f b - f a = f b - f a
Tactic: rw [integral_symm, integral_eq_sub_of_hasDeriv_right_of_le hab hcont hderiv hint.symm, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
⊢ ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
have refine : ∀ (x : ℝ) (hx : x ∈ Ioo a b), F =ᶠ[𝓝 x] f
Tactic: refine fun x hx => (hderiv x hx).congr_of_eventuallyEq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
x : ℝ
hx : x ∈ Ioo a b
⊢ F =ᶠ[𝓝 x] f
have h : ∀ (a_1 : ℝ) (hy : a_1 ∈ Ioo a b), F a_1 = f a_1
Tactic: filter_upwards [Ioo_mem_nhds hx.1 hx.2] with _ hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
x : ℝ
hx : x ∈ Ioo a b
a_1 : ℝ
hy : a_1 ∈ Ioo a b
⊢ update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb a_1 = f a_1
have h : update (β := fun (a : ℝ) ↦ E) f a fa a_1 = f a_1
Tactic: rw [update_of_ne hy.2.ne, update_of_ne hy.1.ne']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
x : ℝ
hx : x ∈ Ioo a b
a_1 : ℝ
hy : a_1 ∈ Ioo a b
h : update (β := fun (a : ℝ) ↦ E) f a fa a_1 = f a_1
⊢ update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb a_1 = f a_1
have h₁ : f a_1 = f a_1
Tactic: rw [update_of_ne hy.2.ne, update_of_ne hy.1.ne']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
⊢ ∫ (y : ℝ) in a..b, f' y = fb - fa
have Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
Tactic: have Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x := by
    refine fun x hx => (hderiv x hx).congr_of_eventuallyEq ?_
    filter_upwards [Ioo_mem_nhds hx.1 hx.2] with _ hy
    unfold F
    rw [update_of_ne hy.2.ne, update_of_ne hy.1.ne']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ ContinuousOn F (Icc a b)
have rw : (ContinuousOn f (Ioo a b) ∧ (a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa))) ∧
  (b ∈ Icc a b → Tendsto (update (β := fun (a : ℝ) ↦ E) f a fa) (𝓝[Ico a b] b) (𝓝 fb))
Tactic: rw [continuousOn_update_iff, continuousOn_update_iff, Icc_diff_right, Ico_diff_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ (ContinuousOn f (Ioo a b) ∧ (a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa))) ∧
    (b ∈ Icc a b → Tendsto (update (β := fun (a : ℝ) ↦ E) f a fa) (𝓝[Ico a b] b) (𝓝 fb))
have refine_1 : a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa)
Tactic: refine ⟨⟨fun z hz => (hderiv z hz).continuousAt.continuousWithinAt, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
refine_1 : a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa)
⊢ (ContinuousOn f (Ioo a b) ∧ (a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa))) ∧
    (b ∈ Icc a b → Tendsto (update (β := fun (a : ℝ) ↦ E) f a fa) (𝓝[Ico a b] b) (𝓝 fb))
have refine_2 : b ∈ Icc a b → Tendsto (update (β := fun (a : ℝ) ↦ E) f a fa) (𝓝[Ico a b] b) (𝓝 fb)
Tactic: refine ⟨⟨fun z hz => (hderiv z hz).continuousAt.continuousWithinAt, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ Tendsto (update (β := fun (a : ℝ) ↦ E) f a fa) (𝓝[Ico a b] b) (𝓝 fb)
have refine_2 : f =ᶠ[𝓝[<] b] update (β := fun (a : ℝ) ↦ E) f a fa
Tactic: refine (hb.congr' ?_).mono_left (nhdsWithin_mono _ Ico_subset_Iio_self)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ f =ᶠ[𝓝[<] b] update (β := fun (a : ℝ) ↦ E) f a fa
have h : ∀ (a_1 : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      x ∈ Ioo a b →
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ f x = update (β := fun (a : ℝ) ↦ E) f a fa x) x} x}
    a_1
Tactic: filter_upwards [Ioo_mem_nhdsLT hab] with _ hz using (update_of_ne hz.1.ne' _ _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
h :
  ∀ (a_1 : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        x ∈ Ioo a b →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ f x = update (β := fun (a : ℝ) ↦ E) f a fa x) x} x}
      a_1
⊢ f =ᶠ[𝓝[<] b] update (β := fun (a : ℝ) ↦ E) f a fa
have h₁ : ∀ a_1 ∈ Ioo a b, f a_1 = update (β := fun (a : ℝ) ↦ E) f a fa a_1
Tactic: filter_upwards [Ioo_mem_nhdsLT hab] with _ hz using (update_of_ne hz.1.ne' _ _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ ∫ (y : ℝ) in a..b, f' y = fb - fa
have hcont : ContinuousOn F (Icc a b)
Tactic: have hcont : ContinuousOn F (Icc a b) := by
    rw [continuousOn_update_iff, continuousOn_update_iff, Icc_diff_right, Ico_diff_left]
    refine ⟨⟨fun z hz => (hderiv z hz).continuousAt.continuousWithinAt, ?_⟩, ?_⟩
    · exact fun _ => ha.mono_left (nhdsWithin_mono _ Ioo_subset_Ioi_self)
    · rintro -
      refine (hb.congr' ?_).mono_left (nhdsWithin_mono _ Ico_subset_Iio_self)
      filter_upwards [Ioo_mem_nhdsLT hab] with _ hz using (update_of_ne hz.1.ne' _ _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f' f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a
have rw : IntervalIntegrable (deriv f) volume a b
Tactic: rw [← hderiv, integral_deriv_eq_sub hdiff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f' f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ IntervalIntegrable (deriv f) volume a b
have rw : IntervalIntegrable f' volume a b
Tactic: rw [hderiv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ uIoo a b, DifferentiableAt ℝ f x
hint : IntervalIntegrable (deriv f) volume a b
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
have inl : ∀ (hab : a ≤ b), ∫ (y : ℝ) in a..b, deriv f y = f b - f a
Tactic: rcases le_total a b with hab | hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ uIoo a b, DifferentiableAt ℝ f x
hint : IntervalIntegrable (deriv f) volume a b
inl : ∀ (hab : a ≤ b), ∫ (y : ℝ) in a..b, deriv f y = f b - f a
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
have inr : ∀ (hab : b ≤ a), ∫ (y : ℝ) in a..b, deriv f y = f b - f a
Tactic: rcases le_total a b with hab | hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ uIoo a b, DifferentiableAt ℝ f x
hint : IntervalIntegrable (deriv f) volume a b
hab : a ≤ b
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
have hcont₁ : ContinuousOn f (Icc a b)
Tactic: simp only [uIcc_of_le, hab, uIoo_of_le] at hcont hderiv
Cleared hypotheses: hcont, hderiv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ uIoo a b, DifferentiableAt ℝ f x
hint : IntervalIntegrable (deriv f) volume a b
hab : a ≤ b
hcont₁ : ContinuousOn f (Icc a b)
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
have hderiv₁ : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
Tactic: simp only [uIcc_of_le, hab, uIoo_of_le] at hcont hderiv
Cleared hypotheses: hcont, hderiv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hint : IntervalIntegrable (deriv f) volume a b
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
have inl : f b - f a = f b - f a
Tactic: rw [integral_eq_sub_of_hasDerivAt_of_le hab hcont (fun x hx => (hderiv x hx).hasDerivAt) hint]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ uIoo a b, DifferentiableAt ℝ f x
hint : IntervalIntegrable (deriv f) volume a b
hab : b ≤ a
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
have hcont₁ : ContinuousOn f (Icc b a)
Tactic: simp only [uIcc_of_ge, hab, uIoo_of_ge] at hcont hderiv
Cleared hypotheses: hcont, hderiv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ uIoo a b, DifferentiableAt ℝ f x
hint : IntervalIntegrable (deriv f) volume a b
hab : b ≤ a
hcont₁ : ContinuousOn f (Icc b a)
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
have hderiv₁ : ∀ x ∈ Ioo b a, DifferentiableAt ℝ f x
Tactic: simp only [uIcc_of_ge, hab, uIoo_of_ge] at hcont hderiv
Cleared hypotheses: hcont, hderiv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hint : IntervalIntegrable (deriv f) volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ x ∈ Ioo b a, DifferentiableAt ℝ f x
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
have inr : -∫ (x : ℝ) in b..a, deriv f x = f b - f a
Tactic: rw [integral_symm, integral_eq_sub_of_hasDerivAt_of_le hab hcont
        (fun x hx => (hderiv x hx).hasDerivAt) hint.symm, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hint : IntervalIntegrable (deriv f) volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ x ∈ Ioo b a, DifferentiableAt ℝ f x
inr : -∫ (x : ℝ) in b..a, deriv f x = f b - f a
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
have inr₁ : -(f a - f b) = f b - f a
Tactic: rw [integral_symm, integral_eq_sub_of_hasDerivAt_of_le hab hcont
        (fun x hx => (hderiv x hx).hasDerivAt) hint.symm, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hint : IntervalIntegrable (deriv f) volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ x ∈ Ioo b a, DifferentiableAt ℝ f x
inr : -∫ (x : ℝ) in b..a, deriv f x = f b - f a
inr₁ : -(f a - f b) = f b - f a
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
have inr₂ : f b - f a = f b - f a
Tactic: rw [integral_symm, integral_eq_sub_of_hasDerivAt_of_le hab hcont
        (fun x hx => (hderiv x hx).hasDerivAt) hint.symm, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn.{0, u_3} (Y := E) (fun (t : ℝ) ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : (t : ℝ) → 𝕜 := fun (t : ℝ) ↦ z₀ + t • z₁
⊢ HSMul.hSMul (β := E) z₁ (∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁)) = f (z₀ + z₁) - f z₀
have hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
Tactic: have hint : IntervalIntegrable (z₁ • (f' ∘ γ)) MeasureTheory.volume 0 1 :=
    (ContinuousOn.const_smul hcont z₁).intervalIntegrable_of_Icc zero_le_one
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn.{0, u_3} (Y := E) (fun (t : ℝ) ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : (t : ℝ) → 𝕜 := fun (t : ℝ) ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
t : ℝ
ht : Membership.mem (γ := Set ℝ) [[0, 1]] t
⊢ HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t
have refine : HasDerivAt (fun (t : ℝ) ↦ t • z₁) z₁ t
Tactic: refine (hderiv t <| (Set.uIcc_of_le (α := ℝ) zero_le_one).symm ▸ ht).scomp t <| .const_add _ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn.{0, u_3} (Y := E) (fun (t : ℝ) ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : (t : ℝ) → 𝕜 := fun (t : ℝ) ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
⊢ HSMul.hSMul (β := E) z₁ (∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁)) = f (z₀ + z₁) - f z₀
have hderiv' : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) [[0, 1]] t), HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t
Tactic: have hderiv' (t) (ht : t ∈ Set.uIcc (0 : ℝ) 1) : HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t := by
    refine (hderiv t <| (Set.uIcc_of_le (α := ℝ) zero_le_one).symm ▸ ht).scomp t <| .const_add _ ?_
    simp [hasDerivAt_iff_isLittleO, sub_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn.{0, u_3} (Y := E) (fun (t : ℝ) ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : (t : ℝ) → 𝕜 := fun (t : ℝ) ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
hderiv' : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) [[0, 1]] t), HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t
⊢ HSMul.hSMul (β := E) z₁ (∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁)) = f (z₀ + z₁) - f z₀
have h : HSMul.hSMul (β := E) z₁ (∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁)) = ∫ (y : ℝ) in 0..1, z₁ • (f' ∘ γ) y
Tactic: convert! (integral_eq_sub_of_hasDerivAt hderiv' hint) using 1