mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (X * (descPochhammer ℤ k).comp (X - 1)).smeval (r + 1) =
    (k + 1) • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ (k + 1)).smeval r

Tactic:
rw [descPochhammer_succ_right, mul_comm (descPochhammer ℤ k)]

Goal state after:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (X * (descPochhammer ℤ k).comp (X - 1)).smeval (r + 1) =
    (k + 1) • (descPochhammer ℤ k).smeval r + ((X - ↑k) * descPochhammer ℤ k).smeval r
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k)) =
    n.choose k • ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k))

Tactic:
nsmul_eq_mul

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ ↑(n.choose k) * ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k)) =
    ↑(n.choose k) * ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k))
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : p n = 0
this : iteratedFDerivWithin 𝕜 n f s x = (p.iteratedFDerivSeries n 0) fun x ↦ 0
⊢ (0 fun x ↦ 0) = 0

Tactic:
zero_apply

Goal state after:
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : p n = 0
this : iteratedFDerivWithin 𝕜 n f s x = (p.iteratedFDerivSeries n 0) fun x ↦ 0
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: x p : ℝ
⊢ deriv (fun x ↦ x ^ p) x = p * x ^ (p - 1)

Tactic:
by_cases! h : p = 0
  · simp [h]
  by_cases! h' : x ≠ 0 ∨ 1 ≤ p
  · apply (Real.hasDerivAt_rpow_const h').deriv
  have h'' := deriv_zero_of_not_differentiableAt (not_differentiableAt_rpow_const_zero h'.2 h ·)
  grind [Real.zero_rpow]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Field β
inst✝ : ContinuousMul β
c : β
hc0 : c ≠ 0
h : SuperpolynomialDecay l k fun n ↦ c * f n
x : α
⊢ c⁻¹ * (c * f x) = f x

Tactic:
by simp [← mul_assoc, inv_mul_cancel₀ hc0]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
⊢ v.FineSubfamilyOn f s ↔ ∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x

Tactic:
refine forall₂_congr fun x hx ↦ ?_

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
x : X
hx : x ∈ s
⊢ (∀ ε > 0, ∃ t ∈ v.setsAt x ∩ f x, t ⊆ closedBall x ε) ↔ ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ 0 ≠ ⊤ ∨ expGrowthInf v ≠ ⊥

Tactic:
· exact .inl zero_ne_top

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ 0 ≠ ⊤ ∨ expGrowthSup v ≠ ⊥

Tactic:
· exact .inl zero_ne_top

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
⊢ expGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, expGrowthInf (u x)

Tactic:
have := map_finset_inf expGrowthInfTopHom hs.toFinset u
  simpa only [expGrowthInfTopHom, InfTopHom.coe_mk, InfHom.coe_mk, Finset.inf_eq_iInf,
    hs.mem_toFinset, comp_apply]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: case a
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ (u ⊔ v) n ≤ (u + v) n

Tactic:
exact sup_le (self_le_add_right (u n) (v n)) (self_le_add_left (v n) (u n))

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
⊢ μ.singularPart ν = 0

Tactic:
← MutuallySingular.self_iff

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
⊢ μ.singularPart ν ⟂ₘ μ.singularPart ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Tactic:
← MutuallySingular.self_iff

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν.withDensity (μ.rnDeriv ν)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity f
⊢ s = μ.singularPart ν

Tactic:
by
  have : HaveLebesgueDecomposition μ ν := ⟨⟨⟨s, f⟩, hf, hs, hadd⟩⟩
  obtain ⟨hmeas, hsing, hadd'⟩ := haveLebesgueDecomposition_spec μ ν
  obtain ⟨⟨S, hS₁, hS₂, hS₃⟩, ⟨T, hT₁, hT₂, hT₃⟩⟩ := hs, hsing
  rw [hadd'] at hadd
  have hνinter : ν (S ∩ T)ᶜ = 0 := by
    rw [compl_inter]
    refine nonpos_iff_eq_zero.1 (le_trans (measure_union_le _ _) ?_)
    rw [hT₃, hS₃, add_zero]
  have heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ := by
    ext1 A hA
    have hf : ν.withDensity f (A ∩ (S ∩ T)ᶜ) = 0 := by
      refine withDensity_absolutelyContinuous ν _ ?_
      rw [← nonpos_iff_eq_zero]
      exact hνinter ▸ measure_mono inter_subset_right
    have hrn : ν.withDensity (μ.rnDeriv ν) (A ∩ (S ∩ T)ᶜ) = 0 := by
      refine withDensity_absolutelyContinuous ν _ ?_
      rw [← nonpos_iff_eq_zero]
      exact hνinter ▸ measure_mono inter_subset_right
    rw [restrict_apply hA, restrict_apply hA, ← add_zero (s (A ∩ (S ∩ T)ᶜ)), ← hf, ← add_apply, ←
      hadd, add_apply, hrn, add_zero]
  have heq' : ∀ A : Set α, MeasurableSet A → s A = s.restrict (S ∩ T)ᶜ A := by
    intro A hA
    have hsinter : s (A ∩ (S ∩ T)) = 0 := by
      rw [← nonpos_iff_eq_zero]
      exact hS₂ ▸ measure_mono (inter_subset_right.trans inter_subset_left)
    rw [restrict_apply hA, ← sdiff_eq, AEDisjoint.measure_sdiff_left hsinter]
  ext1 A hA
  have hμinter : μ.singularPart ν (A ∩ (S ∩ T)) = 0 := by
    rw [← nonpos_iff_eq_zero]
    exact hT₂ ▸ measure_mono (inter_subset_right.trans inter_subset_right)
  rw [heq' A hA, heq, restrict_apply hA, ← sdiff_eq, AEDisjoint.measure_sdiff_left hμinter]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA νA : ℝ≥0
hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : 0 < νA
c : ℝ≥0
hc : 0 < c
n : ℕ
hn : 1 / (↑n + 1) < ↑c * (↑νA)⁻¹
hb₁ : 0 < (↑νA)⁻¹
⊢ νA ≠ 0

Tactic:
exact hb.ne'

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA νA : ℝ≥0
hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : 0 < νA
⊢ μA = 0

pp: case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA νA : ℝ≥0
hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : νA ≤ 0
⊢ μA = 0

Tactic:
· suffices ∀ b, 0 < b → μA ≤ b by
        by_contra h
        have h' := this (μA / 2) (half_pos (zero_lt_iff.2 h))
        rw [← @Classical.not_not (μA ≤ μA / 2)] at h'
        exact h' (not_le.2 (NNReal.half_lt_self h))
      intro c hc
      have : ∃ n : ℕ, 1 / (n + 1 : ℝ) < c * (νA : ℝ)⁻¹ := by
        refine exists_nat_one_div_lt ?_
        positivity
      rcases this with ⟨n, hn⟩
      have hb₁ : (0 : ℝ) < (νA : ℝ)⁻¹ := by rw [_root_.inv_pos]; exact hb
      have h' : 1 / (↑n + 1) * νA < c := by
        rw [← NNReal.coe_lt_coe, ← mul_lt_mul_iff_left₀ hb₁, NNReal.coe_mul, mul_assoc, ←
          NNReal.coe_inv, ← NNReal.coe_mul, mul_inv_cancel₀, ← NNReal.coe_mul, mul_one,
          NNReal.coe_inv]
        · exact hn
        · exact hb.ne'
      refine le_trans ?_ h'.le
      rw [← ENNReal.coe_le_coe, ENNReal.coe_mul]
      exact hA₃ n

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA νA : ℝ≥0
hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : νA ≤ 0
⊢ μA = 0
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: case hfh
f : StieltjesFunction ℝ
x : ℝ
hx : Tendsto (fun a ↦ f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y ↦ (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y ↦ (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L3 :
  Tendsto (fun y ↦ (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[<] x)
    (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x, (↑f b - ↑f x) / (b - x) ≤ (leftLim (↑f) b - ↑f x) / (b - x)

Tactic:
· filter_upwards [self_mem_nhdsWithin]
      rintro y (hy : y < x)
      refine div_le_div_of_nonpos_of_le (by linarith) ?_
      simpa only [sub_le_sub_iff_right] using f.mono.leftLim_le (le_refl y)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ μ₁ (A ∩ E)
⊢ False

Tactic:
hμ₁

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ (μ - ν.withDensity ξ) (A ∩ E)
⊢ False
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this✝ : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ (μ - ν.withDensity ξ) (A ∩ E)
hε₂ : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν ≤ μ (A ∩ E)
hξε : (ξ + E.indicator fun x ↦ ↑ε) ∈ measurableLE ν μ
this : ∫⁻ (a : α), ξ a + E.indicator (fun x ↦ ↑ε) a ∂ν ≤ sSup (measurableLEEval ν μ)
⊢ ∫⁻ (a : α), ξ a ∂ν < ∫⁻ (a : α), ξ a ∂ν + ∫⁻ (a : α), E.indicator (fun x ↦ ↑ε) a ∂ν

Tactic:
lintegral_indicator hE₁,

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this✝ : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ (μ - ν.withDensity ξ) (A ∩ E)
hε₂ : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν ≤ μ (A ∩ E)
hξε : (ξ + E.indicator fun x ↦ ↑ε) ∈ measurableLE ν μ
this : ∫⁻ (a : α), ξ a + E.indicator (fun x ↦ ↑ε) a ∂ν ≤ sSup (measurableLEEval ν μ)
⊢ ∫⁻ (a : α), ξ a ∂ν < ∫⁻ (a : α), ξ a ∂ν + ∫⁻ (a : α) in E, ↑ε ∂ν
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ variationOnFromTo f s a b = variationOnFromTo f s a c ↔ variationOnFromTo f s b c = 0

Tactic:
by
  simp only [← variationOnFromTo.add hf ha hb hc, left_eq_add]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
⊢ μ = (μ₁, ξ).1 + ν.withDensity (μ₁, ξ).2

Tactic:
hμ₁

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
⊢ μ = (μ - ν.withDensity ξ, ξ).1 + ν.withDensity (μ - ν.withDensity ξ, ξ).2
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SigmaFinite ν
this : ∀ (μ : Measure α) [SFinite μ], IsFiniteMeasure μ → μ.HaveLebesgueDecomposition ν
hμ : ¬IsFiniteMeasure μ
⊢ μ.HaveLebesgueDecomposition ν

Tactic:
exact .sfinite_of_isFiniteMeasure fun μ _ ↦ this μ ‹_›

Goal state after:
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inl
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

pp: case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : y ≤ x
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

Tactic:
· rw [variationOnFromTo.eq_of_le _ _ h, variationOnFromTo.eq_of_le _ _ (hφ hx hy h),
      eVariationOn.comp_inter_Icc_eq_of_monotoneOn f φ hφ hx hy]

Goal state after:
case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : y ≤ x
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ min a b
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → DifferentiableAt ℝ f x

Tactic:
filter_upwards [h.locallyBoundedVariationOn.ae_differentiableWithinAt_of_mem, h₁, h₂]
    with x hx₁ hx₂ hx₃ hx₄

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ min a b
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ f (uIcc a b) x
hx₂ : x ≠ min a b
hx₃ : x ≠ max a b
hx₄ : x ∈ uIcc a b
⊢ DifferentiableAt ℝ f x
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ min a b
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ f (uIcc a b) x
hx₂ : x ≠ min a b
hx₃ : x ≠ max a b
hx₄ : min a b ≤ x ∧ x ≤ max a b
⊢ DifferentiableAt ℝ f x

Tactic:
exact (hx₁ hx₄).differentiableAt
    (Icc_mem_nhds (lt_of_le_of_ne hx₄.left hx₂.symm) (lt_of_le_of_ne hx₄.right hx₃))

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {∞}) ≤ (t • ν) (s ∩ f ⁻¹' {∞})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ ∫⁻ (x : α) in s ∩ f ⁻¹' I, ↑t ^ (n + 1) ∂μ ≤ ∫⁻ (x : α) in s ∩ f ⁻¹' I, ↑t * f x ∂μ

Tactic:
apply lintegral_mono_ae ((ae_restrict_iff' M).2 (Eventually.of_forall fun x hx => ?_))
        grw [add_comm, ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top, zpow_one, hx.2.1]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))

Tactic:
let t := μ.withDensity (ρ.rnDeriv μ)
  have eq_add : ρ = ρ.singularPart μ + t := haveLebesgueDecomposition_add _ _
  have A : ∀ᵐ x ∂μ, Tendsto (fun a => ρ.singularPart μ a / μ a) (v.filterAt x) (𝓝 0) :=
    v.ae_eventually_measure_zero_of_singular (mutuallySingular_singularPart ρ μ)
  have B : ∀ᵐ x ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x :=
    rnDeriv_withDensity μ (measurable_rnDeriv ρ μ)
  have C : ∀ᵐ x ∂μ, Tendsto (fun a => t a / μ a) (v.filterAt x) (𝓝 (t.rnDeriv μ x)) :=
    v.ae_tendsto_rnDeriv_of_absolutelyContinuous (withDensity_absolutelyContinuous _ _)
  filter_upwards [A, B, C] with _ Ax Bx Cx
  convert! Ax.add Cx using 1
  · ext1 a
    conv_lhs => rw [eq_add]
    simp only [Pi.add_apply, coe_add, ENNReal.add_div]
  · simp only [Bx, zero_add]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
⊢ BoundedVariationOn f ↑∅

pp: case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
⊢ BoundedVariationOn f ↑s

Tactic:
· simp [BoundedVariationOn]

Goal state after:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
⊢ BoundedVariationOn f ↑s