mathlib-initiative/mathlib-tactics huggingface dataset:
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) μ
⊢ 0 < ∫ (y : α), g i y ∂μ → ‖∫ (y : α), g i y • (f y - c) ∂μ‖ ≤ K * ⨍ (y : α) in a i, ‖f y - c‖ ∂μ

Tactic:
hi_int

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 ∂μ
⊢ ‖∫ (y : α), g i y • (f y - c) ∂μ‖ ≤ K * ⨍ (y : α) in a i, ‖f y - c‖ ∂μ
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:

Tactic:
ρ s' ≤ c * μ s' := v.measure_le_of_frequently_le (c • μ) hρ s' fun x hx => hc x hx.1
    _ < d * μ s' := by gcongr; exact measure_ne_top_of_subset inter_subset_right μo.ne
    _ ≤ ρ s' := v.measure_le_of_frequently_le ρ smul_absolutelyContinuous s' fun x hx ↦ hd x hx.1

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

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

Tactic:
rw [this]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
⊢ (fun x ↦ ⨆ k, ⨆ (_ : k ≤ n), f k x) ∈ measurableLE μ ν

Tactic:
induction n with
  | zero =>
    constructor
    · simp [(hf 0).1]
    · intro A hA; simp [(hf 0).2 A hA]
  | succ m hm =>
    have :
      (fun a : α ↦ ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a) = fun a ↦
        f m.succ a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a :=
      funext fun _ ↦ iSup_succ_eq_sup _ _ _
    refine ⟨.iSup fun n ↦ Measurable.iSup_Prop _ (hf n).1, fun A hA ↦ ?_⟩
    rw [this]; exact (sup_mem_measurableLE (hf m.succ) hm).2 A hA

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
x y z : α
xy : x ≤ y
yz : y ≤ z
xs : x ∈ s
ys : y ∈ s
zs : z ∈ s
⊢ variationOnFromTo f s x z = (eVariationOn f (s ∩ Icc x y)).toReal + variationOnFromTo f s y z

Tactic:
variationOnFromTo.eq_of_le f s yz,

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
x y z : α
xy : x ≤ y
yz : y ≤ z
xs : x ∈ s
ys : y ∈ s
zs : z ∈ s
⊢ variationOnFromTo f s x z = (eVariationOn f (s ∩ Icc x y)).toReal + (eVariationOn f (s ∩ Icc y z)).toReal
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 ≠ ∞
⊢ ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s

Tactic:
intro q

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 α := {x | v.limRatioMeas hρ x = ∞} ∩ o
ρs : ρ s ≠ ∞
q : ℝ≥0
⊢ 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Iio b] b) (𝓝 l)
H :
  Tendsto (fun x ↦ variationOnFromTo f s a b - variationOnFromTo f s x b) (𝓝[s ∩ Iio b] b)
    (𝓝 (variationOnFromTo f s a b - dist (f b) l))
⊢ Tendsto (variationOnFromTo f s a) (𝓝[s ∩ Iio b] b) (𝓝 (variationOnFromTo f s a b - dist (f b) l))

Tactic:
apply Tendsto.congr' _ H
    filter_upwards [self_mem_nhdsWithin] with x hx
    rw [variationOnFromTo.sub_left hf ha hb hx.1]

Goal state after:
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
this : variationOnFromTo f univ a = fun y ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
⊢ ContinuousWithinAt (variationOnFromTo f univ a) (Ici x) x

Tactic:
rw [this]

Goal state after:
α : 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
this : variationOnFromTo f univ a = fun y ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
⊢ ContinuousWithinAt (fun y ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y) (Ici 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ρ : ρ ≪ μ
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 ≠ ∞
⊢ ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s

Tactic:
intro q

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 α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ∞
q : ℝ≥0
⊢ 0 < q → ρ s ≤ ↑q * μ s
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
C D : ℝ≥0∞
hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C
hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D
B : E →L[ℝ] F →L[ℝ] G
n : ℕ
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ ∑ i ∈ Finset.range n, edist ((B (f (u (i + 1)))) (g (u (i + 1)))) ((B (f (u i))) (g (u (i + 1)))) +
      ∑ i ∈ Finset.range n, edist ((B (f (u i))) (g (u (i + 1)))) ((B (f (u i))) (g (u i))) =
    ∑ i ∈ Finset.range n, ‖(B (f (u (i + 1)) - f (u i))) (g (u (i + 1)))‖ₑ +
      ∑ i ∈ Finset.range n, ‖(B (f (u i))) (g (u (i + 1)) - g (u i))‖ₑ

Tactic:
simp [edist_eq_enorm_sub]

Goal state after:
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: α : Type u_2
inst✝⁷ : LinearOrder α
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
𝕜 : Type u_6
f : α → 𝕜
g : α → F
inst✝⁴ : NormedRing 𝕜
inst✝³ : NormedAlgebra ℝ 𝕜
inst✝² : Module 𝕜 F
inst✝¹ : NormSMulClass 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
C D : ℝ≥0∞
s : Set α
hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C
hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D
⊢ ‖ContinuousLinearMap.lsmul ℝ 𝕜‖ₑ * (C * eVariationOn g s + D * eVariationOn f s) ≤
    C * eVariationOn g s + D * eVariationOn f s

Tactic:
grw [ContinuousLinearMap.opENorm_lsmul_le, one_mul]

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
a b : α
⊢ eVariationOn f {a, b} = edist (f a) (f b)

Tactic:
by
  wlog hab : a ≤ b generalizing a b
  · simpa [edist_comm, pair_comm] using this b a (le_of_not_ge hab)
  · apply le_antisymm _ (edist_le f (by simp) (by simp))
    simp only [eVariationOn_eq_strictMonoOn, iSup_le_iff]
    rintro ⟨n, u, hmono, hi⟩
    rcases (by omega : n = 0 ∨ n = 1 ∨ 2 ≤ n) with rfl | rfl | hn
    · simp
    · have := hmono (by simp) (by simp) zero_lt_one
      simp [(by grind : u 0 = a), (by grind : u 1 = b), edist_comm]
    · have := hmono (by simp) (by grind) zero_lt_one
      have := hmono (by grind) (by grind) one_lt_two
      grind

Goal state after:
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 μ
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 : α
hx :
  ∀ (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‖ₑ)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
c : E
hc : c ∈ t
⊢ Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)

Tactic:
obtain ⟨n, xn⟩ : ∃ n, x ∈ A.set n := by simpa [← A.spanning] using mem_univ 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 μ
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 : α
hx :
  ∀ (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‖ₑ)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
c : E
hc : c ∈ t
n : ℕ
xn : x ∈ A.set n
⊢ Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)
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
⊢ map f L ≠ ⊥

Tactic:
simp [neBot_iff.mp h]

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 : α
this :
  (fun y ↦ eVariationOn f (s ∩ Ioc x y)) = fun y ↦
    eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Ico (toDual y) (toDual x))
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Ioc x y)) (𝓝[s] x) (𝓝 0)

Tactic:
rw [this]

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 : α
this :
  (fun y ↦ eVariationOn f (s ∩ Ioc x y)) = fun y ↦
    eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Ico (toDual y) (toDual x))
⊢ Tendsto (fun y ↦ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Ico (toDual y) (toDual x))) (𝓝[s] x) (𝓝 0)
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 α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
H : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))
y : α
hy : y ∈ s ∩ Iio x
N : 𝓝[s ∩ Ici y ∩ Iio x] x = 𝓝[s ∩ Iio x] x
⊢ eVariationOn f (s ∩ Ico y x) + edist (f x) l = eVariationOn f (s ∩ Ici y ∩ Iic x)

Tactic:
eVariationOn_on_inter_Iic_eq_Iio_add_edist (l := l)

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
H : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))
y : α
hy : y ∈ s ∩ Iio x
N : 𝓝[s ∩ Ici y ∩ Iio x] x = 𝓝[s ∩ Iio x] x
⊢ eVariationOn f (s ∩ Ico y x) + edist (f x) l = eVariationOn f (s ∩ Ici y ∩ Iio x) + edist (f x) l

case h
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
H : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))
y : α
hy : y ∈ s ∩ Iio x
N : 𝓝[s ∩ Ici y ∩ Iio x] x = 𝓝[s ∩ Iio x] x
⊢ (𝓝[s ∩ Ici y ∩ Iio x] x).NeBot

case ha
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
H : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))
y : α
hy : y ∈ s ∩ Iio x
N : 𝓝[s ∩ Ici y ∩ Iio x] x = 𝓝[s ∩ Iio x] x
⊢ x ∈ s ∩ Ici y

case h'f
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
H : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))
y : α
hy : y ∈ s ∩ Iio x
N : 𝓝[s ∩ Ici y ∩ Iio x] x = 𝓝[s ∩ Iio x] x
⊢ Tendsto f (𝓝[s ∩ Ici y ∩ Iio x] x) (𝓝 l)
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 α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Ioi x] x) (𝓝 l)
hx : x ∈ s
this :
  (fun y ↦ eVariationOn f (s ∩ Icc x y)) = fun y ↦
    eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Icc x y)) (𝓝[s ∩ Ioi x] x) (𝓝 (edist (f x) l))

Tactic:
rw [this]

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Ioi x] x) (𝓝 l)
hx : x ∈ s
this :
  (fun y ↦ eVariationOn f (s ∩ Icc x y)) = fun y ↦
    eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))
⊢ Tendsto (fun y ↦ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))) (𝓝[s ∩ Ioi x] x)
    (𝓝 (edist (f x) l))
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 α
l : E
hf : LocallyBoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Ioi x] x) (𝓝 l)
hx : x ∈ s
this :
  (fun y ↦ eVariationOn f (s ∩ Icc x y)) = fun y ↦
    eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Icc x y)) (𝓝[s ∩ Ioi x] x) (𝓝 (edist (f x) l))

Tactic:
rw [this]

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : LocallyBoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Ioi x] x) (𝓝 l)
hx : x ∈ s
this :
  (fun y ↦ eVariationOn f (s ∩ Icc x y)) = fun y ↦
    eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))
⊢ Tendsto (fun y ↦ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))) (𝓝[s ∩ Ioi x] x)
    (𝓝 (edist (f x) l))
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 : α
h : ContinuousWithinAt f (s ∩ Ici x) x
this :
  (fun y ↦ eVariationOn f (s ∩ Icc x y)) = fun y ↦
    eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Icc x y)) (𝓝[s] x) (𝓝 0)

Tactic:
rw [this]

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 : α
h : ContinuousWithinAt f (s ∩ Ici x) x
this :
  (fun y ↦ eVariationOn f (s ∩ Icc x y)) = fun y ↦
    eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))
⊢ Tendsto (fun y ↦ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))) (𝓝[s] x) (𝓝 0)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield 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
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
n : ℤ
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfcUnits f a hf' hf ha ^ n = cfcUnits (f ^ n) a ⋯ ⋯ ha

Tactic:
cases n with
  | ofNat _ => simpa using! cfcUnits_pow f a hf' _
  | negSucc n =>
    simp only [zpow_negSucc, ← inv_pow]
    ext
    exact cfc_pow (hf := hf.inv₀ hf') .. |>.symm

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 g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this✝² : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this✝¹ : ∀ᶠ (b : ℕ → E) in Filter.pi fun i ↦ 𝓝 (g (u i)), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : ℕ → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi t ⊆ {b | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
this✝ : ∀ᶠ (b : ℕ → α) in Filter.pi fun i ↦ 𝓝 (u i), ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2
J : Set ℕ
J_fin : J.Finite
k : ℕ → Set α
k_mem : ∀ (i : ℕ), k i ∈ 𝓝 (u i)
hk : J.pi k ⊆ {x | (fun b ↦ ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2) x}
v : ℕ → α
hv : ∀ i ∈ Iic n, f (v i) ∈ t i ∧ v i ∈ k i
h'v : ∀ i ∈ Iic n, v i ∈ s
f' : ℕ → E := fun i ↦ if i ∈ Iic n then f (v i) else g (u i)
this : ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) = ∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i)
⊢ c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))

Tactic:
rw [this]

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this✝² : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this✝¹ : ∀ᶠ (b : ℕ → E) in Filter.pi fun i ↦ 𝓝 (g (u i)), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : ℕ → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi t ⊆ {b | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
this✝ : ∀ᶠ (b : ℕ → α) in Filter.pi fun i ↦ 𝓝 (u i), ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2
J : Set ℕ
J_fin : J.Finite
k : ℕ → Set α
k_mem : ∀ (i : ℕ), k i ∈ 𝓝 (u i)
hk : J.pi k ⊆ {x | (fun b ↦ ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2) x}
v : ℕ → α
hv : ∀ i ∈ Iic n, f (v i) ∈ t i ∧ v i ∈ k i
h'v : ∀ i ∈ Iic n, v i ∈ s
f' : ℕ → E := fun i ↦ if i ∈ Iic n then f (v i) else g (u i)
this : ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) = ∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i)
⊢ c < ∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i)