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

Goal state before:
pp: X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : X → E × F
hf : Integrable f μ
⊢ (∫ (x : X), f x ∂μ).2 = ∫ (x : X), (f x).2 ∂μ

Tactic:
by
  rw [← Prod.fst_swap, swap_integral]
  exact fst_integral <| hf.snd.prodMk hf.fst

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_8
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
hc : c = 0
⊢ ∫ (x : X), f x • c ∂μ = (∫ (x : X), f x ∂μ) • c

pp: case neg
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_8
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
hc : ¬c = 0
⊢ ∫ (x : X), f x • c ∂μ = (∫ (x : X), f x ∂μ) • c

Tactic:
· simp [hc, integral_zero, smul_zero]

Goal state after:
case neg
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_8
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
hc : ¬c = 0
⊢ ∫ (x : X), f x • c ∂μ = (∫ (x : X), f x ∂μ) • c
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
⊢ ∫ (a : α), ∑' (i : ι), f i a ∂μ = ∑' (i : ι), ∫ (a : α), f i a ∂μ

Tactic:
by_cases hG : CompleteSpace G

Goal state after:
case pos
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hG : CompleteSpace G
⊢ ∫ (a : α), ∑' (i : ι), f i a ∂μ = ∑' (i : ι), ∫ (a : α), f i a ∂μ

case neg
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hG : ¬CompleteSpace G
⊢ ∫ (a : α), ∑' (i : ι), f i a ∂μ = ∑' (i : ι), ∫ (a : α), f i a ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos.refine_1.hfi
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
c : E
s : Set X
s_meas : MeasurableSet s
hs : (μ.withDensity fun x ↦ ↑(f x)) s < ∞
⊢ HasFiniteIntegral (fun x ↦ ↑(f x)) (μ.restrict s)

Tactic:
simpa [withDensity_apply _ s_meas, hasFiniteIntegral_iff_enorm] using hs

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
i : ι
⊢ ∫⁻ (a : α), ↑‖F i a‖₊ ∂μ = ↑‖∫ (a : α), ‖F i a‖ ∂μ‖₊

Tactic:
lintegral_coe_eq_integral _ (hF_int i).norm,

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
i : ι
⊢ ENNReal.ofReal (∫ (a : α), ↑‖F i a‖₊ ∂μ) = ↑‖∫ (a : α), ‖F i a‖ ∂μ‖₊
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝³ : TopologicalSpace ε
inst✝² : ENormedAddMonoid ε
inst✝¹ : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
g : ℝ → ε
h : EqOn f g (uIoo a b)
⊢ f =ᵐ[μ.restrict (Ι a b)] g

Tactic:
uIoc,

Goal state after:
ε : Type u_3
inst✝³ : TopologicalSpace ε
inst✝² : ENormedAddMonoid ε
inst✝¹ : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
g : ℝ → ε
h : EqOn f g (uIoo a b)
⊢ f =ᵐ[μ.restrict (Ioc (min a b) (max a b))] g
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝³ : TopologicalSpace ε
inst✝² : ENormedAddMonoid ε
inst✝¹ : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntegrableOn f (Ι a b) μ ↔ IntegrableOn f (Icc (min a b) (max a b)) μ

Tactic:
uIoc,

Goal state after:
ε : Type u_3
inst✝³ : TopologicalSpace ε
inst✝² : ENormedAddMonoid ε
inst✝¹ : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntegrableOn f (Ioc (min a b) (max a b)) μ ↔ IntegrableOn f (Icc (min a b) (max a b)) μ
Module: Mathlib.Analysis.Calculus.TangentCone.Prod

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : x ∈ closure[inst✝⁷] s
z : F
hz : z ∈ tangentConeAt 𝕜 t y
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → F
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, y + d n ∈ t
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 z)
⊢ Tendsto (fun n ↦ c n • (0, d n)) l (𝓝 ((LinearMap.inr 𝕜 E F) z))

Tactic:
simpa using tendsto_const_nhds.prodMk_nhds hcd

Goal state after:
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 ({x_1 | x_1 ≤ x} ∩ Ι b₁ b₂))

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₂
⊢ MeasurableSet {x_1 | x_1 ≤ x}

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₂
⊢ MeasurableSet {x_1 | x_1 ≤ x}

Tactic:
uIoc,

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 ({x_1 | x_1 ≤ x} ∩ Ioc (min b₁ b₂) (max b₁ b₂)))

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₂
⊢ MeasurableSet {x_1 | x_1 ≤ x}

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₂
⊢ MeasurableSet {x_1 | x_1 ≤ 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
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ C * |b - a| = C * volume.real (Ι a b)

Tactic:
uIoc,

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ C * |b - a| = C * volume.real (Ioc (min a b) (max 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 : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ
x₀ : ℝ
a✝ : x₀ ∈ Icc a b
⊢ ContinuousWithinAt (fun x ↦ ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b) x₀

Tactic:
refine continuousWithinAt_primitive (measure_singleton x₀) ?_

Goal state after:
case pos
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
this : ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ
x₀ : ℝ
a✝ : x₀ ∈ Icc a b
⊢ IntervalIntegrable f μ (min a a) (max a b)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case hbc
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 ℝ := ⋯
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
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
I3 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I4 : ∀ᶠ (u : ℝ) in 𝓝[>] t, u ∈ Ioc t (min v b)
x : ℝ
hx : g x - g t ≤ ∫ (w : ℝ) in t..x, (G' w).toReal
h'x : x ∈ Ioc t (min v b)
⊢ Ioc t x ⊆ Icc a b

Tactic:
exact Ioc_subset_Icc_self.trans (Icc_subset_Icc ht.2.1 (h'x.2.trans (min_le_right _ _)))

Goal state after:
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 ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
⊢ ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a, f x ∂μ

Tactic:
by
  rw [integral_interval_add_Ioi _ hb]
  by_cases! h : a ≤ b
  · exact (Ioc_union_Ioi_eq_Ioi h) ▸ IntegrableOn.union
      ((intervalIntegrable_iff_integrableOn_Ioc_of_le h).1 ha) hb
  · exact hb.mono_set <| Ioi_subset_Ioi h.le

Goal state after:
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
⊢ deriv f' x = a (deriv f x)

Tactic:
rw [fderiv_comp_deriv x _ 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
⊢ (fderiv ℝ (⇑a) (f x)) (deriv f x) = a (deriv f x)

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)
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 ℝ
h : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ioc a b → f x = g x
h' : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ioc b a → f x = g x
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
by
  simp only [intervalIntegral, setIntegral_congr_ae measurableSet_Ioc h,
    setIntegral_congr_ae measurableSet_Ioc h']

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

Goal state before:
pp: case left
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
⊢ ∀ᶠ (b : ℕ) in atTop, ε < a * c ^ b / ↑(b - d)!

Tactic:
filter_upwards [eventually_mul_pow_lt_factorial_sub (a * ε⁻¹) c d] with n 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: case right
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
⊢ ∀ᶠ (b : ℕ) in atTop, a * c ^ b / ↑(b - d)! < ε

Tactic:
filter_upwards [eventually_mul_pow_lt_factorial_sub (a * ε⁻¹) c d] with n 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: α : Type u_1
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : FloorRing α
inst✝ : IsStrictOrderedRing α
b : ℤ
⊢ ⌈↑(b - 1)⌉ ≤ b

Tactic:
rw [ceil_intCast]; exact (sub_one_lt _).le

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G' : Type u_1
inst✝¹⁰ : AddGroup G'
inst✝⁹ : MeasurableSpace G'
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : IsTopologicalAddGroup G'
inst✝⁶ : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'
inst✝⁵ : Countable ↥Γ'
inst✝⁴ : MeasurableSpace (G' ⧸ Γ')
inst✝³ : BorelSpace (G' ⧸ Γ')
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ'.IsAddRightInvariant
f : G' → K
f_ℒ_1 : Integrable f μ'
g : G' ⧸ Γ' → K
hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ'.restrict 𝓕')) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))
π : G' → G' ⧸ Γ' := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
H₁ : Integrable (g ∘ π * f) μ'
H₂ : AEStronglyMeasurable (automorphize (g ∘ π * f)) (Measure.map mk (μ'.restrict 𝓕'))
⊢ ∫ (x : G'), g (π x) * f x ∂μ' = ∫ (x : G' ⧸ Γ'), automorphize (g ∘ π * f) x ∂Measure.map mk (μ'.restrict 𝓕')

Tactic:
apply QuotientAddGroup.integral_eq_integral_automorphize h𝓕 H₁ H₂

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G' : Type u_1
inst✝¹⁰ : AddGroup G'
inst✝⁹ : MeasurableSpace G'
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : IsTopologicalAddGroup G'
inst✝⁶ : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'
inst✝⁵ : Countable ↥Γ'
inst✝⁴ : MeasurableSpace (G' ⧸ Γ')
inst✝³ : BorelSpace (G' ⧸ Γ')
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ'.IsAddRightInvariant
f : G' → K
f_ℒ_1 : Integrable f μ'
g : G' ⧸ Γ' → K
hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ'.restrict 𝓕')) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))
⊢ ∫ (x : G'), g ↑x * f x ∂μ' = ∫ (x : G' ⧸ Γ'), g x * automorphize f x ∂Measure.map mk (μ'.restrict 𝓕')

Tactic:
by
  let π : G' → G' ⧸ Γ' := QuotientAddGroup.mk
  have meas_π : Measurable π := continuous_quotient_mk'.measurable
  have H₀ : QuotientAddGroup.automorphize ((g ∘ π) * f) = g * (QuotientAddGroup.automorphize f) :=
    QuotientAddGroup.automorphize_smul_left f g
  calc ∫ (x : G'), g (π x) * f x ∂μ' =
    ∫ (x : G' ⧸ Γ'), QuotientAddGroup.automorphize ((g ∘ π) * f) x ∂μ_𝓕 := ?_
    _ = ∫ (x : G' ⧸ Γ'), g x * (QuotientAddGroup.automorphize f x) ∂μ_𝓕 := by simp [H₀]
  have H₁ : Integrable ((g ∘ π) * f) μ' := by
    have : AEStronglyMeasurable (fun (x : G') ↦ g (x : (G' ⧸ Γ'))) μ' :=
      (hg.mono_ac h𝓕.absolutelyContinuous_map).comp_measurable meas_π
    refine Integrable.essSup_smul f_ℒ_1 this ?_
    have hg' : AEStronglyMeasurable (‖g ·‖ₑ) μ_𝓕 := continuous_enorm.comp_aestronglyMeasurable hg
    rw [← essSup_comp_quotientAddGroup_mk h𝓕 hg'.aemeasurable]
    exact g_ℒ_infinity
  have H₂ : AEStronglyMeasurable (QuotientAddGroup.automorphize ((g ∘ π) * f)) μ_𝓕 := by
    simp_rw [H₀]
    exact hg.mul F_ae_measurable
  apply QuotientAddGroup.integral_eq_integral_automorphize h𝓕 H₁ H₂

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst✝¹ : TopologicalSpace X
f : β → X
inst✝ : SFinite ν
hf : AEStronglyMeasurable (fun x ↦ f x.2) (μ.prod ν)
hμ : μ ≠ 0
this : NeZero μ
y : α
hy : AEStronglyMeasurable (fun y_1 ↦ f (y, y_1).2) ν
⊢ AEStronglyMeasurable f ν

Tactic:
exact hy

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ ∫ (θ : ℝ) in 0..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ < ∫ (x : ℝ) in 0..2 * π, R * C

Tactic:
by
      simp only [deriv_circleMap, norm_smul, norm_mul, norm_circleMap_zero, abs_of_pos hR, norm_I,
        mul_one]
      refine intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt
          Real.two_pi_pos ?_ continuousOn_const (fun θ _ => ?_) ⟨θ₀, Ioc_subset_Icc_self hmem, ?_⟩
      · exact continuousOn_const.mul (hc.comp (continuous_circleMap _ _).continuousOn fun θ _ =>
          circleMap_mem_sphere _ hR.le _).norm
      · gcongr
        exact hf _ <| circleMap_mem_sphere _ hR.le _
      · gcongr

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case inl
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.univ.pi fun j ↦ Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
⊢ (∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (a j) x) j =
    0

Tactic:
rcases eq_or_ne i j with (rfl | hne)

Goal state after:
case inl.inl
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.univ.pi fun j ↦ Set.Ioc (a j) (b j)) = ∅
⊢ (∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i =
    0

case inl.inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.univ.pi fun j ↦ Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
hne : i ≠ j
⊢ (∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (a j) x) j =
    0