awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
⊢ ContinuousOn (Y := ℝ × ℝ) (fun (t : ℝ) ↦ (g b - g t, ∫ (u : ℝ) in t..b, φ u)) (Icc a b)

Tactic:
have : ContinuousOn (fun t => (g b - g t, ∫ u in t..b, φ u)) (Icc a b) := by
      rw [← uIcc_of_le hab] at hcont φint ⊢
      exact (continuousOn_const.sub hcont).prodMk (continuousOn_primitive_interval_left φint)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
this : ContinuousOn (Y := ℝ × ℝ) (fun (t : ℝ) ↦ (g b - g t, ∫ (u : ℝ) in t..b, φ u)) (Icc a b)
simp : IsClosed (Icc a b ∩ {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u})
⊢ IsClosed s

Tactic:
simp only [s, inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
this : ContinuousOn (Y := ℝ × ℝ) (fun (t : ℝ) ↦ (g b - g t, ∫ (u : ℝ) in t..b, φ u)) (Icc a b)
⊢ IsClosed (Icc a b ∩ {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u})

Tactic:
this.preimage_isClosed_of_isClosed isClosed_Icc isClosed_le_prod

Premises used: ContinuousOn.preimage_isClosed_of_isClosed, Set.Mem, setOf, intervalIntegral, isClosed_Icc, Set.preimage, isClosed_le_prod
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
this : ContinuousOn (Y := ℝ × ℝ) (fun (t : ℝ) ↦ (g b - g t, ∫ (u : ℝ) in t..b, φ u)) (Icc a b)
⊢ IsClosed (Icc a b ∩ {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u})

Tactic:
exact this.preimage_isClosed_of_isClosed isClosed_Icc isClosed_le_prod

Premises used: ContinuousOn.preimage_isClosed_of_isClosed, isClosed_Icc, isClosed_le_prod
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
⊢ IsClosed s

Tactic:
have s_closed : IsClosed s := by
    have : ContinuousOn (fun t => (g b - g t, ∫ u in t..b, φ u)) (Icc a b) := by
      rw [← uIcc_of_le hab] at hcont φint ⊢
      exact (continuousOn_const.sub hcont).prodMk (continuousOn_primitive_interval_left φint)
    simp only [s, inter_comm]
    exact this.preimage_isClosed_of_isClosed isClosed_Icc isClosed_le_prod
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
s_closed : IsClosed s
apply : Ioc a b ⊆ s
⊢ closure (Ioc a b) ⊆ s

Tactic:
apply s_closed.closure_subset_iff.2

Premises used: Iff.mpr, IsClosed.closure_subset_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ Ioc a b
⊢ t ∈ s

Tactic:
⟨?_, ⟨ht.1.le, ht.2⟩⟩

Premises used: Set.Mem, setOf, LT.lt.le, Set.inter, And.right, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ Ioc a b
refine : Membership.mem (γ := Set ℝ) {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} t
⊢ t ∈ s

Tactic:
refine ⟨?_, ⟨ht.1.le, ht.2⟩⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ Ioc a b
⊢ Membership.mem (γ := Set ℝ) {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} t

Tactic:
sub_le_integral_of_hasDeriv_right_of_le_Ico ht.2 (hcont.mono (Icc_subset_Icc ht.1.le le_rfl))
        (fun x hx => hderiv x ⟨ht.1.trans_le hx.1, hx.2⟩)
        (φint.mono_set (Icc_subset_Icc ht.1.le le_rfl)) fun x hx => hφg x ⟨ht.1.trans_le hx.1, hx.2⟩

Premises used: le_rfl, Set.Mem, setOf, LT.lt.le, MeasureTheory.IntegrableOn.mono_set, And.right, And.left, LT.lt.trans_le, Set.Icc_subset_Icc, And.intro, ContinuousOn.mono, intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le_Ico
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ Ioc a b
⊢ Membership.mem (γ := Set ℝ) {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} t

Tactic:
exact
      sub_le_integral_of_hasDeriv_right_of_le_Ico ht.2 (hcont.mono (Icc_subset_Icc ht.1.le le_rfl))
        (fun x hx => hderiv x ⟨ht.1.trans_le hx.1, hx.2⟩)
        (φint.mono_set (Icc_subset_Icc ht.1.le le_rfl)) fun x hx => hφg x ⟨ht.1.trans_le hx.1, hx.2⟩

Premises used: le_rfl, LT.lt.le, MeasureTheory.IntegrableOn.mono_set, And.right, And.left, LT.lt.trans_le, Set.Icc_subset_Icc, And.intro, ContinuousOn.mono, intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le_Ico
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
s_closed : IsClosed s
⊢ closure (Ioc a b) ⊆ s

Tactic:
have A : closure (Ioc a b) ⊆ s := by
    apply s_closed.closure_subset_iff.2
    intro t ht
    refine ⟨?_, ⟨ht.1.le, ht.2⟩⟩
    exact
      sub_le_integral_of_hasDeriv_right_of_le_Ico ht.2 (hcont.mono (Icc_subset_Icc ht.1.le le_rfl))
        (fun x hx => hderiv x ⟨ht.1.trans_le hx.1, hx.2⟩)
        (φint.mono_set (Icc_subset_Icc ht.1.le le_rfl)) fun x hx => hφg x ⟨ht.1.trans_le hx.1, hx.2⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
s_closed : IsClosed s
A : closure (Ioc a b) ⊆ s
⊢ Icc a b ⊆ s

Tactic:
rw [closure_Ioc a_lt_b.ne] at A

Premises used: LT.lt.ne, closure_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
s_closed : IsClosed s
A : Icc a b ⊆ s
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y

Tactic:
(A (left_mem_Icc.2 hab)).1

Premises used: Iff.mpr, Set.Mem, And.left, Set.left_mem_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
s_closed : IsClosed s
A : Icc a b ⊆ s
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y

Tactic:
exact (A (left_mem_Icc.2 hab)).1

Premises used: Iff.mpr, And.left, Set.left_mem_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
rw : -(g b - g a) ≤ -∫ (y : ℝ) in a..b, φ y
⊢ ∫ (y : ℝ) in a..b, φ y ≤ g b - g a

Tactic:
rw [← neg_le_neg_iff]

Premises used: neg_le_neg_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -g b - -g a ≤ ∫ (y : ℝ) in a..b, (-φ) y

Tactic:
sub_le_integral_of_hasDeriv_right_of_le hab hcont.neg (fun x hx => (hderiv x hx).neg) φint.neg
      fun x hx => neg_le_neg (hφg x hx)

Premises used: ContinuousOn.neg, intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le, HasDerivWithinAt.neg, neg_le_neg, MeasureTheory.IntegrableOn.neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
h : -(g b - g a) = -g b - -g a
h₁ : Eq (α := ℝ) (-∫ (y : ℝ) in a..b, φ y) (∫ (y : ℝ) in a..b, (-φ) y)
⊢ -(g b - g a) ≤ -∫ (y : ℝ) in a..b, φ y

Tactic:
convert!
    sub_le_integral_of_hasDeriv_right_of_le hab hcont.neg (fun x hx => (hderiv x hx).neg) φint.neg
      fun x hx => neg_le_neg (hφg x hx) using 1

Premises used: ContinuousOn.neg, intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le, HasDerivWithinAt.neg, neg_le_neg, MeasureTheory.IntegrableOn.neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -(g b - g a) = -g b - -g a

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
h : Eq (α := ℝ) (∫ (x : ℝ) in a..b, -φ x) (∫ (y : ℝ) in a..b, (-φ) y)
⊢ Eq (α := ℝ) (-∫ (y : ℝ) in a..b, φ y) (∫ (y : ℝ) in a..b, (-φ) y)

Tactic:
simp only [← integral_neg]

Premises used: intervalIntegral.integral_neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, -φ x) (∫ (y : ℝ) in a..b, (-φ) y)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Icc a b) volume
⊢ ∫ (y : ℝ) in a..b, g' y = g b - g a

Tactic:
le_antisymm (integral_le_sub_of_hasDeriv_right_of_le hab hcont hderiv g'int fun _ _ => le_rfl)
    (sub_le_integral_of_hasDeriv_right_of_le hab hcont hderiv g'int fun _ _ => le_rfl)

Premises used: intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le, le_rfl, le_antisymm, intervalIntegral.integral_le_sub_of_hasDeriv_right_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a

Tactic:
(SeparatingDual.eq_iff_forall_dual_eq (R := ℝ)).2 fun g => ?_

Premises used: Iff.mpr, SeparatingDual.eq_iff_forall_dual_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
refine :
  ∀ (g : StrongDual ℝ E),
    Eq (α := ℝ) ((g : (a : E) → ℝ) (∫ (y : ℝ) in a..b, f' y) : ℝ) ((g : (a : E) → ℝ) (f b - f a) : ℝ)
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a

Tactic:
refine (SeparatingDual.eq_iff_forall_dual_eq (R := ℝ)).2 fun g => ?_

Premises used: Iff.mpr, SeparatingDual.eq_iff_forall_dual_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : StrongDual ℝ E
rw :
  ∫ (x : ℝ) in a..b, (g : (a : E) → ℝ) (f' x) =
    HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) (f b) : ℝ) ((g : (a : E) → ℝ) (f a) : ℝ)
⊢ Eq (α := ℝ) ((g : (a : E) → ℝ) (∫ (y : ℝ) in a..b, f' y) : ℝ) ((g : (a : E) → ℝ) (f b - f a) : ℝ)

Tactic:
rw [← g.intervalIntegral_comp_comm f'int, g.map_sub]

Premises used: ContinuousLinearMap.map_sub, ContinuousLinearMap.intervalIntegral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : StrongDual ℝ E
⊢ ∫ (x : ℝ) in a..b, (g : (a : E) → ℝ) (f' x) =
    HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) (f b) : ℝ) ((g : (a : E) → ℝ) (f a) : ℝ)

Tactic:
integral_eq_sub_of_hasDeriv_right_of_le_real hab (g.continuous.comp_continuousOn hcont)
    (fun x hx => g.hasFDerivAt.comp_hasDerivWithinAt x (hderiv x hx))
    (g.integrable_comp ((intervalIntegrable_iff_integrableOn_Icc_of_le hab enorm_ne_top).1 f'int))

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, ContinuousLinearMap.hasFDerivAt, Continuous.comp_continuousOn, intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le_real, ContinuousLinearMap.integrable_comp, HasFDerivAt.comp_hasDerivWithinAt, ContinuousLinearMap.continuous, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : StrongDual ℝ E
⊢ ∫ (x : ℝ) in a..b, (g : (a : E) → ℝ) (f' x) =
    HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) (f b) : ℝ) ((g : (a : E) → ℝ) (f a) : ℝ)

Tactic:
exact integral_eq_sub_of_hasDeriv_right_of_le_real hab (g.continuous.comp_continuousOn hcont)
    (fun x hx => g.hasFDerivAt.comp_hasDerivWithinAt x (hderiv x hx))
    (g.integrable_comp ((intervalIntegrable_iff_integrableOn_Icc_of_le hab enorm_ne_top).1 f'int))

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, ContinuousLinearMap.hasFDerivAt, Continuous.comp_continuousOn, intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le_real, ContinuousLinearMap.integrable_comp, HasFDerivAt.comp_hasDerivWithinAt, ContinuousLinearMap.continuous, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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
inl : ∀ (hab : a ≤ b), ∫ (y : ℝ) in a..b, f' y = f b - f a
inr : ∀ (hab : b ≤ a), ∫ (y : ℝ) in a..b, f' y = f b - f a
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a

Tactic:
rcases le_total a b with hab | hab

Premises used: le_total
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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
⊢ ContinuousOn f (Icc a b)

Tactic:
simp only [uIcc_of_le, min_eq_left, max_eq_right, hab] at hcont hderiv hint

Premises used: Set.uIcc_of_le, max_eq_right, min_eq_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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)
⊢ ∀ 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

Premises used: Set.uIcc_of_le, max_eq_right, min_eq_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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 : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a

Tactic:
apply integral_eq_sub_of_hasDeriv_right_of_le hab hcont hderiv hint

Premises used: intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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
⊢ ContinuousOn f (Icc b a)

Tactic:
simp only [uIcc_of_ge, min_eq_right, max_eq_left, hab] at hcont hderiv

Premises used: Set.uIcc_of_ge, max_eq_left, min_eq_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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)
⊢ ∀ 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

Premises used: Set.uIcc_of_ge, max_eq_left, min_eq_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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
inr₂ inr₃ : f b - f a = f b - f a
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a

Tactic:
rw [integral_symm, integral_eq_sub_of_hasDeriv_right_of_le hab hcont hderiv hint.symm, neg_sub]

Premises used: neg_sub, intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le, intervalIntegral.integral_symm, IntervalIntegrable.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a

Tactic:
integral_eq_sub_of_hasDeriv_right_of_le hab hcont (fun x hx => (hderiv x hx).hasDerivWithinAt)
    hint

Premises used: HasDerivAt.hasDerivWithinAt, intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hderiv : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a

Tactic:
integral_eq_sub_of_hasDeriv_right (HasDerivAt.continuousOn hderiv)
    (fun _x hx => (hderiv _ (mem_Icc_of_Ioo hx)).hasDerivWithinAt) hint

Premises used: HasDerivAt.hasDerivWithinAt, HasDerivAt.continuousOn, Set.mem_Icc_of_Ioo, intervalIntegral.integral_eq_sub_of_hasDeriv_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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

Tactic:
fun x hx => (hderiv x hx).congr_of_eventuallyEq ?_

Premises used: HasDerivAt.congr_of_eventuallyEq
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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
refine : ∀ (x : ℝ) (hx : x ∈ Ioo a b), F =ᶠ[𝓝 x] f
⊢ ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x

Tactic:
refine fun x hx => (hderiv x hx).congr_of_eventuallyEq ?_

Premises used: HasDerivAt.congr_of_eventuallyEq