awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C((↑(spectrum R a) : Type u_1), R)
hfg : f ≤ g
⊢ LE.le.{u_2} (α := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) g : A)

Tactic:
OrderHomClass.mono (cfcHom ha) hfg

Premises used: cfcHom, OrderHomClass.mono
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
mp : LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) → 0 ≤ f
mpr : 0 ≤ f → LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
⊢ LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) ↔ 0 ≤ f

Tactic:
constructor
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
⊢ LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) → 0 ≤ f

Tactic:
fun hf x ↦ (cfcHom_map_spectrum ha (R := R) _ ▸ spectrum_nonneg_of_nonneg hf) ⟨x, rfl⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
⊢ LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) → 0 ≤ f

Tactic:
exact fun hf x ↦ (cfcHom_map_spectrum ha (R := R) _ ▸ spectrum_nonneg_of_nonneg hf) ⟨x, rfl⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
⊢ 0 ≤ f → LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)

Tactic:
simpa using (cfcHom_mono ha (f := 0) (g := f) ·)

Premises used: cfcHom_mono
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
⊢ IsStrictlyPositive.{u_2} (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) ↔
    ∀ (x : (↑(spectrum R a) : Type u_1)), LT.lt (α := R) (0 : R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)

Tactic:
⟨fun hf x => hf.spectrum_pos <| cfcHom_map_spectrum (R := R) ha _ ▸ Set.mem_range_self x,
    fun h => ⟨cfcHom_nonneg_iff _ |>.mpr fun x => le_of_lt (h x), ?_⟩⟩

Premises used: Iff.mpr, cfcHom_nonneg_iff, le_of_lt, IsStrictlyPositive.spectrum_pos, And.intro, Iff.intro
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
refine :
  ∀
    (h :
      ∀ (x : (↑(spectrum R a) : Type u_1)),
        LT.lt (α := R) (0 : R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)),
    IsUnit.{u_2} (M := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
⊢ IsStrictlyPositive.{u_2} (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) ↔
    ∀ (x : (↑(spectrum R a) : Type u_1)), LT.lt (α := R) (0 : R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)

Tactic:
refine ⟨fun hf x => hf.spectrum_pos <| cfcHom_map_spectrum (R := R) ha _ ▸ Set.mem_range_self x,
    fun h => ⟨cfcHom_nonneg_iff _ |>.mpr fun x => le_of_lt (h x), ?_⟩⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
h : ∀ (x : (↑(spectrum R a) : Type u_1)), LT.lt (α := R) (0 : R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
apply : 0 ∉ spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
⊢ IsUnit.{u_2} (M := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)

Tactic:
apply spectrum.isUnit_of_zero_notMem (R := R)

Premises used: spectrum.isUnit_of_zero_notMem
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
h : ∀ (x : (↑(spectrum R a) : Type u_1)), LT.lt (α := R) (0 : R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
⊢ 0 ∉ spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)

Tactic:
grind [cfcHom_map_spectrum, ne_of_lt]

Premises used: ne_of_lt, cfcHom_map_spectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
pos : ∀ (ha : p a), cfc (p := p) f a ≤ cfc (p := p) g a
neg : ∀ (ha : ¬p a), cfc (p := p) f a ≤ cfc (p := p) g a
⊢ cfc (p := p) f a ≤ cfc (p := p) g a

Tactic:
by_cases ha : p a
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
pos :
  LE.le.{u_2} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
⊢ cfc (p := p) f a ≤ cfc (p := p) g a

Tactic:
rw [cfc_apply f a, cfc_apply g a]

Premises used: cfc_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ LE.le.{u_2} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)

Tactic:
cfcHom_mono ha fun x ↦ h x.1 x.2

Premises used: Subtype.val, cfcHom_mono, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ LE.le.{u_2} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)

Tactic:
exact cfcHom_mono ha fun x ↦ h x.1 x.2

Premises used: cfcHom_mono
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : ¬p a
⊢ cfc (p := p) f a ≤ cfc (p := p) g a

Tactic:
simp only [cfc_apply_of_not_predicate _ ha, le_rfl]

Premises used: le_rfl, cfc_apply_of_not_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
rw :
  (∀ (a_1 : (↑(spectrum R a) : Type u_1)),
      LE.le (α := R) ((0 : (a : (↑(spectrum R a) : Type u_1)) → R) a_1 : R)
        (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(spectrum R a) : Type u_1), R) } :
              (a : (↑(spectrum R a) : Type u_1)) → R)
            a_1 :
          R)) ↔
    ∀ x ∈ spectrum R a, 0 ≤ f x
⊢ 0 ≤ cfc (p := p) f a ↔ ∀ x ∈ spectrum R a, 0 ≤ f x

Tactic:
rw [cfc_apply .., cfcHom_nonneg_iff, ContinuousMap.le_def]

Premises used: ContinuousMap.le_def, cfcHom_nonneg_iff, cfc_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ (∀ (a_1 : (↑(spectrum R a) : Type u_1)),
      LE.le (α := R) ((0 : (a : (↑(spectrum R a) : Type u_1)) → R) a_1 : R)
        (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(spectrum R a) : Type u_1), R) } :
              (a : (↑(spectrum R a) : Type u_1)) → R)
            a_1 :
          R)) ↔
    ∀ x ∈ spectrum R a, 0 ≤ f x

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
⊢ ContinuousOn id (spectrum R a)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
⊢ 0 ≤ cfc.{u_1, u_2} (R := R) (p := p) id a ↔ ∀ x ∈ spectrum R a, 0 ≤ id x

Tactic:
have := cfc_nonneg_iff (id : R → R) a (by fun_prop) ha
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
this : 0 ≤ cfc.{u_1, u_2} (R := R) (p := p) id a ↔ ∀ x ∈ spectrum R a, 0 ≤ id x
⊢ 0 ≤ a ↔ ∀ x ∈ spectrum R a, 0 ≤ x

Tactic:
simpa [cfc_id _ a ha] using this

Premises used: cfc_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
rw :
  (∀ (x : (↑(spectrum R a) : Type u_1)),
      LT.lt (α := R) (0 : R)
        (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(spectrum R a) : Type u_1), R) } :
              (a : (↑(spectrum R a) : Type u_1)) → R)
            x :
          R)) ↔
    ∀ x ∈ spectrum R a, 0 < f x
⊢ IsStrictlyPositive (cfc (p := p) f a) ↔ ∀ x ∈ spectrum R a, 0 < f x

Tactic:
rw [cfc_apply .., cfcHom_isStrictlyPositive_iff]

Premises used: cfc_apply, cfcHom_isStrictlyPositive_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ (∀ (x : (↑(spectrum R a) : Type u_1)),
      LT.lt (α := R) (0 : R)
        (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(spectrum R a) : Type u_1), R) } :
              (a : (↑(spectrum R a) : Type u_1)) → R)
            x :
          R)) ↔
    ∀ x ∈ spectrum R a, 0 < f x

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
⊢ IsStrictlyPositive (cfc.{u_1, u_2} (R := R) (p := p) id a) ↔ ∀ x ∈ spectrum R a, 0 < id x

Tactic:
have := cfc_isStrictlyPositive_iff (id : R → R) a (by fun_prop) ha
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
this : IsStrictlyPositive (cfc.{u_1, u_2} (R := R) (p := p) id a) ↔ ∀ x ∈ spectrum R a, 0 < id x
⊢ IsStrictlyPositive a ↔ ∀ x ∈ spectrum R a, 0 < x

Tactic:
simpa [cfc_id _ a ha] using this

Premises used: cfc_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, 0 ≤ f x
pos : ∀ (hf : ContinuousOn f (spectrum R a)), 0 ≤ cfc (p := p) f a
neg : ∀ (hf : ¬ContinuousOn f (spectrum R a)), 0 ≤ cfc (p := p) f a
⊢ 0 ≤ cfc (p := p) f a

Tactic:
by_cases hf : ContinuousOn f (spectrum R a)

Premises used: spectrum, ContinuousOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, 0 ≤ f x
hf : ContinuousOn f (spectrum R a)
⊢ 0 ≤ cfc (p := p) f a

Tactic:
simpa using cfc_mono h

Premises used: cfc_mono
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, 0 ≤ f x
hf : ¬ContinuousOn f (spectrum R a)
⊢ 0 ≤ cfc (p := p) f a

Tactic:
simp only [cfc_apply_of_not_continuousOn _ hf, le_rfl]

Premises used: le_rfl, cfc_apply_of_not_continuousOn