mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case inl
g' g φ : ℝ → ℝ
a : ℝ
hab : a ≤ a
hcont : ContinuousOn g (Icc a a)
hderiv : ∀ x ∈ Ioo a a, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a a) volume
hφg : ∀ x ∈ Ioo a a, g' x ≤ φ x
⊢ g a - g a ≤ ∫ (y : ℝ) in a..a, φ y

pp: case inr
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 φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y

Tactic:
·

Goal state after:
case inl
g' g φ : ℝ → ℝ
a : ℝ
hab : a ≤ a
hcont : ContinuousOn g (Icc a a)
hderiv : ∀ x ∈ Ioo a a, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a a) volume
hφg : ∀ x ∈ Ioo a a, g' x ≤ φ x
⊢ g a - g a ≤ ∫ (y : ℝ) in a..a, φ y
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case inr
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntegrableOn f (Ioi a) μ
hb : IntegrableOn f (Ioi b) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Ioi a) μ →
      IntegrableOn f (Ioi b) μ →
        a ≤ b → ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a, f x ∂μ
hab : ¬a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a, f x ∂μ

pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
ha : IntegrableOn f (Ioi a) μ
hb : IntegrableOn f (Ioi b) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a, f x ∂μ

Tactic:
·

Goal state after:
case inr
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntegrableOn f (Ioi a) μ
hb : IntegrableOn f (Ioi b) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Ioi a) μ →
      IntegrableOn f (Ioi b) μ →
        a ≤ b → ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a, f x ∂μ
hab : ¬a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case pos
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
h : a ≤ b
⊢ IntegrableOn f (Ioi a) μ

pp: case neg
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
h : b < a
⊢ IntegrableOn f (Ioi a) μ

Tactic:
·

Goal state after:
case pos
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
h : a ≤ b
⊢ IntegrableOn f (Ioi a) μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case neg
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
h : b < a
⊢ IntegrableOn f (Ioi a) μ

Tactic:
·

Goal state after:
case neg
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
h : b < a
⊢ IntegrableOn f (Ioi a) μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case inr
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Ioi a) μ →
      IntegrableOn f (Ioi b) μ →
        a ≤ b → ∫ (x : ℝ) in Ioi a, f x ∂μ - ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ ∫ (x : ℝ) in Ioi a, f x ∂μ - ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ

pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ioi a, f x ∂μ - ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
·

Goal state after:
case inr
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Ioi a) μ →
      IntegrableOn f (Ioi b) μ →
        a ≤ b → ∫ (x : ℝ) in Ioi a, f x ∂μ - ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ ∫ (x : ℝ) in Ioi a, f x ∂μ - ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case e'_3
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 φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -(g b - g a) = -g b - -g a

pp: case e'_4
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 φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -∫ (y : ℝ) in a..b, φ y = ∫ (y : ℝ) in a..b, (-φ) y

Tactic:
·

Goal state after:
case e'_3
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 φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -(g b - g a) = -g b - -g a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case e'_4
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 φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -∫ (y : ℝ) in a..b, φ y = ∫ (y : ℝ) in a..b, (-φ) y

Tactic:
·

Goal state after:
case e'_4
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 φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -∫ (y : ℝ) in a..b, φ y = ∫ (y : ℝ) in a..b, (-φ) y
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case inl
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : 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

pp: case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : 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

Tactic:
·

Goal state after:
case inl
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : 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
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : 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

Tactic:
·

Goal state after:
case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : 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
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case inr
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Iio b) μ →
      IntegrableOn f (Iio a) μ →
        a ≤ b → ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ

pp: E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a✝ b✝ : ℝ
f : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
a b : ℝ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
·

Goal state after:
case inr
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Iio b) μ →
      IntegrableOn f (Iio a) μ →
        a ≤ b → ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case e_a
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ ∫ (t : ℝ) in a₀..s, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f p t ∂μ = ∫ (t : ℝ) in b₀..s, f p t ∂μ

pp: case e_a
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ ∫ (t : ℝ) in a₀..b₀, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f q t ∂μ = ∫ (t : ℝ) in a₀..b₀, f p t - f q t ∂μ

Tactic:
·

Goal state after:
case e_a
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ ∫ (t : ℝ) in a₀..s, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f p t ∂μ = ∫ (t : ℝ) in b₀..s, f p t ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case inr
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : IntegrableOn f (Ici a) μ
hg : IntegrableOn f (Ici b) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Ici a) μ →
      IntegrableOn f (Ici b) μ →
        a ≤ b → ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ

pp: E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a✝ b✝ : ℝ
f : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
a b : ℝ
hf : IntegrableOn f (Ici a) μ
hg : IntegrableOn f (Ici b) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
·

Goal state after:
case inr
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : IntegrableOn f (Ici a) μ
hg : IntegrableOn f (Ici b) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Ici a) μ →
      IntegrableOn f (Ici b) μ →
        a ≤ b → ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case e_a
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ ∫ (t : ℝ) in a₀..b₀, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f q t ∂μ = ∫ (t : ℝ) in a₀..b₀, f p t - f q t ∂μ

Tactic:
·

Goal state after:
case e_a
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ ∫ (t : ℝ) in a₀..b₀, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f q t ∂μ = ∫ (t : ℝ) in a₀..b₀, f p t - f q t ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case refine_1
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : 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 (update f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa)

pp: case refine_2
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : 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 (update f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ b ∈ Icc a b → Tendsto (update f a fa) (𝓝[Ico a b] b) (𝓝 fb)

Tactic:
·

Goal state after:
case refine_1
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : 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 (update f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case refine_1
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : 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 (update f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa)

Tactic:
exact fun _ => ha.mono_left (nhdsWithin_mono _ Ioo_subset_Ioi_self)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case refine_2
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : 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 (update f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ b ∈ Icc a b → Tendsto (update f a fa) (𝓝[Ico a b] b) (𝓝 fb)

Tactic:
·

Goal state after:
case refine_2
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : 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 (update f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ b ∈ Icc a b → Tendsto (update f a fa) (𝓝[Ico a b] b) (𝓝 fb)
Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (fun x ↦ ‖f' x‖) l atTop
x : ℝ
hx : DifferentiableAt ℝ f x
⊢ (fderiv ℝ (⇑a) (f x)) (deriv f x) = a (deriv f x)

pp: E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (fun x ↦ ‖f' x‖) l atTop
x : ℝ
hx : DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ (⇑a) (f x)

Tactic:
·

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (fun x ↦ ‖f' x‖) l atTop
x : ℝ
hx : DifferentiableAt ℝ f x
⊢ (fderiv ℝ (⇑a) (f x)) (deriv f x) = a (deriv f x)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case inl
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

pp: case inr
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

Tactic:
·

Goal state after:
case inl
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case inl
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : 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

pp: case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : 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

Tactic:
·

Goal state after:
case inl
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : 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
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case inr
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

Tactic:
·

Goal state after:
case inr
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ