-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_mono {f g : R → R} {a : A} (h : ∀ x ∈ spectrum R a, f x ≤ g x)
    (hf : ContinuousOn f (spectrum R a)

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.644343) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _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✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.644343) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : p a
⊢ (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } ≤
    (cfcHom ha) { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.644343) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : p a
⊢ (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } ≤
    (cfcHom ha) { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }

Tactic:
exact cfcHom_mono ha fun x ↦ h x.1 x.2

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.644343) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _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✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.644343) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _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✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.644343) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : ¬p a
⊢ cfc f a ≤ cfc g a

Proof state:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : ¬p a
⊢ cfc f a ≤ cfc g a

Tactic:
simp only [cfc_apply_of_not_predicate _ ha, le_rfl]

Result:
no goals