mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.Paracompact

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
w✝ : LinearOrder ι
wf : WellFoundedLT ι
ind : α → ι := fun x ↦ ⋯.min {i | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → x ∈ s i → False
D : ℕ → ι → Set α :=
  fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
hD :
  D = fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ x,
        ⋃ (_ : ind x = i), ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔ ∃ x, ind x = i ∧ eball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
n : ℕ
i : ι
x : α
⊢ x ∈ D n i → x ∈ s i

Tactic:
rw [memD]
    rintro ⟨y, rfl, hsub, -, hyx⟩
    refine hsub (hyx.trans_le <| le_mul_of_one_le_left' ?_)
    norm_num1

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t
j : ι
hj : ¬(f j) x = 0
⊢ WellOrderingRel j i ↔ j ∈ {j ∈ t | WellOrderingRel j i}

Tactic:
rw [Finset.mem_filter, Iff.comm, and_iff_right_iff_imp]

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t
j : ι
hj : ¬(f j) x = 0
⊢ WellOrderingRel j i → j ∈ t
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
c : StrongDual ℝ E
⊢ ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (fun x ↦ c (f x)) s μ

Tactic:
intro s hs hμs

Goal state after:
case refine_1
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
c : StrongDual ℝ E
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ IntegrableOn (fun x ↦ c (f x)) s μ
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
c : StrongDual ℝ E
⊢ ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, c (f x) ∂μ = 0

Tactic:
intro s hs hμs

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
c : StrongDual ℝ E
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, c (f x) ∂μ = 0
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, (f - g) x ∂μ = 0

Tactic:
intro s hs hμs

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, (f - g) x ∂μ = 0
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : SigmaFinite μ
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
⊢ ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, (f - g) x ∂μ = 0

Tactic:
intro s hs hμs

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : SigmaFinite μ
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, (f - g) x ∂μ = 0
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
⊢ ∀ (s : Set α), MeasurableSet s → (μ.restrict t) s < ∞ → IntegrableOn f s (μ.restrict t)

Tactic:
intro s hs hμs

Goal state after:
case refine_1
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμs : (μ.restrict t) s < ∞
⊢ IntegrableOn f s (μ.restrict t)
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
⊢ ∀ (s : Set α), MeasurableSet s → (μ.restrict t) s < ∞ → ∫ (x : α) in s, f x ∂μ.restrict t = 0

Tactic:
intro s hs hμs

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμs : (μ.restrict t) s < ∞
⊢ ∫ (x : α) in s, f x ∂μ.restrict t = 0
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hf : AEFinStronglyMeasurable f μ
hg : AEFinStronglyMeasurable g μ
⊢ ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, (f - g) x ∂μ = 0

Tactic:
intro s hs hμs

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hf : AEFinStronglyMeasurable f μ
hg : AEFinStronglyMeasurable g μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, (f - g) x ∂μ = 0
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
⊢ ∀ (s : Set α), MeasurableSet s → ((μ.restrict t).trim hm) s < ∞ → IntegrableOn f s ((μ.restrict t).trim hm)

Tactic:
intro s hs hμs

Goal state after:
case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ((μ.restrict t).trim hm) s < ∞
⊢ IntegrableOn f s ((μ.restrict t).trim hm)
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
⊢ ∀ (s : Set α), MeasurableSet s → ((μ.restrict t).trim hm) s < ∞ → ∫ (x : α) in s, f x ∂(μ.restrict t).trim hm = 0

Tactic:
intro s hs hμs

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ((μ.restrict t).trim hm) s < ∞
⊢ ∫ (x : α) in s, f x ∂(μ.restrict t).trim hm = 0
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case hfh
E : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range E.1, volume (uIoc (E.2 i).1 (E.2 i).2) =
    ∑ i ∈ Finset.range E.1, ENNReal.ofReal (dist (E.2 i).1 (E.2 i).2)

Tactic:
apply Finset.sum_congr rfl

Goal state after:
case hfh
E : ℕ × (ℕ → ℝ × ℝ)
⊢ ∀ x ∈ Finset.range E.1, volume (uIoc (E.2 x).1 (E.2 x).2) = ENNReal.ofReal (dist (E.2 x).1 (E.2 x).2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: case right
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
ebound : ∫⁻ (x : ℝ) in uIcc a b, ‖deriv f x‖ₑ ∂volume ≤ ENNReal.ofReal (f b - f a)
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a

Tactic:
uIcc_of_le hab,

Goal state after:
case right
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
ebound : ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ ∂volume ≤ ENNReal.ofReal (f b - f a)
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: case right
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a

Tactic:
· have ebound := lintegral_enorm_le_liminf_of_tendsto
      ((MeasureTheory.ae_restrict_iff' (by measurability) |>.mpr hGf))
      (fun n ↦ (hG n).aemeasurable.enorm)
    grw [hG'] at ebound
    rw [uIcc_of_le hab,
        ← MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm integrable_f_deriv,
        ENNReal.ofReal_le_ofReal_iff (by linarith),
        integral_Icc_eq_integral_Ioc,
        ← intervalIntegral.integral_of_le hab] at ebound
    convert! ebound using 1
    refine intervalIntegral.integral_congr_uIoo ?_
    rw [uIoo_of_le hab]
    intro x hx
    exact Eq.symm <| abs_eq_self.mpr <| f_deriv_nonneg hx

Goal state after:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case h₂
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n)).PairwiseDisjoint fun i ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2) ≤ D * dist (f (I i).1) (f (I i).2)

Tactic:
rw [mul_comm]

Goal state after:
case h₂
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n)).PairwiseDisjoint fun i ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2) ≤ dist (f (I i).1) (f (I i).2) * D
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
u : Set (ℝ × ℝ)
hu₁ : ∀ x ∈ u, (d < x.1 ∧ x.1 < x.2 ∧ x.2 < b) ∧ dist (slope f x.1 x.2) (f' x.1) < η
hu₂ : u.Countable
hu₃ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
this✝ : Countable ↑u
this : Pairwise (Disjoint on fun z ↦ Icc (↑z).1 (↑z).2)
hu₄ : volume (Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2) = 0
⊢ ⋃ z ∈ u, Icc z.1 z.2 ⊆ Ioo d b

Tactic:
by simp only [iUnion_subset_iff]; grind

Goal state after:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
this :
  ∀ (i : ℕ) {c : ℝ} {c' : E}, HasDerivAt (fun x ↦ (c * (x - x₀) ^ i) • c') ((c * (↑i * (x - x₀) ^ (i - 1) * 1)) • c') x
⊢ ∑ k ∈ Finset.range (n + 1),
      ((↑(k + 1)!)⁻¹ * (↑(k + 1) * (x - x₀) ^ (k + 1 - 1) * 1)) • iteratedDerivWithin (k + 1) f s x₀ =
    ∑ k ∈ Finset.range (n + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k (derivWithin f s) s x₀

Tactic:
apply Finset.sum_congr rfl

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
this :
  ∀ (i : ℕ) {c : ℝ} {c' : E}, HasDerivAt (fun x ↦ (c * (x - x₀) ^ i) • c') ((c * (↑i * (x - x₀) ^ (i - 1) * 1)) • c') x
⊢ ∀ x_1 ∈ Finset.range (n + 1),
    ((↑(x_1 + 1)!)⁻¹ * (↑(x_1 + 1) * (x - x₀) ^ (x_1 + 1 - 1) * 1)) • iteratedDerivWithin (x_1 + 1) f s x₀ =
      ((↑x_1 !)⁻¹ * (x - x₀) ^ x_1) • iteratedDerivWithin x_1 (derivWithin f s) s x₀
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: case h₂
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ‖ρ • (L y - L w)‖ ≤ ρ * (‖L‖ * ‖y - w‖)

Tactic:
norm_smul,

Goal state after:
case h₂
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ‖ρ‖ * ‖L y - L w‖ ≤ ρ * (‖L‖ * ‖y - w‖)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
⊢ (b - a) / (↑n + 1) < δ

Tactic:
convert! mul_lt_mul_of_pos_right hn hab₁ using 1 <;> field

Goal state after:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x₀ : ℝ
n : ℕ
hf : ContDiff ℝ (↑n) f
⊢ (fun x ↦ f x - taylorWithinEval f n univ x₀ x) =o[𝓝 x₀] fun x ↦ (x - x₀) ^ n

Tactic:
by
  simpa using taylor_isLittleO convex_univ (mem_univ x₀) hf.contDiffOn

Goal state after: