-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_mono {f g : R → R} {a : A} (h : ∀ x ∈ σₙ R a, f x ≤ g x)
    (hf : ContinuousOn f (σₙ R 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.940962) [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 g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha : p a
⊢ cfcₙ f a ≤ cfcₙ g a

Tactic:
rw [cfcₙ_apply f a, cfcₙ_apply g a]

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.940962) [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 g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha : p a
⊢ (cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } ≤
    (cfcₙHom ha) { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }

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.940962) [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 g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha : p a
⊢ (cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } ≤
    (cfcₙHom ha) { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }

Tactic:
exact cfcₙHom_mono ha fun x ↦ h x.1 x.2

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 g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha : ¬p a
⊢ cfcₙ f a ≤ cfcₙ g a

Tactic:
simp only [cfcₙ_apply_of_not_predicate _ ha, le_rfl]

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.940962) [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 g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
⊢ cfcₙ f a ≤ cfcₙ g a

Tactic:
by_cases ha : p a

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.940962) [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 g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha : p a
⊢ cfcₙ f a ≤ cfcₙ g 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.940962) [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 g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha : ¬p a
⊢ cfcₙ f a ≤ cfcₙ g a