awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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
⊢ 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)
have rw : a = (φ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) (ContinuousMapZero.id (σₙ R a) : C((↑(σₙ R a) : Type u_1), R)₀)
Tactic: rw [cfcₙHom_id ha, hφ₂]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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)₀)
⊢ 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)
have rw₁ : a = a
Tactic: rw [cfcₙHom_id ha, hφ₂]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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) ψ
⊢ 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)
have suffices : cfcₙHom (p := p) sorry = φ
Tactic: suffices cfcₙHom (cfcₙHom_predicate ha f) = φ from DFunLike.congr_fun this.symm g
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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) ⋯ = φ
have 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)
Tactic: refine cfcₙHom_eq_of_continuous_of_map_id (cfcₙHom_predicate ha f) φ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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)
⊢ cfcₙHom (p := p) ⋯ = φ
have 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)
Tactic: refine cfcₙHom_eq_of_continuous_of_map_id (cfcₙHom_predicate ha f) φ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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)
have 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)₀))
Tactic: refine (cfcₙHom_continuous ha).comp <| continuous_induced_rng.mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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) ψ
⊢ 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)
have refine_2 : Eq.{u_2 + 1} (α := A)
  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      (comp
        (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)))
        f') :
    A)
  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)
Tactic: simp only [φ, ψ, NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_mk',
      NonUnitalAlgHom.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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) ψ
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (comp
          (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)))
          f') :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)
have refine_2 : comp
    (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)))
    f' =
  f
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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) ψ
⊢ comp
      (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)))
      f' =
    f
have refine_2 : ∀ (x : (↑(σₙ R a) : Type u_1)),
  Eq (α := R)
    ((comp
            (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)))
            f' :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        x :
      R)
    ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
⊢ cfcₙ (p := p) f a =
    (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := hf0 }
have rw : Eq.{u_2 + 1} (α := A)
  (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
      (cfcₙHom (p := p) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry }
    else 0 :
    A)
  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := hf0 } :
    A)
Tactic: rw [cfcₙ_def, dif_pos ⟨ha, hf, hf0⟩]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
        (cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }
      else 0 :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := hf0 } :
      A)
⊢ cfcₙ (p := p) f a =
    (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := hf0 }
have rw₁ : Eq.{u_2 + 1} (α := A)
  ((cfcₙHom (p := p) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry } :
    A)
  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := hf0 } :
    A)
Tactic: rw [cfcₙ_def, dif_pos ⟨ha, hf, hf0⟩]