mathlib-initiative/mathlib-tactics huggingface dataset:
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
this :
  Tendsto (fun y ↦ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
y : ℝ
hy : x < y
⊢ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x) ≤ (f y - f x) / (y - x)

Tactic:
← sub_pos

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
this :
  Tendsto (fun y ↦ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
y : ℝ
hy : 0 < y - x
⊢ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x) ≤ (f y - f x) / (y - x)
Module: Mathlib.Analysis.Calculus.Monotone

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

Tactic:
← sub_pos

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
this :
  Tendsto (fun y ↦ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
y : ℝ
hy : 0 < y - x
⊢ (f y - f x) / (y - x) ≤ (↑hf.stieltjesFunction y - f x) / (y - x)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case succ.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
n m : ℕ
v : ℕ → α
v_mono : StrictMonoOn v (Iic m)
v_mem : ∀ i ∈ Iic m, v i ∈ s
hv : ↑⟨m, ⟨v, ⋯⟩⟩.snd ⟨m, ⟨v, ⋯⟩⟩.fst = u n
h'v :
  ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) =
    ∑ i ∈ Finset.range ⟨m, ⟨v, ⋯⟩⟩.fst, edist (f (↑⟨m, ⟨v, ⋯⟩⟩.snd (i + 1))) (f (↑⟨m, ⟨v, ⋯⟩⟩.snd i))
hn : u n < u (n + 1)
⊢ ∃ a a_1,
    a_1 a = u (n + 1) ∧
      (StrictMonoOn a_1 (Iic a) ∧ ∀ i ≤ a, a_1 i ∈ s) ∧
        ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) + edist (f (u (n + 1))) (f (u n)) =
          ∑ x ∈ Finset.range a, edist (f (a_1 (x + 1))) (f (a_1 x))

Tactic:
· refine ⟨m + 1, fun i ↦ if i ≤ m then v i else u (n + 1), by simp,
            by grind [StrictMonoOn], ?_⟩
          simp only [h'v, ← hv, Order.add_one_le_iff, Finset.sum_range_succ, lt_self_iff_false,
            ↓reduceIte, le_refl]
          congr 1
          exact Finset.sum_congr rfl (by grind)

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ρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = ∞}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : ρ o < ∞
s : Set α := {x | v.limRatioMeas hρ x = ∞} ∩ o
ρs : ρ s ≠ ∞
A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s
B : Tendsto (fun q ↦ (↑q)⁻¹ * ρ s) atTop (𝓝 0)
⊢ μ s ≤ 0

Tactic:
apply ge_of_tendsto B

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = ∞}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : ρ o < ∞
s : Set α := ⋯
ρs : ρ s ≠ ∞
A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s
B : Tendsto (fun q ↦ (↑q)⁻¹ * ρ s) atTop (𝓝 0)
⊢ ∀ᶠ (c : ℝ≥0) in atTop, μ s ≤ (↑c)⁻¹ * ρ s
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
f : α → E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
⊢ ContinuousWithinAt (variationOnFromTo f univ a) (Ici x) x

Tactic:
by
  have : variationOnFromTo f univ a =
      fun y ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y := by
    ext y
    rw [variationOnFromTo.add hf.locallyBoundedVariationOn (mem_univ _) (mem_univ _) (mem_univ _)]
  rw [this]
  apply continuousWithinAt_const.add
  suffices H : ContinuousWithinAt (fun y ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (Ici x) x from
    H.congr_of_mem (fun y hy ↦ by grind [variationOnFromTo]) self_mem_Iic
  simp only [ContinuousWithinAt, Icc_self]
  rw [eVariationOn.subsingleton _ (by grind [Set.Subsingleton])]
  apply (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp
  apply Tendsto.mono_left _ (nhdsWithin_mono _ (subset_univ _))
  exact hf.tendsto_eVariationOn_Icc_zero_right _ (by simpa using hx)

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ρ : ρ ≪ μ
x : α
x✝ : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : μ o < ∞
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ∞
A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s
B : Tendsto (fun q ↦ ↑q * μ s) (𝓝[>] 0) (𝓝 0)
⊢ ρ s ≤ 0

Tactic:
apply ge_of_tendsto B

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : μ o < ∞
s : Set α := ⋯
μs : μ s ≠ ∞
A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s
B : Tendsto (fun q ↦ ↑q * μ s) (𝓝[>] 0) (𝓝 0)
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[>] 0, ρ s ≤ ↑c * μ s
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case e_a
α : 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)
hw : Monotone w
Npos : 0 < N
⊢ ∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)) + edist (f (u N)) (f (u (N - 1))) =
    ∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)) + edist (f (w (N + 1))) (f (w (N - 1)))

pp: case e_a
α : 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)
hw : Monotone w
Npos : 0 < N
⊢ ∑ i ∈ Finset.Ico N n, edist (f (w (1 + i + 1))) (f (w (1 + i))) =
    ∑ i ∈ Finset.Ico (N + 1) (n + 1), edist (f (w (i + 1))) (f (w i))

Tactic:
· grind

Goal state after:
case e_a
α : 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)
hw : Monotone w
Npos : 0 < N
⊢ ∑ i ∈ Finset.Ico N n, edist (f (w (1 + i + 1))) (f (w (1 + i))) =
    ∑ i ∈ Finset.Ico (N + 1) (n + 1), edist (f (w (i + 1))) (f (w 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
⊢ ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})

Tactic:
measure_mono inter_subset_right,

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
⊢ ρ (f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case e_a
α : 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))
⊢ ∑ i ∈ Finset.range m, edist (f (v (i + 1))) (f (v i)) =
    ∑ i ∈ Finset.range m,
      edist (f (if n + 1 + i + 1 ≤ n then u (n + 1 + i + 1) else v (n + 1 + i + 1 - (n + 1))))
        (f (if n + 1 + i ≤ n then u (n + 1 + i) else v (n + 1 + i - (n + 1))))

Tactic:
· grind

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 α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this✝¹ : u (n + 1) ≤ a
hn : u (n + 1) = a
this✝ :
  Tendsto (fun y ↦ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (eVariationOn f (s ∩ Iio a) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
⊢ ∑ i ∈ Finset.range (n + 1), edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)

Tactic:
let v i := if i ≤ n then u i else if i = n + 1 then y else a

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this✝¹ : u (n + 1) ≤ a
hn : u (n + 1) = a
this✝ :
  Tendsto (fun y ↦ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (eVariationOn f (s ∩ Iio a) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
v : ℕ → α := fun i ↦ if i ≤ n then u i else if i = n + 1 then y else a
⊢ ∑ i ∈ Finset.range (n + 1), edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case h
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h✝ : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this✝¹ : u (n + 1) ≤ a
hn : u (n + 1) = a
this✝ :
  Tendsto (fun y ↦ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (eVariationOn f (s ∩ Iio a) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
v : ℕ → α := fun i ↦ if i ≤ n then u i else if i = n + 1 then y else a
i : ℕ
h : i ∈ Finset.range n
⊢ edist (f (u (i + 1))) (f (u i)) ≤ edist (f (v (i + 1))) (f (v i))

pp: case h₂
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this✝¹ : u (n + 1) ≤ a
hn : u (n + 1) = a
this✝ :
  Tendsto (fun y ↦ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (eVariationOn f (s ∩ Iio a) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
v : ℕ → α := ⋯
⊢ edist (f (u (n + 1))) (f (u n)) ≤ edist (f (v (n + 1))) (f (v n)) + edist (f (v (n + (1 + 1)))) (f (v (n + 1)))

Tactic:
· grind

Goal state after:
case h₂
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this✝¹ : u (n + 1) ≤ a
hn : u (n + 1) = a
this✝ :
  Tendsto (fun y ↦ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (eVariationOn f (s ∩ Iio a) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
v : ℕ → α := ⋯
⊢ edist (f (u (n + 1))) (f (u n)) ≤ edist (f (v (n + 1))) (f (v n)) + edist (f (v (n + (1 + 1)))) (f (v (n + 1)))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this✝¹ : u (n + 1) ≤ a
hn : u (n + 1) = a
this✝ :
  Tendsto (fun y ↦ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (eVariationOn f (s ∩ Iio a) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
v : ℕ → α := ⋯
A :
  ∑ i ∈ Finset.range (n + 1), edist (f (u (i + 1))) (f (u i)) ≤
    ∑ i ∈ Finset.range (n + 2), edist (f (v (i + 1))) (f (v i))
⊢ edist (f (v (n + 1 + 1))) (f (v (n + 1))) ≤ edist (f a) (f y)

Tactic:
· grind

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 α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
b : α
hb : b ∈ s ∩ Iio a
this✝¹ : Nonempty ((n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iio a })
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iio a
this✝ :
  Tendsto (fun y ↦ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
h'y : y ∈ s ∩ Iio a
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) (f y) ≤ eVariationOn f (s ∩ Iic a)

Tactic:
let v i := if i ≤ n then u i else if i = n + 1 then y else a

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
b : α
hb : b ∈ s ∩ Iio a
this✝¹ : Nonempty ((n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iio a })
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iio a
this✝ :
  Tendsto (fun y ↦ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
h'y : y ∈ s ∩ Iio a
v : ℕ → α := fun i ↦ if i ≤ n then u i else if i = n + 1 then y else a
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) (f y) ≤ eVariationOn f (s ∩ Iic a)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case h
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h✝ : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
b : α
hb : b ∈ s ∩ Iio a
this✝¹ : Nonempty ((n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iio a })
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iio a
this✝ :
  Tendsto (fun y ↦ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
h'y : y ∈ s ∩ Iio a
v : ℕ → α := fun i ↦ if i ≤ n then u i else if i = n + 1 then y else a
i : ℕ
h : i ∈ Finset.range n
⊢ edist (f (u (i + 1))) (f (u i)) ≤ edist (f (v (i + 1))) (f (v i))

pp: case h₂
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
b : α
hb : b ∈ s ∩ Iio a
this✝¹ : Nonempty ((n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iio a })
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iio a
this✝ :
  Tendsto (fun y ↦ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
h'y : y ∈ s ∩ Iio a
v : ℕ → α := ⋯
⊢ edist (f a) (f y) ≤ edist (f (v (n + 1))) (f (v n)) + edist (f (v (n + (1 + 1)))) (f (v (n + 1)))

Tactic:
· grind

Goal state after:
case h₂
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
b : α
hb : b ∈ s ∩ Iio a
this✝¹ : Nonempty ((n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iio a })
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iio a
this✝ :
  Tendsto (fun y ↦ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
h'y : y ∈ s ∩ Iio a
v : ℕ → α := ⋯
⊢ edist (f a) (f y) ≤ edist (f (v (n + 1))) (f (v n)) + edist (f (v (n + (1 + 1)))) (f (v (n + 1)))
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
f : R → R
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ cfc f a = (cfcL ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }

Tactic:
rw [cfc_def, dif_pos ⟨ha, hf⟩, cfcL_apply]

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

Goal state before:
pp: case hn
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ < ε
H : ∃ᶠ (x : α) in L, ε ≤ eVariationOn f (s ∩ Ici x)
y : α → α
y_mem : ∀ y_1 ∈ s, y y_1 ∈ s ∩ Ici y_1
le_y : ∀ y_1 ∈ s, δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : ℕ → α := ⋯
I : ∀ (n : ℕ), v n ∈ s
n : ℕ
⊢ ∀ (i : ℕ), 0 < i → i < n → v i ∈ s

Tactic:
· grind

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
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (fun x ↦ f x + r) a = cfc f a + (algebraMap R A) r

Tactic:
rw [add_comm (cfc f a)]

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (fun x ↦ f x + r) a = (algebraMap R A) r + cfc f a
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁶ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SecondCountableTopology α
inst✝³ : BorelSpace α
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
a : Set α
ha : 0 < μ a
h'a : μ a < ∞
h''a : IntegrableOn f a μ
⊢ ‖⨍ (y : α) in a, f y ∂μ - f x‖ ≤ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ

Tactic:
← setAverage_const ha.ne' h'a.ne (f x)

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 μ
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
a : Set α
ha : 0 < μ a
h'a : μ a < ∞
h''a : IntegrableOn f a μ
⊢ ‖⨍ (y : α) in a, f y ∂μ - ⨍ (x_1 : α) in a, f x ∂μ‖ ≤ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ