mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x
N_0 : N 0 = 0
s : PointedCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (LinearMap.id.toPMap ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ x ∈ s, 0 ≤ g x
g_eq : ∀ (x : ↥f.domain) (y : ℝ), g (↑x, y) = y - ↑f x
x : ↥f.domain
⊢ (-g ∘ₗ inl ℝ E ℝ) ↑x = ↑f x

Tactic:
simp [g_eq x 0]

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

Goal state before:
pp: case e'_4
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
ε : ℝ≥0
εpos : 0 < ↑ε
If : ∫⁻ (x : α), ↑(f x) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ↑ε
Ig : ∫⁻ (x : α), ↑(g x) ∂μ < ∞
⊢ (∫⁻ (a : α), ENNReal.ofReal ↑(g a) ∂μ).toReal + ↑ε = (∫⁻ (x : α), ↑(g x) ∂μ + ↑ε).toReal

pp: case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
ε : ℝ≥0
εpos : 0 < ↑ε
If : ∫⁻ (x : α), ↑(f x) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ↑ε
Ig : ∫⁻ (x : α), ↑(g x) ∂μ < ∞
⊢ ∫⁻ (x : α), ↑(g x) ∂μ + ↑ε ≠ ∞

Tactic:
· rw [ENNReal.toReal_add Ig.ne ENNReal.coe_ne_top]; simp

Goal state after:
case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
ε : ℝ≥0
εpos : 0 < ↑ε
If : ∫⁻ (x : α), ↑(f x) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ↑ε
Ig : ∫⁻ (x : α), ↑(g x) ∂μ < ∞
⊢ ∫⁻ (x : α), ↑(g x) ∂μ + ↑ε ≠ ∞
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝¹⁵ : Field R
inst✝¹⁴ : AddCommGroup V
inst✝¹³ : TopologicalSpace R
inst✝¹² : TopologicalSpace V
inst✝¹¹ : IsTopologicalRing R
inst✝¹⁰ : Module R V
inst✝⁹ : SeparatingDual R V
inst✝⁸ : IsTopologicalAddGroup V
inst✝⁷ : ContinuousSMul R V
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S V
inst✝⁴ : SMulCommClass R S V
inst✝³ : Algebra S R
inst✝² : IsScalarTower S R V
inst✝¹ : ContinuousConstSMul S V
inst✝ : Algebra.IsCentral S R
f : V →L[R] V
hf : f ∈ Subalgebra.center S (V →L[R] V)
a✝ : Nontrivial V
x : V
hx : x ≠ 0
g : StrongDual R V
hg : g x = 1
this : ∀ (y : V), g (f x) • y = f y
⊢ g (f x) ∈ Subalgebra.center S R ∧ f = g (f x) • ContinuousLinearMap.id R V

Tactic:
simp [this, ContinuousLinearMap.ext_iff]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
x : E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
this : ContinuousSMul ℝ E
⊢ ∃ f, ∀ a ∈ s, re (f a) < re (f x)

Tactic:
obtain ⟨f, h⟩ := _root_.geometric_hahn_banach_open_point hs₁ hs₂ disj

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
x : E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
h : ∀ a ∈ s, f a < f x
⊢ ∃ f, ∀ a ∈ s, re (f a) < re (f x)
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun x ↦ (f x).toNNReal
int_fp : Integrable (fun x ↦ ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (fun x ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + ↑δ
fm : α → ℝ≥0 := fun x ↦ (-f x).toNNReal
int_fm : Integrable (fun x ↦ ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x ↦ ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - ↑δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x ↦ ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
x : α
⊢ ↑(f x) < g x

Tactic:
rw [EReal.coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal (f x)]

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun x ↦ (f x).toNNReal
int_fp : Integrable (fun x ↦ ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (fun x ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + ↑δ
fm : α → ℝ≥0 := fun x ↦ (-f x).toNNReal
int_fm : Integrable (fun x ↦ ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x ↦ ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - ↑δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x ↦ ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
x : α
⊢ ↑↑(f x).toNNReal - ↑↑(-f x).toNNReal < g x
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case h_add
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
f g : X → E
a✝ : Disjoint (Function.support f) (Function.support g)
f_int : Integrable f μ
⊢ Integrable g μ →
    ∫ (x : X), L (f x) ∂μ = L (∫ (x : X), f x ∂μ) →
      ∫ (x : X), L (g x) ∂μ = L (∫ (x : X), g x ∂μ) → ∫ (x : X), L ((f + g) x) ∂μ = L (∫ (x : X), (f + g) x ∂μ)

Tactic:
g_int

Goal state after:
case h_add
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
f g : X → E
a✝ : Disjoint (Function.support f) (Function.support g)
f_int : Integrable f μ
g_int : Integrable g μ
⊢ ∫ (x : X), L (f x) ∂μ = L (∫ (x : X), f x ∂μ) →
    ∫ (x : X), L (g x) ∂μ = L (∫ (x : X), g x ∂μ) → ∫ (x : X), L ((f + g) x) ∂μ = L (∫ (x : X), (f + g) x ∂μ)
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
⊢ y - x ≤ (1 / 2) ^ (n e + 1)

Tactic:
linarith [hy.2]

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

Tactic:
simp [hx]

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 ℝ
h : a ≤ b
⊢ ∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ = ∫ (x : ℝ) in a..b, ‖f x‖ ∂μ

Tactic:
uIoc_of_le h,

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : a ≤ b
⊢ ∫ (x : ℝ) in Ioc a b, ‖f x‖ ∂μ = ∫ (x : ℝ) in a..b, ‖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
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ volume (Ι a b) < ∞

Tactic:
· simp [uIoc, Real.volume_Ioc]

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 ∈ 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
⊢ (u - t) * y = ∫ (x : ℝ) in Icc t u, y

Tactic:
by
          simp only [MeasureTheory.integral_const, MeasurableSet.univ, measureReal_restrict_apply,
            univ_inter, hu.left.le, Real.volume_real_Icc_of_le, smul_eq_mul]

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 c : ℝ
f : ℝ → E
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, f (x * c) = c⁻¹ • ∫ (x : ℝ) in a * c..b * c, f x

Tactic:
have A : MeasurableEmbedding fun x => x * c :=
    (Homeomorph.mulRight₀ c hc).isClosedEmbedding.measurableEmbedding

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
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})
⊢ IsOpen[instTopologicalSpaceProd] {p | p.2 ∈ B (f p.1) K r s t}

Tactic:
convert! H

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.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case refine_3
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.1 s - F x₀ s ∂μ) (x₀, b₀)

Tactic:
· suffices Tendsto (fun x : X × ℝ ↦ ∫ s in b₀..x.2, F x.1 s - F x₀ s ∂μ) (𝓝 (x₀, b₀)) (𝓝 0) by
      simpa [ContinuousAt]
    have : ∀ᶠ p : X × ℝ in 𝓝 (x₀, b₀),
        ‖∫ s in b₀..p.2, F p.1 s - F x₀ s ∂μ‖ ≤ |∫ s in b₀..p.2, 2 * bound s ∂μ| := by
      rw [nhds_prod_eq]
      refine (h_bound.prod_mk Ioo_nhds).mono ?_
      rintro ⟨x, t⟩ ⟨hx : ∀ᵐ t ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t, ht : t ∈ Ioo a b⟩
      have H : ∀ᵐ t : ℝ ∂μ.restrict (Ι b₀ t), ‖F x t - F x₀ t‖ ≤ 2 * bound t := by
        apply (ae_restrict_of_ae_restrict_of_subset (hsub hb₀ ht) (hx.and hx₀)).mono
        rintro s ⟨hs₁, hs₂⟩
        calc
          ‖F x s - F x₀ s‖ ≤ ‖F x s‖ + ‖F x₀ s‖ := norm_sub_le _ _
          _ ≤ 2 * bound s := by linarith only [hs₁, hs₂]
      exact intervalIntegral.norm_integral_le_abs_of_norm_le H
        ((bound_integrable.mono_set' <| hsub hb₀ ht).const_mul 2)
    apply squeeze_zero_norm' this
    have : Tendsto (fun t ↦ ∫ s in b₀..t, 2 * bound s ∂μ) (𝓝 b₀) (𝓝 0) := by
      suffices ContinuousAt (fun t ↦ ∫ s in b₀..t, 2 * bound s ∂μ) b₀ by
        simpa [ContinuousAt] using this
      apply ContinuousWithinAt.continuousAt _ Icc_nhds
      apply intervalIntegral.continuousWithinAt_primitive hμb₀
      apply IntervalIntegrable.const_mul
      apply bound_integrable.mono_set'
      rw [min_eq_right hb₀.1.le, max_eq_right hb₀.2.le]
    rw [nhds_prod_eq]
    exact (continuous_abs.tendsto' _ _ abs_zero).comp (this.comp tendsto_snd)

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
inst✝² : CompleteSpace E
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
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k
hfd : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z
hg : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntegrableOn (fun x ↦ C * ‖g x‖) k volume
⊢ False

Tactic:
obtain ⟨c, hc, d, hd, hlt⟩ : ∃ c ∈ s, ∃ d ∈ s, (‖f c‖ + ∫ y in k, C * ‖g y‖) < ‖f d‖ := by
    rcases Filter.nonempty_of_mem hsl with ⟨c, hc⟩
    have : ∀ᶠ x in l, (‖f c‖ + ∫ y in k, C * ‖g y‖) < ‖f x‖ :=
      hf.eventually (eventually_gt_atTop _)
    exact ⟨c, hc, (this.and hsl).exists.imp fun d hd => ⟨hd.2, hd.1⟩⟩

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace E
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
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k
hfd : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z
hg : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntegrableOn (fun x ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in k, C * ‖g y‖ < ‖f d‖
⊢ False
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
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a

Tactic:
refine (SeparatingDual.eq_iff_forall_dual_eq (R := ℝ)).2 fun g => ?_
  rw [← g.intervalIntegral_comp_comm f'int, g.map_sub]
  exact integral_eq_sub_of_hasDeriv_right_of_le_real hab (g.continuous.comp_continuousOn hcont)
    (fun x hx => g.hasFDerivAt.comp_hasDerivWithinAt x (hderiv x hx))
    (g.integrable_comp ((intervalIntegrable_iff_integrableOn_Icc_of_le hab enorm_ne_top).1 f'int))

Goal state after:
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]]
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
hderiv

Goal state after:
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]]
⊢ IntervalIntegrable f' volume a b
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
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
l : Filter ℝ
hl : TendstoIxxClass Icc l l
hl' : l.NeBot
hle : l ≤ 𝓝 c
hmem : [[a, b]] \ {c} ∈ l
⊢ ¬IntervalIntegrable g volume a b

Tactic:
have : l ≤ 𝓝[[[a, b]] \ {c}] c := le_inf hle (le_principal_iff.2 hmem)

Goal state after:
E : Type u_1
F : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
l : Filter ℝ
hl : TendstoIxxClass Icc l l
hl' : l.NeBot
hle : l ≤ 𝓝 c
hmem : [[a, b]] \ {c} ∈ l
this : l ≤ 𝓝[[[a, b]] \ {c}] c
⊢ ¬IntervalIntegrable g volume a b
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 : ℕ
⊢ Tendsto (fun n ↦ a * c ^ n / ↑(n - d)!) atTop (𝓝 0)

Tactic:
tendsto_order

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 : ℕ
⊢ (∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < a * c ^ b / ↑(b - d)!) ∧
    ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, a * c ^ b / ↑(b - d)! < a'
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case hg
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NullSingletonClass μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ IntegrableOn g (Ioo a b) μ

Tactic:
apply hg.1.mono Ioo_subset_Ioc_self le_rfl

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Ring α
inst✝⁵ : LinearOrder α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : IsStrictOrderedRing α
inst✝¹ : OrderClosedTopology α
inst✝ : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto (fun x ↦ ↑⌊x⌋) (𝓝[<] ↑n) (𝓝 (↑n - 1))

Tactic:
exact tendsto_floor_left' n

Goal state after:
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
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝⁵ : ν.IsMulLeftInvariant
inst✝⁴ : Countable ↥Γ
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : μ V ≠ 0
hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)
neTopV : μ V ≠ ∞
U : Set (G ⧸ Γ)
a✝ : MeasurableSet U
meas_π : Measurable QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := ⋯
has_fund : HasFundamentalDomain (↥Γ.op) G ν
i : QuotientMeasureEqMeasurePreimage ν μ'
this✝ : μ'.IsMulLeftInvariant
this : SigmaFinite μ'
⊢ (μ' V / ν (QuotientGroup.mk ⁻¹' V ∩ s)) • μ = μ

Tactic:
suffices (μ' V / ν (QuotientGroup.mk ⁻¹' V ∩ s)) = 1 by rw [this, one_smul]

Goal state after:
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝⁵ : ν.IsMulLeftInvariant
inst✝⁴ : Countable ↥Γ
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : μ V ≠ 0
hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)
neTopV : μ V ≠ ∞
U : Set (G ⧸ Γ)
a✝ : MeasurableSet U
meas_π : Measurable QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)
has_fund : HasFundamentalDomain (↥Γ.op) G ν
i : QuotientMeasureEqMeasurePreimage ν μ'
this✝ : μ'.IsMulLeftInvariant
this : SigmaFinite μ'
⊢ μ' V / ν (QuotientGroup.mk ⁻¹' V ∩ s) = 1
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
a : ℝ
h : Measurable ⇑(measurableEquivIoc T a)
s : Set ↑(Ioc a (a + T))
hs : MeasurableSet s
x : ℝ
⊢ x ∈ Ioc a (a + T) ∧ (equivIoc T a) ↑x ∈ s ↔ ∃ (x_1 : x ∈ Ioc a (a + T)), ⟨x, ⋯⟩ ∈ s

Tactic:
← exists_prop

Goal state after:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h : Measurable ⇑(measurableEquivIoc T a)
s : Set ↑(Ioc a (a + T))
hs : MeasurableSet s
x : ℝ
⊢ (∃ (_ : x ∈ Ioc a (a + T)), (equivIoc T a) ↑x ∈ s) ↔ ∃ (x_1 : x ∈ Ioc a (a + T)), ⟨x, ⋯⟩ ∈ s