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
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 0
pos : ∀ (hf : ContinuousOn f (spectrum R a)), cfc (p := p) f a ≤ 0
neg : ∀ (hf : ¬ContinuousOn f (spectrum R a)), cfc (p := p) f a ≤ 0
⊢ cfc (p := p) f a ≤ 0

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, f x ≤ 0
hf : ContinuousOn f (spectrum R a)
⊢ cfc (p := p) f a ≤ 0

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, f x ≤ 0
hf : ¬ContinuousOn f (spectrum R a)
⊢ cfc (p := p) f a ≤ 0

Tactic:
simp only [cfc_apply_of_not_continuousOn _ hf, le_rfl]

Premises used: le_rfl, cfc_apply_of_not_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
r : R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ r
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (p := p) f a ≤ (algebraMap R A : (a : R) → A) r

Tactic:
cfc_const r a ▸ cfc_mono h

Premises used: Eq.rec, cfc_mono, cfc_const
-- 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
r : R
a : A
h : ∀ x ∈ spectrum R a, r ≤ f x
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ (algebraMap R A : (a : R) → A) r ≤ cfc (p := p) f a

Tactic:
cfc_const r a ▸ cfc_mono h

Premises used: Eq.rec, cfc_mono, cfc_const
-- 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
r : R
a : A
h : ∀ x ∈ spectrum R a, x ≤ r
ha : p a
rw : cfc.{u_1, u_2} (R := R) (p := p) id a ≤ (algebraMap R A : (a : R) → A) r
⊢ a ≤ (algebraMap R A : (a : R) → A) r

Tactic:
rw [← cfc_id R a]

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
r : R
a : A
h : ∀ x ∈ spectrum R a, x ≤ r
ha : p a
⊢ cfc.{u_1, u_2} (R := R) (p := p) id a ≤ (algebraMap R A : (a : R) → A) r

Tactic:
cfc_le_algebraMap id r a h

Premises used: id, cfc_le_algebraMap
-- 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
r : R
a : A
h : ∀ x ∈ spectrum R a, x ≤ r
ha : p a
⊢ cfc.{u_1, u_2} (R := R) (p := p) id a ≤ (algebraMap R A : (a : R) → A) r

Tactic:
exact cfc_le_algebraMap id r a h

Premises used: id, cfc_le_algebraMap
-- 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
r : R
a : A
h : ∀ x ∈ spectrum R a, r ≤ x
ha : p a
rw : (algebraMap R A : (a : R) → A) r ≤ cfc.{u_1, u_2} (R := R) (p := p) id a
⊢ (algebraMap R A : (a : R) → A) r ≤ a

Tactic:
rw [← cfc_id R a]

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
r : R
a : A
h : ∀ x ∈ spectrum R a, r ≤ x
ha : p a
⊢ (algebraMap R A : (a : R) → A) r ≤ cfc.{u_1, u_2} (R := R) (p := p) id a

Tactic:
algebraMap_le_cfc id r a h

Premises used: id, algebraMap_le_cfc
-- 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
r : R
a : A
h : ∀ x ∈ spectrum R a, r ≤ x
ha : p a
⊢ (algebraMap R A : (a : R) → A) r ≤ cfc.{u_1, u_2} (R := R) (p := p) id a

Tactic:
exact algebraMap_le_cfc id r a h

Premises used: id, algebraMap_le_cfc
-- 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, f x ≤ 1
⊢ LE.le.{u_2} (α := A) 0 1

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
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 1
apply :
  ∀ (hf : ContinuousOn f (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)
      (1 : A)
⊢ cfc (p := p) f a ≤ 1

Tactic:
apply cfc_cases (· ≤ 1) _ _ (by simp) fun hf ha ↦ ?_

Premises used: LE.le, cfc_cases, OfNat.ofNat
-- 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, f x ≤ 1
hf : ContinuousOn f (spectrum R a)
ha : p a
rw :
  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) 1 : 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)
    (1 : A)

Tactic:
rw [← map_one (cfcHom ha (R := R))]

Premises used: cfcHom, map_one
-- 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, f x ≤ 1
hf : ContinuousOn f (spectrum R a)
ha : p a
apply :
  { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
      C((↑(spectrum R a) : Type u_1), R) } ≤
    1
⊢ 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) 1 : A)

Tactic:
apply cfcHom_mono ha

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 : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 1
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
      C((↑(spectrum R a) : Type u_1), R) } ≤
    1

Tactic:
simpa [ContinuousMap.le_def] using h

Premises used: ContinuousMap.le_def
-- 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, 1 ≤ f x
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ 1 ≤ cfc (p := p) f a

Tactic:
simpa using algebraMap_le_cfc f 1 a h

Premises used: algebraMap_le_cfc, OfNat.ofNat
-- 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
h : ∀ x ∈ spectrum R a, x ≤ 1
ha : p a
⊢ a ≤ 1

Tactic:
simpa using le_algebraMap_of_spectrum_le h

Premises used: le_algebraMap_of_spectrum_le
-- 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
h : ∀ x ∈ spectrum R a, 1 ≤ x
ha : p a
⊢ 1 ≤ a

Tactic:
simpa using algebraMap_le_of_le_spectrum h

Premises used: algebraMap_le_of_le_spectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : Algebra ℝ≥0 A
inst_5 : ContinuousFunctionalCalculus ℝ≥0 A fun (x : A) ↦ 0 ≤ x
a : Aˣ
ha : 0 ≤ (↑a : A)
⊢ 0 ≤ (↑a⁻¹ : A)

Tactic:
cfc_inv_id (R := ℝ≥0) a ▸ cfc_predicate _ (a : A)

Premises used: Units.val, Eq.rec, cfc_inv_id, cfc_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : Algebra ℝ≥0 A
inst_5 : ContinuousFunctionalCalculus ℝ≥0 A fun (x : A) ↦ 0 ≤ x
a : Aˣ
⊢ 0 ≤ (↑a⁻¹ : A) ↔ 0 ≤ (↑a : A)

Tactic:
⟨fun _ ↦ inv_inv a ▸ inv_nonneg_of_nonneg a⁻¹, fun _ ↦ inv_nonneg_of_nonneg a⟩

Premises used: Eq.rec, Inv.inv, inv_inv, Iff.intro, CFC.inv_nonneg_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing 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 g : C((↑(spectrum R a) : Type u_1), R)
rw :
  0 ≤
      HSub.hSub (α := A) (β := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) g : A)
        ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) ↔
    f ≤ g
rw₁ :
  LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) (g - f) : A) ↔ f ≤ g
rw₂ : 0 ≤ g - f ↔ f ≤ g
rw₃ rw₄ : f ≤ g ↔ 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) ↔
    f ≤ g

Tactic:
rw [← sub_nonneg, ← map_sub, cfcHom_nonneg_iff, sub_nonneg]

Premises used: map_sub, cfcHom_nonneg_iff, sub_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing 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 g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
rw :
  (∀ (a_1 : (↑(spectrum R a) : Type u_1)),
      LE.le (α := 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)
        (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, 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, f x ≤ g x
⊢ cfc (p := p) f a ≤ cfc (p := p) g a ↔ ∀ x ∈ spectrum R a, f x ≤ g x

Tactic:
rw [cfc_apply f a, cfc_apply g a, cfcHom_le_iff (show p a from ha), ContinuousMap.le_def]

Premises used: ContinuousMap.le_def, cfcHom_le_iff, cfc_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing 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 g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ (∀ (a_1 : (↑(spectrum R a) : Type u_1)),
      LE.le (α := 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)
        (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, 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, f x ≤ g x

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing 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
simp_rw : 0 ≤ cfc (p := p) (fun (x : R) ↦ -f x) a ↔ ∀ x ∈ spectrum R a, 0 ≤ -f x
⊢ cfc (p := p) f a ≤ 0 ↔ ∀ x ∈ spectrum R a, f x ≤ 0

Tactic:
simp_rw [← neg_nonneg, ← cfc_neg]

Premises used: cfc_neg, neg_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing 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
⊢ 0 ≤ cfc (p := p) (fun (x : R) ↦ -f x) a ↔ ∀ x ∈ spectrum R a, 0 ≤ -f x

Tactic:
cfc_nonneg_iff (fun x ↦ -f x) a

Premises used: cfc_nonneg_iff, Neg.neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing 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
⊢ 0 ≤ cfc (p := p) (fun (x : R) ↦ -f x) a ↔ ∀ x ∈ spectrum R a, 0 ≤ -f x

Tactic:
exact cfc_nonneg_iff (fun x ↦ -f x) a

Premises used: cfc_nonneg_iff, Neg.neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing 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
r : R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
rw : cfc (p := p) f a ≤ cfc (p := p) (fun (x : R) ↦ r) a ↔ ∀ x ∈ spectrum R a, f x ≤ r
rw₁ rw₂ : (∀ x ∈ spectrum R a, f x ≤ r) ↔ ∀ x ∈ spectrum R a, f x ≤ r
⊢ cfc (p := p) f a ≤ (algebraMap R A : (a : R) → A) r ↔ ∀ x ∈ spectrum R a, f x ≤ r

Tactic:
rw [← cfc_const r a, cfc_le_iff ..]

Premises used: cfc_const, cfc_le_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing 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
r : R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
rw : cfc (p := p) (fun (x : R) ↦ r) a ≤ cfc (p := p) f a ↔ ∀ x ∈ spectrum R a, r ≤ f x
rw₁ rw₂ : (∀ x ∈ spectrum R a, r ≤ f x) ↔ ∀ x ∈ spectrum R a, r ≤ f x
⊢ (algebraMap R A : (a : R) → A) r ≤ cfc (p := p) f a ↔ ∀ x ∈ spectrum R a, r ≤ f x

Tactic:
rw [← cfc_const r a, cfc_le_iff ..]

Premises used: cfc_const, cfc_le_iff