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 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
simp :
  (∀ (a_1 : R) (b : a_1 ∈ σₙ R a),
      (0 : (a : (↑(σₙ R a) : Type u_1)) → R) (Subtype.mk (p := fun (a_2 : R) ↦ a_2 ∈ σₙ R a) a_1 b) ≤ f a_1) ↔
    ∀ x ∈ σₙ R a, 0 ≤ f x
⊢ (∀ (x : (↑(σₙ R a) : Type u_1)),
      LE.le (α := R) ((0 : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            x :
          R)) ↔
    ∀ x ∈ σₙ R a, 0 ≤ f x

Tactic:
simp only [ContinuousMapZero.coe_mk, ContinuousMap.coe_mk, Set.restrict_apply, Subtype.forall]

Premises used: Set.restrict_apply, ContinuousMapZero.coe_mk, Subtype.forall, ContinuousMap.coe_mk
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ (∀ (a_1 : R) (b : a_1 ∈ σₙ R a),
      (0 : (a : (↑(σₙ R a) : Type u_1)) → R) (Subtype.mk (p := fun (a_2 : R) ↦ a_2 ∈ σₙ R a) a_1 b) ≤ f a_1) ↔
    ∀ x ∈ σₙ R a, 0 ≤ f x

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 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
a : A
ha : p a
⊢ ContinuousOn id (σₙ R a)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
a : A
ha : p a
⊢ 0 ≤ cfcₙ.{u_1, u_2} (R := R) (p := p) id a ↔ ∀ x ∈ σₙ R a, 0 ≤ id x

Tactic:
have := cfcₙ_nonneg_iff (id : R → R) a (by fun_prop)
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
a : A
ha : p a
this : 0 ≤ cfcₙ.{u_1, u_2} (R := R) (p := p) id a ↔ ∀ x ∈ σₙ R a, 0 ≤ id x
⊢ 0 ≤ a ↔ ∀ x ∈ σₙ R a, 0 ≤ x

Tactic:
simpa [cfcₙ_id _ a ha] using this

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 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
pos : ∀ (hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0), 0 ≤ cfcₙ (p := p) f a
neg : ∀ (hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)), 0 ≤ cfcₙ (p := p) f a
⊢ 0 ≤ cfcₙ (p := p) f a

Tactic:
by_cases hf : 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 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ ContinuousOn f (σₙ R a)

Tactic:
obtain ⟨h₁, h₂⟩ := hf
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
h₁ : ContinuousOn f (σₙ R a)
⊢ f 0 = 0

Tactic:
obtain ⟨h₁, h₂⟩ := hf
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
h₁ : ContinuousOn f (σₙ R a)
h₂ : f 0 = 0
⊢ 0 ≤ cfcₙ (p := p) f a

Tactic:
simpa using cfcₙ_mono h

Premises used: cfcₙ_mono
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0

Tactic:
simp only [not_and_or] at hf

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 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
neg : ∀ (hf : ¬ContinuousOn f (σₙ R a)), 0 ≤ cfcₙ (p := p) f a
neg₁ : ∀ (hf : ¬f 0 = 0), 0 ≤ cfcₙ (p := p) f a
⊢ 0 ≤ cfcₙ (p := p) f a

Tactic:
obtain (hf | hf) := hf
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬ContinuousOn f (σₙ 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
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬f 0 = 0
⊢ 0 ≤ cfcₙ (p := p) f a

Tactic:
simp only [cfcₙ_apply_of_not_map_zero _ hf, le_rfl]

Premises used: le_rfl, 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 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
pos : ∀ (hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0), cfcₙ (p := p) f a ≤ 0
neg : ∀ (hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)), cfcₙ (p := p) f a ≤ 0
⊢ cfcₙ (p := p) f a ≤ 0

Tactic:
by_cases hf : 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 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ ContinuousOn f (σₙ R a)

Tactic:
obtain ⟨h₁, h₂⟩ := hf
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
h₁ : ContinuousOn f (σₙ R a)
⊢ f 0 = 0

Tactic:
obtain ⟨h₁, h₂⟩ := hf
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
h₁ : ContinuousOn f (σₙ R a)
h₂ : f 0 = 0
⊢ cfcₙ (p := p) f a ≤ 0

Tactic:
simpa using cfcₙ_mono h

Premises used: cfcₙ_mono
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0

Tactic:
simp only [not_and_or] at hf

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 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
neg : ∀ (hf : ¬ContinuousOn f (σₙ R a)), cfcₙ (p := p) f a ≤ 0
neg₁ : ∀ (hf : ¬f 0 = 0), cfcₙ (p := p) f a ≤ 0
⊢ cfcₙ (p := p) f a ≤ 0

Tactic:
obtain (hf | hf) := hf
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬ContinuousOn f (σₙ 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.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬f 0 = 0
⊢ cfcₙ (p := p) f a ≤ 0

Tactic:
simp only [cfcₙ_apply_of_not_map_zero _ hf, le_rfl]

Premises used: le_rfl, 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 : CommRing R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalRing R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
rw :
  0 ≤
      HSub.hSub (α := A) (β := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A)
        ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A) ↔
    f ≤ g
rw₁ : LE.le.{u_2} (α := A) (0 : A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) (g - f) : A) ↔ f ≤ g
rw₂ : 0 ≤ g - f ↔ f ≤ g
rw₃ rw₄ : f ≤ g ↔ f ≤ g
⊢ LE.le.{u_2} (α := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)
      ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A) ↔
    f ≤ g

Tactic:
rw [← sub_nonneg, ← map_sub, cfcₙHom_nonneg_iff, sub_nonneg]

Premises used: map_sub, sub_nonneg, cfcₙHom_nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalRing R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
ha : p a
rw :
  (∀ (x : (↑(σₙ R a) : Type u_1)),
      LE.le (α := R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            x :
          R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := ⋯ } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            x :
          R)) ↔
    ∀ x ∈ σₙ R a, f x ≤ g x
⊢ cfcₙ (p := p) f a ≤ cfcₙ (p := p) g a ↔ ∀ x ∈ σₙ R a, f x ≤ g x

Tactic:
rw [cfcₙ_apply f a, cfcₙ_apply g a, cfcₙHom_le_iff (show p a from ha), ContinuousMapZero.le_def]

Premises used: cfcₙHom_le_iff, ContinuousMapZero.le_def, cfcₙ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalRing R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
ha : p a
⊢ (∀ (x : (↑(σₙ R a) : Type u_1)),
      LE.le (α := R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            x :
          R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := ⋯ } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            x :
          R)) ↔
    ∀ x ∈ σₙ R a, f x ≤ g x

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalRing R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
simp_rw : 0 ≤ cfcₙ (p := p) (fun (x : R) ↦ -f x) a ↔ ∀ x ∈ σₙ R a, 0 ≤ -f x
⊢ cfcₙ (p := p) f a ≤ 0 ↔ ∀ x ∈ σₙ R a, f x ≤ 0

Tactic:
simp_rw [← neg_nonneg, ← cfcₙ_neg]

Premises used: cfcₙ_neg, neg_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalRing R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ 0 ≤ cfcₙ (p := p) (fun (x : R) ↦ -f x) a ↔ ∀ x ∈ σₙ R a, 0 ≤ -f x

Tactic:
cfcₙ_nonneg_iff (fun x ↦ -f x) a

Premises used: cfcₙ_nonneg_iff, Neg.neg