mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
z : ℝ
hz'' : z ∈ Ioc a b
⊢ 𝓝[Ioc a b] z = 𝓝[Icc a b] z

Tactic:
refine nhdsWithin_eq_nhdsWithin' (s := Ioi a) (Ioi_mem_nhds hz''.1) ?_

Goal state after:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
z : ℝ
hz'' : z ∈ Ioc a b
⊢ Ioc a b ∩ Ioi a = Icc a b ∩ Ioi a
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
⊢ ∃ i, -a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo (-a) i → deriv f' x = (-deriv f ∘ Neg.neg) x

Tactic:
refine ⟨-b, by linarith, fun x hx => ?_⟩

Goal state after:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
x : ℝ
hx : x ∈ Ioo (-a) (-b)
⊢ deriv f' x = (-deriv f ∘ Neg.neg) x
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : ℕ → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), (eapproxDiff f n) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg : ∀ (n : ℕ), ∫⁻ (x : α), ↑(g n x) ∂μ ≤ ∫⁻ (x : α), ↑((eapproxDiff f n) x) ∂μ + δ n
⊢ LowerSemicontinuous fun x ↦ ∑' (n : ℕ), ↑(g n x)

Tactic:
refine lowerSemicontinuous_tsum fun n => ?_

Goal state after:
case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : ℕ → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), (eapproxDiff f n) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg : ∀ (n : ℕ), ∫⁻ (x : α), ↑(g n x) ∂μ ≤ ∫⁻ (x : α), ↑((eapproxDiff f n) x) ∂μ + δ n
n : ℕ
⊢ LowerSemicontinuous fun x ↦ ↑(g n x)
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case refine_3
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : ℕ → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), (eapproxDiff f n) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg : ∀ (n : ℕ), ∫⁻ (x : α), ↑(g n x) ∂μ ≤ ∫⁻ (x : α), ↑((eapproxDiff f n) x) ∂μ + δ n
⊢ ∫⁻ (x : α), (fun x ↦ ∑' (n : ℕ), ↑(g n x)) x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε

Tactic:
· calc
      ∫⁻ x, ∑' n : ℕ, g n x ∂μ = ∑' n, ∫⁻ x, g n x ∂μ := by
        rw [lintegral_tsum fun n => (gcont n).measurable.coe_nnreal_ennreal.aemeasurable]
      _ ≤ ∑' n, ((∫⁻ x, eapproxDiff f n x ∂μ) + δ n) := ENNReal.tsum_le_tsum hg
      _ = ∑' n, ∫⁻ x, eapproxDiff f n x ∂μ + ∑' n, δ n := ENNReal.tsum_add
      _ ≤ (∫⁻ x : α, f x ∂μ) + ε := by
        refine add_le_add ?_ hδ.le
        rw [← lintegral_tsum]
        · simp_rw [tsum_eapproxDiff f hf, le_refl]
        · intro n; exact (SimpleFunc.measurable _).coe_nnreal_ennreal.aemeasurable

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁ C₂ : ConvexCone R M
h : C₁ ≤ C₂
hgen : C₁.IsGenerating
⊢ C₂.IsGenerating

Tactic:
by
  rw [IsGenerating, ← top_le_iff] at hgen ⊢
  exact hgen.trans (Submodule.span_mono h)

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
x : M
⊢ (∃ c, 0 < c ∧ c • x ∈ s) → ∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x

Tactic:
rintro ⟨c, hc, hcx⟩
    exact ⟨c⁻¹, inv_pos.2 hc, _, hcx, by rw [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]⟩

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: 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
⊢ 0 ∈ {p | N p.1 ≤ p.2}

Tactic:
by simp [N_0]

Goal state after:
Module: Mathlib.Analysis.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : Module 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : Dual ℝ F
fc : F → 𝕜 := fun x ↦ ↑(fr x) - I * ↑(fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(fr (↑c • x)) = ↑c * ↑(fr x)
c : ℝ
x : F
⊢ fc (↑c • x) = ↑c * fc x

Tactic:
simp only [fc, A, smul_comm I, mul_comm I, mul_sub, mul_assoc]

Goal state after:
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
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
this✝ : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : y ∈ ball 0 ((1 / 2) ^ (n e + 1))
y_pos : ¬y = 0
yzero : 0 < ‖y‖
y_lt : ‖y‖ < (1 / 2) ^ (n e + 1)
yone : ‖y‖ ≤ 1
k : ℕ
hk : (1 / 2) ^ (k + 1) < ‖y‖
h'k : ‖y‖ ≤ (1 / 2) ^ k
this : n e + 1 < k + 1
⊢ n e < k

Tactic:
lia

Goal state after:
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
⊢ gauge (ball 0 r) x = ‖x‖ / r

Tactic:
rcases hr.eq_or_lt with rfl | hr
  · simp
  · rw [← smul_unitBall_of_pos hr, gauge_smul_left, Pi.smul_apply, gauge_unit_ball, smul_eq_mul,
    abs_of_nonneg hr.le, div_eq_inv_mul]
    simp_rw [mem_ball_zero_iff, norm_neg]
    exact fun _ => id

Goal state after:
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)
⊢ f ∈ ⊥

Tactic:
suffices ∃ α ∈ Subalgebra.center S R, f = α • .id R V from
      have ⟨_, ⟨y, _⟩, _⟩ := Algebra.IsCentral.center_eq_bot S R ▸ this
      ⟨y, by aesop⟩

Goal state after:
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)
⊢ ∃ α ∈ Subalgebra.center S R, f = α • ContinuousLinearMap.id R V
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : StrongDual ℝ E), ∃ y ∈ s, i x ≤ i y}
h : x ∉ s
⊢ False

Tactic:
obtain ⟨l, s, hlA, hl⟩ := geometric_hahn_banach_closed_point hs₁ hs₂ h

Goal state after:
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s✝ : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
x : E
hx : x ∈ {x | ∀ (i : StrongDual ℝ E), ∃ y ∈ s✝, i x ≤ i y}
h : x ∉ s✝
l : StrongDual ℝ E
s : ℝ
hlA : ∀ a ∈ s✝, l a < s
hl : s < l x
⊢ False
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
this : ContinuousSMul ℝ E
g : StrongDual ℝ E
hg : g x₀ = 1 ∧ ∀ x ∈ s, g x < 1
⊢ re ((StrongDual.extendRCLikeₗ g) x₀) = 1 ∧ ∀ x ∈ s, re ((StrongDual.extendRCLikeₗ g) x) < 1

Tactic:
simpa [g.extendRCLikeₗ_apply]

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

Goal state before:
pp: case pos
α : 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
⊢ HasSum (fun x ↦ ∫ (a : α), F x a ∂μ) (∑' (i : ι), ∫ (a : α), F i a ∂μ)

pp: case pos
α : 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‖ₑ ∂μ ≠ ∞

Tactic:
· exact (hF_sum.of_norm_bounded fun i ↦ norm_integral_le_integral_norm _).hasSum

Goal state after:
case pos
α : 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‖ₑ ∂μ ≠ ∞
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_le : y - x ≤ (1 / 2) ^ (n e + 1)
yone : y - x ≤ 1
k : ℕ
hk : (1 / 2) ^ (k + 1) < y - x
h'k : y - x ≤ (1 / 2) ^ k
this : n e + 1 < k + 1
⊢ n e < k

Tactic:
lia

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} ∩ Ioc (min b₁ b₂) (max 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:
Iic_def,

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 (Iic 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.FundThmCalculus

Goal state before:
pp: case refine_1
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1.1..t.1.2, f x) - ∫ (x : ℝ) in t.2.1..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ ∀ (x : (ℝ × ℝ) × ℝ × ℝ),
    ((∫ (x : ℝ) in x.1.1..x.1.2, f x) - ∫ (x : ℝ) in x.2.1..x.2.2, f x) -
        ((x.1.2 - x.2.2) • cb - (x.1.1 - x.2.1) • ca) =
      ((∫ (x : ℝ) in x.1.1..x.1.2, f x) - ∫ (x : ℝ) in x.2.1..x.2.2, f x) -
        ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (x.1 - x.2)

Tactic:
simp [sub_smul]

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

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

Tactic:
nhds_prod_eq

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

Goal state before:
pp: case refine_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝¹ : FTCFilter a (𝓝[s] a) la
inst✝ : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter f la volume
hmeas_b : StronglyMeasurableAtFilter f lb volume
ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1..t.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca)) =o[𝓝[s ×ˢ t] (a, b)]
    fun t ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ ∀ (x : ℝ × ℝ),
    ((∫ (x : ℝ) in x.1..x.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((x.2 - b) • cb - (x.1 - a) • ca) =
      ((∫ (x : ℝ) in x.1..x.2, f x) - ∫ (x : ℝ) in (a, b).1..(a, b).2, f x) -
        ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (x - (a, b))

Tactic:
simp [sub_smul]

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

Tactic:
simp [hc, integral_comp_mul_left]

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

Tactic:
simp [hc, integral_comp_mul_left]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

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

Tactic:
rw [← dist_eq_norm]
        change dist (f.uncurry (a', z)) (f.uncurry (a, z)) ≤ ε
        apply (hu _ _ _).le
        · exact ha'x'.1
        · simp [dzx]

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

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

Tactic:
nhds_prod_eq

Goal state after:
E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x ↦ F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
⊢ ∀ᶠ (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 ∂μ|