awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0
ha : p a
hf : ContinuousOn f (σₙ R a)
⊢ f 0 = 0

Tactic:
obtain ⟨ha, hf, h0⟩ := h
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : p a
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
pos :
  Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ -f x, continuous_toFun := ⋯,
          map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (-{ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }) :
      A)
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a

Tactic:
rw [cfcₙ_apply f a, ← map_neg, cfcₙ_apply ..]

Premises used: map_neg, cfcₙ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : p a
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ -f x, continuous_toFun := ⋯,
          map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (-{ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }) :
      A)

Tactic:
congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ ¬p a ∨ ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0

Tactic:
simp only [not_and_or] at h

Premises used: not_and_or
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬p a ∨ ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
neg : ∀ (ha : ¬p a), cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
neg₁ : ∀ (hf : ¬ContinuousOn f (σₙ R a)), cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
neg₂ : ∀ (h0 : ¬f 0 = 0), cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a

Tactic:
obtain (ha | hf | h0) := h
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : ¬p a
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a

Tactic:
simp [cfcₙ_apply_of_not_predicate a ha]

Premises used: cfcₙ_apply_of_not_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
neg : ¬ContinuousOn (Y := R) (fun (x : R) ↦ -f x) (σₙ R a)
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a

Tactic:
rw [cfcₙ_apply_of_not_continuousOn a hf, cfcₙ_apply_of_not_continuousOn, neg_zero]

Premises used: neg_zero, cfcₙ_apply_of_not_continuousOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
hf_neg : ContinuousOn (Y := R) (fun (x : R) ↦ -f x) (σₙ R a)
⊢ ContinuousOn f (σₙ R a)

Tactic:
simpa using hf_neg.neg

Premises used: ContinuousOn.neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
⊢ ¬ContinuousOn (Y := R) (fun (x : R) ↦ -f x) (σₙ R a)

Tactic:
exact fun hf_neg ↦ hf <| by simpa using hf_neg.neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h0 : ¬f 0 = 0
neg : ¬-f 0 = 0
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a

Tactic:
rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero, neg_zero]

Premises used: cfcₙ_apply_of_not_map_zero, neg_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h0 : ¬f 0 = 0
⊢ ¬-f 0 = 0

Tactic:
(h0 <| neg_eq_zero.mp ·)

Premises used: neg_eq_zero, Iff.mp, Not
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h0 : ¬f 0 = 0
⊢ ¬-f 0 = 0

Tactic:
exact (h0 <| neg_eq_zero.mp ·)

Premises used: neg_eq_zero, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
h : ∀ (a : A), cfcₙ (p := p) (-f) a = (-cfcₙ (p := p) f) a
⊢ cfcₙ (p := p) (-f) = -cfcₙ (p := p) f

Tactic:
ext1 a
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
⊢ cfcₙ (p := p) (-f) a = (-cfcₙ (p := p) f) a

Tactic:
(cfcₙ_neg f a)

Premises used: cfcₙ_neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
⊢ cfcₙ (p := p) (-f) a = (-cfcₙ (p := p) f) a

Tactic:
exact (cfcₙ_neg f a)

Premises used: cfcₙ_neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
rw : -cfcₙ (p := p) (fun (x : R) ↦ x) a = -a
rw₁ rw₂ : -a = -a
⊢ cfcₙ (p := p) (fun (x : R) ↦ -x) a = -a

Tactic:
rw [cfcₙ_neg .., cfcₙ_id' R a]

Premises used: cfcₙ_neg, cfcₙ_id'
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
inst_13 : UniqueHom R A
hf : ContinuousOn f ((fun (x : R) ↦ -x) '' σₙ R a)
h0 : f 0 = 0
ha : p a
rw : cfcₙ (p := p) f (cfcₙ.{u_1, u_2} (R := R) (p := p) Neg.neg a) = cfcₙ (p := p) f (-a)
rw₁ rw₂ : cfcₙ (p := p) f (-a) = cfcₙ (p := p) f (-a)
⊢ cfcₙ (p := p) (fun (x : R) ↦ f (-x)) a = cfcₙ (p := p) f (-a)

Tactic:
rw [cfcₙ_comp' .., cfcₙ_neg_id _]

Premises used: cfcₙ_neg_id, cfcₙ_comp'
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
hfg : f ≤ g
⊢ LE.le.{u_2} (α := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A)

Tactic:
OrderHomClass.mono (cfcₙHom ha) hfg

Premises used: OrderHomClass.mono, cfcₙHom
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
mp : LE.le.{u_2} (α := A) (0 : A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A) → 0 ≤ f
mpr : 0 ≤ f → LE.le.{u_2} (α := A) (0 : A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)
⊢ LE.le.{u_2} (α := A) (0 : A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A) ↔ 0 ≤ f

Tactic:
constructor
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
⊢ LE.le.{u_2} (α := A) (0 : A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A) → 0 ≤ f

Tactic:
fun hf x ↦
      (cfcₙHom_map_quasispectrum ha (R := R) _ ▸ quasispectrum_nonneg_of_nonneg (cfcₙHom ha f) hf)
      _ ⟨x, rfl⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
⊢ LE.le.{u_2} (α := A) (0 : A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A) → 0 ≤ f

Tactic:
exact fun hf x ↦
      (cfcₙHom_map_quasispectrum ha (R := R) _ ▸ quasispectrum_nonneg_of_nonneg (cfcₙHom ha f) hf)
      _ ⟨x, rfl⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
⊢ 0 ≤ f → LE.le.{u_2} (α := A) (0 : A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)

Tactic:
simpa using (cfcₙHom_mono ha (f := 0) (g := f) ·)

Premises used: cfcₙHom_mono
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
pos : ∀ (ha : p a), cfcₙ (p := p) f a ≤ cfcₙ (p := p) g a
neg : ∀ (ha : ¬p a), cfcₙ (p := p) f a ≤ cfcₙ (p := p) g a
⊢ cfcₙ (p := p) f a ≤ cfcₙ (p := p) g a

Tactic:
by_cases ha : p a
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
ha : p a
pos :
  LE.le.{u_2} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := ⋯ } :
      A)
⊢ cfcₙ (p := p) f a ≤ cfcₙ (p := p) g a

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

Premises used: cfcₙ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
ha : p a
⊢ LE.le.{u_2} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := ⋯ } :
      A)

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

Premises used: cfcₙHom_mono, Subtype.val, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
ha : p a
⊢ LE.le.{u_2} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := ⋯ } :
      A)

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

Premises used: cfcₙHom_mono
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
ha : ¬p a
⊢ cfcₙ (p := p) f a ≤ cfcₙ (p := p) g a

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

Premises used: le_rfl, cfcₙ_apply_of_not_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
rw :
  (∀ (x : (↑(σₙ R a) : Type u_1)),
      LE.le (α := R) ((0 : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            x :
          R)) ↔
    ∀ x ∈ σₙ R a, 0 ≤ f x
⊢ 0 ≤ cfcₙ (p := p) f a ↔ ∀ x ∈ σₙ R a, 0 ≤ f x

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

Premises used: ContinuousMapZero.le_def, cfcₙ_apply, cfcₙHom_nonneg_iff