awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
Goal:
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommRing S
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : Algebra R S
inst_8 : NonUnitalRing A
inst_9 : NonUnitalRing B
inst_10 : Module S A
inst_11 : Module R A
inst_12 : Module R B
inst_13 : Module S B
inst_14 : SMulCommClass R A A
inst_15 : SMulCommClass R B B
inst_16 : IsScalarTower R A A
inst_17 : IsScalarTower R B B
inst_18 : StarRing A
inst_19 : StarRing B
inst_20 : TopologicalSpace A
inst_21 : TopologicalSpace B
inst_22 : IsScalarTower R S A
inst_23 : IsScalarTower R S B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst_24 : NonUnitalContinuousFunctionalCalculus R (A × B) pab
inst_25 : NonUnitalContinuousFunctionalCalculus R A pa
inst_26 : NonUnitalContinuousFunctionalCalculus R B pb
inst_27 : ContinuousMapZero.UniqueHom R A
inst_28 : 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
⊢ cfcₙ (p := pab) f (a, b) = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b)

Tactic:
case neg =>
    simp [cfcₙ_apply_of_not_map_zero _ hf₀, eqComm]

Premises used: cfcₙ_apply_of_not_map_zero, eqComm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : CommRing S
inst_6 : Algebra R S
inst_7 : (i : ι) → Ring (A i)
inst_8 : (i : ι) → Algebra.{u_3, u_4} S (A i)
inst_9 : (i : ι) → Algebra.{u_2, u_4} R (A i)
inst_10 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R S (A i)
hinst : IsScalarTower R S ((i : ι) → A i)
inst_11 : (i : ι) → StarRing (A i)
inst_12 : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst_13 : ContinuousFunctionalCalculus R ((i : ι) → A i) p
inst_14 : ∀ (i : ι), ContinuousFunctionalCalculus R (A i) (q i)
inst_15 : ∀ (i : ι), ContinuousMap.UniqueHom.{u_2, u_4} 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)
h : ∀ (i : ι), cfc (p := p) f a i = cfc (p := q i) f (a i)
⊢ cfc (p := p) f a = fun (i : ι) ↦ cfc (p := q i) f (a i)

Tactic:
ext i
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : CommRing S
inst_6 : Algebra R S
inst_7 : (i : ι) → Ring (A i)
inst_8 : (i : ι) → Algebra.{u_3, u_4} S (A i)
inst_9 : (i : ι) → Algebra.{u_2, u_4} R (A i)
inst_10 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R S (A i)
hinst : IsScalarTower R S ((i : ι) → A i)
inst_11 : (i : ι) → StarRing (A i)
inst_12 : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst_13 : ContinuousFunctionalCalculus R ((i : ι) → A i) p
inst_14 : ∀ (i : ι), ContinuousFunctionalCalculus R (A i) (q i)
inst_15 : ∀ (i : ι), ContinuousMap.UniqueHom.{u_2, u_4} 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
rwa rwa₁ rwa₂ rwa₃ : ContinuousOn f (⋃ (i : ι), spectrum R (a i))
⊢ ContinuousOn f (spectrum R a)

Tactic:
rwa [Pi.spectrum_eq]

Premises used: Pi.spectrum_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : CommRing S
inst_6 : Algebra R S
inst_7 : (i : ι) → Ring (A i)
inst_8 : (i : ι) → Algebra.{u_3, u_4} S (A i)
inst_9 : (i : ι) → Algebra.{u_2, u_4} R (A i)
inst_10 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R S (A i)
hinst : IsScalarTower R S ((i : ι) → A i)
inst_11 : (i : ι) → StarRing (A i)
inst_12 : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst_13 : ContinuousFunctionalCalculus R ((i : ι) → A i) p
inst_14 : ∀ (i : ι), ContinuousFunctionalCalculus R (A i) (q i)
inst_15 : ∀ (i : ι), ContinuousMap.UniqueHom.{u_2, u_4} 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
⊢ cfc (p := p) f a i = cfc (p := q i) f (a i)

Tactic:
exact φ.map_cfc f a (by rwa [Pi.spectrum_eq]) (continuous_apply i) ha (ha' i)

Premises used: StarAlgHom.map_cfc, continuous_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
Goal:
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : CommRing S
inst_6 : Algebra R S
inst_7 : Ring A
inst_8 : Ring B
inst_9 : Algebra S A
inst_10 : Algebra S B
inst_11 : Algebra R A
inst_12 : Algebra R B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
inst_15 : StarRing A
inst_16 : StarRing B
inst_17 : TopologicalSpace A
inst_18 : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst_19 : ContinuousFunctionalCalculus R (A × B) pab
inst_20 : ContinuousFunctionalCalculus R A pa
inst_21 : ContinuousFunctionalCalculus R B pb
inst_22 : ContinuousMap.UniqueHom R A
inst_23 : 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
ext : (cfc (p := pab) f (a, b)).1 = (cfc (p := pa) f a, cfc (p := pb) f b).1
ext₁ : (cfc (p := pab) f (a, b)).2 = (cfc (p := pa) f a, cfc (p := pb) f b).2
⊢ cfc (p := pab) f (a, b) = (cfc (p := pa) f a, cfc (p := pb) f b)

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
Goal:
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : CommRing S
inst_6 : Algebra R S
inst_7 : Ring A
inst_8 : Ring B
inst_9 : Algebra S A
inst_10 : Algebra S B
inst_11 : Algebra R A
inst_12 : Algebra R B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
inst_15 : StarRing A
inst_16 : StarRing B
inst_17 : TopologicalSpace A
inst_18 : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst_19 : ContinuousFunctionalCalculus R (A × B) pab
inst_20 : ContinuousFunctionalCalculus R A pa
inst_21 : ContinuousFunctionalCalculus R B pb
inst_22 : ContinuousMap.UniqueHom R A
inst_23 : 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
rwa rwa₁ rwa₂ rwa₃ : ContinuousOn f (spectrum R a ∪ spectrum R b)
⊢ ContinuousOn f (spectrum R (a, b))

Tactic:
rwa [Prod.spectrum_eq]

Premises used: Prod.spectrum_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
Goal:
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : CommRing S
inst_6 : Algebra R S
inst_7 : Ring A
inst_8 : Ring B
inst_9 : Algebra S A
inst_10 : Algebra S B
inst_11 : Algebra R A
inst_12 : Algebra R B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
inst_15 : StarRing A
inst_16 : StarRing B
inst_17 : TopologicalSpace A
inst_18 : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst_19 : ContinuousFunctionalCalculus R (A × B) pab
inst_20 : ContinuousFunctionalCalculus R A pa
inst_21 : ContinuousFunctionalCalculus R B pb
inst_22 : ContinuousMap.UniqueHom R A
inst_23 : 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
⊢ (cfc (p := pab) f (a, b)).1 = (cfc (p := pa) f a, cfc (p := pb) f b).1

Tactic:
exact φ.map_cfc f (a, b) (by rwa [Prod.spectrum_eq]) continuous_fst hab ha

Premises used: StarAlgHom.map_cfc, continuous_fst, Prod.mk
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
Goal:
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : CommRing S
inst_6 : Algebra R S
inst_7 : Ring A
inst_8 : Ring B
inst_9 : Algebra S A
inst_10 : Algebra S B
inst_11 : Algebra R A
inst_12 : Algebra R B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
inst_15 : StarRing A
inst_16 : StarRing B
inst_17 : TopologicalSpace A
inst_18 : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst_19 : ContinuousFunctionalCalculus R (A × B) pab
inst_20 : ContinuousFunctionalCalculus R A pa
inst_21 : ContinuousFunctionalCalculus R B pb
inst_22 : ContinuousMap.UniqueHom R A
inst_23 : 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 (p := pab) f (a, b)).1 = (cfc (p := pa) f a, cfc (p := pb) f b).1

Tactic:
case fst =>
    let φ := StarAlgHom.fst S A B
    exact φ.map_cfc f (a, b) (by rwa [Prod.spectrum_eq]) continuous_fst hab ha
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
Goal:
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : CommRing S
inst_6 : Algebra R S
inst_7 : Ring A
inst_8 : Ring B
inst_9 : Algebra S A
inst_10 : Algebra S B
inst_11 : Algebra R A
inst_12 : Algebra R B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
inst_15 : StarRing A
inst_16 : StarRing B
inst_17 : TopologicalSpace A
inst_18 : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst_19 : ContinuousFunctionalCalculus R (A × B) pab
inst_20 : ContinuousFunctionalCalculus R A pa
inst_21 : ContinuousFunctionalCalculus R B pb
inst_22 : ContinuousMap.UniqueHom R A
inst_23 : 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
rwa rwa₁ rwa₂ rwa₃ : ContinuousOn f (spectrum R a ∪ spectrum R b)
⊢ ContinuousOn f (spectrum R (a, b))

Tactic:
rwa [Prod.spectrum_eq]

Premises used: Prod.spectrum_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
Goal:
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : CommRing S
inst_6 : Algebra R S
inst_7 : Ring A
inst_8 : Ring B
inst_9 : Algebra S A
inst_10 : Algebra S B
inst_11 : Algebra R A
inst_12 : Algebra R B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
inst_15 : StarRing A
inst_16 : StarRing B
inst_17 : TopologicalSpace A
inst_18 : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst_19 : ContinuousFunctionalCalculus R (A × B) pab
inst_20 : ContinuousFunctionalCalculus R A pa
inst_21 : ContinuousFunctionalCalculus R B pb
inst_22 : ContinuousMap.UniqueHom R A
inst_23 : 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
⊢ (cfc (p := pab) f (a, b)).2 = (cfc (p := pa) f a, cfc (p := pb) f b).2

Tactic:
exact φ.map_cfc f (a, b) (by rwa [Prod.spectrum_eq]) continuous_snd hab hb

Premises used: StarAlgHom.map_cfc, continuous_snd, Prod.mk
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
Goal:
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : CommRing S
inst_6 : Algebra R S
inst_7 : Ring A
inst_8 : Ring B
inst_9 : Algebra S A
inst_10 : Algebra S B
inst_11 : Algebra R A
inst_12 : Algebra R B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
inst_15 : StarRing A
inst_16 : StarRing B
inst_17 : TopologicalSpace A
inst_18 : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst_19 : ContinuousFunctionalCalculus R (A × B) pab
inst_20 : ContinuousFunctionalCalculus R A pa
inst_21 : ContinuousFunctionalCalculus R B pb
inst_22 : ContinuousMap.UniqueHom R A
inst_23 : 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
case case₁ case₂ : (cfc (p := pab) f (a, b)).2 = (cfc (p := pa) f a, cfc (p := pb) f b).2
⊢ (cfc (p := pab) f (a, b)).2 = (cfc (p := pa) f a, cfc (p := pb) f b).2

Tactic:
case snd =>
    let φ := StarAlgHom.snd S A B
    exact φ.map_cfc f (a, b) (by rwa [Prod.spectrum_eq]) continuous_snd hab hb
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Field R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : Module R A
inst_9 : IsScalarTower R A A
inst_10 : SMulCommClass R A A
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ IsIdempotentElem a ↔ quasispectrum R a ⊆ {0, 1}

Tactic:
⟨IsIdempotentElem.quasispectrum_subset R, fun h ↦ ?_⟩

Premises used: Iff.intro, IsIdempotentElem.quasispectrum_subset
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Field R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : Module R A
inst_9 : IsScalarTower R A A
inst_10 : SMulCommClass R A A
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
refine : ∀ (h : quasispectrum R a ⊆ {0, 1}), IsIdempotentElem a
⊢ IsIdempotentElem a ↔ quasispectrum R a ⊆ {0, 1}

Tactic:
refine ⟨IsIdempotentElem.quasispectrum_subset R, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Field R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : Module R A
inst_9 : IsScalarTower R A A
inst_10 : SMulCommClass R A A
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
h : quasispectrum R a ⊆ {0, 1}
rw : cfcₙ (p := p) (fun (x : R) ↦ x * x) a = cfcₙ (p := p) (fun (x : R) ↦ x) a
⊢ IsIdempotentElem a

Tactic:
rw [IsIdempotentElem, ← cfcₙ_id' R a, ← cfcₙ_mul _ _]

Premises used: cfcₙ_id', IsIdempotentElem, cfcₙ_mul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Field R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : Module R A
inst_9 : IsScalarTower R A A
inst_10 : SMulCommClass R A A
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
h : quasispectrum R a ⊆ {0, 1}
x : R
hx : x ∈ quasispectrum R a
⊢ x * x = x

Tactic:
grind
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Field R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : Module R A
inst_9 : IsScalarTower R A A
inst_10 : SMulCommClass R A A
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
h : quasispectrum R a ⊆ {0, 1}
⊢ cfcₙ (p := p) (fun (x : R) ↦ x * x) a = cfcₙ (p := p) (fun (x : R) ↦ x) a

Tactic:
exact cfcₙ_congr fun x hx ↦ by grind

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Field R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ IsIdempotentElem a ↔ spectrum R a ⊆ {0, 1}

Tactic:
grind [quasispectrum_eq_spectrum_union_zero, isIdempotentElem_iff_quasispectrum_subset R]

Premises used: isIdempotentElem_iff_quasispectrum_subset, quasispectrum_eq_spectrum_union_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℝ A
inst_4 : IsScalarTower ℝ A A
inst_5 : SMulCommClass ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
x : A
⊢ IsIdempotentElem (star x * x) ↔ IsIdempotentElem (x * star x)

Tactic:
simp [isIdempotentElem_iff_quasispectrum_subset ℝ, quasispectrum.mul_comm]

Premises used: Real, isIdempotentElem_iff_quasispectrum_subset, quasispectrum.mul_comm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
a : A
ha : p a
rw :
  Eq (α := StarSubalgebra 𝕜 A)
    (StarSubalgebra.topologicalClosure
      (adjoin 𝕜
        (Set.image (α := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
          (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
          {ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)})))
    (elemental 𝕜 a)
⊢ Eq (α := StarSubalgebra 𝕜 A) (StarAlgHom.range (A := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) (cfcHom (p := p) ha))
    (elemental 𝕜 a)

Tactic:
rw [StarAlgHom.range_eq_map_top, ← ContinuousMap.elemental_id_eq_top, StarAlgebra.elemental,
    ← StarSubalgebra.topologicalClosure_map _ _ (cfcHom_isClosedEmbedding ha (R := 𝕜)).isClosedMap
      (cfcHom_continuous ha), StarAlgHom.map_adjoin]

Premises used: cfcHom_continuous, cfcHom_isClosedEmbedding, Topology.IsClosedEmbedding.isClosedMap, StarAlgebra.elemental, StarSubalgebra.topologicalClosure_map, StarAlgHom.range_eq_map_top, ContinuousMap.elemental_id_eq_top, StarAlgHom.map_adjoin
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
a : A
ha : p a
e_s :
  Eq (α := Set A)
    (Set.image (α := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
      (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      {ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)})
    {a}
⊢ Eq (α := StarSubalgebra 𝕜 A)
    (StarSubalgebra.topologicalClosure
      (adjoin 𝕜
        (Set.image (α := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
          (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
          {ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)})))
    (elemental 𝕜 a)

Tactic:
congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
a : A
ha : p a
⊢ Eq (α := Set A)
    (Set.image (α := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
      (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      {ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)})
    {a}

Tactic:
simpa using cfcHom_id ha

Premises used: cfcHom_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
a : A
ha : p a
rw :
  (↑(StarAlgHom.range (A := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) (cfcHom (p := p) ha)) : Set A) =
    (↑(elemental 𝕜 a) : Set A)
rw₁ rw₂ : (↑(elemental 𝕜 a) : Set A) = (↑(elemental 𝕜 a) : Set A)
⊢ (Set.range fun (x : 𝕜 → 𝕜) ↦ cfc (p := p) x a) = (↑(elemental 𝕜 a) : Set A)

Tactic:
rw [range_cfc_eq_range_cfcHom 𝕜 ha, range_cfcHom 𝕜 ha]

Premises used: range_cfc_eq_range_cfcHom, range_cfcHom
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
a : A
ha : p a
grw :
  LE.le (α := StarSubalgebra 𝕜 A)
    (StarSubalgebra.topologicalClosure
      (adjoin 𝕜
        (Set.image (α := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
          (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
          {ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)})))
    (elemental 𝕜 a)
⊢ LE.le (α := StarSubalgebra 𝕜 A) (StarAlgHom.range (A := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) (cfcHom (p := p) ha))
    (elemental 𝕜 a)

Tactic:
grw [StarAlgHom.range_eq_map_top, ← ContinuousMap.elemental_id_eq_top, StarAlgebra.elemental,
    StarSubalgebra.map_topologicalClosure_le _ _ (cfcHom_continuous ha (R := 𝕜)),
    StarAlgHom.map_adjoin]

Premises used: cfcHom_continuous, StarAlgebra.elemental, StarAlgHom.range_eq_map_top, StarSubalgebra.map_topologicalClosure_le, ContinuousMap.elemental_id_eq_top, StarAlgHom.map_adjoin
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
a : A
ha : p a
⊢ LE.le (α := StarSubalgebra 𝕜 A)
    (StarSubalgebra.topologicalClosure
      (adjoin 𝕜
        (Set.image (α := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
          (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
          {ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)})))
    (elemental 𝕜 a)

Tactic:
simp [cfcHom_id ha, elemental]

Premises used: cfcHom_id, StarAlgebra.elemental
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
a : A
ha : p a
grw :
  (↑(StarAlgHom.range (A := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) (cfcHom (p := p) ha)) : Set A) ⊆
    (↑(elemental 𝕜 a) : Set A)
grw₁ grw₂ : (↑(elemental 𝕜 a) : Set A) ⊆ (↑(elemental 𝕜 a) : Set A)
⊢ (Set.range fun (x : 𝕜 → 𝕜) ↦ cfc (p := p) x a) ⊆ (↑(elemental 𝕜 a) : Set A)

Tactic:
grw [range_cfc_eq_range_cfcHom 𝕜 ha, range_cfcHom_le 𝕜 ha]

Premises used: range_cfc_eq_range_cfcHom, range_cfcHom_le