mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
hf : AEMeasurable f μ
g : X → E
f' : X → ℝ≥0 := AEMeasurable.mk f hf
x : X
⊢ f x = AEMeasurable.mk f hf x → f' x • g x = f x • g x

Tactic:
hx

Goal state after:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
hf : AEMeasurable f μ
g : X → E
f' : X → ℝ≥0 := AEMeasurable.mk f hf
x : X
hx : f x = AEMeasurable.mk f hf x
⊢ f' x • g x = f x • g x
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
hf : AEMeasurable f μ
g : X → E
f' : X → ℝ≥0 := AEMeasurable.mk f hf
x : X
hx : f x = AEMeasurable.mk f hf x
⊢ f' x • g x = f x • g x

Tactic:
hx

Goal state after:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
hf : AEMeasurable f μ
g : X → E
f' : X → ℝ≥0 := AEMeasurable.mk f hf
x : X
hx : f x = AEMeasurable.mk f hf x
⊢ f' x • g x = AEMeasurable.mk f hf x • g x
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case pos.h_bound
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
i : ι
x : ℝ
⊢ x ∈ Ι a b → ‖(f i) x‖ ≤ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖

Tactic:
hx

Goal state after:
case pos.h_bound
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
i : ι
x : ℝ
hx : x ∈ Ι a b
⊢ ‖(f i) x‖ ≤ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case neg
ι : Type u_1
a b : ℝ
μ : Measure ℝ
ε : Type u_8
inst✝³ : TopologicalSpace ε
inst✝² : ENormedAddCommMonoid ε
inst✝¹ : ContinuousAdd ε
inst✝ : PseudoMetrizableSpace ε
f : ι → ℝ → ε
h : ∀ (i : ι), IntervalIntegrable (f i) μ a b
h₁ : ¬(support f).Finite
⊢ IntervalIntegrable 0 μ a b

Tactic:
apply intervalIntegrable_const_iff (c := 0) (by simp) |>.2

Goal state after:
case neg
ι : Type u_1
a b : ℝ
μ : Measure ℝ
ε : Type u_8
inst✝³ : TopologicalSpace ε
inst✝² : ENormedAddCommMonoid ε
inst✝¹ : ContinuousAdd ε
inst✝ : PseudoMetrizableSpace ε
f : ι → ℝ → ε
h : ∀ (i : ι), IntervalIntegrable (f i) μ a b
h₁ : ¬(support f).Finite
⊢ 0 = 0 ∨ μ (Ι a b) < ∞
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case pos
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₂
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀

Tactic:
have h₁₂ : b₁ ≤ b₂ := h₀.1.trans h₀.2

Goal state after:
case pos
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₂
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
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 : ℝ
⊢ x ∈ Icc b₁ b₂ → AEStronglyMeasurable ({x_1 | x_1 ≤ x}.indicator f) (μ.restrict (Ι b₁ b₂))

Tactic:
hx

Goal state after:
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 ({x_1 | x_1 ≤ x}.indicator f) (μ.restrict (Ι b₁ b₂))
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:
min₁₂

Goal state after:
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 b₁ x))
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 : ℝ
⊢ x ∈ {b₀}ᶜ → x < b₀ ∨ b₀ < x

Tactic:
hx

Goal state after:
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 ∈ {b₀}ᶜ
⊢ x < b₀ ∨ b₀ < x
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 ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
x : ℝ
⊢ x₀ < x → {t | t ≤ x}.indicator f x₀ = f x₀

Tactic:
hx

Goal state after:
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 ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
x : ℝ
hx : x₀ < x
⊢ {t | t ≤ x}.indicator f x₀ = f x₀
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 ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
x : ℝ
⊢ x < x₀ → {t | t ≤ x}.indicator f x₀ = 0

Tactic:
hx

Goal state after:
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 ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
x : ℝ
hx : x < x₀
⊢ {t | t ≤ x}.indicator f x₀ = 0
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case refine_2
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
⊢ ContinuousAt (fun x ↦ ∫ (s : ℝ) in b₀..x.2, F x₀ s ∂μ) (x₀, b₀)

Tactic:
refine (?_ : ContinuousAt (fun t ↦ ∫ s in b₀..t, F x₀ s ∂μ) b₀).snd'

Goal state after:
case refine_2
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
⊢ ContinuousAt (fun t ↦ ∫ (s : ℝ) in b₀..t, F x₀ s ∂μ) b₀
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
C1 : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc t u), G' x < ↑∞
C2 : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc t u), x ∈ Icc t u
x : ℝ
G'x : G' x < ↑∞
⊢ x ∈ Icc t u → y ≤ (G' x).toReal

Tactic:
hx

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
C1 : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc t u), G' x < ↑∞
C2 : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc t u), x ∈ Icc t u
x : ℝ
G'x : G' x < ↑∞
hx : x ∈ Icc t u
⊢ y ≤ (G' x).toReal
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
c d : ℝ
hc : c = 0
⊢ c⁻¹ • ∫ (x : ℝ) in a..b, f (d + x / c) = ∫ (x : ℝ) in d + a / c..d + b / c, f x

Tactic:
simp [hc, integral_comp_add_div]

Goal state after:
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
c d : ℝ
hc : ¬c = 0
⊢ c⁻¹ • ∫ (x : ℝ) in a..b, f (d + x / c) = ∫ (x : ℝ) in d + a / c..d + b / c, f x

Tactic:
simp [hc, integral_comp_add_div]

Goal state after:
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) μ
aux : (fun x ↦ ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ
⊢ ContinuousOn (fun x ↦ ∫ (t : ℝ) in Icc a x, f t ∂μ) (Icc a b)

Tactic:
aux

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) μ
aux : (fun x ↦ ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ
⊢ ContinuousOn (fun x ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc 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
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
⊢ Measurable fun p ↦ fderiv 𝕜 (f p.1) p.2

Tactic:
refine measurable_of_isClosed (fun s hs ↦ ?_)
  have :
    (fun (p : α × E) ↦ 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 : E →L[𝕜] F) ∈ s} :=
    Set.ext (fun x ↦ mem_preimage.trans fderiv_mem_iff)
  rw [this]
  exact
    (measurableSet_of_differentiableAt_of_isComplete_with_param hf hs.isComplete).union
      ((measurableSet_of_differentiableAt_with_param _ hf).compl.inter (MeasurableSet.const _))

Goal state after:
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 ∈ 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
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:
refine ⟨?_, ⟨ht.1.le, ht.2⟩⟩

Goal state after:
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
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 ∈ {t | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u}
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
x : ℝ
⊢ DifferentiableAt ℝ f x → DifferentiableAt ℝ f' x

Tactic:
hx

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
x : ℝ
hx : DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ f' x
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 : ℝ
⊢ DifferentiableAt ℝ f x → ‖deriv f' x‖ = ‖deriv f x‖

Tactic:
hx

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
⊢ ‖deriv f' x‖ = ‖deriv f x‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
h : EqOn f g (uIoo a b)
x : ℝ
a✝ : x ≠ max a b
⊢ x ∈ Ι a b → f x = g x

Tactic:
hx

Goal state after:
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
h : EqOn f g (uIoo a b)
x : ℝ
a✝ : x ≠ max a b
hx : x ∈ Ι a b
⊢ f x = g x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
h : EqOn f g (uIoo a b)
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
apply integral_congr_ae
  filter_upwards [μ.ae_ne <| a ⊔ b] with x _ hx
  exact h ⟨hx.left, lt_of_le_of_ne hx.right ‹_›⟩

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
x : ℝ
⊢ x ∈ Ioo a b → 0 x ≤ f x

Tactic:
hx

Goal state after:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
x : ℝ
hx : x ∈ Ioo a b
⊢ 0 x ≤ f x
Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable

Goal state before:
pp: F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x ↦ (x - c)⁻¹) =O[𝓝[≠] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
x : ℝ
⊢ x ∈ {c}ᶜ → HasDerivAt (fun x ↦ Real.log (x - c)) (x - c)⁻¹ x

Tactic:
hx

Goal state after:
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x ↦ (x - c)⁻¹) =O[𝓝[≠] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
x : ℝ
hx : x ∈ {c}ᶜ
⊢ HasDerivAt (fun x ↦ Real.log (x - c)) (x - c)⁻¹ x
Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable

Goal state before:
pp: a x : ℝ
⊢ x ∈ Ioi 0 → HasDerivAt (fun x ↦ Real.log x) x⁻¹ x

Tactic:
hx

Goal state after:
a x : ℝ
hx : x ∈ Ioi 0
⊢ HasDerivAt (fun x ↦ Real.log x) x⁻¹ x
Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable

Goal state before:
pp: a : ℝ
A : ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun x ↦ Real.log x) x⁻¹ x
⊢ ¬IntegrableOn (fun x ↦ x⁻¹) (Ici a) volume

Tactic:
have B : Tendsto (fun x => ‖Real.log x‖) atTop atTop :=
    tendsto_norm_atTop_atTop.comp Real.tendsto_log_atTop

Goal state after:
a : ℝ
A : ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun x ↦ Real.log x) x⁻¹ x
B : Tendsto (fun x ↦ ‖Real.log x‖) atTop atTop
⊢ ¬IntegrableOn (fun x ↦ x⁻¹) (Ici a) volume
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:
Nat.cast_pow

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε < 0
n : ℕ
h : a * ε⁻¹ * c ^ n < ↑(n - d)!
⊢ ε < a * c ^ n / ↑(n - d)!

Tactic:
rw [mul_right_comm, ← div_eq_mul_inv] at h

Goal state after:
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε < 0
n : ℕ
h : a * c ^ n / ε < ↑(n - d)!
⊢ ε < a * c ^ n / ↑(n - d)!
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * ε⁻¹ * c ^ n < ↑(n - d)!
⊢ a * c ^ n / ↑(n - d)! < ε

Tactic:
rw [mul_right_comm, ← div_eq_mul_inv] at h

Goal state after:
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * c ^ n / ε < ↑(n - d)!
⊢ a * c ^ n / ↑(n - d)! < ε
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable g (map QuotientGroup.mk (μ.restrict 𝓕))
⊢ essSup g (map QuotientGroup.mk (μ.restrict 𝓕)) = essSup (fun x ↦ g ↑x) μ

Tactic:
by
  have hπ : Measurable (QuotientGroup.mk : G → G ⧸ Γ) := continuous_quotient_mk'.measurable
  rw [essSup_map_measure g_ae_measurable hπ.aemeasurable]
  refine h𝓕.essSup_measure_restrict ?_
  intro ⟨γ, hγ⟩ x
  dsimp
  congr 1
  exact QuotientGroup.mk_mul_of_mem x hγ

Goal state after: