mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case refine_2
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
this : ∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ gauge s x
⊢ ∃ f, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1

Tactic:
obtain ⟨φ, hφ₁, hφ₂⟩ := this
    have hφ₃ : φ x₀ = 1 := by
      rw [← f.domain.coe_mk x₀ (Submodule.mem_span_singleton_self _), hφ₁,
        LinearPMap.mkSpanSingleton'_apply_self]
    have hφ₄ : ∀ x ∈ s, φ x < 1 := fun x hx =>
      (hφ₂ x).trans_lt (gauge_lt_one_of_mem_of_isOpen hs₂ hx)
    refine ⟨⟨φ, ?_⟩, hφ₃, hφ₄⟩
    refine
      φ.continuous_of_nonzero_on_open _ (hs₂.vadd (-x₀)) (Nonempty.vadd_set ⟨0, hs₀⟩)
        (vadd_set_subset_iff.mpr fun x hx => ?_)
    change φ (-x₀ + x) ≠ 0
    rw [map_add, map_neg]
    specialize hφ₄ x hx
    linarith

Goal state after:
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 : α), (↑(gp x)).toReal ∂μ - ∫ (x : α), ↑(gm x) ∂μ < ∫ (x : α), ↑(fp x) ∂μ + ↑δ - ∫ (x : α), ↑(gm x) ∂μ

Tactic:
apply sub_lt_sub_right

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := ⋯
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 := ⋯
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 := ⋯
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
⊢ ∫ (x : α), (↑(gp x)).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + ↑δ
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
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ ∃ l c, ⋂ n, {x | re ((l n) x) ≤ c n} = s

Tactic:
set ι := Σ (l : StrongDual 𝕜 E), { c : ℝ // ∀ y ∈ s, re (l y) ≤ c }
  set l : ι → StrongDual 𝕜 E := fun lc ↦ lc.1
  set c : ι → ℝ := fun lc ↦ lc.2.val
  set hc : ∀ i, ∀ y ∈ s, re (l i y) ≤ c i := fun lc ↦ lc.2.prop
  have : Nonempty ι := ⟨0, 0, fun _ _ ↦ by simp⟩
  have : ⋂ i : ι, { x | re (l i x) ≤ c i } = s := by
    simpa only [ι, iInter_sigma, iInter_subtype, l, c] using iInter_halfSpaces_eq' hs₁ hs₂
  obtain ⟨k, hk⟩ := eq_closed_inter_nat (fun i : ι ↦ { x | re (l i x) ≤ c i })
    (fun i ↦ isClosed_le (continuous_re.comp (l i).continuous) continuous_const)
  exact ⟨l ∘ k, c ∘ k, hk.trans this⟩

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

Goal state before:
pp: case h_ind
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 φ μ
⊢ ∀ (c : E) ⦃s : Set X⦄,
    MeasurableSet s →
      μ s < ∞ → ∫ (x : X), L (s.indicator (fun x ↦ c) x) ∂μ = L (∫ (x : X), s.indicator (fun x ↦ c) x ∂μ)

Tactic:
intro e s s_meas _

Goal state after:
case h_ind
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 φ μ
e : E
s : Set X
s_meas : MeasurableSet s
a✝ : μ s < ∞
⊢ ∫ (x : X), L (s.indicator (fun x ↦ e) x) ∂μ = L (∫ (x : X), s.indicator (fun x ↦ e) x ∂μ)
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
⊢ ∑' (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ ≠ ∞

Tactic:
have (i : ι) : ∫⁻ a, ‖F i a‖ₑ ∂μ = ‖∫ a, ‖F i a‖ ∂μ‖ₑ := by
    dsimp [enorm]
    rw [lintegral_coe_eq_integral _ (hF_int i).norm, coe_nnreal_eq, coe_nnnorm,
      Real.norm_of_nonneg (integral_nonneg (fun a ↦ norm_nonneg (F i a)))]
    simp only [coe_nnnorm]

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
this : ∀ (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ = ‖∫ (a : α), ‖F i a‖ ∂μ‖ₑ
⊢ ∑' (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ ≠ ∞
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a ↦ ‖f a‖
h_int_eq : (fun i ↦ ∫ (a : α) in s i, f a ∂μ) = fun i ↦ ∫ (a : α), (s i).indicator f a ∂μ
⊢ Tendsto (fun i ↦ ∫ (a : α), (s i).indicator f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ n, s n, f a ∂μ))

Tactic:
← integral_indicator (MeasurableSet.iInter hsm)

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a ↦ ‖f a‖
h_int_eq : (fun i ↦ ∫ (a : α) in s i, f a ∂μ) = fun i ↦ ∫ (a : α), (s i).indicator f a ∂μ
⊢ Tendsto (fun i ↦ ∫ (a : α), (s i).indicator f a ∂μ) atTop (𝓝 (∫ (x : α), (⋂ b, s b).indicator f x ∂μ))
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: ι : 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)‖
⊢ HasSum (fun i ↦ ∫ (x : ℝ) in a..b, (f i) x) (∫ (x : ℝ) in a..b, ∑' (i : ι), (f i) x)

Tactic:
by_cases hE : CompleteSpace E; swap
  · simp [intervalIntegral, integral, hE, hasSum_zero]
  apply hasSum_integral_of_dominated_convergence
    (fun i (x : ℝ) => ‖(f i).restrict ↑(⟨uIcc a b, isCompact_uIcc⟩ : Compacts ℝ)‖)
    (fun i => (map_continuous <| f i).aestronglyMeasurable)
  · intro i; filter_upwards with x hx
    apply ContinuousMap.norm_coe_le_norm ((f i).restrict _) ⟨x, _⟩
    exact ⟨hx.1.le, hx.2⟩
  · exact ae_of_all _ fun x _ => hf_sum
  · exact intervalIntegrable_const
  · refine ae_of_all _ fun x hx => Summable.hasSum ?_
    let x : (⟨uIcc a b, isCompact_uIcc⟩ : Compacts ℝ) := ⟨x, ⟨hx.1.le, hx.2⟩⟩
    have := hf_sum.of_norm
    simpa only [Compacts.coe_mk, ContinuousMap.restrict_apply]
      using ContinuousMap.summable_apply this x

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
inst✝³ : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
f : ℝ → 𝕜
g : ℝ → E
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
hg : IntervalIntegrable g μ a b
hf : ContinuousOn f [[a, b]]
⊢ IntervalIntegrable (fun x ↦ f x • g x) μ a b

Tactic:
rw [intervalIntegrable_iff] at hg ⊢

Goal state after:
𝕜 : Type u_2
E : Type u_5
inst✝³ : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
f : ℝ → 𝕜
g : ℝ → E
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
hg : IntegrableOn g (Ι a b) μ
hf : ContinuousOn f [[a, b]]
⊢ IntegrableOn (fun x ↦ f x • g x) (Ι a b) μ
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 : ¬IntegrableOn f (Ι a b) μ
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ = 0

Tactic:
integral_undef h,

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : ¬IntegrableOn f (Ι a b) μ
⊢ (if a ≤ b then 1 else -1) • 0 = 0
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:
rw [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.MeasureTheory.Integral.IntervalIntegral.Basic

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

Tactic:
suffices Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c by rw [this]
    rw [Ioc_union_Ioc_union_Ioc_cycle, union_right_comm, Ioc_union_Ioc_union_Ioc_cycle,
      min_left_comm, max_left_comm]

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✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, dist (f p x) (f q x) < δ
⊢ ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε

Tactic:
have : v ×ˢ (Ioo (b₀ - δ) (b₀ + δ)) ∈ 𝓝 (q, b₀) := by
    rw [nhdsWithin_univ] at v_mem
    simp only [prod_mem_nhds_iff, v_mem, true_and]
    apply Ioo_mem_nhds <;> linarith

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, dist (f p x) (f q x) < δ
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
⊢ ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
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
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y

Tactic:
by
  -- This follows from the version on a closed-open interval (applied to `[t, b)` for `t` close to
  -- `a`) and a continuity argument.
  obtain rfl | a_lt_b := hab.eq_or_lt
  · simp
  set s := {t | g b - g t ≤ ∫ u in t..b, φ u} ∩ Icc a b
  have s_closed : IsClosed s := by
    have : ContinuousOn (fun t => (g b - g t, ∫ u in t..b, φ u)) (Icc a b) := by
      rw [← uIcc_of_le hab] at hcont φint ⊢
      exact (continuousOn_const.sub hcont).prodMk (continuousOn_primitive_interval_left φint)
    simp only [s, inter_comm]
    exact this.preimage_isClosed_of_isClosed isClosed_Icc isClosed_le_prod
  have A : closure (Ioc a b) ⊆ s := by
    apply s_closed.closure_subset_iff.2
    intro t ht
    refine ⟨?_, ⟨ht.1.le, ht.2⟩⟩
    exact
      sub_le_integral_of_hasDeriv_right_of_le_Ico ht.2 (hcont.mono (Icc_subset_Icc ht.1.le le_rfl))
        (fun x hx => hderiv x ⟨ht.1.trans_le hx.1, hx.2⟩)
        (φint.mono_set (Icc_subset_Icc ht.1.le le_rfl)) fun x hx => hφg x ⟨ht.1.trans_le hx.1, hx.2⟩
  rw [closure_Ioc a_lt_b.ne] at A
  exact (A (left_mem_Icc.2 hab)).1

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, φ x ≤ g' x
⊢ ∫ (y : ℝ) in a..b, φ y ≤ g b - g a

Tactic:
rw [← neg_le_neg_iff]

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, φ x ≤ g' x
⊢ -(g b - g a) ≤ -∫ (y : ℝ) in a..b, φ y
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 : ℝ) ∂volume.restrict (Ioc a b), 0 x ≤ f x

Tactic:
refine ae_restrict_of_ae_eq_of_ae_restrict Ioo_ae_eq_Ioc ?_

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 : ℝ) ∂volume.restrict (Ioo a b), 0 x ≤ f x
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 α
x : α
⊢ ↑(⌈x⌉ - 1) < x

Tactic:
rw [cast_sub, cast_one, sub_lt_iff_lt_add]; exact ceil_lt_add_one _

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

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_1 : NormedSpace ℝ E],
    Periodic f T → ∀ (t s : ℝ), 0 < T → ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x
hT✝ : ¬0 < T
hT : T < 0
⊢ ∫ (x : ℝ) in t + T..t, f x = ∫ (x : ℝ) in s + T..s, f x

Tactic:
simpa only [← sub_eq_add_neg, add_sub_cancel_right] using
        this hf.neg (t + T) (s + T) (neg_pos.mpr hT)

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

Goal state before:
pp: case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Ici a) a

Tactic:
· simpa [ha] using (hf.mono_set (Ioi_subset_Ioi ha)).continuousWithinAt_Ici_primitive_Ioi

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

Goal state before:
pp: case mp
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' ↦ circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, f θ' ∈ ball 0 1 \ {0}
⊢ (fun x ↦ (circleMap c R x - circleMap c R θ)⁻¹) =O[𝓝 θ ⊓ 𝓟 {θ}ᶜ] fun θ_1 ↦
    (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n

Tactic:
refine IsBigO.of_bound |R|⁻¹ (this.mono fun θ' hθ' => ?_)

Goal state after:
case mp
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' ↦ circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤ |R|⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
⊢ sInf ((fun t ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0..T, g x ≤ ∫ (x : ℝ) in 0..t, g x

Tactic:
by
  let h'_int := hg.intervalIntegrable₀ hT.ne' h_int
  let ε := Int.fract (t / T) * T
  conv_rhs =>
    rw [← Int.fract_div_mul_self_add_zsmul_eq T t hT.ne',
      ← integral_add_adjacent_intervals (h'_int 0 ε) (h'_int _ _)]
  rw [hg.intervalIntegral_add_zsmul_eq ⌊t / T⌋ ε (hg.intervalIntegrable₀ hT.ne' h_int),
    hg.intervalIntegral_add_eq ε 0, zero_add, add_le_add_iff_right]
  exact (continuous_primitive h'_int 0).continuousOn.sInf_image_Icc_le <|
    mem_Icc_of_Ico (Int.fract_div_mul_self_mem_Ico T t hT)

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

Goal state before:
pp: case h_lim
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ₀ : 0 < δ
hRδ : R * δ < ε
i : ι
hi : ∀ x ∈ sphere c R, dist (g x) (f i x) < δ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ R * dist (g (circleMap c R x)) (f i (circleMap c R x)) < ε

Tactic:
grw [← hRδ, hi (circleMap c R x) (by simp [hR])]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
⊢ HasFiniteIntegral f (μ.prod ν) ↔
    (∀ᵐ (x : α) ∂μ, HasFiniteIntegral (fun y ↦ f (x, y)) ν) ∧ HasFiniteIntegral (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ

Tactic:
by
  simp only [hasFiniteIntegral_iff_enorm, lintegral_prod _ h1f.enorm.aemeasurable]
  have (x : _) : ∀ᵐ y ∂ν, 0 ≤ ‖f (x, y)‖ := by filter_upwards with y using norm_nonneg _
  simp_rw [integral_eq_lintegral_of_nonneg_ae (this _)
      (h1f.norm.comp_measurable measurable_prodMk_left).aestronglyMeasurable,
    enorm_eq_ofReal toReal_nonneg, ofReal_norm]
  -- this fact is probably too specialized to be its own lemma
  have : ∀ {p q r : Prop} (_ : r → p), (r ↔ p ∧ q) ↔ p → (r ↔ q) := fun {p q r} h1 => by
    rw [← and_congr_right_iff, and_iff_right_of_imp h1]
  rw [this]
  · intro h2f; rw [lintegral_congr_ae]
    filter_upwards [h2f] with x hx
    rw [ofReal_toReal]; rw [← lt_top_iff_ne_top]; exact hx
  · intro h2f; refine ae_lt_top ?_ h2f.ne; exact h1f.enorm.lintegral_prod_right'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ Integrable f (μ.prod ν) ↔
    (∀ᵐ (x : α) ∂μ, Integrable (fun y ↦ f (x, y)) ν) ∧ Integrable (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ

Tactic:
simp [Integrable, h1f, hasFiniteIntegral_prod_iff', h1f.norm.integral_prod_right',
    h1f.prodMk_left]

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

Goal state before:
pp: case pos
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| ∧ n < -1
⊢ ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0

pp: case neg
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
⊢ ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0

Tactic:
· rcases H with ⟨hw, hn⟩
    exact integral_sub_zpow_of_undef (hn.trans (by decide)) hw

Goal state after:
case neg
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
⊢ ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ sphere c r
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))

Tactic:
specialize hzne z hz

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hzne : z ≠ c
hz : z ∈ sphere c r
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))