awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
f : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜
ι : C((↑(σ 𝕜 a) : Type u_1), (↑(σₙ 𝕜 a) : Type u_1)) :=
  { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) ⋯, continuous_toFun := ⋯ }
hx : 0 ∈ σₙ 𝕜 a
inl :
  norm (E := 𝕜) ((f : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜) 0 : 𝕜) ≤
    norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι)
⊢ norm (E := 𝕜)
      (((↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
          (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σₙ 𝕜 a) 0 hx) :
        𝕜) ≤
    norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι)

Tactic:
change ‖f 0‖ ≤ _

Premises used: OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
f : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜
ι : C((↑(σ 𝕜 a) : Type u_1), (↑(σₙ 𝕜 a) : Type u_1)) :=
  { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) ⋯, continuous_toFun := ⋯ }
hx : 0 ∈ σₙ 𝕜 a
⊢ norm (E := 𝕜) ((f : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜) 0 : 𝕜) ≤
    norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
f : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜
ι : C((↑(σ 𝕜 a) : Type u_1), (↑(σₙ 𝕜 a) : Type u_1)) :=
  { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) ⋯, continuous_toFun := ⋯ }
x : 𝕜
hx : x ∈ σₙ 𝕜 a
hx' : x ∈ σ 𝕜 a
⊢ norm (E := 𝕜)
      (((↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
          (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σₙ 𝕜 a) x hx) :
        𝕜) ≤
    norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι)

Tactic:
(f : C(σₙ 𝕜 a, 𝕜)).comp ι |>.norm_coe_le_norm ⟨x, hx'⟩

Premises used: ContinuousMap.norm_coe_le_norm, Set.Mem, ContinuousMap.comp, toContinuousMap, Subtype.mk
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
f : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜
ι : C((↑(σ 𝕜 a) : Type u_1), (↑(σₙ 𝕜 a) : Type u_1)) :=
  { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) ⋯, continuous_toFun := ⋯ }
x : 𝕜
hx : x ∈ σₙ 𝕜 a
hx' : x ∈ σ 𝕜 a
⊢ norm (E := 𝕜)
      (((↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
          (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σₙ 𝕜 a) x hx) :
        𝕜) ≤
    norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι)

Tactic:
exact (f : C(σₙ 𝕜 a, 𝕜)).comp ι |>.norm_coe_le_norm ⟨x, hx'⟩

Premises used: ContinuousMap.norm_coe_le_norm, ContinuousMap.comp, toContinuousMap, Subtype.mk
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : Nontrivial R
a : A
⊢ Fact (0 ∈ σₙ R a)

Tactic:
⟨quasispectrum.zero_mem R a⟩

Premises used: quasispectrum.zero_mem, Fact.mk
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
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 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
⊢ IsCompact (σₙ R a)

Tactic:
isCompact_iff_compactSpace.mpr inferInstance

Premises used: Iff.mpr, isCompact_iff_compactSpace, inferInstance
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
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 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : UniqueHom R A
a : A
inst_13 : CompactSpace.{u_1} (↑(σₙ R a) : Type u_1)
φ ψ : C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A
hφ : Continuous[_, inst_8] (⇑φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
hψ : Continuous[_, inst_8] (⇑ψ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
h :
  Eq.{u_2 + 1} (α := A)
    ((φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀) : A)
    ((ψ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀) : A)
⊢ φ = ψ

Tactic:
UniqueHom.eq_of_continuous_of_map_id _ φ ψ hφ hψ h

Premises used: ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
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 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ Continuous[_, inst_8] (⇑(cfcₙHom (p := p) ha) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
(NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose_spec.1

Premises used: Exists.choose_spec, And.left, NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
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 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := C((↑(σₙ R a) : Type u_1), R)₀) (β := A)
    (⇑(cfcₙHom (p := p) ha) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
(NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose_spec.2.1

Premises used: Exists.choose_spec, And.right, And.left, NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
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 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀) =
    a

Tactic:
(NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose_spec.2.2.1

Premises used: Exists.choose_spec, ContinuousMapZero.id, And.right, And.left, NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
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 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
⊢ quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A) =
    Set.range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)

Tactic:
(NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose_spec.2.2.2.1 f

Premises used: Exists.choose_spec, And.right, And.left, NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
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 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
⊢ p ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)

Tactic:
(NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose_spec.2.2.2.2 f

Premises used: Exists.choose_spec, And.right, NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
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 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
inst_12 : UniqueHom R A
φ : C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A
hφ₁ : Continuous[_, inst_8] (⇑φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
hφ₂ : (φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀) = a
rw : a = (φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀)
rw₁ rw₂ : a = a
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀) :
      A)
    ((φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀) : A)

Tactic:
rw [cfcₙHom_id ha, hφ₂]

Premises used: cfcₙHom_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
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 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
inst_12 : UniqueHom R A
f : C((↑(σₙ R a) : Type u_1), R)₀
f' :
  C((↑(σₙ R a) : Type u_1),
    (↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1))₀
hff' :
  ∀ (x : (↑(σₙ R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(σₙ R a) : Type u_1)) →
                  (↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀
ψ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  C((↑(σₙ R a) : Type u_1), R)₀ :=
  {
    toFun :=
      fun
        (x :
          C((↑(quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
              Type u_1),
            R)₀) ↦
      x.comp f',
    map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  A :=
  NonUnitalStarAlgHom.comp (cfcₙHom (p := p) ha) ψ
suffices : cfcₙHom (p := p) ⋯ = φ
⊢ Eq.{u_2 + 1} (α := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) (g.comp f') : A)
    ((cfcₙHom (p := p) ⋯ :
          (a : C((↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1), R)₀) → A)
        g :
      A)

Tactic:
suffices cfcₙHom (cfcₙHom_predicate ha f) = φ from DFunLike.congr_fun this.symm g
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
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 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
inst_12 : UniqueHom R A
f : C((↑(σₙ R a) : Type u_1), R)₀
f' :
  C((↑(σₙ R a) : Type u_1),
    (↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1))₀
hff' :
  ∀ (x : (↑(σₙ R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(σₙ R a) : Type u_1)) →
                  (↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀
ψ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  C((↑(σₙ R a) : Type u_1), R)₀ :=
  {
    toFun :=
      fun
        (x :
          C((↑(quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
              Type u_1),
            R)₀) ↦
      x.comp f',
    map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  A :=
  NonUnitalStarAlgHom.comp (cfcₙHom (p := p) ha) ψ
⊢ cfcₙHom (p := p) ⋯ = φ

Tactic:
cfcₙHom_eq_of_continuous_of_map_id (cfcₙHom_predicate ha f) φ ?_ ?_

Premises used: cfcₙHom_predicate, cfcₙHom_eq_of_continuous_of_map_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
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 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
inst_12 : UniqueHom R A
f : C((↑(σₙ R a) : Type u_1), R)₀
f' :
  C((↑(σₙ R a) : Type u_1),
    (↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1))₀
hff' :
  ∀ (x : (↑(σₙ R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(σₙ R a) : Type u_1)) →
                  (↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀
ψ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  C((↑(σₙ R a) : Type u_1), R)₀ :=
  {
    toFun :=
      fun
        (x :
          C((↑(quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
              Type u_1),
            R)₀) ↦
      x.comp f',
    map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  A :=
  NonUnitalStarAlgHom.comp (cfcₙHom (p := p) ha) ψ
refine_1 :
  Continuous[_, inst_8]
    (⇑φ : (a : C((↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1), R)₀) → A)
refine_2 :
  Eq.{u_2 + 1} (α := A)
    ((φ : (a : C((↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1), R)₀) → A)
        (ContinuousMapZero.id
            (quasispectrum.{u_1, u_2} R (A := A)
              ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
          C((↑(quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
              Type u_1),
            R)₀) :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)
⊢ cfcₙHom (p := p) ⋯ = φ

Tactic:
refine cfcₙHom_eq_of_continuous_of_map_id (cfcₙHom_predicate ha f) φ ?_ ?_

Premises used: cfcₙHom_predicate, cfcₙHom_eq_of_continuous_of_map_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
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 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
inst_12 : UniqueHom R A
f : C((↑(σₙ R a) : Type u_1), R)₀
f' :
  C((↑(σₙ R a) : Type u_1),
    (↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1))₀
hff' :
  ∀ (x : (↑(σₙ R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(σₙ R a) : Type u_1)) →
                  (↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀
ψ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  C((↑(σₙ R a) : Type u_1), R)₀ :=
  {
    toFun :=
      fun
        (x :
          C((↑(quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
              Type u_1),
            R)₀) ↦
      x.comp f',
    map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  A :=
  NonUnitalStarAlgHom.comp (cfcₙHom (p := p) ha) ψ
⊢ Continuous[_, inst_8]
    (⇑φ : (a : C((↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1), R)₀) → A)

Tactic:
(cfcₙHom_continuous ha).comp <| continuous_induced_rng.mpr ?_

Premises used: Iff.mpr, Continuous.comp, cfcₙHom_continuous, continuous_induced_rng
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
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 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
inst_12 : UniqueHom R A
f : C((↑(σₙ R a) : Type u_1), R)₀
f' :
  C((↑(σₙ R a) : Type u_1),
    (↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1))₀
hff' :
  ∀ (x : (↑(σₙ R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(σₙ R a) : Type u_1)) →
                  (↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀
ψ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  C((↑(σₙ R a) : Type u_1), R)₀ :=
  {
    toFun :=
      fun
        (x :
          C((↑(quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
              Type u_1),
            R)₀) ↦
      x.comp f',
    map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  A :=
  NonUnitalStarAlgHom.comp (cfcₙHom (p := p) ha) ψ
refine_1 :
  Continuous (X :=
    C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
        Type u_1),
      R)₀)
    (Y := C((↑(σₙ R a) : Type u_1), R))
    (Function.comp (β := C((↑(σₙ R a) : Type u_1), R)₀) _root_.toContinuousMap
      (⇑(↑ψ.toNonUnitalAlgHom :
            C((↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1), R)₀ →ₙ*
              C((↑(σₙ R a) : Type u_1), R)₀) :
        (a_1 : C((↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1), R)₀) →
          C((↑(σₙ R a) : Type u_1), R)₀))
⊢ Continuous[_, inst_8]
    (⇑φ : (a : C((↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1), R)₀) → A)

Tactic:
refine (cfcₙHom_continuous ha).comp <| continuous_induced_rng.mpr ?_

Premises used: Iff.mpr, Continuous.comp, cfcₙHom_continuous, continuous_induced_rng