mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: case refine_2
α : 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ᶜ
this : d t ≤ 0
⊢ ↑(μ t).toNNReal ≤ ν t

Tactic:
← to_nnreal_ν,

Goal state after:
case refine_2
α : 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ᶜ
this : d t ≤ 0
⊢ ↑(μ t).toNNReal ≤ ↑(ν t).toNNReal
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : IsFiniteMeasure μ
⊢ μ - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν

Tactic:
← singularPart_add_rnDeriv μ ν

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : IsFiniteMeasure μ
⊢ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : IsFiniteMeasure μ
⊢ μ - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν

Tactic:
by
  nth_rw 1 [← singularPart_add_rnDeriv μ ν]
  exact Measure.add_sub_cancel

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ρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
z : ℝ≥0∞
hz : z > 0
⊢ ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < z

Tactic:
obtain ⟨w, w_pos, w_lt⟩ : ∃ w : ℝ≥0, (0 : ℝ≥0∞) < w ∧ (w : ℝ≥0∞) < z :=
    ENNReal.lt_iff_exists_nnreal_btwn.1 hz

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
⊢ ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < z
Module: Mathlib.MeasureTheory.Covering.OneDim

Goal state before:
pp: x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ Icc x y ⊆ Metric.closedBall x ε

Tactic:
rw [closedBall_eq_Icc]

Goal state after:
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ Icc x y ⊆ Icc (x - ε) (x + ε)
Module: Mathlib.MeasureTheory.Covering.OneDim

Goal state before:
pp: x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Metric.closedBall x ε

Tactic:
rw [closedBall_eq_Icc]

Goal state after:
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Icc (x - ε) (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ρ : ρ ≪ μ
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) ≠ ∞
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
I : ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < ↑p
a : Set α
ha : ρ a / μ a < ↑p
⊢ ρ a ≤ (p • μ) a

Tactic:
coe_nnreal_smul_apply

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 α := {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) ≠ ∞
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
I : ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < ↑p
a : Set α
ha : ρ a / μ a < ↑p
⊢ ρ a ≤ ↑p * μ a
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)
⊢ Tendsto (fun y ↦ (f y - f x) / (y - x)) (𝓝[<] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hx.1 this

Goal state after:
case hgf
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)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x, (↑hf.stieltjesFunction b - f x) / (b - x) ≤ (f b - f x) / (b - x)

case hfh
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)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x, (f b - f x) / (b - x) ≤ (↑hf.stieltjesFunction (b + -1 * (b - x) ^ 2) - f x) / (b - 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ρ : ρ ≪ μ
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))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
I : ∀ᶠ (b : Set α) in v.filterAt x, ↑q < ρ b / μ b
a : Set α
ha : ↑q < ρ a / μ a
⊢ (q • μ) a ≤ ρ a

Tactic:
coe_nnreal_smul_apply

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 α := {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))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
I : ∀ᶠ (b : Set α) in v.filterAt x, ↑q < ρ b / μ b
a : Set α
ha : ↑q < ρ a / μ a
⊢ ↑q * μ a ≤ ρ 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 ρ
hρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}
t : Set α := {x | Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : μ tᶜ = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < ↑p
a : Set α
ha : ρ a / μ a < ↑p
⊢ ρ a ≤ (p • μ) a

Tactic:
coe_nnreal_smul_apply

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}
t : Set α := {x | Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : μ tᶜ = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < ↑p
a : Set α
ha : ρ a / μ a < ↑p
⊢ ρ a ≤ ↑p * μ 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 ρ
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
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (a : Set α) in v.filterAt x, ↑q < ρ a / μ a
a : Set α
ha : ↑q < ρ a / μ a
⊢ (q • μ) a ≤ ρ a

Tactic:
coe_nnreal_smul_apply

Goal state after:
α : 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
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (a : Set α) in v.filterAt x, ↑q < ρ a / μ a
a : Set α
ha : ↑q < ρ a / μ a
⊢ ↑q * μ a ≤ ρ a
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 : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
⊢ variationOnFromTo f s a b ≤ variationOnFromTo f s a b + variationOnFromTo f s b c

Tactic:
exact le_add_of_nonneg_right (variationOnFromTo.nonneg_of_le f s bc)

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 α
n : ℕ
u : ℕ → α
hu : Monotone u
hus : ∀ (i : ℕ), u i ∈ s
⊢ ∀ i ≤ n, u i ∈ s ∩ Icc (u 0) (u n)

Tactic:
by grind [Monotone]

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 α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : u n ≤ x
v : ℕ → α := fun i ↦ if i ≤ n then u i else x
⊢ Monotone v

Tactic:
by grind [Monotone]

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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : ℕ → α := fun i ↦ if i ≤ n then u i else v (i - (n + 1))
⊢ Monotone w

Tactic:
by grind [Monotone]

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 α
inst✝ : Finite ↑s
⊢ BoundedVariationOn f s

Tactic:
simpa using BoundedVariationOn.of_finset f s.toFinite.toFinset

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

Goal state before:
pp: case e'_3.a.inl.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
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
xu : x ≤ u
uy : u ≤ y
⊢ φ u ∈ φ '' (t ∩ Icc x y)

Tactic:
exact ⟨u, ⟨us, ⟨xu, uy⟩⟩, rfl⟩

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
a b : α
h : (𝓝[>] a).NeBot
h' : ContinuousWithinAt f (Ici a) a
hab : a < b
⊢ 𝓝[Iic b ∩ Ioi a] a = 𝓝[>] a

Tactic:
exact nhdsWithin_inter_of_mem (mem_nhdsWithin_of_mem_nhds (Iic_mem_nhds hab))

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
a b : α
h : (𝓝[<] a).NeBot
h' : ContinuousWithinAt f (Iic a) a
⊢ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Ico b a) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Icc b a)

Tactic:
← Ioc_toDual,

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
a b : α
h : (𝓝[<] a).NeBot
h' : ContinuousWithinAt f (Iic a) a
⊢ eVariationOn (f ∘ ⇑ofDual) (Ioc (toDual a) (toDual b)) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Icc b a)
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 (Iic a) a
⊢ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Ico b a) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Icc b a)

Tactic:
← Ioc_toDual,

Goal state after:
α : 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 (Iic a) a
⊢ eVariationOn (f ∘ ⇑ofDual) (Ioc (toDual a) (toDual b)) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Icc b a)
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
S : Type u_3
inst✝⁴ : SMul S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
⊢ cfc (fun x ↦ s • f x) a = s • cfc f a

Tactic:
by
  by_cases ha : p a
  · rw [cfc_apply f a, cfc_apply _ a]
    simp_rw [← Pi.smul_def, ← smul_one_smul R s _]
    rw [← map_smul]
    congr
  · simp [cfc_apply_of_not_predicate a ha]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case succ.right
n k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν ↦ bernsteinPolynomial ℚ n ↑ν
h : k + 1 ≤ n + 1
⊢ bernsteinPolynomial ℚ n ↑(Fin.last k) ∉ span ℚ (Set.range (Fin.init fun ν ↦ bernsteinPolynomial ℚ n ↑ν))

Tactic:
clear ih

Goal state after:
case succ.right
n k : ℕ
h : k + 1 ≤ n + 1
⊢ bernsteinPolynomial ℚ n ↑(Fin.last k) ∉ span ℚ (Set.range (Fin.init fun ν ↦ bernsteinPolynomial ℚ n ↑ν))
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
this : eval 1 ((⇑derivative)^[n - k] p) = 0
⊢ eval 1 ((⇑derivative)^[n - k] p) ≠ eval 1 ((⇑derivative)^[n - k] (bernsteinPolynomial ℚ n k))

Tactic:
by
        rw [this]
        exact (iterate_derivative_at_1_ne_zero ℚ n k h).symm

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

Goal state before:
pp: case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : Subalgebra.comap W (polynomialFunctions I).topologicalClosure = Subalgebra.comap W ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
simp only [Algebra.comap_top] at p

Goal state after:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : Subalgebra.comap W (polynomialFunctions I).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
Module: Mathlib.Topology.ContinuousMap.Weierstrass

Goal state before:
pp: a b : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b)
ε : ℝ
pos : 0 < ε
⊢ ∃ p, ∀ x ∈ Set.Icc a b, |Polynomial.eval x p - f x| < ε

Tactic:
let f' : C(Set.Icc a b, ℝ) := ⟨fun x => f x, continuousOn_iff_continuous_domRestrict.mp c⟩
  obtain ⟨p, b⟩ := exists_polynomial_near_continuousMap a b f' ε pos
  use p
  rw [norm_lt_iff _ pos] at b
  intro x m
  exact b ⟨x, m⟩

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : TopologicalSpace A
inst✝³ : T2Space A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra 𝕜 A
s : Set 𝕜
x✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) = ψ (ContinuousMap.restrict s (ContinuousMap.id 𝕜))
⊢ φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X)

Tactic:
by
      convert! h using 1
      all_goals exact congr_arg _ (by ext; simp)

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

Goal state before:
pp: case star_id
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id s) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id s)) * a = 0
hφ : Continuous ⇑φ
⊢ φ (star (ContinuousMapZero.id s)) * a = 0

Tactic:
exact hmul_star_id

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

Goal state before:
pp: case star_id
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id s) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id s)) = 0
hφ : Continuous ⇑φ
⊢ a * φ (star (ContinuousMapZero.id s)) = 0

Tactic:
exact hmul_star_id

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
u : Set β
⊢ (f ⁻¹' Iic uᶜ)ᶜ = {x | (f x ∩ u).Nonempty}

Tactic:
simp [Set.ext_iff, Iic, Set.mem_compl_iff, Set.not_subset, Set.Nonempty]

Goal state after: