mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case refine_1.inl
α : 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)
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iic a
this : u n ≤ a
hn : u n = a
⊢ ∑ i ∈ Finset.range ⟨n, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨n, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨n, ⟨u, ⋯⟩⟩.snd i)) ≤
    eVariationOn f (s ∩ Iio a) + edist (f a) l

pp: case refine_1.inr
α : 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)
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iic a
this : u n ≤ a
hn : u n < a
⊢ ∑ i ∈ Finset.range ⟨n, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨n, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨n, ⟨u, ⋯⟩⟩.snd i)) ≤
    eVariationOn f (s ∩ Iio a) + edist (f a) l

Tactic:
;

Goal state after:
case refine_1.inl
α : 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)
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iic a
this : u n ≤ a
hn : u n = a
⊢ ∑ i ∈ Finset.range ⟨n, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨n, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨n, ⟨u, ⋯⟩⟩.snd i)) ≤
    eVariationOn f (s ∩ Iio a) + edist (f a) l

case refine_1.inr
α : 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)
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iic a
this : u n ≤ a
hn : u n < a
⊢ ∑ i ∈ Finset.range ⟨n, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨n, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨n, ⟨u, ⋯⟩⟩.snd i)) ≤
    eVariationOn f (s ∩ Iio a) + edist (f a) l
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
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 < ∞
⊢ ∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ ≤ ∫⁻ (y : α) in a, ‖f y - c‖ₑ + ‖f x - c‖ₑ ∂μ

Tactic:
apply lintegral_mono fun 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
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 : α
⊢ ‖f x - f x✝‖ₑ ≤ ‖f x - c‖ₑ + ‖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✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
h : s ∩ Iio a = ∅
⊢ 𝓝[s ∩ Iio a] a = ⊥

Tactic:
;

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
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
h : s ∩ Iio a = ∅
⊢ 𝓝[s ∩ Iio a] a = ⊥
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
x✝ : ↑(spectrum R a)
⊢ f x✝ = (spectrum R a).domRestrict (Function.extend Subtype.val (⇑f) g) x✝

Tactic:
;

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
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
x✝ : ↑(spectrum R a)
⊢ f x✝ = (spectrum R a).domRestrict (Function.extend Subtype.val (⇑f) g) x✝
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)

Tactic:
rw [cfc_apply f a h.1 h.2]

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 ((cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
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
x✝ : R
⊢ r + f x✝ = (fun x ↦ r) x✝ + f x✝

Tactic:
;

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
x✝ : R
⊢ r + f x✝ = (fun x ↦ r) x✝ + f x✝
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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
x✝ : R
⊢ s.sum f x✝ = ∑ i ∈ s, f i x✝

Tactic:
;

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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
x✝ : R
⊢ s.sum f x✝ = ∑ i ∈ s, f i x✝
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁷ : Semifield R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : Semifield S
inst✝¹¹ : StarRing S
inst✝¹⁰ : MetricSpace S
inst✝⁹ : IsTopologicalSemiring S
inst✝⁸ : ContinuousStar S
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : IsScalarTower R S A
inst✝¹ : StarModule R S
inst✝ : ContinuousSMul R S
a : A
φ : C(↑(spectrum S a), S) →⋆ₐ[S] A
f : C(S, R)
h : SpectrumRestricts a ⇑f
h_id : φ (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a
⊢ (starAlgHom φ h) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a

Tactic:
simp only [SpectrumRestricts.starAlgHom_apply]
  convert! h_id
  ext x
  exact h.rightInvOn x.2

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] x) (𝓝 0) ∧
    Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)

Tactic:
simp [A, B]

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 : α
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Ioc x y)) (𝓝[s] x) (𝓝 0)

Tactic:
by
  have : (fun y ↦ eVariationOn f (s ∩ Ioc x y)) =
      (fun y ↦ eVariationOn (f ∘ ofDual) (ofDual ⁻¹' s ∩ Ico (toDual y) (toDual x))) := by
    ext y
    rw [Ico_toDual, ← preimage_inter, comp_ofDual]
  rw [this]
  exact hf.ofDual.tendsto_eVariationOn_Ico_zero (toDual x)

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
inst✝ : DenselyOrdered α
f : α → E
a : α
hf : BoundedVariationOn f univ
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
ha : IsBot a
x : α
⊢ x ∈ Iic a ↔ x ∈ {a}

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : CompleteSpace E
inst✝ : DenselyOrdered α
f : α → E
a : α
hf : BoundedVariationOn f univ
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
ha : IsBot a
x : α
⊢ x ∈ Iic a ↔ x ∈ {a}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
x : ↑(spectrum R a)
⊢ (spectrum R a).domRestrict f x ∈ f '' spectrum R a

Tactic:
;

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
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
x : ↑(spectrum R a)
⊢ (spectrum R a).domRestrict f x ∈ f '' spectrum R a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case h
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
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
x : ↑(spectrum R a)
⊢ ↑x ∈ spectrum R a ∧ f ↑x = (spectrum R a).domRestrict f x

Tactic:
;

Goal state after:
case h
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
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
x : ↑(spectrum R a)
⊢ ↑x ∈ spectrum R a ∧ f ↑x = (spectrum R a).domRestrict f x
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case e_s
α : 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 ∩ Ico y x = s ∩ Ici y ∩ Iio x

Tactic:
;

Goal state after:
case e_s
α : 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 ∩ Ico y x = s ∩ Ici y ∩ Iio x
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 ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : s ∩ Iio x = ∅
⊢ 𝓝[s ∩ Iio x] x = ⊥

Tactic:
;

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 ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : s ∩ Iio x = ∅
⊢ 𝓝[s ∩ Iio x] x = ⊥
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁵ : Semifield R
inst✝²⁴ : StarRing R
inst✝²³ : MetricSpace R
inst✝²² : IsTopologicalSemiring R
inst✝²¹ : ContinuousStar R
inst✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : TopologicalSpace A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus S A q
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts a ⇑f
g : R → R
hg : ContinuousOn g (σₙ R a) ∧ g 0 = 0
⊢ cfcₙ g a = cfcₙ (fun x ↦ (algebraMap R S) (g (f x))) a

Tactic:
obtain ⟨hg, hg0⟩ := hg
    rw [cfcₙ_apply g a, cfcₙHom_eq_restrict f hpa hqa h, nonUnitalStarAlgHom_apply,
      cfcₙHom_eq_cfcₙ_extend 0]
    apply cfcₙ_congr fun x hx ↦ ?_
    lift x to σₙ S a using hx
    simp

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✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
⊢ cfc (-f) a = (-cfc f) a

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
⊢ cfc (-f) a = (-cfc f) a
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
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
x✝ : ↑(σₙ R a)
⊢ f x✝ = (σₙ R a).domRestrict (Function.extend Subtype.val (⇑f) g) x✝

Tactic:
;

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
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
x✝ : ↑(σₙ R a)
⊢ f x✝ = (σₙ R a).domRestrict (Function.extend Subtype.val (⇑f) g) x✝
Module: Mathlib.Topology.Algebra.StarSubalgebra

Goal state before:
pp: case e'_2
R : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed[inst✝⁴] ↑S₁
⊢ ↑S₁ = {x | x ∈ S₁}

Tactic:
;

Goal state after:
case e'_2
R : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed[inst✝⁴] ↑S₁
⊢ ↑S₁ = {x | x ∈ S₁}
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
a : A
h : ∀ x ∈ spectrum R a, 1 ≤ x
ha : p a
⊢ 1 ≤ a

Tactic:
simpa using algebraMap_le_of_le_spectrum h

Goal state after:
Module: Mathlib.Topology.Algebra.StarSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Semiring A
inst✝¹² : StarRing A
inst✝¹¹ : IsSemitopologicalSemiring A
inst✝¹⁰ : ContinuousStar A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : StarRing B
inst✝⁴ : Algebra R B
inst✝³ : T2Space B
F : Type u_4
a : A
inst✝² : FunLike F (↥(elemental R a)) B
inst✝¹ : AlgHomClass F R (↥(elemental R a)) B
inst✝ : StarHomClass F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst✝⁷] ⇑φ
hψ : Continuous[instTopologicalSpaceSubtype, inst✝⁷] ⇑ψ
h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
⊢ φ = ψ

Tactic:
refine StarAlgHomClass.ext_topologicalClosure hφ hψ fun x => ?_
  refine adjoin_induction_subtype x ?_ ?_ ?_ ?_ ?_
  exacts [fun y hy => by simpa only [Set.mem_singleton_iff.mp hy] using! h, fun r => by
    simp only [AlgHomClass.commutes], fun x y hx hy => by simp only [map_add, hx, hy],
    fun x y hx hy => by simp only [map_mul, hx, hy], fun x hx => by simp only [map_star, hx]]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
a b : α
hf : MonotoneOn f s
as : a ∈ s
bs : b ∈ s
hab : a ≤ b
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Set.Icc a b
⊢ ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) =
    ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i)))

Tactic:
by
          rw [ofReal_sum_of_nonneg]
          exact fun i _ ↦ sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))

Goal state after: