mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case refine_2
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✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : MetricSpace A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts a ⇑f
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a)) R
x : ↑(σₙ R a)
⊢ dist (↑g₁ x) (↑g₂ x) ≤
    dist
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        (g₁.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        (g₂.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))

Tactic:
·

Goal state after:
case refine_2
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✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : MetricSpace A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts a ⇑f
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a)) R
x : ↑(σₙ R a)
⊢ dist (↑g₁ x) (↑g₂ x) ≤
    dist
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        (g₁.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        (g₂.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k ∈ σ 𝕜 ↑u
⊢ ‖k‖ ≤ 1

pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k ∈ σ 𝕜 ↑u
⊢ 1 ≤ ‖k‖

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k ∈ σ 𝕜 ↑u
⊢ ‖k‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k ∈ σ 𝕜 ↑u
⊢ 1 ≤ ‖k‖

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k ∈ σ 𝕜 ↑u
⊢ 1 ≤ ‖k‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inl
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h✝ : Subsingleton A
⊢ ‖cfc f a‖₊ ≤ c

pp: case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h✝ : Nontrivial A
⊢ ‖cfc f a‖₊ ≤ c

Tactic:
·

Goal state after:
case inl
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h✝ : Subsingleton A
⊢ ‖cfc f a‖₊ ≤ c
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h✝ : Nontrivial A
⊢ ‖cfc f a‖₊ ≤ c

Tactic:
·

Goal state after:
case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h✝ : Nontrivial A
⊢ ‖cfc f a‖₊ ≤ c
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inl
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h✝ : Subsingleton A
⊢ ‖cfc f a‖₊ < c

pp: case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h✝ : Nontrivial A
⊢ ‖cfc f a‖₊ < c

Tactic:
·

Goal state after:
case inl
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h✝ : Subsingleton A
⊢ ‖cfc f a‖₊ < c
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h✝ : Nontrivial A
⊢ ‖cfc f a‖₊ < c

Tactic:
·

Goal state after:
case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h✝ : Nontrivial A
⊢ ‖cfc f a‖₊ < c
Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula

Goal state before:
pp: A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
H₁ : Differentiable ℂ fun z ↦ resolvent a z
⊢ Tendsto (fun z ↦ resolvent a z) (cocompact ℂ) (𝓝 ?m.100)

Tactic:
simpa [Metric.cobounded_eq_cocompact] using resolvent_tendsto_cobounded a (𝕜 := ℂ)

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
this✝ : NormedAlgebra ℚ A
hu : NormedSpace.exp (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
this : NormedSpace.exp (I • z) ∈ σ ℂ (NormedSpace.exp (I • a))
⊢ z.im = (↑z.re).im

Tactic:
by
    simpa only [← Complex.exp_eq_exp_ℂ, mem_sphere_zero_iff_norm, norm_exp, Real.exp_eq_one_iff,
      smul_eq_mul, I_mul, neg_eq_zero] using!
      spectrum.subset_circle_of_unitary hu this

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {U | IsOpen[instTopologicalSpaceProd] U}
⊢ IsOpen ((SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' 𝒫 U)

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {V | IsOpen[instTopologicalSpaceProd] V}
⊢ IsOpen ((SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' (fun V ↦ {s | (s ∩ V).Nonempty}) U)

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {U | IsOpen[instTopologicalSpaceProd] U}
⊢ IsOpen ((SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' 𝒫 U)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
⊢ ‖0‖₊ < c

pp: case refine_2
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : { toFun := (σₙ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : 0 ≤ a
⊢ ‖(cfcₙHom ha) { toFun := (σₙ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }‖₊ < c

Tactic:
·

Goal state after:
case refine_1
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
⊢ ‖0‖₊ < c
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : { toFun := (σₙ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : 0 ≤ a
⊢ ‖(cfcₙHom ha) { toFun := (σₙ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }‖₊ < c

Tactic:
·

Goal state after:
case refine_2
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : { toFun := (σₙ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : 0 ≤ a
⊢ ‖(cfcₙHom ha) { toFun := (σₙ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }‖₊ < c
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
⊢ ‖cfcₙ f a‖₊ < c

Tactic:
refine cfcₙ_cases (‖·‖₊ < c) a f ?_ fun hf hf0 ha ↦ ?_
  · simpa using (h 0 (quasispectrum.zero_mem ℝ≥0 _)).pos
  · simp only [← cfcₙ_apply f a, (IsGreatest.nnnorm_cfcₙ_nnreal f a hf hf0 ha |>.lt_iff)]
    rintro - ⟨x, hx, rfl⟩
    exact h x hx

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {V | IsOpen[instTopologicalSpaceProd] V}
⊢ IsOpen ((SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' (fun V ↦ {s | (s ∩ V).Nonempty}) U)

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {V | IsOpen[instTopologicalSpaceProd] V}
⊢ IsOpen ((SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' (fun V ↦ {s | (s ∩ V).Nonempty}) U)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ ∀ (x : ↑(σ 𝕜 a)), ‖((↑f).comp ι) x‖ ≤ ‖↑f‖

pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ ∀ (x : ↑(σₙ 𝕜 a)), ‖↑f x‖ ≤ ‖(↑f).comp ι‖

Tactic:
·

Goal state after:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ ∀ (x : ↑(σ 𝕜 a)), ‖((↑f).comp ι) x‖ ≤ ‖↑f‖
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsUnit a

pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ (a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a * a⋆)

pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ ↑(a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a⋆ * a)

Tactic:
·

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsUnit a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ ∀ (x : ↑(σₙ 𝕜 a)), ‖↑f x‖ ≤ ‖(↑f).comp ι‖

Tactic:
·

Goal state after:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ ∀ (x : ↑(σₙ 𝕜 a)), ‖↑f x‖ ≤ ‖(↑f).comp ι‖
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ (a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a * a⋆)

pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ ↑(a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a⋆ * a)

Tactic:
·

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ (a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a * a⋆)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inl
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
hx : 0 ∈ σₙ 𝕜 a
⊢ ‖↑f ⟨0, hx⟩‖ ≤ ‖(↑f).comp ι‖

pp: case inr
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
x : 𝕜
hx : x ∈ σₙ 𝕜 a
hx' : x ∈ σ 𝕜 a
⊢ ‖↑f ⟨x, hx⟩‖ ≤ ‖(↑f).comp ι‖

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
hx : 0 ∈ σₙ 𝕜 a
⊢ ‖↑f ⟨0, hx⟩‖ ≤ ‖(↑f).comp ι‖
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ ↑(a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a⋆ * a)

Tactic:
·

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ ↑(a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a⋆ * a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inr
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
x : 𝕜
hx : x ∈ σₙ 𝕜 a
hx' : x ∈ σ 𝕜 a
⊢ ‖↑f ⟨x, hx⟩‖ ≤ ‖(↑f).comp ι‖

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
x : 𝕜
hx : x ∈ σₙ 𝕜 a
hx' : x ∈ σ 𝕜 a
⊢ ‖↑f ⟨x, hx⟩‖ ≤ ‖(↑f).comp ι‖
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x : Unitization ℂ A
this : ∀ {s : Unitization ℂ A}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊
⊢ ‖ψ x‖₊ ≤ ‖x‖₊

Tactic:
refine nonneg_le_nonneg_of_sq_le_sq zero_le ?_
      simp_rw [← nnnorm_star_mul_self, ← map_star, ← map_mul]
      exact this <| .star_mul_self x

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
this :
  ∀ (K₁ K₂ : Compacts α),
    K₁ ≠ K₂ → ¬K₁ ≤ K₂ → (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) K₁ K₂
h' : ¬¬K₁ ≤ K₂
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v

pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
h' : ¬K₁ ≤ K₂
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
this :
  ∀ (K₁ K₂ : Compacts α),
    K₁ ≠ K₂ → ¬K₁ ≤ K₂ → (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) K₁ K₂
h' : ¬¬K₁ ≤ K₂
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
hK : K ∈ (fun a ↦ {a_1 | ↑a_1 ⊆ a}) U
⊢ ∃ s ∈ 𝓝ˢ ((fun a ↦ {a_1 | ↑a_1 ⊆ a}) U)ᶜ, ∃ t ∈ 𝓝 K, Disjoint s t

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
hK : K ∈ (fun a ↦ {a_1 | (↑a_1 ∩ a).Nonempty}) U
⊢ ∃ s ∈ 𝓝ˢ ((fun a ↦ {a_1 | (↑a_1 ∩ a).Nonempty}) U)ᶜ, ∃ t ∈ 𝓝 K, Disjoint s t

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
hK : K ∈ (fun a ↦ {a_1 | ↑a_1 ⊆ a}) U
⊢ ∃ s ∈ 𝓝ˢ ((fun a ↦ {a_1 | ↑a_1 ⊆ a}) U)ᶜ, ∃ t ∈ 𝓝 K, Disjoint s t