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
⊢ cfcₙ (p := p) (fun (x : R) ↦ star x) a = star a
have rw : star (cfcₙ (p := p) (fun (x : R) ↦ x) a) = star a
Tactic: rw [cfcₙ_star _ a, cfcₙ_id' R a]
-- 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
rw : star (cfcₙ (p := p) (fun (x : R) ↦ x) a) = star a
⊢ cfcₙ (p := p) (fun (x : R) ↦ star x) a = star a
have rw₁ : star a = star a
Tactic: rw [cfcₙ_star _ a, cfcₙ_id' R a]
-- 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
⊢ (Set.range fun (x : R → R) ↦ cfcₙ (p := p) x a) =
    (↑(NonUnitalStarAlgHom.range (F := C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A) (cfcₙHom (p := p) ha)) : Set A)
have h : ∀ (x : A),
  Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfcₙ (p := p) x a) x ↔
    x ∈ (↑(NonUnitalStarAlgHom.range (F := C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A) (cfcₙHom (p := p) ha)) : Set A)
Tactic: ext
-- 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
x : A
⊢ Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfcₙ (p := p) x a) x ↔
    x ∈ (↑(NonUnitalStarAlgHom.range (F := C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A) (cfcₙHom (p := p) ha)) : Set A)
have h : Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfcₙ (p := p) x a) x →
  x ∈ (↑(NonUnitalStarAlgHom.range (F := C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A) (cfcₙHom (p := p) ha)) : Set A)
Tactic: constructor
-- 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
x : A
h :
  Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfcₙ (p := p) x a) x →
    x ∈ (↑(NonUnitalStarAlgHom.range (F := C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A) (cfcₙHom (p := p) ha)) : Set A)
⊢ Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfcₙ (p := p) x a) x ↔
    x ∈ (↑(NonUnitalStarAlgHom.range (F := C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A) (cfcₙHom (p := p) ha)) : Set A)
have h₁ : x ∈ (↑(NonUnitalStarAlgHom.range (F := C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A) (cfcₙHom (p := p) ha)) : Set A) →
  Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfcₙ (p := p) x a) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
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
inst_12 : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
⊢ cfcₙ (p := p) (g ∘ f) a = cfcₙ (p := p) g (cfcₙ (p := p) f a)
have this : ContinuousOn (g ∘ f) (σₙ R a)
Tactic: have := hg.comp hf <| (σₙ R a).mapsTo_image 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
inst_12 : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
⊢ quasispectrum.{u_1, u_2} R (A := A)
      ((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' := hf0 :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A) =
    f '' σₙ R a
have rw : Set.range (ι := (↑(σₙ R a) : Type u_1))
    (⇑{ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := hf0 } :
      (a : (↑(σₙ R a) : Type u_1)) → R) =
  f '' σₙ R a
Tactic: rw [cfcₙHom_map_quasispectrum (by exact ha) _]
-- 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
inst_12 : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
⊢ Set.range (ι := (↑(σₙ R a) : Type u_1))
      (⇑{ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := hf0 } :
        (a : (↑(σₙ R a) : Type u_1)) → R) =
    f '' σₙ R a
have h : ∀ (x : R),
  Membership.mem (γ := Set R)
      (Set.range (ι := (↑(σₙ R a) : Type u_1))
        (⇑{ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := hf0 } :
          (a : (↑(σₙ R a) : Type u_1)) → R))
      x ↔
    x ∈ f '' σₙ R a
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
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
inst_12 : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
⊢ cfcₙ (p := p) (g ∘ f) a = cfcₙ (p := p) g (cfcₙ (p := p) f a)
have sp_eq : quasispectrum.{u_1, u_2} R (A := 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' := hf0 :
          C((↑(σₙ R a) : Type u_1), R)₀ } :
      A) =
  f '' σₙ R a
Tactic: have sp_eq :
      σₙ R (cfcₙHom (show p a from ha) ⟨ContinuousMap.mk _ hf.restrict, hf0⟩) = f '' (σₙ R a) := by
    rw [cfcₙHom_map_quasispectrum (by exact ha) _]
    ext
    simp
-- 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
inst_12 : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq :
  quasispectrum.{u_1, u_2} R (A := A)
      ((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' := hf0 :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A) =
    f '' σₙ R a
⊢ cfcₙ (p := p) (g ∘ f) a = cfcₙ (p := p) g (cfcₙ (p := p) f a)
have rw : Eq.{u_2 + 1} (α := A)
  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (g ∘ f), continuous_toFun := sorry, map_zero' := sorry } :
    A)
  ((cfcₙHom (p := p) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      (comp
        {
          toFun :=
            (quasispectrum.{u_1, u_2} R (A := 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 :
                        C((↑(σₙ R a) : Type u_1), R)₀ } :
                    A)).restrict
              (π := fun (a : R) ↦ R) g,
          continuous_toFun := sorry, map_zero' := sorry }
        {
          toFun :=
            Set.codRestrict ((σₙ R a).restrict (π := fun (a : R) ↦ R) f)
              (quasispectrum.{u_1, u_2} R (A := 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))
              sorry,
          continuous_toFun := sorry, map_zero' := sorry }) :
    A)
Tactic: rw [cfcₙ_apply .., cfcₙ_apply f a,
    cfcₙ_apply _ _ (by convert! hg) (ha := cfcₙHom_predicate (show p a from ha) _),
    ← cfcₙHom_comp _ _]
-- 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
inst_12 : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq :
  quasispectrum.{u_1, u_2} R (A := A)
      ((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' := hf0 :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A) =
    f '' σₙ R a
rw :
  Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (g ∘ f), continuous_toFun := ⋯, map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (comp
          {
            toFun :=
              (quasispectrum.{u_1, u_2} R (A := A)
                    ((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' := ⋯ :
                          C((↑(σₙ R a) : Type u_1), R)₀ } :
                      A)).restrict
                (π := fun (a : R) ↦ R) g,
            continuous_toFun := ⋯, map_zero' := ⋯ }
          {
            toFun :=
              Set.codRestrict ((σₙ R a).restrict (π := fun (a : R) ↦ R) f)
                (quasispectrum.{u_1, u_2} R (A := A)
                  ((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' := ⋯ } :
                    A))
                ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ }) :
      A)
⊢ cfcₙ (p := p) (g ∘ f) a = cfcₙ (p := p) g (cfcₙ (p := p) f a)
have f' : C((↑(σₙ R a) : Type u_1),
  (↑(quasispectrum.{u_1, u_2} R (A := 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 :
              C((↑(σₙ R a) : Type u_1), R)₀ } :
          A)) :
    Type u_1))₀
Tactic: rw [cfcₙ_apply .., cfcₙ_apply f a,
    cfcₙ_apply _ _ (by convert! hg) (ha := cfcₙHom_predicate (show p a from ha) _),
    ← cfcₙHom_comp _ _]
-- 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
inst_12 : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq :
  quasispectrum.{u_1, u_2} R (A := A)
      ((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' := hf0 :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A) =
    f '' σₙ R a
x : (↑(σₙ R a) : Type u_1)
⊢ (σₙ R a).restrict (π := fun (a : R) ↦ R) f x ∈
    quasispectrum.{u_1, u_2} R (A := A)
      ((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' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A)
have rw : (σₙ R a).restrict (π := fun (a : R) ↦ R) f x ∈ f '' σₙ R a
Tactic: rw [sp_eq]
-- 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
inst_12 : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq :
  quasispectrum.{u_1, u_2} R (A := A)
      ((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' := hf0 :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A) =
    f '' σₙ R a
x : (↑(σₙ R a) : Type u_1)
⊢ (σₙ R a).restrict (π := fun (a : R) ↦ R) f x ∈ f '' σₙ R a
have h : (↑x : R) ∈ σₙ R a ∧ f (↑x : R) = (σₙ R a).restrict (π := fun (a : R) ↦ R) f x
Tactic: use x.1
-- 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
inst_12 : UniqueHom R A
S : Type u_3
inst_13 : SMulZeroClass S R
inst_14 : ContinuousConstSMul S R
inst_15 : SMulZeroClass S A
inst_16 : IsScalarTower S R A
inst_17 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f ((fun (x : R) ↦ s • x) '' σₙ R a)
hf0 : f 0 = 0
ha : p a
⊢ cfcₙ (p := p) (fun (x : R) ↦ f (s • x)) a = cfcₙ (p := p) f (s • a)
have rw : cfcₙ (p := p) f (cfcₙ (p := p) (fun (x : R) ↦ s • x) a) = cfcₙ (p := p) f (s • a)
Tactic: rw [cfcₙ_comp' f (s • ·) a, cfcₙ_smul_id s a]
-- 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
inst_12 : UniqueHom R A
S : Type u_3
inst_13 : SMulZeroClass S R
inst_14 : ContinuousConstSMul S R
inst_15 : SMulZeroClass S A
inst_16 : IsScalarTower S R A
inst_17 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f ((fun (x : R) ↦ s • x) '' σₙ R a)
hf0 : f 0 = 0
ha : p a
rw : cfcₙ (p := p) f (cfcₙ (p := p) (fun (x : R) ↦ s • x) a) = cfcₙ (p := p) f (s • a)
⊢ cfcₙ (p := p) (fun (x : R) ↦ f (s • x)) a = cfcₙ (p := p) f (s • a)
have rw₁ : cfcₙ (p := p) f (s • a) = cfcₙ (p := p) f (s • a)
Tactic: rw [cfcₙ_comp' f (s • ·) a, cfcₙ_smul_id s a]
-- 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
inst_12 : UniqueHom R A
r : R
f : R → R
a : A
hf : ContinuousOn f ((fun (x : R) ↦ r * x) '' σₙ R a)
hf0 : f 0 = 0
ha : p a
⊢ cfcₙ (p := p) (fun (x : R) ↦ f (r * x)) a = cfcₙ (p := p) f (r • a)
have rw : cfcₙ (p := p) f (cfcₙ (p := p) (fun (x : R) ↦ r * x) a) = cfcₙ (p := p) f (r • a)
Tactic: rw [cfcₙ_comp' f (r * ·) a, cfcₙ_const_mul_id r a]
-- 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
inst_12 : UniqueHom R A
r : R
f : R → R
a : A
hf : ContinuousOn f ((fun (x : R) ↦ r * x) '' σₙ R a)
hf0 : f 0 = 0
ha : p a
rw : cfcₙ (p := p) f (cfcₙ (p := p) (fun (x : R) ↦ r * x) a) = cfcₙ (p := p) f (r • a)
⊢ cfcₙ (p := p) (fun (x : R) ↦ f (r * x)) a = cfcₙ (p := p) f (r • a)
have rw₁ : cfcₙ (p := p) f (r • a) = cfcₙ (p := p) f (r • a)
Tactic: rw [cfcₙ_comp' f (r * ·) a, cfcₙ_const_mul_id r a]
-- 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
inst_12 : UniqueHom R A
hf : ContinuousOn f (star '' σₙ R a)
hf0 : f 0 = 0
ha : p a
⊢ cfcₙ (p := p) (fun (x : R) ↦ f (star x)) a = cfcₙ (p := p) f (star a)
have rw : cfcₙ (p := p) f (cfcₙ.{u_1, u_2} (R := R) (p := p) star a) = cfcₙ (p := p) f (star a)
Tactic: rw [cfcₙ_comp' f star a, cfcₙ_star_id a]
-- 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
inst_12 : UniqueHom R A
hf : ContinuousOn f (star '' σₙ R a)
hf0 : f 0 = 0
ha : p a
rw : cfcₙ (p := p) f (cfcₙ.{u_1, u_2} (R := R) (p := p) star a) = cfcₙ (p := p) f (star a)
⊢ cfcₙ (p := p) (fun (x : R) ↦ f (star x)) a = cfcₙ (p := p) f (star a)
have rw₁ : cfcₙ (p := p) f (star a) = cfcₙ (p := p) f (star a)
Tactic: rw [cfcₙ_comp' f star a, cfcₙ_star_id a]
-- 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
⊢ quasispectrum.{u_1, u_2} R (A := A) 0 = {0}
have refine : ∀ (x : R) (hx : x ∈ quasispectrum.{u_1, u_2} R (A := A) 0), x = 0
Tactic: refine Set.eq_singleton_iff_unique_mem.mpr ⟨quasispectrum.zero_mem R 0, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
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
x : R
hx : x ∈ quasispectrum.{u_1, u_2} R (A := A) 0
⊢ x = 0
have hx₁ : Membership.mem (γ := Set R) (0 '' quasispectrum.{u_1, u_2} R (A := A) 0) x
Tactic: rw [← cfcₙ_zero R (0 : A),
    cfcₙ_map_quasispectrum _ _ (by cfc_cont_tac) (by cfc_zero_tac) (cfcₙ_predicate_zero R)] at hx
Cleared hypotheses: hx
-- 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
⊢ cfcₙ (p := p) f 0 = 0
have pos : ∀ (hf0 : f 0 = 0), cfcₙ (p := p) f 0 = 0
Tactic: by_cases hf0 : f 0 = 0