-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_nonneg_iff [NonnegSpectrumClass R A] (f : R → R) (a : A)
    (hf : ContinuousOn f (σₙ R a)

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_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
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
h0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ (∀ (x : ↑(σₙ R a)), 0 x ≤ { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } x) ↔
    ∀ x ∈ σₙ R a, 0 ≤ f x

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

Result:
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
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
h0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ (∀ (a_1 : R) (b : a_1 ∈ σₙ R a), 0 ⟨a_1, b⟩ ≤ f a_1) ↔ ∀ x ∈ σₙ R a, 0 ≤ f x

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_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
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
h0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ (∀ (a_1 : R) (b : a_1 ∈ σₙ R a), 0 ⟨a_1, b⟩ ≤ f a_1) ↔ ∀ x ∈ σₙ R a, 0 ≤ f x

Tactic:
congr!

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.959757) [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
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
h0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ 0 ≤ cfcₙ f a ↔ ∀ x ∈ σₙ R a, 0 ≤ f x

Tactic:
rw [cfcₙ_apply .., cfcₙHom_nonneg_iff, ContinuousMapZero.le_def]

Result:
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
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
h0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ (∀ (x : ↑(σₙ R a)), 0 x ≤ { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } x) ↔
    ∀ x ∈ σₙ R a, 0 ≤ f x