awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha₀ : 0 ≤ a
ha₁ : ∀ x ∈ spectrum ℝ a, x ≤ 1
n m : ℕ
hnm : n ≤ m
x : ℝ
hx : x ∈ spectrum ℝ a
this : x ≤ 1
⊢ x ^ m ≤ x ^ n

Tactic:
pow_le_pow_of_le_one (spectrum_nonneg_of_nonneg ha₀ hx) (ha₁ x hx) hnm

Premises used: pow_le_pow_of_le_one, spectrum_nonneg_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha₀ : 0 ≤ a
ha₁ : ∀ x ∈ spectrum ℝ a, x ≤ 1
n m : ℕ
hnm : n ≤ m
x : ℝ
hx : x ∈ spectrum ℝ a
this : x ≤ 1
⊢ x ^ m ≤ x ^ n

Tactic:
exact pow_le_pow_of_le_one (spectrum_nonneg_of_nonneg ha₀ hx) (ha₁ x hx) hnm

Premises used: pow_le_pow_of_le_one, spectrum_nonneg_of_nonneg
-- 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 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : (i : ι) → NonUnitalRing (A i)
inst_9 : (i : ι) → Module.{u_3, u_4} S (A i)
inst_10 : (i : ι) → Module.{u_2, u_4} R (A i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R S (A i)
inst_12 : ∀ (i : ι), SMulCommClass.{u_2, u_4, u_4} R (A i) (A i)
inst_13 : ∀ (i : ι), IsScalarTower.{u_2, u_4, u_4} R (A i) (A i)
inst_14 : (i : ι) → StarRing (A i)
inst_15 : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst_16 : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst_17 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst_18 : ∀ (i : ι), ContinuousMapZero.UniqueHom.{u_2, u_4} 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)
pos : ∀ (hf₀ : f 0 = 0), cfcₙ (p := p) f a = fun (i : ι) ↦ cfcₙ (p := q i) f (a i)
neg : ∀ (hf₀ : ¬f 0 = 0), cfcₙ (p := p) f a = fun (i : ι) ↦ cfcₙ (p := q i) f (a i)
⊢ cfcₙ (p := p) f a = fun (i : ι) ↦ cfcₙ (p := q i) f (a i)

Tactic:
by_cases hf₀ : f 0 = 0

Premises used: OfNat.ofNat
-- 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 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : (i : ι) → NonUnitalRing (A i)
inst_9 : (i : ι) → Module.{u_3, u_4} S (A i)
inst_10 : (i : ι) → Module.{u_2, u_4} R (A i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R S (A i)
inst_12 : ∀ (i : ι), SMulCommClass.{u_2, u_4, u_4} R (A i) (A i)
inst_13 : ∀ (i : ι), IsScalarTower.{u_2, u_4, u_4} R (A i) (A i)
inst_14 : (i : ι) → StarRing (A i)
inst_15 : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst_16 : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst_17 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst_18 : ∀ (i : ι), ContinuousMapZero.UniqueHom.{u_2, u_4} 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
pos : ∀ (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 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : (i : ι) → NonUnitalRing (A i)
inst_9 : (i : ι) → Module.{u_3, u_4} S (A i)
inst_10 : (i : ι) → Module.{u_2, u_4} R (A i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R S (A i)
inst_12 : ∀ (i : ι), SMulCommClass.{u_2, u_4, u_4} R (A i) (A i)
inst_13 : ∀ (i : ι), IsScalarTower.{u_2, u_4, u_4} R (A i) (A i)
inst_14 : (i : ι) → StarRing (A i)
inst_15 : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst_16 : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst_17 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst_18 : ∀ (i : ι), ContinuousMapZero.UniqueHom.{u_2, u_4} 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 : ι
⊢ Nonempty ι

Tactic:
have : Nonempty ι := ⟨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 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : (i : ι) → NonUnitalRing (A i)
inst_9 : (i : ι) → Module.{u_3, u_4} S (A i)
inst_10 : (i : ι) → Module.{u_2, u_4} R (A i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R S (A i)
inst_12 : ∀ (i : ι), SMulCommClass.{u_2, u_4, u_4} R (A i) (A i)
inst_13 : ∀ (i : ι), IsScalarTower.{u_2, u_4, u_4} R (A i) (A i)
inst_14 : (i : ι) → StarRing (A i)
inst_15 : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst_16 : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst_17 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst_18 : ∀ (i : ι), ContinuousMapZero.UniqueHom.{u_2, u_4} 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
rwa rwa₁ rwa₂ rwa₃ : ContinuousOn f (⋃ (i : ι), quasispectrum R (a i))
⊢ ContinuousOn f (quasispectrum R a)

Tactic:
rwa [Pi.quasispectrum_eq]

Premises used: Pi.quasispectrum_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 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : (i : ι) → NonUnitalRing (A i)
inst_9 : (i : ι) → Module.{u_3, u_4} S (A i)
inst_10 : (i : ι) → Module.{u_2, u_4} R (A i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R S (A i)
inst_12 : ∀ (i : ι), SMulCommClass.{u_2, u_4, u_4} R (A i) (A i)
inst_13 : ∀ (i : ι), IsScalarTower.{u_2, u_4, u_4} R (A i) (A i)
inst_14 : (i : ι) → StarRing (A i)
inst_15 : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst_16 : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst_17 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst_18 : ∀ (i : ι), ContinuousMapZero.UniqueHom.{u_2, u_4} 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
⊢ cfcₙ (p := p) f a i = cfcₙ (p := q i) f (a i)

Tactic:
exact φ.map_cfcₙ f a (by rwa [Pi.quasispectrum_eq]) hf₀ (continuous_apply i) ha (ha' i)

Premises used: NonUnitalStarAlgHom.map_cfcₙ, continuous_apply
-- 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 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : (i : ι) → NonUnitalRing (A i)
inst_9 : (i : ι) → Module.{u_3, u_4} S (A i)
inst_10 : (i : ι) → Module.{u_2, u_4} R (A i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R S (A i)
inst_12 : ∀ (i : ι), SMulCommClass.{u_2, u_4, u_4} R (A i) (A i)
inst_13 : ∀ (i : ι), IsScalarTower.{u_2, u_4, u_4} R (A i) (A i)
inst_14 : (i : ι) → StarRing (A i)
inst_15 : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst_16 : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst_17 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst_18 : ∀ (i : ι), ContinuousMapZero.UniqueHom.{u_2, u_4} 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
⊢ cfcₙ (p := p) f a = fun (i : ι) ↦ cfcₙ (p := q i) f (a i)

Tactic:
simp only [cfcₙ_apply_of_not_map_zero _ hf₀, Pi.zero_def]

Premises used: cfcₙ_apply_of_not_map_zero, Pi.zero_def
-- 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
by_cases : ∀ (hf₀ : f 0 = 0), cfcₙ (p := pab) f (a, b) = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b)
by_cases₁ : ∀ (hf₀ : ¬f 0 = 0), cfcₙ (p := pab) f (a, b) = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b)
⊢ cfcₙ (p := pab) f (a, b) = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b)

Tactic:
by_cases hf₀ : f 0 = 0

Premises used: OfNat.ofNat
-- 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
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 : 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
φ : A × B →⋆ₙₐ[S] A := NonUnitalStarAlgHom.fst S A B
rwa rwa₁ rwa₂ rwa₃ : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
⊢ ContinuousOn f (quasispectrum R (a, b))

Tactic:
rwa [Prod.quasispectrum_eq]

Premises used: Prod.quasispectrum_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 : 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
φ : A × B →⋆ₙₐ[S] A := NonUnitalStarAlgHom.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.quasispectrum_eq]) hf₀ continuous_fst hab ha

Premises used: NonUnitalStarAlgHom.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 : 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)).1 = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b).1

Tactic:
case fst =>
      let φ := NonUnitalStarAlgHom.fst S A B
      exact φ.map_cfcₙ f (a, b) (by rwa [Prod.quasispectrum_eq]) hf₀ 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 : 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
φ : A × B →⋆ₙₐ[S] B := NonUnitalStarAlgHom.snd S A B
rwa rwa₁ rwa₂ rwa₃ : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
⊢ ContinuousOn f (quasispectrum R (a, b))

Tactic:
rwa [Prod.quasispectrum_eq]

Premises used: Prod.quasispectrum_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 : 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
φ : A × B →⋆ₙₐ[S] B := NonUnitalStarAlgHom.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.quasispectrum_eq]) hf₀ continuous_snd hab hb

Premises used: NonUnitalStarAlgHom.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 : 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
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 φ := NonUnitalStarAlgHom.snd S A B
      exact φ.map_cfcₙ f (a, b) (by rwa [Prod.quasispectrum_eq]) hf₀ continuous_snd hab hb
-- 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 pos =>
    ext
    case fst =>
      let φ := NonUnitalStarAlgHom.fst S A B
      exact φ.map_cfcₙ f (a, b) (by rwa [Prod.quasispectrum_eq]) hf₀ continuous_fst hab ha
    case snd =>
      let φ := NonUnitalStarAlgHom.snd S A B
      exact φ.map_cfcₙ f (a, b) (by rwa [Prod.quasispectrum_eq]) hf₀ continuous_snd hab hb
-- 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:
simp [cfcₙ_apply_of_not_map_zero _ hf₀, eqComm]

Premises used: cfcₙ_apply_of_not_map_zero, eqComm