-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_nonneg {f : R → R} {a : A} (h : ∀ x ∈ σₙ R a, 0 ≤ f x) :
    0 ≤ cfcₙ f a

Proof state:
case pos.intro
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type ?u.999960) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
h₁ : ContinuousOn f (σₙ R a)
h₂ : f 0 = 0
⊢ 0 ≤ cfcₙ f a

Tactic:
simpa using cfcₙ_mono h

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type ?u.999960) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
⊢ 0 ≤ cfcₙ f a

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

Result:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type ?u.999960) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ 0 ≤ cfcₙ f a

case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type ?u.999960) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ 0 ≤ cfcₙ f a

Proof state:
case neg.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬ContinuousOn f (σₙ R a)
⊢ 0 ≤ cfcₙ f a

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

Result:
no goals

Proof state:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
⊢ 0 ≤ cfcₙ f a

Tactic:
obtain (hf | hf) := hf

Result:
case neg.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬ContinuousOn f (σₙ R a)
⊢ 0 ≤ cfcₙ f a

case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬f 0 = 0
⊢ 0 ≤ cfcₙ f a

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type ?u.999960) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ 0 ≤ cfcₙ f a

Tactic:
obtain ⟨h₁, h₂⟩ := hf

Result:
case pos.intro
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type ?u.999960) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
h₁ : ContinuousOn f (σₙ R a)
h₂ : f 0 = 0
⊢ 0 ≤ cfcₙ f a