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

Goal state before:
pp: case pos.refine_3
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) =o[lt] fun i ↦ μ.real (Ioc (u i) (v i))
B :
  (fun i ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) =o[lt] fun i ↦ μ.real (Ioc (v i) (u i))
t : ι
⊢ ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - μ.real (Ioc (u t) (v t)) • c -
      (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ - μ.real (Ioc (v t) (u t)) • c) =
    ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c)

Tactic:
[

Goal state after:
case pos.refine_3
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) =o[lt] fun i ↦ μ.real (Ioc (u i) (v i))
B :
  (fun i ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) =o[lt] fun i ↦ μ.real (Ioc (v i) (u i))
t : ι
⊢ ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - μ.real (Ioc (u t) (v t)) • c -
      (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ - μ.real (Ioc (v t) (u t)) • c) =
    ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c)
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: 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 : ℝ
hx : x ∈ Icc b₁ b₂
⊢ AEStronglyMeasurable f (μ.restrict (Ioc (min b₁ b₂) x))

Tactic:
rw [min₁₂]
        exact (h_int' hx).1.aestronglyMeasurable

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

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable (fun x ↦ f (c + x)) volume (a - c) (b - c) ↔ IntervalIntegrable f volume a b

Tactic:
[

Goal state after:
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable (fun x ↦ f (c + x)) volume (a - c) (b - c) ↔ IntervalIntegrable f volume a b
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable (fun x ↦ f (x - c)) volume (a + c) (b + c) ↔ IntervalIntegrable f volume a b

Tactic:
[

Goal state after:
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable (fun x ↦ f (x - c)) volume (a + c) (b + c) ↔ IntervalIntegrable f volume a b
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℝ → E
c : E
la la' : Filter ℝ
lt : Filter ι
a b : ℝ
u v : ι → ℝ
inst✝ : FTCFilter a la la'
hab : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter f la' volume
hf : Tendsto f (la' ⊓ ae volume) (𝓝 c)
hu : Tendsto u lt la
hv : Tendsto v lt la
⊢ (fun t ↦ ((∫ (x : ℝ) in v t..b, f x) - ∫ (x : ℝ) in u t..b, f x) + (v t - u t) • c) =o[lt] (v - u)

Tactic:
simpa only [integral_const, smul_eq_mul, mul_one] using!
    measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left hab hmeas hf hu hv

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

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
⊢ ‖∫ (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
f : ℝ → E
a b : ℝ
μ : Measure ℝ
⊢ ‖∫ (x : ℝ) in a..b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
μ : Measure ℝ
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b : ℝ
φ : ℝ → F →L[𝕜] E
hφ : IntervalIntegrable φ μ a b
v : F
⊢ (∫ (x : ℝ) in a..b, φ x ∂μ) v = ∫ (x : ℝ) in a..b, (φ x) v ∂μ

Tactic:
[

Goal state after:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
μ : Measure ℝ
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b : ℝ
φ : ℝ → F →L[𝕜] E
hφ : IntervalIntegrable φ μ a b
v : F
⊢ (∫ (x : ℝ) in a..b, φ x ∂μ) v = ∫ (x : ℝ) in a..b, (φ x) v ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
L : E →L[𝕜] F
hf : IntervalIntegrable f μ a b
⊢ ∫ (x : ℝ) in a..b, L (f x) ∂μ = L (∫ (x : ℝ) in a..b, f x ∂μ)

Tactic:
[

Goal state after:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
L : E →L[𝕜] F
hf : IntervalIntegrable f μ a b
⊢ ∫ (x : ℝ) in a..b, L (f x) ∂μ = L (∫ (x : ℝ) in a..b, f x ∂μ)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
L : E →L[𝕜] F
hf : IntervalIntegrable f μ a b
⊢ ∫ (x : ℝ) in Ioc a b, L (f x) ∂μ - ∫ (x : ℝ) in Ioc b a, L (f x) ∂μ =
    L (∫ (x : ℝ) in Ioc a b, f x ∂μ - ∫ (x : ℝ) in Ioc b a, f x ∂μ)

Tactic:
L.integral_comp_comm hf.1,

Goal state after:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
L : E →L[𝕜] F
hf : IntervalIntegrable f μ a b
⊢ L (∫ (x : ℝ) in Ioc a b, f x ∂μ) - ∫ (x : ℝ) in Ioc b a, L (f x) ∂μ =
    L (∫ (x : ℝ) in Ioc a b, f x ∂μ - ∫ (x : ℝ) in Ioc b a, f x ∂μ)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
L : E →ₗᵢ[𝕜] F
f : ℝ → E
⊢ ∫ (x : ℝ) in a..b, L (f x) ∂μ = L (∫ (x : ℝ) in a..b, f x ∂μ)

Tactic:
[

Goal state after:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
L : E →ₗᵢ[𝕜] F
f : ℝ → E
⊢ ∫ (x : ℝ) in a..b, L (f x) ∂μ = L (∫ (x : ℝ) in a..b, f x ∂μ)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
B : ∀ᶠ (u : ℝ) in 𝓝 t, ↑y < G' u
m M : ℝ
H : Ioo m M ⊆ {x | (fun u ↦ ↑y < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
I : Icc t u ⊆ Icc a b
⊢ ∫ (x : ℝ) in Icc t u, y ≤ ∫ (x : ℝ) in Ioc t u, (G' x).toReal ∂volume

Tactic:
← integral_Icc_eq_integral_Ioc

Goal state after:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
B : ∀ᶠ (u : ℝ) in 𝓝 t, ↑y < G' u
m M : ℝ
H : Ioo m M ⊆ {x | (fun u ↦ ↑y < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
I : Icc t u ⊆ Icc a b
⊢ ∫ (x : ℝ) in Icc t u, y ≤ ∫ (t : ℝ) in Icc t u, (G' t).toReal ∂volume
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c
⊢ ∫ (x : ℝ) in a..b, f (x * c) =
    c⁻¹ • ∫ (x : ℝ) in a * c..b * c, f x ∂ENNReal.ofReal |c| • Measure.map (fun x ↦ x * c) volume

Tactic:
[

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c
⊢ ∫ (x : ℝ) in a..b, f (x * c) =
    c⁻¹ • ∫ (x : ℝ) in a * c..b * c, f x ∂ENNReal.ofReal |c| • Measure.map (fun x ↦ x * c) volume
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
x : ℝ
x_in : x ∈ Icc a b
⊢ ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ

Tactic:
[

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
x : ℝ
x_in : x ∈ Icc a b
⊢ ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f 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
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
⊢ MeasurableSet {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}

Tactic:
this

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
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
⊢ MeasurableSet {p | p.2 ∈ D (f p.1) K}
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
this : Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c
⊢ ∫ (x : ℝ) in Ioc a b ∪ Ioc b c ∪ Ioc c a, f x ∂μ = ∫ (x : ℝ) in Ioc b a ∪ Ioc c b ∪ Ioc a c, f x ∂μ

Tactic:
this

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
this : Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c
⊢ ∫ (x : ℝ) in Ioc b a ∪ Ioc c b ∪ Ioc a c, f x ∂μ = ∫ (x : ℝ) in Ioc b a ∪ Ioc c b ∪ Ioc a c, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ Ioc (min b (min a c)) (max a (max b c)) = Ioc (min b (min a c)) (max b (max a c))

Tactic:
max_left_comm

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ Ioc (min b (min a c)) (max b (max a c)) = Ioc (min b (min a c)) (max b (max a c))
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
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
s : Set (E →L[𝕜] F)
hs : IsClosed s
this :
  (fun p ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s =
    {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | 0 ∈ s}
⊢ MeasurableSet ((fun p ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s)

Tactic:
this

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
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
s : Set (E →L[𝕜] F)
hs : IsClosed s
this :
  (fun p ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s =
    {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | 0 ∈ s}
⊢ MeasurableSet
    ({p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | 0 ∈ s})
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

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

Tactic:
rw [← hderiv, integral_deriv_eq_sub hdiff]
  rw [hderiv]
  exact hcont.intervalIntegrable

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

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ ∫ (x : ℝ) in {x | x ≤ a₂} ∩ Ioc a₁ a₃, f x ∂μ = ∫ (x : ℝ) in Ioc a₁ a₂, f x ∂μ

pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}

pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}

Tactic:
this

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ ∫ (x : ℝ) in Ioc a₁ a₂, f x ∂μ = ∫ (x : ℝ) in Ioc a₁ a₂, f x ∂μ

E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}

E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case e'_2
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn (fun t ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ t ∈ Icc 0 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : ℝ → 𝕜 := fun t ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
hderiv' : ∀ t ∈ [[0, 1]], HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t
⊢ z₁ • ∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁) = ∫ (y : ℝ) in 0..1, z₁ • (f' ∘ γ) y

Tactic:
[

Goal state after:
case e'_2
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn (fun t ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ t ∈ Icc 0 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : ℝ → 𝕜 := fun t ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
hderiv' : ∀ t ∈ [[0, 1]], HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t
⊢ z₁ • ∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁) = ∫ (y : ℝ) in 0..1, z₁ • (f' ∘ γ) y
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst✝⁷ : QuotientMeasureEqMeasurePreimage ν μ
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : PolishSpace G
inst✝² : T2Space (G ⧸ Γ)
inst✝¹ : SecondCountableTopology (G ⧸ Γ)
inst✝ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this : QuotientGroup.mk ⁻¹' (fun x ↦ g • x) ⁻¹' A = (fun x ↦ g * x) ⁻¹' π_preA
⊢ ν (QuotientGroup.mk ⁻¹' (fun x ↦ g • x) ⁻¹' A ∩ 𝓕) = ν (π_preA ∩ g • 𝓕)

Tactic:
this

Goal state after:
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst✝⁷ : QuotientMeasureEqMeasurePreimage ν μ
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : PolishSpace G
inst✝² : T2Space (G ⧸ Γ)
inst✝¹ : SecondCountableTopology (G ⧸ Γ)
inst✝ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this : QuotientGroup.mk ⁻¹' (fun x ↦ g • x) ⁻¹' A = (fun x ↦ g * x) ⁻¹' π_preA
⊢ ν ((fun x ↦ g * x) ⁻¹' π_preA ∩ 𝓕) = ν (π_preA ∩ g • 𝓕)
Module: Mathlib.Order.Filter.AtTopBot.Floor

Goal state before:
pp: case calc_2
K : Type u_1
inst✝³ : Ring K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ ↑⌈|a|⌉₊ * ↑⌈|c|⌉₊ ^ n = ↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n)

Tactic:
[

Goal state after:
case calc_2
K : Type u_1
inst✝³ : Ring K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ ↑⌈|a|⌉₊ * ↑⌈|c|⌉₊ ^ n = ↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
hfi : Integrable f μ
y : ℝ
⊢ HasSum (fun n ↦ ∫ (x : ℝ) in y + ↑n..y + ↑n + 1, f x ∂μ) (∫ (x : ℝ), f x ∂μ)

Tactic:
[

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
hfi : Integrable f μ
y : ℝ
⊢ HasSum (fun n ↦ ∫ (x : ℝ) in y + ↑n..y + ↑n + 1, f x ∂μ) (∫ (x : ℝ), f x ∂μ)