awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
S : Type u_3
inst_12 : SMulZeroClass S R
inst_13 : ContinuousConstSMul S R
inst_14 : SMulZeroClass S A
inst_15 : IsScalarTower S R A
inst_16 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
pos :
  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) (HSMul.hSMul (β := R) s 1 • f), continuous_toFun := ⋯,
          map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (HSMul.hSMul (β := C((↑(σₙ R a) : Type u_1), R)₀) (HSMul.hSMul (β := R) s 1)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ }) :
      A)
⊢ (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (HSMul.hSMul (β := R) s 1 • f), continuous_toFun := ⋯,
        map_zero' := ⋯ } =
    HSMul.hSMul (β := A) (HSMul.hSMul (β := R) s 1)
      ((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' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A)

Tactic:
rw [← map_smul]

Premises used: map_smul
-- 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
S : Type u_3
inst_12 : SMulZeroClass S R
inst_13 : ContinuousConstSMul S R
inst_14 : SMulZeroClass S A
inst_15 : IsScalarTower S R A
inst_16 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ 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) (HSMul.hSMul (β := R) s 1 • f), continuous_toFun := ⋯,
          map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (HSMul.hSMul (β := C((↑(σₙ R a) : Type u_1), R)₀) (HSMul.hSMul (β := R) s 1)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ }) :
      A)

Tactic:
congr
-- 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
S : Type u_3
inst_12 : SMulZeroClass S R
inst_13 : ContinuousConstSMul S R
inst_14 : SMulZeroClass S A
inst_15 : IsScalarTower S R A
inst_16 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : ¬p a
⊢ cfcₙ (p := p) (fun (x : R) ↦ s • f x) a = s • cfcₙ (p := p) f a

Tactic:
simp [cfcₙ_apply_of_not_predicate a ha]

Premises used: cfcₙ_apply_of_not_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
r : R
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
⊢ cfcₙ (p := p) (fun (x : R) ↦ r * f x) a = r • cfcₙ (p := p) f a

Tactic:
cfcₙ_smul r f a

Premises used: cfcₙ_smul
-- 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
f : R → R
a : A
pos :
  ∀ (h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0), cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
neg :
  ∀ (h : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)),
    cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)

Tactic:
by_cases h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0

Premises used: quasispectrum, ContinuousOn, OfNat.ofNat
-- 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
f : R → R
a : A
h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ p a

Tactic:
obtain ⟨ha, hf, h0⟩ := h
-- 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
f : R → R
a : A
h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0
ha : p a
⊢ ContinuousOn f (σₙ R a)

Tactic:
obtain ⟨ha, hf, h0⟩ := h
-- 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
f : R → R
a : A
h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0
ha : p a
hf : ContinuousOn f (σₙ R a)
⊢ f 0 = 0

Tactic:
obtain ⟨ha, hf, h0⟩ := h
-- 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
f : R → R
a : A
ha : p a
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
pos :
  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) fun (x : R) ↦ star (f x), continuous_toFun := ⋯,
          map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (star { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }) :
      A)
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)

Tactic:
rw [cfcₙ_apply f a, ← map_star, cfcₙ_apply _ a]

Premises used: StarHomClass.map_star, cfcₙ_apply
-- 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
f : R → R
a : A
ha : p a
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
⊢ 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) fun (x : R) ↦ star (f x), continuous_toFun := ⋯,
          map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (star { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }) :
      A)

Tactic:
congr
-- 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
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ ¬p a ∨ ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0

Tactic:
simp only [not_and_or] at h

Premises used: not_and_or
-- 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
f : R → R
a : A
h : ¬p a ∨ ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
neg : ∀ (ha : ¬p a), cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
neg₁ : ∀ (hf : ¬ContinuousOn f (σₙ R a)), cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
neg₂ : ∀ (h0 : ¬f 0 = 0), cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)

Tactic:
obtain (ha | hf | h0) := h
-- 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
f : R → R
a : A
ha : ¬p a
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)

Tactic:
simp [cfcₙ_apply_of_not_predicate a ha]

Premises used: cfcₙ_apply_of_not_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
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
neg : ¬ContinuousOn (Y := R) (fun (x : R) ↦ star (f x)) (σₙ R a)
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)

Tactic:
rw [cfcₙ_apply_of_not_continuousOn a hf, cfcₙ_apply_of_not_continuousOn, star_zero]

Premises used: star_zero, cfcₙ_apply_of_not_continuousOn
-- 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
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
hf_star : ContinuousOn (Y := R) (fun (x : R) ↦ star (f x)) (σₙ R a)
⊢ ContinuousOn f (σₙ R a)

Tactic:
simpa using hf_star.star

Premises used: ContinuousOn.star
-- 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
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
⊢ ¬ContinuousOn (Y := R) (fun (x : R) ↦ star (f x)) (σₙ R a)

Tactic:
exact fun hf_star ↦ hf <| by simpa using hf_star.star
-- 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
f : R → R
a : A
h0 : ¬f 0 = 0
neg : ¬star (f 0) = 0
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)

Tactic:
rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero, star_zero]

Premises used: cfcₙ_apply_of_not_map_zero, star_zero
-- 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
f : R → R
a : A
h0 : ¬f 0 = 0
hf0 : star (f 0) = 0
⊢ f 0 = 0

Tactic:
simpa using congr(star $(hf0))
-- 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
f : R → R
a : A
h0 : ¬f 0 = 0
⊢ ¬star (f 0) = 0

Tactic:
exact fun hf0 ↦ h0 <| by simpa using congr(star $(hf0))
-- 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
S : Type u_3
inst_12 : SMulZeroClass S R
inst_13 : ContinuousConstSMul S R
inst_14 : SMulZeroClass S A
inst_15 : IsScalarTower S R A
inst_16 : IsScalarTower S R (R → R)
s : S
a : A
ha : p a
rw : s • cfcₙ (p := p) (fun (x : R) ↦ x) a = s • a
rw₁ rw₂ : s • a = s • a
⊢ cfcₙ (p := p) (fun (x : R) ↦ s • x) a = s • a

Tactic:
rw [cfcₙ_smul s _ a, cfcₙ_id' R a]

Premises used: cfcₙ_id', cfcₙ_smul
-- 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
r : R
a : A
ha : p a
⊢ cfcₙ (p := p) (fun (x : R) ↦ r * x) a = r • a

Tactic:
cfcₙ_smul_id r a

Premises used: cfcₙ_smul_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
rw : star (cfcₙ (p := p) (fun (x : R) ↦ x) a) = star a
rw₁ rw₂ : star a = star a
⊢ cfcₙ (p := p) (fun (x : R) ↦ star x) a = star a

Tactic:
rw [cfcₙ_star _ a, cfcₙ_id' R a]

Premises used: cfcₙ_id', cfcₙ_star
-- 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
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)
⊢ (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)

Tactic:
ext
-- 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
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)
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
⊢ 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
-- 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 : R → R
⊢ (fun (x : R → R) ↦ cfcₙ (p := p) x a) f ∈
    (↑(NonUnitalStarAlgHom.range (F := C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A) (cfcₙHom (p := p) ha)) : Set A)

Tactic:
cfcₙ_cases _ a f (zero_mem _) fun hf hf₀ ha ↦ ⟨_, rfl⟩

Premises used: Set.Mem, ContinuousMap.mk, quasispectrum, ContinuousOn.restrict, Exists.intro, ContinuousMapZero.mk, ZeroMemClass.zero_mem, Set.restrict, cfcₙ_cases, rfl
-- 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 : R → R
⊢ (fun (x : R → R) ↦ cfcₙ (p := p) x a) f ∈
    (↑(NonUnitalStarAlgHom.range (F := C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A) (cfcₙHom (p := p) ha)) : Set A)

Tactic:
exact cfcₙ_cases _ a f (zero_mem _) fun hf hf₀ ha ↦ ⟨_, rfl⟩
-- 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)₀
⊢ Membership.mem.{u_2, u_2} (α := A) (γ := Set A) (Set.range fun (x : R → R) ↦ cfcₙ (p := p) x a)
    (((↑(NonUnitalAlgHomClass.toNonUnitalAlgHom (F := C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A) (cfcₙHom (p := p) ha)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ+* A) :
          (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        f :
      A)

Tactic:
⟨Subtype.val.extend f 0, cfcₙHom_eq_cfcₙ_extend _ ha _ |>.symm⟩

Premises used: Set.Mem, setOf, cfcₙHom_eq_cfcₙ_extend, Function.extend, Exists.intro, Set.range, OfNat.ofNat, Eq.symm, Subtype.val, DFunLike.coe
-- 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)₀
⊢ Membership.mem.{u_2, u_2} (α := A) (γ := Set A) (Set.range fun (x : R → R) ↦ cfcₙ (p := p) x a)
    (((↑(NonUnitalAlgHomClass.toNonUnitalAlgHom (F := C((↑(σₙ R a) : Type u_1), R)₀ →⋆ₙₐ[R] A) (cfcₙHom (p := p) ha)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ+* A) :
          (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        f :
      A)

Tactic:
exact ⟨Subtype.val.extend f 0, cfcₙHom_eq_cfcₙ_extend _ ha _ |>.symm⟩