mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case h₂
α : 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} := ⋯
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
M : ∀ c ∈ t, Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)
ε : ℝ≥0∞
εpos : ε > 0
c : E
ct : c ∈ t
xc : ‖f x - c‖ₑ < ε / 2
a : Set α
ha : (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a < ε / 2
h'a : 0 < μ a
h''a : μ a < ∞
⊢ ∫⁻ (x_1 : α) in a, ‖f x - c‖ₑ ∂μ ≤ ε / 2 * μ a

Tactic:
·

Goal state after:
case h₂
α : 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} := ⋯
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
M : ∀ c ∈ t, Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)
ε : ℝ≥0∞
εpos : ε > 0
c : E
ct : c ∈ t
xc : ‖f x - c‖ₑ < ε / 2
a : Set α
ha : (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a < ε / 2
h'a : 0 < μ a
h''a : μ a < ∞
⊢ ∫⁻ (x_1 : α) in a, ‖f x - c‖ₑ ∂μ ≤ ε / 2 * μ 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:
·

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 : ℕ → α := 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))
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 : ℕ → α := ⋯
⊢ edist (f a) (f y) ≤ edist (f (v (n + 1))) (f (v n)) + edist (f (v (n + (1 + 1)))) (f (v (n + 1)))

Tactic:
·

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: case refine_1
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
ha : p a
inst✝ : UniqueHom R A
f : C(↑(spectrum R a), R)
f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))
hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)
g : C(↑(spectrum R ((cfcHom ha) f)), R)
φ : C(↑(spectrum R ((cfcHom ha) f)), R) →⋆ₐ[R] A := (cfcHom ha).comp (compStarAlgHom' R R f')
⊢ Continuous[_, inst✝⁴] ⇑φ

pp: case refine_2
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
ha : p a
inst✝ : UniqueHom R A
f : C(↑(spectrum R a), R)
f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))
hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)
g : C(↑(spectrum R ((cfcHom ha) f)), R)
φ : C(↑(spectrum R ((cfcHom ha) f)), R) →⋆ₐ[R] A := (cfcHom ha).comp (compStarAlgHom' R R f')
⊢ φ (restrict (spectrum R ((cfcHom ha) f)) (ContinuousMap.id R)) = (cfcHom ha) f

Tactic:
·

Goal state after:
case refine_1
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
ha : p a
inst✝ : UniqueHom R A
f : C(↑(spectrum R a), R)
f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))
hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)
g : C(↑(spectrum R ((cfcHom ha) f)), R)
φ : C(↑(spectrum R ((cfcHom ha) f)), R) →⋆ₐ[R] A := (cfcHom ha).comp (compStarAlgHom' R R f')
⊢ Continuous[_, inst✝⁴] ⇑φ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case refine_2
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
ha : p a
inst✝ : UniqueHom R A
f : C(↑(spectrum R a), R)
f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))
hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)
g : C(↑(spectrum R ((cfcHom ha) f)), R)
φ : C(↑(spectrum R ((cfcHom ha) f)), R) →⋆ₐ[R] A := (cfcHom ha).comp (compStarAlgHom' R R f')
⊢ φ (restrict (spectrum R ((cfcHom ha) f)) (ContinuousMap.id R)) = (cfcHom ha) f

Tactic:
·

Goal state after:
case refine_2
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
ha : p a
inst✝ : UniqueHom R A
f : C(↑(spectrum R a), R)
f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))
hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)
g : C(↑(spectrum R ((cfcHom ha) f)), R)
φ : C(↑(spectrum R ((cfcHom ha) f)), R) →⋆ₐ[R] A := (cfcHom ha).comp (compStarAlgHom' R R f')
⊢ φ (restrict (spectrum R ((cfcHom ha) f)) (ContinuousMap.id R)) = (cfcHom ha) f
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
ha : a ∈ s
⊢ eVariationOn f (s ∩ Iio a) = eVariationOn f (s ∩ Iic a)

pp: case neg
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
ha : a ∉ s
⊢ eVariationOn f (s ∩ Iio a) = eVariationOn f (s ∩ Iic a)

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
ha : a ∈ s
⊢ eVariationOn f (s ∩ Iio a) = eVariationOn f (s ∩ Iic a)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
ha : a ∉ s
⊢ eVariationOn f (s ∩ Iio a) = eVariationOn f (s ∩ Iic a)

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
ha : a ∉ s
⊢ eVariationOn f (s ∩ Iio a) = eVariationOn f (s ∩ Iic a)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inl
α : 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 : b ≤ a
⊢ eVariationOn f (Ioc a b) = eVariationOn f (Icc a b)

pp: case inr
α : 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
⊢ eVariationOn f (Ioc a b) = eVariationOn f (Icc a b)

Tactic:
·

Goal state after:
case inl
α : 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 : b ≤ a
⊢ eVariationOn f (Ioc a b) = eVariationOn f (Icc a b)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case pos
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)
⊢ cfc f a = (cfcHom ha) (mkD ((spectrum R a).domRestrict f) 0)

pp: case neg
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)
⊢ cfc f a = (cfcHom ha) (mkD ((spectrum R a).domRestrict f) 0)

Tactic:
·

Goal state after:
case pos
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)
⊢ cfc f a = (cfcHom ha) (mkD ((spectrum R a).domRestrict f) 0)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inl
α : 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 (Ici a) a
hab : b ≤ a
⊢ eVariationOn f (Ioc a b) = eVariationOn f (Icc a b)

pp: case inr
α : 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 (Ici a) a
hab : a < b
⊢ eVariationOn f (Ioc a b) = eVariationOn f (Icc a b)

Tactic:
·

Goal state after:
case inl
α : 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 (Ici a) a
hab : b ≤ a
⊢ eVariationOn f (Ioc a b) = eVariationOn f (Icc a b)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case neg
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)
⊢ cfc f a = (cfcHom ha) (mkD ((spectrum R a).domRestrict f) 0)

Tactic:
·

Goal state after:
case neg
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)
⊢ cfc f a = (cfcHom ha) (mkD ((spectrum R a).domRestrict f) 0)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case pos
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
h : p a ∧ ContinuousOn f (spectrum R a)
⊢ P (cfc f a)

pp: case neg
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
⊢ P (cfc f a)

Tactic:
·

Goal state after:
case pos
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
h : p a ∧ ContinuousOn f (spectrum R a)
⊢ P (cfc f a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case neg
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
⊢ P (cfc f a)

Tactic:
·

Goal state after:
case neg
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
⊢ P (cfc f a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case neg.inl
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
h : ¬p a
⊢ P (cfc f a)

pp: case neg.inr
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
h : ¬ContinuousOn f (spectrum R a)
⊢ P (cfc f a)

Tactic:
·

Goal state after:
case neg.inl
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
h : ¬p a
⊢ P (cfc f a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case neg.inr
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
h : ¬ContinuousOn f (spectrum R a)
⊢ P (cfc f a)

Tactic:
·

Goal state after:
case neg.inr
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
h : ¬ContinuousOn f (spectrum R a)
⊢ P (cfc f a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case pos
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 g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : p a ∧ ContinuousOn g (spectrum R a)
⊢ cfc f a = cfc g a

pp: case neg
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 g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : ¬(p a ∧ ContinuousOn g (spectrum R a))
⊢ cfc f a = cfc g a

Tactic:
·

Goal state after:
case pos
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 g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : p a ∧ ContinuousOn g (spectrum R a)
⊢ cfc f a = cfc g a