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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
⊢ ∀ x ∈ {a, b}, ∀ y ∈ {a, b}, x * y = y * x

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
⊢ ∀ a_1 ∈ {a, b}, ∀ b_1 ∈ {a, b}, a_1 * star b_1 = star b_1 * a_1

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
x✝¹ : NonUnitalCommRing ↥S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S :=
  { toNonUnitalNormedRing := (nonUnitalCStarAlgebra S).toNonUnitalNormedRing, mul_comm := ⋯,
    toStarRing := (nonUnitalCStarAlgebra S).toStarRing, toCompleteSpace := ⋯, toCStarRing := ⋯,
    toNormedSpace := (nonUnitalCStarAlgebra S).toNormedSpace, toIsScalarTower := ⋯, toSMulCommClass := ⋯,
    toStarModule := ⋯ }
⊢ ⟨a, ?m.172⟩ * ⟨b, ?m.175⟩ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
⊢ ∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
by

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
x✝¹ : NonUnitalCommRing ↥S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S :=
  { toNonUnitalNormedRing := (nonUnitalCStarAlgebra S).toNonUnitalNormedRing, mul_comm := ⋯,
    toStarRing := (nonUnitalCStarAlgebra S).toStarRing, toCompleteSpace := ⋯, toCStarRing := ⋯,
    toNormedSpace := (nonUnitalCStarAlgebra S).toNormedSpace, toIsScalarTower := ⋯, toSMulCommClass := ⋯,
    toStarModule := ⋯ }
⊢ a ∈ S

Tactic:
apply le_topologicalClosure; aesop

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

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
x✝¹ : NonUnitalCommRing ↥S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S :=
  { toNonUnitalNormedRing := (nonUnitalCStarAlgebra S).toNonUnitalNormedRing, mul_comm := ⋯,
    toStarRing := (nonUnitalCStarAlgebra S).toStarRing, toCompleteSpace := ⋯, toCStarRing := ⋯,
    toNormedSpace := (nonUnitalCStarAlgebra S).toNormedSpace, toIsScalarTower := ⋯, toSMulCommClass := ⋯,
    toStarModule := ⋯ }
⊢ b ∈ S

Tactic:
apply le_topologicalClosure; aesop

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
⊢ ‖a + b‖ = max ‖a‖ ‖b‖

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
⊢ a * -b = 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
⊢ ‖a - b‖ = max ‖a‖ ‖b‖

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ Commute a b

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ a * -b = 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ ‖a - b‖ = max ‖a‖ ‖b‖

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsSelfAdjoint (f i)) → ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
h : ∀ i ∈ insert j s, IsSelfAdjoint (f i)
this : f j * ∑ i ∈ s, f i = 0
⊢ j ∈ insert j s

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsSelfAdjoint (f i)) → ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
h : ∀ i ∈ insert j s, IsSelfAdjoint (f i)
this : f j * ∑ i ∈ s, f i = 0
⊢ IsSelfAdjoint (∑ i ∈ s, f i)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsSelfAdjoint (f i)) → ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
h : ∀ i ∈ insert j s, IsSelfAdjoint (f i)
this : f j * ∑ i ∈ s, f i = 0
⊢ ‖∑ i ∈ insert j s, f i‖₊ = (insert j s).sup fun x ↦ ‖f x‖₊

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsSelfAdjoint (f i)) → ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
h : ∀ i ∈ insert j s, IsSelfAdjoint (f i)
i : ι
hi : i ∈ s
⊢ j ≠ i

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
h : ∀ i ∈ s, IsSelfAdjoint (f i)
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
⊢ ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommCStarAlgebra A
inst✝ : CommCStarAlgebra B
φ : A →⋆ₐ[ℂ] B
⊢ (↑(gelfandStarTransform B)).comp φ =
    (ContinuousMap.compStarAlgHom' ℂ ℂ (compContinuousMap φ)).comp ↑(gelfandStarTransform A)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : (i : ι) → NonUnitalRing (A i)
inst✝⁹ : (i : ι) → Module S (A i)
inst✝⁸ : (i : ι) → Module R (A i)
inst✝⁷ : ∀ (i : ι), IsScalarTower R S (A i)
inst✝⁶ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R (A i) (A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMapZero.UniqueHom R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ i, quasispectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
hf₀ : f 0 = 0
i : ι
this : Nonempty ι
φ : ((i : ι) → A i) →⋆ₙₐ[S] A i := Pi.evalNonUnitalStarAlgHom S A i
⊢ ContinuousOn f (quasispectrum R a)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
⊢ 0⁺ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
⊢ 0⁻ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : (i : ι) → NonUnitalRing (A i)
inst✝⁹ : (i : ι) → Module S (A i)
inst✝⁸ : (i : ι) → Module R (A i)
inst✝⁷ : ∀ (i : ι), IsScalarTower R S (A i)
inst✝⁶ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R (A i) (A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMapZero.UniqueHom R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ i, quasispectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
⊢ cfcₙ f a = fun i ↦ cfcₙ f (a i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ a⁺ * a⁻ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ a⁻ * a⁺ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst✝²⁸ : CommSemiring R
inst✝²⁷ : CommRing S
inst✝²⁶ : Nontrivial R
inst✝²⁵ : StarRing R
inst✝²⁴ : MetricSpace R
inst✝²³ : IsTopologicalSemiring R
inst✝²² : ContinuousStar R
inst✝²¹ : Algebra R S
inst✝²⁰ : NonUnitalRing A
inst✝¹⁹ : NonUnitalRing B
inst✝¹⁸ : Module S A
inst✝¹⁷ : Module R A
inst✝¹⁶ : Module R B
inst✝¹⁵ : Module S B
inst✝¹⁴ : SMulCommClass R A A
inst✝¹³ : SMulCommClass R B B
inst✝¹² : IsScalarTower R A A
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : StarRing A
inst✝⁹ : StarRing B
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : IsScalarTower R S B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R (A × B) pab
inst✝³ : NonUnitalContinuousFunctionalCalculus R A pa
inst✝² : NonUnitalContinuousFunctionalCalculus R B pb
inst✝¹ : ContinuousMapZero.UniqueHom R A
inst✝ : ContinuousMapZero.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
hf₀ : f 0 = 0
φ : A × B →⋆ₙₐ[S] A := NonUnitalStarAlgHom.fst S A B
⊢ ContinuousOn f (quasispectrum R (a, b))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ a⁺ - a⁻ = a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ a⁺ - a⁻ = a

Tactic:
by
  rw [posPart_def, negPart_def]
  rw [← cfcₙ_sub _ _]
  conv_rhs => rw [← cfcₙ_id ℝ a]
  congr! 2 with
  exact _root_.posPart_sub_negPart _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : NonUnitalRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
a : A
ha : ¬IsSelfAdjoint a
h : IsSelfAdjoint (-a)
⊢ IsSelfAdjoint a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst✝²⁸ : CommSemiring R
inst✝²⁷ : CommRing S
inst✝²⁶ : Nontrivial R
inst✝²⁵ : StarRing R
inst✝²⁴ : MetricSpace R
inst✝²³ : IsTopologicalSemiring R
inst✝²² : ContinuousStar R
inst✝²¹ : Algebra R S
inst✝²⁰ : NonUnitalRing A
inst✝¹⁹ : NonUnitalRing B
inst✝¹⁸ : Module S A
inst✝¹⁷ : Module R A
inst✝¹⁶ : Module R B
inst✝¹⁵ : Module S B
inst✝¹⁴ : SMulCommClass R A A
inst✝¹³ : SMulCommClass R B B
inst✝¹² : IsScalarTower R A A
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : StarRing A
inst✝⁹ : StarRing B
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : IsScalarTower R S B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R (A × B) pab
inst✝³ : NonUnitalContinuousFunctionalCalculus R A pa
inst✝² : NonUnitalContinuousFunctionalCalculus R B pb
inst✝¹ : ContinuousMapZero.UniqueHom R A
inst✝ : ContinuousMapZero.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
hf₀ : f 0 = 0
φ : A × B →⋆ₙₐ[S] B := NonUnitalStarAlgHom.snd S A B
⊢ ContinuousOn f (quasispectrum R (a, b))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : NonUnitalRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
a : A
⊢ (-a)⁺ = a⁻

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst✝²⁸ : CommSemiring R
inst✝²⁷ : CommRing S
inst✝²⁶ : Nontrivial R
inst✝²⁵ : StarRing R
inst✝²⁴ : MetricSpace R
inst✝²³ : IsTopologicalSemiring R
inst✝²² : ContinuousStar R
inst✝²¹ : Algebra R S
inst✝²⁰ : NonUnitalRing A
inst✝¹⁹ : NonUnitalRing B
inst✝¹⁸ : Module S A
inst✝¹⁷ : Module R A
inst✝¹⁶ : Module R B
inst✝¹⁵ : Module S B
inst✝¹⁴ : SMulCommClass R A A
inst✝¹³ : SMulCommClass R B B
inst✝¹² : IsScalarTower R A A
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : StarRing A
inst✝⁹ : StarRing B
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : IsScalarTower R S B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R (A × B) pab
inst✝³ : NonUnitalContinuousFunctionalCalculus R A pa
inst✝² : NonUnitalContinuousFunctionalCalculus R B pb
inst✝¹ : ContinuousMapZero.UniqueHom R A
inst✝ : ContinuousMapZero.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
⊢ cfcₙ f (a, b) = (cfcₙ f a, cfcₙ f b)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : NonUnitalRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
a : A
⊢ (-a)⁻ = a⁺

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : (i : ι) → Ring (A i)
inst✝⁷ : (i : ι) → Algebra S (A i)
inst✝⁶ : (i : ι) → Algebra R (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R S (A i)
hinst : IsScalarTower R S ((i : ι) → A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : ContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), ContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMap.UniqueHom R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ i, spectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
i : ι
φ : ((i : ι) → A i) →⋆ₐ[S] A i := Pi.evalStarAlgHom S A i
⊢ ContinuousOn f (spectrum R a)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : (i : ι) → Ring (A i)
inst✝⁷ : (i : ι) → Algebra S (A i)
inst✝⁶ : (i : ι) → Algebra R (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R S (A i)
hinst : IsScalarTower R S ((i : ι) → A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : ContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), ContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMap.UniqueHom R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ i, spectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
⊢ cfc f a = fun i ↦ cfc f (a i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst✝²³ : CommSemiring R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
inst✝¹⁶ : Ring A
inst✝¹⁵ : Ring B
inst✝¹⁴ : Algebra S A
inst✝¹³ : Algebra S B
inst✝¹² : Algebra R A
inst✝¹¹ : Algebra R B
inst✝¹⁰ : IsScalarTower R S A
inst✝⁹ : IsScalarTower R S B
inst✝⁸ : StarRing A
inst✝⁷ : StarRing B
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst✝⁴ : ContinuousFunctionalCalculus R (A × B) pab
inst✝³ : ContinuousFunctionalCalculus R A pa
inst✝² : ContinuousFunctionalCalculus R B pb
inst✝¹ : ContinuousMap.UniqueHom R A
inst✝ : ContinuousMap.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (spectrum R a ∪ spectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
φ : A × B →⋆ₐ[S] A := StarAlgHom.fst S A B
⊢ ContinuousOn f (spectrum R (a, b))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst✝²³ : CommSemiring R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
inst✝¹⁶ : Ring A
inst✝¹⁵ : Ring B
inst✝¹⁴ : Algebra S A
inst✝¹³ : Algebra S B
inst✝¹² : Algebra R A
inst✝¹¹ : Algebra R B
inst✝¹⁰ : IsScalarTower R S A
inst✝⁹ : IsScalarTower R S B
inst✝⁸ : StarRing A
inst✝⁷ : StarRing B
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst✝⁴ : ContinuousFunctionalCalculus R (A × B) pab
inst✝³ : ContinuousFunctionalCalculus R A pa
inst✝² : ContinuousFunctionalCalculus R B pb
inst✝¹ : ContinuousMap.UniqueHom R A
inst✝ : ContinuousMap.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (spectrum R a ∪ spectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
φ : A × B →⋆ₐ[S] B := StarAlgHom.snd S A B
⊢ ContinuousOn f (spectrum R (a, b))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst✝²³ : CommSemiring R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
inst✝¹⁶ : Ring A
inst✝¹⁵ : Ring B
inst✝¹⁴ : Algebra S A
inst✝¹³ : Algebra S B
inst✝¹² : Algebra R A
inst✝¹¹ : Algebra R B
inst✝¹⁰ : IsScalarTower R S A
inst✝⁹ : IsScalarTower R S B
inst✝⁸ : StarRing A
inst✝⁷ : StarRing B
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst✝⁴ : ContinuousFunctionalCalculus R (A × B) pab
inst✝³ : ContinuousFunctionalCalculus R A pa
inst✝² : ContinuousFunctionalCalculus R B pb
inst✝¹ : ContinuousMap.UniqueHom R A
inst✝ : ContinuousMap.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (spectrum R a ∪ spectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
⊢ cfc f (a, b) = (cfc f a, cfc f b)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ≥0
a : A
⊢ (r • a)⁺ = r • a⁺

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ≥0
a : A
⊢ (r • a)⁻ = r • a⁻

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
⊢ (r • a)⁺ = -r • a⁻

Tactic:
by

Goal state after: