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 : CommRing R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalRing R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
rw :
  0 ≤
      HSub.hSub (α := A) (β := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A)
        ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A) ↔
    f ≤ g
rw₁ : LE.le.{u_2} (α := A) (0 : A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) (g - f) : A) ↔ f ≤ g
rw₂ : 0 ≤ g - f ↔ f ≤ g
⊢ LE.le.{u_2} (α := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)
      ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A) ↔
    f ≤ g
have rw₃ : f ≤ g ↔ f ≤ g
Tactic: rw [← sub_nonneg, ← map_sub, cfcₙHom_nonneg_iff, sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalRing R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
ha : p a
⊢ cfcₙ (p := p) f a ≤ cfcₙ (p := p) g a ↔ ∀ x ∈ σₙ R a, f x ≤ g x
have rw : (∀ (x : (↑(σₙ R a) : Type u_1)),
    LE.le (α := R)
      (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry } :
            (a : (↑(σₙ R a) : Type u_1)) → R)
          x :
        R)
      (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := sorry, map_zero' := sorry } :
            (a : (↑(σₙ R a) : Type u_1)) → R)
          x :
        R)) ↔
  ∀ x ∈ σₙ R a, f x ≤ g x
Tactic: rw [cfcₙ_apply f a, cfcₙ_apply g a, cfcₙHom_le_iff (show p a from ha), ContinuousMapZero.le_def]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalRing R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ cfcₙ (p := p) f a ≤ 0 ↔ ∀ x ∈ σₙ R a, f x ≤ 0
have simp_rw : 0 ≤ cfcₙ (p := p) (fun (x : R) ↦ -f x) a ↔ ∀ x ∈ σₙ R a, 0 ≤ -f x
Tactic: simp_rw [← neg_nonneg, ← cfcₙ_neg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus 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_of_cfcHom R (p := p) ha) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
have refine : ∀ (f g : C((↑(σₙ R a) : Type u_1), R)₀)
  (h :
    Eq (α := C((↑(spectrum R a) : Type u_1), R))
      (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                  (NonUnitalStarAlgHom.comp
                    (↑(compStarAlgHom' R R
                          { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) sorry, continuous_toFun := sorry }) :
                      C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                    toContinuousMapHom)) :
              C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
            (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
          f :
        C((↑(spectrum R a) : Type u_1), R))
      (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                  (NonUnitalStarAlgHom.comp
                    (↑(compStarAlgHom' R R
                          { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) sorry, continuous_toFun := sorry }) :
                      C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                    toContinuousMapHom)) :
              C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
            (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
          g :
        C((↑(spectrum R a) : Type u_1), R))),
  f = g
Tactic: refine (cfcHom_injective ha).comp fun f g 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 : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
h :
  Eq (α := C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        f :
      C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        g :
      C((↑(spectrum R a) : Type u_1), R))
⊢ f = g
have h₁ : ∀ (x : (↑(σₙ R a) : Type u_1)),
  Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) ((g : (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 : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
h :
  Eq (α := C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        f :
      C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        g :
      C((↑(spectrum R a) : Type u_1), R))
x : (↑(σₙ R a) : Type u_1)
⊢ Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) ((g : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
have h₁ : Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) 0 : R) ((g : (a : (↑(σₙ R a) : Type u_1)) → R) 0 : R)
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: 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 : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
h :
  Eq (α := C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        f :
      C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        g :
      C((↑(spectrum R a) : Type u_1), R))
x : (↑(σₙ R a) : Type u_1)
h₁ : Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) 0 : R) ((g : (a : (↑(σₙ R a) : Type u_1)) → R) 0 : R)
⊢ Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) ((g : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
have h₂ : ∀ (hx : x ≠ 0),
  Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) ((g : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
h :
  Eq (α := C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        f :
      C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        g :
      C((↑(spectrum R a) : Type u_1), R))
x : (↑(σₙ R a) : Type u_1)
hx : x ≠ 0
⊢ Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) ((g : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
have this : (↑x : R) = 0 ∨ (↑x : R) ∈ spectrum R a
Tactic: have := by simpa [quasispectrum_eq_spectrum_union_zero] using x.prop
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
h :
  Eq (α := C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        f :
      C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        g :
      C((↑(spectrum R a) : Type u_1), R))
x : (↑(σₙ R a) : Type u_1)
hx : x ≠ 0
this : (↑x : R) = 0 ∨ (↑x : R) ∈ spectrum R a
⊢ Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) ((g : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
have this₁ : (↑x : R) ∈ spectrum R a
Tactic: replace := this.resolve_left (Subtype.val_injective.ne_iff.mpr hx)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus 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_of_cfcHom R (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A) =
    range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)
have simp : quasispectrum.{u_1, u_2} R (A := A)
    ((NonUnitalStarAlgHom.comp (↑(cfcHom (p := p) ha) : C((↑(spectrum R a) : Type u_1), R) →⋆ₙₐ[R] A)
            (NonUnitalStarAlgHom.comp
              (↑(compStarAlgHom' R R
                    { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) sorry, continuous_toFun := sorry :
                      C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) }) :
                C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
              toContinuousMapHom) :
          (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        f :
      A) =
  range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)
Tactic: simp only [cfcₙHom_of_cfcHom]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
⊢ quasispectrum.{u_1, u_2} R (A := A)
      ((NonUnitalStarAlgHom.comp (↑(cfcHom (p := p) ha) : C((↑(spectrum R a) : Type u_1), R) →⋆ₙₐ[R] A)
              (NonUnitalStarAlgHom.comp
                (↑(compStarAlgHom' R R
                      { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ :
                        C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) }) :
                  C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                toContinuousMapHom) :
            (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          f :
        A) =
    range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)
have rw : spectrum.{u_1, u_2} R (A := A)
      ((NonUnitalStarAlgHom.comp (↑(cfcHom (p := p) ha) : C((↑(spectrum R a) : Type u_1), R) →⋆ₙₐ[R] A)
              (NonUnitalStarAlgHom.comp
                (↑(compStarAlgHom' R R
                      { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) sorry, continuous_toFun := sorry :
                        C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) }) :
                  C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                toContinuousMapHom) :
            (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          f :
        A) ∪
    {0} =
  range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)
Tactic: rw [quasispectrum_eq_spectrum_union_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
⊢ spectrum.{u_1, u_2} R (A := A)
        ((NonUnitalStarAlgHom.comp (↑(cfcHom (p := p) ha) : C((↑(spectrum R a) : Type u_1), R) →⋆ₙₐ[R] A)
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ :
                          C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom) :
              (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
            f :
          A) ∪
      {0} =
    range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)
have simp : spectrum.{u_1, u_2} R (A := A)
      ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
          ((compStarAlgHom' R R
                  { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) sorry, continuous_toFun := sorry :
                    C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) } :
                (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
              ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
            C((↑(spectrum R a) : Type u_1), R)) :
        A) ∪
    {0} =
  range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)
Tactic: simp only [NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_coe]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
⊢ spectrum.{u_1, u_2} R (A := A)
        ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
            ((compStarAlgHom' R R
                    { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ :
                      C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          A) ∪
      {0} =
    range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)
have rw : Eq (α := Set R)
  (range (ι := (↑(spectrum R a) : Type u_1))
      (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) sorry, continuous_toFun := sorry } :
                (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
              ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
            C((↑(spectrum R a) : Type u_1), R)) :
        (a : (↑(spectrum R a) : Type u_1)) → R) ∪
    {0})
  (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R))
Tactic: rw [cfcHom_map_spectrum ha]