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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
hg : SuperpolynomialDecay l k g
z : ℕ
⊢ Tendsto (fun a ↦ k a ^ z * (f * g) a) l (𝓝 0)

Tactic:
by
  simpa only [mul_assoc, one_mul, mul_zero, pow_zero] using! (hf z).mul (hg 0)

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ (u a).log / ↑a) ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * ↑n).exp ≤ u n

Tactic:
refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Goal state after:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : 1 ≤ n
⊢ b ≤ (u n).log / ↑n ↔ (b * ↑n).exp ≤ u n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: ⊢ expGrowthInf 0 = ⊥

Tactic:
apply le_bot_iff.1

Goal state after:
⊢ expGrowthInf 0 ≤ ⊥
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthSup (u * v) ≤ expGrowthSup u + expGrowthSup v

Tactic:
refine (limsup_add_le h h').trans_eq' (limsup_congr (Eventually.of_forall fun n ↦ ?_))
  rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
by
  by_cases hμ : IsFiniteMeasure μ; swap
  · rw [not_isFiniteMeasure_iff] at hμ
    simp [laverage_eq, hμ]
  by_cases hν : IsFiniteMeasure ν; swap
  · rw [not_isFiniteMeasure_iff] at hν
    simp [laverage_eq, hν]
  simp only [← ENNReal.mul_div_right_comm, measure_mul_laverage, ← ENNReal.add_div,
    ← lintegral_add_measure, ← Measure.add_apply, ← laverage_eq]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
d_Inter :
  ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
n : ℕ
this : γ - (1 / 2) ^ n < γ
s : Set α
hs : s ∈ {s | MeasurableSet s}
hlt : γ - (1 / 2) ^ n < d s
⊢ ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s

Tactic:
exact ⟨s, hs, hlt⟩

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s : Set α
⊢ ⨍ (x : α) in s, f x ∂μ = (μ.real s)⁻¹ • ∫ (x : α) in s, f x ∂μ

Tactic:
rw [average_eq, measureReal_restrict_apply_univ]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
this✝ : Fact (μ s < ∞)
this : Fact (μ t < ∞)
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    (μ.real s / (μ.real s + μ.real t)) • ⨍ (x : α) in s, f x ∂μ +
      (μ.real t / (μ.real s + μ.real t)) • ⨍ (x : α) in t, f x ∂μ

Tactic:
rw [restrict_union₀ hd ht, average_add_measure hfs hft, measureReal_restrict_apply_univ,
    measureReal_restrict_apply_univ]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
d_Inter :
  ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c
f_succ : ∀ (n m : ℕ), n ≤ m → f n (m + 1) = f n m ∩ e (m + 1)
n✝ m : ℕ
h : m ≤ n✝
n : ℕ
hmn : m ≤ n
ih : γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
⊢ γ + (γ - 2 * (1 / 2) ^ m + ((1 / 2) ^ n - (1 / 2) ^ (n + 1))) =
    γ - (1 / 2) ^ (n + 1) + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n)

Tactic:
by
          simp only [sub_eq_add_neg]; abel

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x ↦ μ t - ν t) ⋯ ⋯
t : Set α
h_t_measurable_set : MeasurableSet t
⊢ (ν + measure_sub) t = μ t

Tactic:
simp only [Pi.add_apply, coe_add]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x ↦ μ t - ν t) ⋯ ⋯
t : Set α
h_t_measurable_set : MeasurableSet t
⊢ ν t + measure_sub t = μ t
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ μ t ≤ (ν' + ν + ⊤.restrict sᶜ) t

Tactic:
repeat rw [← measure_inter_add_sdiff t h_meas_s]

Goal state after:
case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ μ (t ∩ s) + μ (t \ s) ≤ (ν' + ν + ⊤.restrict sᶜ) (t ∩ s) + (ν' + ν + ⊤.restrict sᶜ) (t \ s)
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)ᶜ
A : Set α
hA : MeasurableSet A
hsinter : s (A ∩ (S ∩ T)) = 0
⊢ s A = (s.restrict (S ∩ T)ᶜ) A

Tactic:
rw [restrict_apply hA, ← sdiff_eq, AEDisjoint.measure_sdiff_left hsinter]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst✝¹ : μ₁.HaveLebesgueDecomposition ν
inst✝ : μ₂.HaveLebesgueDecomposition ν
⊢ (μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν

Tactic:
refine (eq_singularPart ((measurable_rnDeriv μ₁ ν).add (measurable_rnDeriv μ₂ ν))
    ((mutuallySingular_singularPart _ _).add_left (mutuallySingular_singularPart _ _)) ?_).symm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst✝¹ : μ₁.HaveLebesgueDecomposition ν
inst✝ : μ₂.HaveLebesgueDecomposition ν
⊢ μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + ν.withDensity (μ₁.rnDeriv ν + μ₂.rnDeriv ν)
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
hsing : (μ.singularPart ν) (A ∩ (S ∩ T)) = 0
⊢ (ν.withDensity f) (A ∩ (S ∩ T)) = (ν.withDensity (μ.rnDeriv ν)) (A ∩ (S ∩ T))

Tactic:
← add_zero (ν.withDensity f (A ∩ (S ∩ T))),

Goal state after:
α : 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
hsing : (μ.singularPart ν) (A ∩ (S ∩ T)) = 0
⊢ (ν.withDensity f) (A ∩ (S ∩ T)) + 0 = (ν.withDensity (μ.rnDeriv ν)) (A ∩ (S ∩ T))
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 : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)
A : Set α
hA : MeasurableSet A
hνfinter : (ν.withDensity f) (A ∩ (S ∩ T)ᶜ) = 0
⊢ (ν.withDensity f) A = (ν.withDensity f) (A ∩ (S ∩ T))

Tactic:
← add_zero (ν.withDensity f (A ∩ (S ∩ T))),

Goal state after:
α : 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 : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)
A : Set α
hA : MeasurableSet A
hνfinter : (ν.withDensity f) (A ∩ (S ∩ T)ᶜ) = 0
⊢ (ν.withDensity f) A = (ν.withDensity f) (A ∩ (S ∩ T)) + 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 μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
⊢ ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a

Tactic:
intro ε εpos

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
ε : ℝ≥0
εpos : ε > 0
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
Module: Mathlib.MeasureTheory.Covering.OneDim

Goal state before:
pp: case refine_2
x : ℝ
⊢ ∀ ε > 0, ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ⊆ Metric.closedBall x ε

Tactic:
intro ε εpos

Goal state after:
case refine_2
x ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ⊆ Metric.closedBall x ε
Module: Mathlib.MeasureTheory.Covering.OneDim

Goal state before:
pp: case refine_2
x : ℝ
⊢ ∀ ε > 0, ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ⊆ Metric.closedBall x ε

Tactic:
intro ε εpos

Goal state after:
case refine_2
x ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ⊆ Metric.closedBall x ε
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ∫⁻ (x : α) in A ∩ {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in A ∩ {x | g x < f x}, f x ∂μ ≤ ν A

Tactic:
refine (add_le_add (hg.2 _ h₁) (hf.2 _ h₂)).trans_eq ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ν (A ∩ {a | f a ≤ g a}) + ν (A ∩ {a | g a < f a}) = ν A
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case succ
α : Type u_1
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x ↦ ⨆ k, ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this : (fun a ↦ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a) = fun a ↦ max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (a : α) in A, max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a) ∂μ ≤ ν A

Tactic:
exact (sup_mem_measurableLE (hf m.succ) hm).2 A hA

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

Goal state before:
pp: α : 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 ∂ν
x✝ : α
⊢ ξ x✝ = ⨆ i, ⨆ k, ⨆ (_ : k ≤ i), f k x✝

Tactic:
simp [hξ]

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

Goal state before:
pp: case hinf
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n ↦ s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n ↦ s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n
m n : ℕ
I : (ρ + μ) (u m) ≠ ∞
J : (ρ + μ) (w n) ≠ ∞
A :
  ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ (ρ + μ) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ∞

Tactic:
apply (lt_of_le_of_lt (measure_mono inter_subset_left) _).ne

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := ⋯
o : ℕ → Set α := ⋯
u : ℕ → Set α := ⋯
w : ℕ → Set α := ⋯
m n : ℕ
I : (ρ + μ) (u m) ≠ ∞
J : (ρ + μ) (w n) ≠ ∞
A :
  ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ (ρ + μ) (toMeasurable (ρ + μ) (u m)) < ∞
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_3
inst✝¹ : PseudoMetricSpace E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
hb : (𝓝[>] b).NeBot
⊢ Function.rightLim (variationOnFromTo f univ a) b = variationOnFromTo f univ a b + dist (f b) (Function.rightLim f b)

Tactic:
apply rightLim_eq_of_tendsto

Goal state after:
case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_3
inst✝¹ : PseudoMetricSpace E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
this✝ : TopologicalSpace α := ⋯
this : OrderTopology α
hb : (𝓝[>] b).NeBot
⊢ Tendsto (variationOnFromTo f univ a) (𝓝[>] b) (𝓝 (variationOnFromTo f univ a b + dist (f b) (Function.rightLim f b)))
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr.refine_4
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ (fun x ↦ (variationOnFromTo f s c x + f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x + f x) / 2) x +
      ((fun x ↦ (variationOnFromTo f s c x - f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x - f x) / 2) x) =
    variationOnFromTo f s x y

Tactic:
rw [← variationOnFromTo.add h hx cs hy, variationOnFromTo.eq_neg_swap]

Goal state after:
case inr.refine_4
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ (fun x ↦ (variationOnFromTo f s c x + f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x + f x) / 2) x +
      ((fun x ↦ (variationOnFromTo f s c x - f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x - f x) / 2) x) =
    -variationOnFromTo f s c x + variationOnFromTo f s c y
Module: Mathlib.Topology.ContinuousMap.StarOrdered

Goal state before:
pp: case mp.add_left
α : Type u_1
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : Zero α
R : Type u_2
inst✝⁸ : TopologicalSpace R
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : NoZeroDivisors R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : IsTopologicalSemiring R
inst✝¹ : ContinuousStar R
inst✝ : StarOrderedRing C(α, R)
p✝ p : C(α, R)
p_mem : p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hp' : ∀ (f g : C(α, R)₀), ↑g = ↑f + p → ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p
f g : C(α, R)₀
s : C(α, R)
hp : ↑g = ↑f + (star s * s + p)
h₀ : (star s * s + p) 0 = 0
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p

Tactic:
rw [← add_assoc] at hp

Goal state after:
case mp.add_left
α : Type u_1
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : Zero α
R : Type u_2
inst✝⁸ : TopologicalSpace R
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : NoZeroDivisors R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : IsTopologicalSemiring R
inst✝¹ : ContinuousStar R
inst✝ : StarOrderedRing C(α, R)
p✝ p : C(α, R)
p_mem : p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hp' : ∀ (f g : C(α, R)₀), ↑g = ↑f + p → ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p
f g : C(α, R)₀
s : C(α, R)
hp : ↑g = ↑f + star s * s + p
h₀ : (star s * s + p) 0 = 0
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict

Goal state before:
pp: 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✝¹⁴ : Semifield S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalSemiring S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : Algebra S A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : IsScalarTower R S A
inst✝³ : StarModule R S
inst✝² : ContinuousSMul R S
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousFunctionalCalculus S A q
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(spectrum R a), R)
⊢ p ((starAlgHom (cfcHom ⋯) ⋯) g)

Tactic:
rw [h]

Goal state after:
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✝¹⁴ : Semifield S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalSemiring S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : Algebra S A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : IsScalarTower R S A
inst✝³ : StarModule R S
inst✝² : ContinuousSMul R S
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousFunctionalCalculus S A q
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(spectrum R a), R)
⊢ q ((starAlgHom (cfcHom ⋯) ⋯) g) ∧ SpectrumRestricts ((starAlgHom (cfcHom ⋯) ⋯) g) ⇑f
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict

Goal state before:
pp: case hφ₂
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✝¹⁶ : Semifield S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalSemiring S
inst✝¹² : ContinuousStar S
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus S A q
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
⊢ (starAlgHom (cfcHom hqa) h) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a

Tactic:
· exact h.starAlgHom_id (cfcHom_id hqa)

Goal state after:
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
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
x : ↑(spectrum R a)
⊢ (spectrum R a).domRestrict f x ∈
    spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })

Tactic:
by rw [sp_eq]; use x.1; simp

Goal state after: