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

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

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

Tactic:
NNReal.coe_inv

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

α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA νA : ℝ≥0
hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : 0 < νA
c : ℝ≥0
hc : 0 < c
n : ℕ
hn : 1 / (↑n + 1) < ↑c * (↑νA)⁻¹
hb₁ : 0 < (↑νA)⁻¹
⊢ νA ≠ 0
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ρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a
hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a
x : α
x✝ : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : μ o < ∞
s' : Set α := ⋯
h : ¬μ (s ∩ o) = 0
⊢ μ s' ≠ ∞

Tactic:
exact measure_ne_top_of_subset inter_subset_right μo.ne

Goal state after:
Module: Mathlib.Analysis.Calculus.Monotone

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

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

Tactic:
· filter_upwards [self_mem_nhdsWithin]
      rintro y (hy : y < x)
      refine div_le_div_of_nonpos_of_le (by linarith) ((sub_le_sub_iff_right _).2 ?_)
      apply f.mono.le_leftLim
      have : ↑0 < (x - y) ^ 2 := sq_pos_of_pos (sub_pos.2 hy)
      linarith

Goal state after:
case hfh
f : StieltjesFunction ℝ
x : ℝ
hx : Tendsto (fun a ↦ f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y ↦ (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y ↦ (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L3 :
  Tendsto (fun y ↦ (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[<] x)
    (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x, (↑f b - ↑f x) / (b - x) ≤ (leftLim (↑f) b - ↑f x) / (b - x)
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 ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ (μ - ν.withDensity ξ) (A ∩ E)
hε₂ : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν ≤ μ (A ∩ E)
⊢ (ξ + E.indicator fun x ↦ ↑ε) ∈ measurableLE ν μ

Tactic:
refine ⟨hξm.add (measurable_const.indicator hE₁), fun A hA ↦ ?_⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ (μ - ν.withDensity ξ) (A ∩ E)
hε₂ : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν ≤ μ (A ∩ E)
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (x : α) in A, (ξ + E.indicator fun x ↦ ↑ε) x ∂ν ≤ μ 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {∞}) ≤ (t • ν) (s ∩ f ⁻¹' {∞})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ ρ (s ∩ f ⁻¹' I) ≤ ↑t ^ (n + 1) * μ (s ∩ f ⁻¹' I)

Tactic:
rw [← ENNReal.coe_zpow t_ne_zero']

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

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

Tactic:
have C :
    ∀ n : ℤ,
      ρ (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) ≤
        (t • ν) (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) := by
    intro n
    let I := Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))
    have M : MeasurableSet (s ∩ f ⁻¹' I) := hs.inter (f_meas measurableSet_Ico)
    simp only [ν, I, M, withDensity_apply, coe_nnreal_smul_apply]
    calc
      ρ (s ∩ f ⁻¹' I) ≤ (t : ℝ≥0∞) ^ (n + 1) * μ (s ∩ f ⁻¹' I) := by
        rw [← ENNReal.coe_zpow t_ne_zero']
        apply v.measure_le_mul_of_subset_limRatioMeas_lt hρ
        intro x hx
        apply hx.2.2.trans_le (le_of_eq _)
        rw [ENNReal.coe_zpow t_ne_zero']
      _ = ∫⁻ _ in s ∩ f ⁻¹' I, (t : ℝ≥0∞) ^ (n + 1) ∂μ := by
        simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
      _ ≤ ∫⁻ x in s ∩ f ⁻¹' I, t * f x ∂μ := by
        apply lintegral_mono_ae ((ae_restrict_iff' M).2 (Eventually.of_forall fun x hx => ?_))
        grw [add_comm, ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top, zpow_one, hx.2.1]
      _ = t * ∫⁻ x in s ∩ f ⁻¹' I, f x ∂μ := lintegral_const_mul _ f_meas

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

Goal state before:
pp: case neg.hab
α : Type u_1
inst✝¹ : LinearOrder α
E✝ : Type u_2
inst✝ : PseudoEMetricSpace E✝
f : α → E✝
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ E 0 ≤ E n

Tactic:
apply hE

Goal state after:
case neg.hab
α : Type u_1
inst✝¹ : LinearOrder α
E✝ : Type u_2
inst✝ : PseudoEMetricSpace E✝
f : α → E✝
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ 0 ≤ n
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case neg.hbc
α : Type u_1
inst✝¹ : LinearOrder α
E✝ : Type u_2
inst✝ : PseudoEMetricSpace E✝
f : α → E✝
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ E n ≤ E (n + 1)

Tactic:
apply hE

Goal state after:
case neg.hbc
α : Type u_1
inst✝¹ : LinearOrder α
E✝ : Type u_2
inst✝ : PseudoEMetricSpace E✝
f : α → E✝
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ n ≤ n + 1
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case ha
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i ∈ Finset.range n
⊢ 0 ≤ i

Tactic:
rw [Finset.mem_range] at hi

Goal state after:
case ha
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i < n
⊢ 0 ≤ i
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case hb
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i ∈ Finset.range n
⊢ i + 1 ≤ n

Tactic:
rw [Finset.mem_range] at hi

Goal state after:
case hb
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i < n
⊢ i + 1 ≤ n
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case e_a
α : 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 μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K} :=
  μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x ↦ c) x‖ₑ)
x : α
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
c : E
hc : c ∈ t
n : ℕ
xn : x ∈ A.set n
hx :
  Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)
a : Set α
ha : a ⊆ A.set n
h'a : MeasurableSet a
⊢ ∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ ∂μ = ∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ

Tactic:
apply setLIntegral_congr_fun h'a (fun y hy ↦ ?_)

Goal state after:
α : 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 μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K} :=
  μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x ↦ c) x‖ₑ)
x : α
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
c : E
hc : c ∈ t
n : ℕ
xn : x ∈ A.set n
hx :
  Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)
a : Set α
ha : a ⊆ A.set n
h'a : MeasurableSet a
y : α
hy : y ∈ a
⊢ ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ = ‖f y - c‖ₑ
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
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ spectrum R (cfc f a) = f '' spectrum R a

Tactic:
by
  simp [cfc_apply f a, cfcHom_map_spectrum (p := p)]

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✝ : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ y ∈ s, eVariationOn f (s ∩ Ici y) < ε

Tactic:
have W := hf.tendsto_eVariationOn_Ici_zero_of_filter L hL
    rcases (((tendsto_order.1 W).2 ε εpos).and (hL x₀ hx₀)).exists with ⟨y, hy, h'y⟩
    exact ⟨y, h'y.1, hy⟩

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 α
hf : BoundedVariationOn f s
x : α
A : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
B : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x ∪ s ∩ Ici x] x) (𝓝 0)

Tactic:
rw [nhdsWithin_union, tendsto_sup]

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
A : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
B : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0) ∧
    Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
f : R → R
ha : p a
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
⊢ (cfcₙHom ⋯) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙL ha) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }

Tactic:
cfcₙL_apply

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
f : R → R
ha : p a
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
⊢ (cfcₙHom ⋯) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ha) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }
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✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalSemiring R
inst✝⁹ : ContinuousStar R
inst✝⁸ : ContinuousSqrt R
inst✝⁷ : StarOrderedRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
⊢ IsStrictlyPositive a ↔ ∀ x ∈ spectrum R a, 0 < x

Tactic:
by
  have := cfc_isStrictlyPositive_iff (id : R → R) a (by fun_prop) ha
  simpa [cfc_id _ a ha] using this

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
C : ℝ
hf : MonotoneOn f s
h : ∀ x ∈ s, |f x| ≤ C
⊢ eVariationOn f s ≤ ENNReal.ofReal (2 * C)

Tactic:
rw [eVariationOn.eq_biSup_inter_Icc]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
C : ℝ
hf : MonotoneOn f s
h : ∀ x ∈ s, |f x| ≤ C
⊢ ⨆ p ∈ {p | p.1 ∈ s ∧ p.2 ∈ s ∧ p.1 ≤ p.2}, eVariationOn f (s ∩ Set.Icc p.1 p.2) ≤ ENNReal.ofReal (2 * C)
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * ↑(ν + 1) = ↑(n + 1) * ↑(n.choose ν)

Tactic:
exact mod_cast congr_arg (fun m : ℕ => (m : R[X])) (Nat.add_one_mul_choose_eq n ν).symm

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module R A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
inst✝⁵ : UniqueHom R A
S : Type u_3
inst✝⁴ : SMulZeroClass 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 ((fun x ↦ s • x) '' σₙ R a)
hf0 : f 0 = 0
ha : p a
⊢ cfcₙ (fun x ↦ f (s • x)) a = cfcₙ f (s • a)

Tactic:
cfcₙ_comp' f (s • ·) a,

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module R A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
inst✝⁵ : UniqueHom R A
S : Type u_3
inst✝⁴ : SMulZeroClass 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 ((fun x ↦ s • x) '' σₙ R a)
hf0 : f 0 = 0
ha : p a
⊢ cfcₙ f (cfcₙ (fun x ↦ s • x) a) = cfcₙ f (s • a)
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
⊢ ↑(toContinuousMapOnAlgHom s) p ∈ R[(toContinuousMapOnAlgHom s) X]

Tactic:
rw [AlgHom.coe_toRingHom]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
⊢ (toContinuousMapOnAlgHom s) p ∈ R[(toContinuousMapOnAlgHom s) X]