mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case neg
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun n ↦ ↑(v n)
a_top' : a' ≠ ⊤
⊢ ∃ᶠ (n : ℕ) in atTop, a * b * ↑n ≤ (u ∘ v) n

Tactic:
have a_0' := a_0.trans a_a'

Goal state after:
case neg
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun n ↦ ↑(v n)
a_top' : a' ≠ ⊤
a_0' : 0 < a'
⊢ ∃ᶠ (n : ℕ) in atTop, a * b * ↑n ≤ (u ∘ v) n
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case neg.refine_1
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * ↑n ≤ ↑(v n)
b_u : ∃ᶠ (x : ℕ) in atTop, (b * ↑x ≤ u x ∧ 0 < x) ∧ ∃ m, a'⁻¹ * ↑x ≤ ↑m ∧ ↑m ≤ a⁻¹ * ↑x
M M' : ℕ
aM_M' : a' * ↑M ≤ ↑M'
n : ℕ
n_M' : M' ≤ n
bn_un : b * ↑n ≤ u n
right✝ : 0 < n
k : ℕ
an_k' : a'⁻¹ * ↑n ≤ ↑k
k_an : ↑k ≤ a⁻¹ * ↑n
⊢ M ≤ k

Tactic:
rw [mul_comm a', ← le_div_iff_mul_le a_0' a_top', EReal.div_eq_inv_mul] at aM_M'

Goal state after:
case neg.refine_1
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * ↑n ≤ ↑(v n)
b_u : ∃ᶠ (x : ℕ) in atTop, (b * ↑x ≤ u x ∧ 0 < x) ∧ ∃ m, a'⁻¹ * ↑x ≤ ↑m ∧ ↑m ≤ a⁻¹ * ↑x
M M' : ℕ
aM_M' : ↑M ≤ a'⁻¹ * ↑M'
n : ℕ
n_M' : M' ≤ n
bn_un : b * ↑n ≤ u n
right✝ : 0 < n
k : ℕ
an_k' : a'⁻¹ * ↑n ≤ ↑k
k_an : ↑k ≤ a⁻¹ * ↑n
⊢ M ≤ k
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ (∀ᵐ (x : α) ∂μ, c ≤ f x) ↔ ∀ b < c, μ {x | f x ≤ b} = 0

Tactic:
by
  simp_rw [eventually_const_le_iff_forall_lt_eventually_const_lt, ae_iff, not_lt]

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

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure (μ.restrict s)
hμ0 : ¬μ s = 0
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ

Tactic:
apply le_of_le_of_eq (laverage_mono_ae <| Eventually.filter_mono ae_restrict_le ae_le_essSup)

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure (μ.restrict s)
hμ0 : ¬μ s = 0
⊢ ⨍⁻ (a : α) in s, essSup f μ ∂μ = essSup f μ
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᵐ[μ.restrict (s ∪ t)] g
⊢ ∀ᵐ (x : α) ∂μ.restrict (s ∪ t)ᶜ, f x = g x

Tactic:
simp only [Set.compl_union]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᵐ[μ.restrict (s ∪ t)] g
⊢ ∀ᵐ (x : α) ∂μ.restrict (sᶜ ∩ tᶜ), f x = g x
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ μ - 0 = μ

Tactic:
rw [sub_def]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ sInf {d | μ ≤ d + 0} = μ
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ (μ - ν).restrict s = μ.restrict s - ν.restrict s

Tactic:
rw [sub_def]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ (sInf {d | μ ≤ d + ν}).restrict s = μ.restrict s - ν.restrict s
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ (sInf {d | μ ≤ d + ν}).restrict s = μ.restrict s - ν.restrict s

Tactic:
rw [sub_def]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ (sInf {d | μ ≤ d + ν}).restrict s = sInf {d | μ.restrict s ≤ d + ν.restrict s}
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ (sInf {d | μ ≤ d + ν}).restrict s = sInf {d | μ.restrict s ≤ d + ν.restrict s}

Tactic:
rw [sub_def]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ (sInf {d | μ ≤ d + ν}).restrict s = sInf {d | μ.restrict s ≤ d + ν.restrict s}
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ (if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ⋯).1 else 0) ≤ μ

Tactic:
dif_neg hl

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ 0 ≤ μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
heq' : ∀ (A : Set α), MeasurableSet A → s A = (s.restrict (S ∩ T)ᶜ) A
A : Set α
hA : MeasurableSet A
⊢ (μ.singularPart ν) (A ∩ (S ∩ T)) ≤ 0

Tactic:
exact hT₂ ▸ measure_mono (inter_subset_right.trans inter_subset_right)

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

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ Measurable (s.indicator (μ.rnDeriv ν))

Tactic:
exact (μ.measurable_rnDeriv ν).indicator hs

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ≥0
h : ∀ (x : α), ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
⊢ ∀ (s : Set α) (f : α → Set (Set α)),
    (∀ x ∈ s,
        f x ⊆
          {a |
            IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
              (interior a).Nonempty ∧ ∃ r, a ⊆ closedBall x r ∧ μ (closedBall x (3 * r)) ≤ ↑C * μ a}) →
      (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε) →
        ∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p ↦ p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0

Tactic:
intro s

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ≥0
h : ∀ (x : α), ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
s : Set α
⊢ ∀ (f : α → Set (Set α)),
    (∀ x ∈ s,
        f x ⊆
          {a |
            IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
              (interior a).Nonempty ∧ ∃ r, a ⊆ closedBall x r ∧ μ (closedBall x (3 * r)) ≤ ↑C * μ a}) →
      (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε) →
        ∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p ↦ p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
A : Set α
hA : MeasurableSet A
hs : s (A ∩ (S ∩ T)) = 0
⊢ (μ.singularPart ν) (A ∩ (S ∩ T)) ≤ 0

Tactic:
exact hT₂ ▸ measure_mono (inter_subset_right.trans inter_subset_right)

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ≥0
h : ∀ (x : α), ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧ ∃ r, a ⊆ closedBall x r ∧ μ (closedBall x (3 * r)) ≤ ↑C * μ a}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      μ (closedBall p.2.1 (3 * p.1)) ≤ ↑C * μ p.2.2 ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
x : α
xs : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x

Tactic:
rcases ffine x xs ε εpos with ⟨a, ha, h'a⟩

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ≥0
h : ∀ (x : α), ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧ ∃ r, a ⊆ closedBall x r ∧ μ (closedBall x (3 * r)) ≤ ↑C * μ a}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      μ (closedBall p.2.1 (3 * p.1)) ≤ ↑C * μ p.2.2 ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
x : α
xs : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
ha : a ∈ f x
h'a : a ⊆ closedBall x ε
⊢ ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
L1 : Tendsto (fun y ↦ (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
this :
  Tendsto (fun y ↦ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[<] x)
    (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
y : ℝ
hy : y - x < 0
⊢ f y - f x ≤ ↑hf.stieltjesFunction y - f x

Tactic:
exact (sub_le_sub_iff_right _).2 (hf.le_rightLim (le_refl _))

Goal state after:
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
b : α
bs : b ∈ s
a : α
as : a ∈ s
c : α
cs : c ∈ s
ac : a ≤ c
⊢ variationOnFromTo f s c b ≤ variationOnFromTo f s a b

Tactic:
rw [← variationOnFromTo.add hf as cs bs]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
b : α
bs : b ∈ s
a : α
as : a ∈ s
c : α
cs : c ∈ s
ac : a ≤ c
⊢ variationOnFromTo f s c b ≤ variationOnFromTo f s a c + variationOnFromTo f s c b
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ρ : ρ ≪ μ
x : α
x✝ : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : μ o < ∞
s : Set α := ⋯
μs : μ s ≠ ∞
A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s
⊢ Tendsto ENNReal.ofNNReal (𝓝[>] 0) (𝓝 ↑0)

Tactic:
rw [ENNReal.tendsto_coe]

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : μ o < ∞
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ∞
A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s
⊢ Tendsto (fun a ↦ a) (𝓝[>] 0) (𝓝 0)
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 μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))

Tactic:
have A : (∫⁻ y, hf.mk f y ∂μ) ≠ ∞ := by
    convert! h'f using 1
    apply lintegral_congr_ae
    exact hf.ae_eq_mk.symm

Goal state after:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
I : Integrable (AEStronglyMeasurable.mk f ⋯) μ
x : α
hx :
  Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ) / μ a)
    (v.filterAt x) (𝓝 0)
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
a : Set α
y : α
hy : f y = AEStronglyMeasurable.mk f ⋯ y
⊢ ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ = ‖f y - f x‖ₑ

Tactic:
rw [hy, h'x]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
E : Type u_2
inst✝³ : PseudoEMetricSpace E
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : α → E
a b : α
h' : ContinuousWithinAt f (Ici a) a
⊢ eVariationOn f (Ioc a b) = eVariationOn f (Icc a b)

Tactic:
by
  rcases le_or_gt b a with hab | hab
  · simp [hab]
  have : (𝓝[Ioi a] a).NeBot := nhdsGT_neBot_of_exists_gt ⟨b, hab⟩
  exact eVariationOn_Ioc_eq_Icc_of_continuousWithinAt' h'

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ < ε
H : ∃ᶠ (x : α) in L, ε ≤ eVariationOn f (s ∩ Ici x)
y : α
hy : y ∈ s
⊢ ∃ y' ∈ s ∩ Ici y, δ ≤ eVariationOn f (s ∩ Icc y y')

Tactic:
obtain ⟨y', hy', y'_mem⟩ : ∃ y', ε ≤ eVariationOn f (s ∩ Ici y') ∧ y' ∈ s ∩ Ici y :=
      (H.and_eventually (hL y hy)).exists

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ < ε
H : ∃ᶠ (x : α) in L, ε ≤ eVariationOn f (s ∩ Ici x)
y : α
hy : y ∈ s
y' : α
hy' : ε ≤ eVariationOn f (s ∩ Ici y')
y'_mem : y' ∈ s ∩ Ici y
⊢ ∃ y' ∈ s ∩ Ici y, δ ≤ eVariationOn f (s ∩ Icc y y')
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
⊢ cfc 0 a = 0

Tactic:
by_cases ha : p a
  · exact cfc_apply (0 : R → R) a ▸ map_zero (cfcHom ha)
  · rw [cfc_apply_of_not_predicate a ha]

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
H : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))
y : α
hy : y ∈ s ∩ Iio x
⊢ eVariationOn f (s ∩ Ico y x) + edist (f x) l = eVariationOn f (s ∩ Icc y x)

Tactic:
have N : 𝓝[s ∩ Ici y ∩ Iio x] x = 𝓝[s ∩ Iio x] x := by
      rw [show s ∩ Ici y ∩ Iio x = s ∩ Iio x ∩ Ici y by grind, nhdsWithin_inter_of_mem']
      exact mem_nhdsWithin_of_mem_nhds (Ici_mem_nhds hy.2)

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
H : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))
y : α
hy : y ∈ s ∩ Iio x
N : 𝓝[s ∩ Ici y ∩ Iio x] x = 𝓝[s ∩ Iio x] x
⊢ eVariationOn f (s ∩ Ico y x) + edist (f x) l = eVariationOn f (s ∩ Icc y x)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
⊢ spectrum R ((algebraMap R A) r) ⊆ {r}

Tactic:
rw [← cfc_const r 0 (cfc_predicate_zero R),
    cfc_map_spectrum (fun _ ↦ r) 0 (cfc_predicate_zero R)]

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
⊢ (fun x ↦ r) '' spectrum R 0 ⊆ {r}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁵ : Semifield R
inst✝²⁴ : StarRing R
inst✝²³ : MetricSpace R
inst✝²² : IsTopologicalSemiring R
inst✝²¹ : ContinuousStar R
inst✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : TopologicalSpace A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus S A q
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts a ⇑f
g : R → R
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
⊢ cfcₙ g a = cfcₙ (fun x ↦ (algebraMap R S) (g (f x))) a

Tactic:
rw [cfcₙ_apply g a, cfcₙHom_eq_restrict f hpa hqa h, nonUnitalStarAlgHom_apply,
      cfcₙHom_eq_cfcₙ_extend 0]

Goal state after:
case pos
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁵ : Semifield R
inst✝²⁴ : StarRing R
inst✝²³ : MetricSpace R
inst✝²² : IsTopologicalSemiring R
inst✝²¹ : ContinuousStar R
inst✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : TopologicalSpace A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus S A q
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts a ⇑f
g : R → R
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
⊢ cfcₙ
      (Function.extend Subtype.val
        (⇑({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
            ({ toFun := (σₙ R a).domRestrict g, continuous_toFun := ⋯, map_zero' := ⋯ }.comp
              { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })))
        0)
      a =
    cfcₙ (fun x ↦ (algebraMap R S) (g (f x))) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ cfcₙ (fun x ↦ -x) a = -a

Tactic:
by
  rw [cfcₙ_neg .., cfcₙ_id' R a]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ ↑f ⊔ ↑g ∈ A

Tactic:
by
  convert! sup_mem_subalgebra_closure A f g
  apply SetLike.ext'
  simp

Goal state after: