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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      Eq (α := R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(σₙ R a) : Type u_1), R) } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            0 :
          R)
        (0 : R))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
h : ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a
pos :
  P
    ((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' := ⋯ })
⊢ P (cfcₙ (p := p) f a)

Tactic:
rw [cfcₙ_apply f a h.1 h.2.1 h.2.2]

Premises used: And.right, And.left, 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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      Eq (α := R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(σₙ R a) : Type u_1), R) } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            0 :
          R)
        (0 : R))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
h : ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a
⊢ P
    ((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' := ⋯ })

Tactic:
haf h.1 h.2.1 h.2.2

Premises used: And.right, And.left
-- 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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      Eq (α := R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(σₙ R a) : Type u_1), R) } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            0 :
          R)
        (0 : R))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
h : ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a
⊢ P
    ((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' := ⋯ })

Tactic:
exact haf h.1 h.2.1 h.2.2

Premises used: And.right, And.left
-- 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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      Eq (α := R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(σₙ R a) : Type u_1), R) } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            0 :
          R)
        (0 : R))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
h : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a)
⊢ ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0 ∨ ¬p a

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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      Eq (α := R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(σₙ R a) : Type u_1), R) } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            0 :
          R)
        (0 : R))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
h : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0 ∨ ¬p a
neg : ∀ (h : ¬ContinuousOn f (σₙ R a)), P (cfcₙ (p := p) f a)
neg₁ : ∀ (h : ¬f 0 = 0), P (cfcₙ (p := p) f a)
neg₂ : ∀ (h : ¬p a), P (cfcₙ (p := p) f a)
⊢ P (cfcₙ (p := p) f a)

Tactic:
obtain (h | h | h) := 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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      Eq (α := R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(σₙ R a) : Type u_1), R) } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            0 :
          R)
        (0 : R))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
h : ¬ContinuousOn f (σₙ R a)
neg neg₁ neg₂ neg₃ : P 0
⊢ P (cfcₙ (p := p) f a)

Tactic:
rwa [cfcₙ_apply_of_not_continuousOn _ h]

Premises used: 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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      Eq (α := R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(σₙ R a) : Type u_1), R) } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            0 :
          R)
        (0 : R))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
h : ¬f 0 = 0
neg neg₁ neg₂ neg₃ : P 0
⊢ P (cfcₙ (p := p) f a)

Tactic:
rwa [cfcₙ_apply_of_not_map_zero _ h]

Premises used: cfcₙ_apply_of_not_map_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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      Eq (α := R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(σₙ R a) : Type u_1), R) } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            0 :
          R)
        (0 : R))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
h : ¬p a
neg neg₁ neg₂ neg₃ : P 0
⊢ P (cfcₙ (p := p) f a)

Tactic:
rwa [cfcₙ_apply_of_not_predicate _ h]

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 g : R → R
a : A
⊢ (fun (x : A) ↦ Commute x (cfcₙ (p := p) g a)) 0

Tactic:
simp
-- 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 g : R → R
a : A
refine :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (hf0 :
      Eq (α := R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(σₙ R a) : Type u_1), R) } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            0 :
          R)
        (0 : R))
    (ha : p a),
    (fun (x : A) ↦ Commute x (cfcₙ (p := p) g 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 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
⊢ Commute (cfcₙ (p := p) f a) (cfcₙ (p := p) g a)

Tactic:
refine cfcₙ_cases (fun x ↦ Commute x (cfcₙ g a)) a f (by simp) fun hf hf0 ha ↦ ?_

Premises used: cfcₙ, Commute, cfcₙ_cases
-- 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 g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 :
  Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ : C((↑(σₙ R a) : Type u_1), R) } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        0 :
      R)
    (0 : R)
ha : p a
⊢ (fun (x : A) ↦
      Commute
        ((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 :
            C((↑(σₙ R a) : Type u_1), R)₀ })
        x)
    0

Tactic:
simp
-- 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 g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 :
  Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ : C((↑(σₙ R a) : Type u_1), R) } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        0 :
      R)
    (0 : R)
ha : p a
refine :
  ∀ (hg : ContinuousOn g (σₙ R a))
    (hg0 :
      Eq (α := R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ :
                C((↑(σₙ R a) : Type u_1), R) } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            0 :
          R)
        (0 : R))
    (x : p a),
    (fun (x : A) ↦
        Commute
          ((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 :
              C((↑(σₙ R a) : Type u_1), R)₀ })
          x)
      ((cfcₙHom (p := p) x : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := hg0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
⊢ Commute
    ((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 :
        C((↑(σₙ R a) : Type u_1), R)₀ })
    (cfcₙ (p := p) g a)

Tactic:
refine cfcₙ_cases (fun x ↦ Commute _ x) a g (by simp) fun hg hg0 _ ↦ ?_

Premises used: Commute, cfcₙ_cases
-- 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 g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 :
  Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ : C((↑(σₙ R a) : Type u_1), R) } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        0 :
      R)
    (0 : R)
ha : p a
hg : ContinuousOn g (σₙ R a)
hg0 :
  Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ : C((↑(σₙ R a) : Type u_1), R) } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        0 :
      R)
    (0 : R)
h : p a
⊢ (fun (x : A) ↦
      Commute
        ((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 :
            C((↑(σₙ R a) : Type u_1), R)₀ })
        x)
    ((cfcₙHom (p := p) h : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := hg0 :
        C((↑(σₙ R a) : Type u_1), R)₀ })

Tactic:
Commute.all _ _ |>.map _

Premises used: Commute.map, Commute.all
-- 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 g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 :
  Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ : C((↑(σₙ R a) : Type u_1), R) } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        0 :
      R)
    (0 : R)
ha : p a
hg : ContinuousOn g (σₙ R a)
hg0 :
  Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ : C((↑(σₙ R a) : Type u_1), R) } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        0 :
      R)
    (0 : R)
h : p a
⊢ (fun (x : A) ↦
      Commute
        ((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 :
            C((↑(σₙ R a) : Type u_1), R)₀ })
        x)
    ((cfcₙHom (p := p) h : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := hg0 :
        C((↑(σₙ R a) : Type u_1), R)₀ })

Tactic:
exact Commute.all _ _ |>.map _

Premises used: Commute.map, Commute.all
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ cfcₙ.{u_1, u_2} (R := R) (p := p) id a = a

Tactic:
cfcₙ_apply (id : R → R) a ▸ cfcₙHom_id (p := p) ha

Premises used: cfcₙHom_id, Eq.rec, id, Eq.symm, 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
a : A
ha : p a
⊢ cfcₙ (p := p) (fun (x : R) ↦ x) a = a

Tactic:
cfcₙ_id R a

Premises used: cfcₙ_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
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
⊢ σₙ R (cfcₙ (p := p) f a) = f '' σₙ R a

Tactic:
simp [cfcₙ_apply f a, cfcₙHom_map_quasispectrum (p := p)]

Premises used: cfcₙHom_map_quasispectrum, 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
⊢ p 0

Tactic:
NonUnitalContinuousFunctionalCalculus.predicate_zero (R := R)

Premises used: NonUnitalContinuousFunctionalCalculus.predicate_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
⊢ p (cfcₙ (p := p) f a)

Tactic:
cfcₙ_cases p a f (cfcₙ_predicate_zero R) fun _ _ _ ↦ cfcₙHom_predicate ..

Premises used: ContinuousMap.mk, cfcₙ_predicate_zero, quasispectrum, cfcₙHom_predicate, ContinuousOn.restrict, ContinuousMapZero.mk, Set.restrict, cfcₙ_cases
-- 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 g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
pos : ∀ (h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0), cfcₙ (p := p) f a = cfcₙ (p := p) g a
neg : ∀ (h : ¬(p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0)), cfcₙ (p := p) f a = cfcₙ (p := p) g a
⊢ cfcₙ (p := p) f a = cfcₙ (p := p) g a

Tactic:
by_cases h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 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 g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0
pos :
  Eq.{u_2 + 1} (α := 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)
    ((cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := ⋯ } :
      A)
⊢ cfcₙ (p := p) f a = cfcₙ (p := p) g a

Tactic:
rw [cfcₙ_apply f a (h.2.1.congr hfg) (hfg (quasispectrum.zero_mem R a) ▸ h.2.2) h.1,
      cfcₙ_apply g a h.2.1 h.2.2 h.1]

Premises used: quasispectrum.zero_mem, Eq.rec, ContinuousOn.congr, And.right, And.left, Eq.symm, cfcₙ_apply