mathlib-initiative/mathlib-tactics huggingface dataset:
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:
simp only [sub_eq_add_neg]; abel

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

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
⊢ (μ.withDensity g) Set.univ ≠ ∞

Tactic:
← hfg,

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
⊢ (μ.withDensity f) Set.univ ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
⊢ (μ - ν) s = μ s - ν s

Tactic:
by
  -- We begin by defining `measure_sub`, which will be equal to `(μ - ν)`.
  let measure_sub : Measure α := MeasureTheory.Measure.ofMeasurable
    (fun (t : Set α) (_ : MeasurableSet t) => μ t - ν t) (by simp)
    (fun g h_meas h_disj ↦ by
      simp only [measure_iUnion h_disj h_meas]
      rw [ENNReal.tsum_sub _ (h₂ <| g ·)]
      rw [← measure_iUnion h_disj h_meas]
      apply measure_ne_top)
  -- Now, we demonstrate `μ - ν = measure_sub`, and apply it.
  have h_measure_sub_add : ν + measure_sub = μ := by
    ext1 t h_t_measurable_set
    simp only [Pi.add_apply, coe_add]
    rw [MeasureTheory.Measure.ofMeasurable_apply _ h_t_measurable_set, add_comm,
      tsub_add_cancel_of_le (h₂ t)]
  have h_measure_sub_eq : μ - ν = measure_sub := by
    rw [MeasureTheory.Measure.sub_def]
    apply le_antisymm
    · apply sInf_le
      simp [add_comm, h_measure_sub_add]
    apply le_sInf
    intro d h_d
    rw [← h_measure_sub_add, mem_ofPred_eq, add_comm d] at h_d
    apply Measure.le_of_add_le_add_left h_d
  rw [h_measure_sub_eq]
  apply Measure.ofMeasurable_apply _ h₁

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)
le_d_f : ∀ (n m : ℕ), m ≤ n → γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ m, ⋂ n, f m n
γ_le_d_s : γ ≤ d s
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ sᶜ
⊢ γ + d t ≤ d s + d t

Tactic:
by gcongr

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 μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
x✝ : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : μ (closedBall x K) < ∞
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : ∑' (a : ↑v), μ (B ↑a) < ∞
w : Finset ↑v
hw : ∑' (a : { a // a ∉ w }), μ (B ↑↑a) < ε / ↑C
M : (s \ ⋃ a ∈ u, B a) ∩ ball x (R x) ⊆ ⋃ a, closedBall (c ↑↑a) (3 * r ↑↑a)
this : Countable ↑v
⊢ ↑C * ∑' (a : { a // a ∉ w }), μ (B ↑↑a) ≤ ↑C * (ε / ↑C)

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
x : α
⊢ (↑r • r⁻¹ • μ.rnDeriv ν) x = μ.rnDeriv ν x

Tactic:
simp only [Pi.smul_apply]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
x : α
⊢ ↑r • r⁻¹ • μ.rnDeriv ν x = μ.rnDeriv ν x
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)
x : α
ε : ℝ
εpos : ε > 0
r : ℝ
μr : μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
rpos : 0 < r
rε : r ≤ ε
⊢ closedBall x r ⊆ closedBall x ε

Tactic:
by gcongr

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 α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I : ∀ᶠ (i : ι) in l, ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ
this✝ : Tendsto (fun x ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : 0 < ∫ (y : α), g i y ∂μ
mu_ai : μ (a i) < ∞
this : ∀ x ∉ a i, ‖g i x‖ * ‖f x - c‖ = 0
⊢ Integrable (fun x ↦ c) (μ.restrict (a i))

Tactic:
change IntegrableOn (fun _ ↦ c) (a i) μ

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I : ∀ᶠ (i : ι) in l, ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ
this✝ : Tendsto (fun x ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : 0 < ∫ (y : α), g i y ∂μ
mu_ai : μ (a i) < ∞
this : ∀ x ∉ a i, ‖g i x‖ * ‖f x - c‖ = 0
⊢ IntegrableOn (fun x ↦ c) (a i) μ
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
⊢ (ν.withDensity f) A = ((ν.withDensity f).restrict (S ∩ T)) A

Tactic:
have hνfinter : ν.withDensity f (A ∩ (S ∩ T)ᶜ) = 0 := by
      rw [← nonpos_iff_eq_zero]
      exact withDensity_absolutelyContinuous ν f hνinter ▸ measure_mono inter_subset_right

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).restrict (S ∩ T)) A
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 ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ρ o = 0
μo : μ oᶜ = 0
⊢ μ (s ∩ o) + μ oᶜ = μ (s ∩ o)

Tactic:
μo,

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ρ o = 0
μo : μ oᶜ = 0
⊢ μ (s ∩ o) + 0 = μ (s ∩ o)
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)
y : ℝ
hy : y ∈ Ioo (x - 1) x
⊢ y + -1 * (y - x) ^ 2 ∈ Iio x

Tactic:
rw [mem_Ioo] at hy

Goal state after:
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)
y : ℝ
hy : x - 1 < y ∧ y < x
⊢ y + -1 * (y - x) ^ 2 ∈ Iio x
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ρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}
t : Set α := {x | Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : μ tᶜ = 0
H : (q • μ) (s ∩ t) ≤ ρ (s ∩ t)
⊢ ↑q * μ s ≤ ρ s

Tactic:
calc
    (q • μ) s = (q • μ) (s ∩ t ∪ s ∩ tᶜ) := by rw [inter_union_compl]
    _ ≤ (q • μ) (s ∩ t) + (q • μ) (s ∩ tᶜ) := measure_union_le _ _
    _ ≤ ρ (s ∩ t) + (q • μ) tᶜ := by gcongr; apply inter_subset_right
    _ = ρ (s ∩ t) := by simp [A]
    _ ≤ ρ s := by gcongr; apply inter_subset_left

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝¹ : SigmaFinite ν
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (ν (s n) < ∞)
ξ : ℕ → Measure α := fun n ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun n ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
hξ : sum ξ ⟂ₘ ν
⊢ (sum fun n ↦ ξ n + ν.withDensity (f n)) = sum fun n ↦ μ.restrict (s n)

Tactic:
simp_rw [ξ, f, withDensity_indicator (hsm _), singularPart_add_rnDeriv]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ ENNReal.ofReal (dist (f x) (f y)) ≤ eVariationOn f s

Tactic:
← edist_dist

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ edist (f x) (f y) ≤ eVariationOn f s
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
⊢ ∃ v m,
    Monotone v ∧
      (∀ (i : ℕ), v i ∈ s) ∧
        x ∈ v '' Iio m ∧
          ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))

Tactic:
have hN : N ≤ n ∧ x < u N := Nat.find_spec exists_N

Goal state after:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
⊢ ∃ v m,
    Monotone v ∧
      (∀ (i : ℕ), v i ∈ s) ∧
        x ∈ v '' Iio m ∧
          ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
hi : i + 1 = N
⊢ w i ≤ w (i + 1)

Tactic:
have A : i < N := hi ▸ i.lt_succ_self

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
hi : i + 1 = N
A : i < N
⊢ w i ≤ w (i + 1)
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: α : Type u_2
inst✝⁶ : LinearOrder α
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set α
f : α → E
g : α → F
hf : BoundedVariationOn f s
hg : BoundedVariationOn g s
B : E →L[ℝ] F →L[ℝ] G
⊢ BoundedVariationOn (fun x ↦ (B (f x)) (g x)) s

Tactic:
by
  rcases s.eq_empty_or_nonempty with rfl | ⟨⟨x, hx⟩⟩
  · simp
  suffices eVariationOn (fun x ↦ (B (f x)) (g x)) s < ∞ from ne_of_lt this
  have A (y) (hy : y ∈ s) : ‖f y‖ₑ ≤ ‖f x‖ₑ + eVariationOn f s := by
    grw [show f y = f x + (f y - f x) by abel, enorm_add_le, ← edist_eq_enorm_sub,
      eVariationOn.edist_le _ hy hx]
  have A' (y) (hy : y ∈ s) : ‖g y‖ₑ ≤ ‖g x‖ₑ + eVariationOn g s := by
    grw [show g y = g x + (g y - g x) by abel, enorm_add_le, ← edist_eq_enorm_sub,
      eVariationOn.edist_le _ hy hx]
  grw [eVariationOn_bilinear_comp_le A A']
  simp [mul_add, ENNReal.mul_lt_top_iff, hf.lt_top, hg.lt_top]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : PartialOrder R
inst✝⁶ : NonUnitalSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : TopologicalSpace R
inst✝² : ContinuousStar R
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousSqrt R
f g : C(α, R)
⊢ (∃ s, g = f + star s * s) → f ≤ g

Tactic:
· rintro ⟨p, rfl⟩
    exact fun x ↦ le_add_of_nonneg_right (star_mul_self_nonneg (p x))

Goal state after:
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'₀ : 0 ≤ p 0
s₉ : (star s * s) 0 = 0
s₀' : s 0 = 0
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p

Tactic:
let s' : C(α, R)₀ := ⟨s, s₀'⟩

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'₀ : 0 ≤ p 0
s₉ : (star s * s) 0 = 0
s₀' : s 0 = 0
s' : C(α, R)₀ := { toContinuousMap := s, map_zero' := s₀' }
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
u : ℕ → α
hu : Monotone u
n : ℕ
⊢ eVariationOn f (u '' Iic n) = ∑ i ∈ Finset.range n, edist (f (u i)) (f (u (i + 1)))

Tactic:
induction n with
  | zero => simp [Iic]
  | succ n ih =>
    rw [(by grind : u '' Iic (n + 1) = u '' Iic n ∪ {u n, u (n + 1)}), union f]
    · simp [Finset.sum_range_succ, ih]
    · simpa [IsGreatest, upperBounds] using ⟨⟨n, by simp⟩, fun a ha ↦ hu ha⟩
    · simp [IsLeast, hu n.le_succ]

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
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
h : ⇑f = (spectrum R a).domRestrict (Function.extend Subtype.val (⇑f) g)
⊢ (cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) a

Tactic:
have hg : ContinuousOn (Function.extend Subtype.val f g) (spectrum R a) :=
    continuousOn_iff_continuous_domRestrict.mpr <| h ▸ map_continuous f

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
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
h : ⇑f = (spectrum R a).domRestrict (Function.extend Subtype.val (⇑f) g)
hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (spectrum R a)
⊢ (cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) a
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)
⊢ q ((starAlgHom (cfcHom ⋯) ⋯) g) ∧ SpectrumRestricts ((starAlgHom (cfcHom ⋯) ⋯) g) ⇑f

Tactic:
refine ⟨cfcHom_predicate _ _, ?_⟩

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)
⊢ SpectrumRestricts ((starAlgHom (cfcHom ⋯) ⋯) g) ⇑f