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

Goal state before:
pp: case inr
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
⊢ IntegrableOn (fun x ↦ f (c * x)) [[a / c, b / c]] volume

Tactic:
rw [← Real.smul_map_volume_mul_right (inv_ne_zero hc), IntegrableOn, Measure.restrict_smul,
    integrable_smul_measure (by simpa : ENNReal.ofReal |c⁻¹| ≠ 0) ENNReal.ofReal_ne_top,
    ← IntegrableOn, MeasurableEmbedding.integrableOn_map_iff A]

Goal state after:
case inr
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
⊢ IntegrableOn ((fun x ↦ f (c * x)) ∘ fun x ↦ x * c⁻¹) ((fun x ↦ x * c⁻¹) ⁻¹' [[a / c, b / c]]) volume
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case e'_6
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
x✝ : ℝ
⊢ ((fun x ↦ f (c * x)) ∘ fun x ↦ x * c⁻¹) x✝ = f x✝

Tactic:
;

Goal state after:
case e'_6
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
x✝ : ℝ
⊢ ((fun x ↦ f (c * x)) ∘ fun x ↦ x * c⁻¹) x✝ = f x✝
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case e'_6
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
x✝ : ℝ
⊢ f (c * (x✝ * c⁻¹)) = f x✝

Tactic:
;

Goal state after:
case e'_6
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
x✝ : ℝ
⊢ f (c * (x✝ * c⁻¹)) = f x✝
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case e'_6
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
x✝ : ℝ
⊢ c * (x✝ * c⁻¹) = x✝

Tactic:
;

Goal state after:
case e'_6
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
x✝ : ℝ
⊢ c * (x✝ * c⁻¹) = x✝
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case e'_7
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
⊢ [[a / c / c⁻¹, b / c / c⁻¹]] = [[a, b]]

Tactic:
;

Goal state after:
case e'_7
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
⊢ [[a / c / c⁻¹, b / c / c⁻¹]] = [[a, b]]
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
B : Continuous[instTopologicalSpaceProd, _] fun p ↦ ‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖
⊢ 0 ≤ t

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
B : Continuous[instTopologicalSpaceProd, _] fun p ↦ ‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖
⊢ 0 ≤ t
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
ca cb : E
la la' lb lb' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : FTCFilter a la la'
inst✝ : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this : la'.IsMeasurablyGenerated
⊢ (fun t ↦
      ∫ (x : ℝ) in va t..vb t, f x ∂μ - ∫ (x : ℝ) in ua t..ub t, f x ∂μ -
        (∫ (x : ℝ) in ub t..vb t, cb ∂μ - ∫ (x : ℝ) in ua t..va t, ca ∂μ)) =o[lt]
    fun t ↦ ‖∫ (x : ℝ) in ua t..va t, 1 ∂μ‖ + ‖∫ (x : ℝ) in ub t..vb t, 1 ∂μ‖

Tactic:
;

Goal state after:
ι : Type u_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
ca cb : E
la la' lb lb' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : FTCFilter a la la'
inst✝ : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this : la'.IsMeasurablyGenerated
⊢ (fun t ↦
      ∫ (x : ℝ) in va t..vb t, f x ∂μ - ∫ (x : ℝ) in ua t..ub t, f x ∂μ -
        (∫ (x : ℝ) in ub t..vb t, cb ∂μ - ∫ (x : ℝ) in ua t..va t, ca ∂μ)) =o[lt]
    fun t ↦ ‖∫ (x : ℝ) in ua t..va t, 1 ∂μ‖ + ‖∫ (x : ℝ) in ub t..vb t, 1 ∂μ‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
this :
  ∀ {a b : ℝ},
    IntervalIntegrable f volume a b →
      ‖f (min a b)‖ₑ ≠ ∞ →
        ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞ → a ≤ b → IntervalIntegrable (fun x ↦ f (x + c)) volume (a - c) (b - c)
hab : ¬a ≤ b
⊢ ‖f (min a b)‖ₑ ≠ ∞

Tactic:
;

Goal state after:
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
this :
  ∀ {a b : ℝ},
    IntervalIntegrable f volume a b →
      ‖f (min a b)‖ₑ ≠ ∞ →
        ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞ → a ≤ b → IntervalIntegrable (fun x ↦ f (x + c)) volume (a - c) (b - c)
hab : ¬a ≤ b
⊢ ‖f (min a b)‖ₑ ≠ ∞
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
this :
  ∀ {a b : ℝ},
    IntervalIntegrable f volume a b →
      ‖f (min a b)‖ₑ ≠ ∞ →
        ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞ → a ≤ b → IntervalIntegrable (fun x ↦ f (x + c)) volume (a - c) (b - c)
hab : ¬a ≤ b
⊢ ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞

Tactic:
;

Goal state after:
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
this :
  ∀ {a b : ℝ},
    IntervalIntegrable f volume a b →
      ‖f (min a b)‖ₑ ≠ ∞ →
        ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞ → a ≤ b → IntervalIntegrable (fun x ↦ f (x + c)) volume (a - c) (b - c)
hab : ¬a ≤ b
⊢ ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b ↦ ∫ (x : ℝ) in b₁..b₂, {x | x ≤ b}.indicator f x ∂μ
x : ℝ
⊢ ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ‖{x_1 | x_1 ≤ x}.indicator f t‖ ≤ ‖f t‖

Tactic:
;

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b ↦ ∫ (x : ℝ) in b₁..b₂, {x | x ≤ b}.indicator f x ∂μ
x : ℝ
⊢ ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ‖{x_1 | x_1 ≤ x}.indicator f t‖ ≤ ‖f t‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝ : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable (fun x ↦ f (-1 * x)) volume (a / -1) (b / -1) ↔
    IntervalIntegrable (fun x ↦ f (-x)) volume (-a) (-b)

Tactic:
;

Goal state after:
E : Type u_5
inst✝ : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable (fun x ↦ f (-1 * x)) volume (a / -1) (b / -1) ↔
    IntervalIntegrable (fun x ↦ f (-x)) volume (-a) (-b)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
| fun x ↦ f (-x)

Tactic:
;

Goal state after:
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
| fun x ↦ f (-x)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t✝ : ℝ
ht : ‖f (min 0 t✝)‖ₑ ≠ ∞
h : t✝ < 0
t : ℝ
| f (-t)

Tactic:
;

Goal state after:
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t✝ : ℝ
ht : ‖f (min 0 t✝)‖ₑ ≠ ∞
h : t✝ < 0
t : ℝ
| f (-t)
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∉ Icc b₁ b₂
⊢ b₀ ∉ closure (Icc b₁ b₂)

Tactic:
closure_Icc

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∉ Icc b₁ b₂
⊢ b₀ ∉ Icc b₁ b₂
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
| fun x ↦ f (-x)

Tactic:
;

Goal state after:
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
| fun x ↦ f (-x)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t✝ : ℝ
ht : ‖f (min 0 t✝)‖ₑ ≠ ∞
h : t✝ < 0
t : ℝ
| f (-t)

Tactic:
;

Goal state after:
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t✝ : ℝ
ht : ‖f (min 0 t✝)‖ₑ ≠ ∞
h : t✝ < 0
t : ℝ
| f (-t)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}

Tactic:
;

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this✝ : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst✝] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ f a' z - f a' y - (L z - L y) = f a' z - f a z + (f a y - f a' y) + (f a z - f a y - (L z - L y))

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this✝ : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst✝] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ f a' z - f a' y - (L z - L y) = f a' z - f a z + (f a y - f a' y) + (f a z - f a y - (L z - L y))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
⊢ -∫ (a : ℝ) in Ioc a b, f a ∂μ - -∫ (a : ℝ) in Ioc b a, f a ∂μ =
    -(∫ (a : ℝ) in Ioc a b, f a ∂μ - ∫ (a : ℝ) in Ioc b a, f a ∂μ)

Tactic:
;

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
⊢ -∫ (a : ℝ) in Ioc a b, f a ∂μ - -∫ (a : ℝ) in Ioc b a, f a ∂μ =
    -(∫ (a : ℝ) in Ioc a b, f a ∂μ - ∫ (a : ℝ) in Ioc b a, f a ∂μ)
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x ↦ F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
this :
  ∀ᶠ (p : X × ℝ) in 𝓝 (x₀, b₀),
    ∫ (s : ℝ) in a₀..p.2, F p.1 s ∂μ =
      ∫ (s : ℝ) in a₀..b₀, F p.1 s ∂μ + ∫ (s : ℝ) in b₀..p.2, F x₀ s ∂μ + ∫ (s : ℝ) in b₀..p.2, F p.1 s - F x₀ s ∂μ
⊢ ContinuousAt
    (fun x ↦
      ∫ (s : ℝ) in a₀..b₀, F x.1 s ∂μ + ∫ (s : ℝ) in b₀..x.2, F x₀ s ∂μ + ∫ (s : ℝ) in b₀..x.2, F x.1 s - F x₀ s ∂μ)
    (x₀, b₀)

Tactic:
;

Goal state after:
E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x ↦ F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
this :
  ∀ᶠ (p : X × ℝ) in 𝓝 (x₀, b₀),
    ∫ (s : ℝ) in a₀..p.2, F p.1 s ∂μ =
      ∫ (s : ℝ) in a₀..b₀, F p.1 s ∂μ + ∫ (s : ℝ) in b₀..p.2, F x₀ s ∂μ + ∫ (s : ℝ) in b₀..p.2, F p.1 s - F x₀ s ∂μ
⊢ ContinuousAt
    (fun x ↦
      ∫ (s : ℝ) in a₀..b₀, F x.1 s ∂μ + ∫ (s : ℝ) in b₀..x.2, F x₀ s ∂μ + ∫ (s : ℝ) in b₀..x.2, F x.1 s - F x₀ s ∂μ)
    (x₀, b₀)
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
H : IsOpen[instTopologicalSpaceProd] (⋃ L ∈ K, {p | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})
⊢ {p | p.2 ∈ B (f p.1) K r s t} = ⋃ L ∈ K, {p | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t}

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
H : IsOpen[instTopologicalSpaceProd] (⋃ L ∈ K, {p | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})
⊢ {p | p.2 ∈ B (f p.1) K r s t} = ⋃ L ∈ K, {p | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t}
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
H : IsOpen[instTopologicalSpaceProd] (⋃ L ∈ K, {p | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})
p : α × E
⊢ p ∈ {p | p.2 ∈ B (f p.1) K r s t} ↔ p ∈ ⋃ L ∈ K, {p | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t}

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
H : IsOpen[instTopologicalSpaceProd] (⋃ L ∈ K, {p | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})
p : α × E
⊢ p ∈ {p | p.2 ∈ B (f p.1) K r s t} ↔ p ∈ ⋃ L ∈ K, {p | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s 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 ℝ
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 b..a, f x ∂μ + (∫ (x : ℝ) in b..a, f x ∂μ + ∫ (x : ℝ) in Ioi a, 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 b..a, f x ∂μ + (∫ (x : ℝ) in b..a, f x ∂μ + ∫ (x : ℝ) in Ioi a, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ