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

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.1025025) [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, f x ≤ 0
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ cfcₙ f a ≤ 0

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.1025025) [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, f x ≤ 0
h₁ : ContinuousOn f (σₙ R a)
h₂ : f 0 = 0
⊢ cfcₙ f a ≤ 0

Proof state:
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, f x ≤ 0
hf : ¬f 0 = 0
⊢ cfcₙ f a ≤ 0

Tactic:
simp only [cfcₙ_apply_of_not_map_zero _ 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, f x ≤ 0
hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ cfcₙ f a ≤ 0

Tactic:
simp only [not_and_or] at hf

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

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.1025025) [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, f x ≤ 0
⊢ cfcₙ f a ≤ 0

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.1025025) [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, f x ≤ 0
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ cfcₙ f a ≤ 0

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.1025025) [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, f x ≤ 0
hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ cfcₙ f a ≤ 0

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

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

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, f x ≤ 0
hf : ¬f 0 = 0
⊢ cfcₙ f a ≤ 0