awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalRing R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
a : A
⊢ cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a
have pos : ∀ (h : p a ∧ ContinuousOn f (spectrum R a)), cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a
Tactic: by_cases h : p a ∧ ContinuousOn f (spectrum R a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalRing R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
a : A
pos : ∀ (h : p a ∧ ContinuousOn f (spectrum R a)), 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
have neg : ∀ (h : ¬(p a ∧ ContinuousOn f (spectrum R a))), cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a
Tactic: by_cases h : p a ∧ ContinuousOn f (spectrum R a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (hypothesis)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalRing R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : p a ∧ ContinuousOn f (spectrum R a)
⊢ cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a
have ha : p a
Tactic: obtain ⟨ha, hf⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (hypothesis)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalRing R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : p a ∧ ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a
have hf : ContinuousOn f (spectrum R a)
Tactic: obtain ⟨ha, hf⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalRing R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a
have pos : Eq.{u_2 + 1} (α := A)
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ -f x, continuous_toFun := sorry :
        C((↑(spectrum R a) : Type u_1), R) } :
    A)
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (-{ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
          C((↑(spectrum R a) : Type u_1), R) }) :
    A)
Tactic: rw [cfc_apply f a, ← map_neg, cfc_apply ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalRing R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
⊢ cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a
have neg : ∀ (ha : ¬p a), cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a
Tactic: obtain (ha | hf) := not_and_or.mp h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalRing R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
neg : ∀ (ha : ¬p a), 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
have neg₁ : ∀ (hf : ¬ContinuousOn f (spectrum R a)), cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a
Tactic: obtain (ha | hf) := not_and_or.mp h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalRing R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ cfc (p := p) (fun (x : R) ↦ -f x) a = -cfc (p := p) f a
have neg : ¬ContinuousOn (Y := R) (fun (x : R) ↦ -f x) (spectrum R a)
Tactic: rw [cfc_apply_of_not_continuousOn a hf, cfc_apply_of_not_continuousOn, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalRing R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
⊢ cfc (p := p) (-f) = -cfc (p := p) f
have h : ∀ (a : A), cfc (p := p) (-f) a = (-cfc (p := p) f) a
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalRing R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ -x) a = -a
have rw : -cfc (p := p) (fun (x : R) ↦ x) a = -a
Tactic: rw [cfc_neg _ a, cfc_id' R a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalRing R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
rw : -cfc (p := p) (fun (x : R) ↦ x) a = -a
⊢ cfc (p := p) (fun (x : R) ↦ -x) a = -a
have rw₁ : -a = -a
Tactic: rw [cfc_neg _ a, cfc_id' R a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalRing R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
a : A
inst_10 : UniqueHom R A
hf : ContinuousOn f ((fun (x : R) ↦ -x) '' spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ f (-x)) a = cfc (p := p) f (-a)
have rw : cfc (p := p) f (cfc.{u_1, u_2} (R := R) (p := p) Neg.neg a) = cfc (p := p) f (-a)
Tactic: rw [cfc_comp' .., cfc_neg_id _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalRing R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
a : A
inst_10 : UniqueHom R A
hf : ContinuousOn f ((fun (x : R) ↦ -x) '' spectrum R a)
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)
⊢ cfc (p := p) (fun (x : R) ↦ f (-x)) a = cfc (p := p) f (-a)
have rw₁ : cfc (p := p) f (-a) = cfc (p := p) f (-a)
Tactic: rw [cfc_comp' .., cfc_neg_id _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
⊢ LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) ↔ 0 ≤ f
have mp : LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) → 0 ≤ f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
mp : LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) → 0 ≤ f
⊢ LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) ↔ 0 ≤ f
have mpr : 0 ≤ f → LE.le.{u_2} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
⊢ IsStrictlyPositive.{u_2} (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) ↔
    ∀ (x : (↑(spectrum R a) : Type u_1)), LT.lt (α := R) (0 : R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
have refine : ∀
  (h :
    ∀ (x : (↑(spectrum R a) : Type u_1)), LT.lt (α := R) (0 : R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)),
  IsUnit.{u_2} (M := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
Tactic: refine ⟨fun hf x => hf.spectrum_pos <| cfcHom_map_spectrum (R := R) ha _ ▸ Set.mem_range_self x,
    fun h => ⟨cfcHom_nonneg_iff _ |>.mpr fun x => le_of_lt (h x), ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
h : ∀ (x : (↑(spectrum R a) : Type u_1)), LT.lt (α := R) (0 : R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
⊢ IsUnit.{u_2} (M := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
have apply : 0 ∉ spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
Tactic: apply spectrum.isUnit_of_zero_notMem (R := R)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
⊢ cfc (p := p) f a ≤ cfc (p := p) g a
have pos : ∀ (ha : p a), cfc (p := p) f a ≤ cfc (p := p) g a
Tactic: by_cases ha : p a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
pos : ∀ (ha : p a), cfc (p := p) f a ≤ cfc (p := p) g a
⊢ cfc (p := p) f a ≤ cfc (p := p) g a
have neg : ∀ (ha : ¬p a), cfc (p := p) f a ≤ cfc (p := p) g a
Tactic: by_cases ha : p a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ cfc (p := p) f a ≤ cfc (p := p) g a
have pos : LE.le.{u_2} (α := A)
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
        C((↑(spectrum R a) : Type u_1), R) } :
    A)
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := sorry :
        C((↑(spectrum R a) : Type u_1), R) } :
    A)
Tactic: rw [cfc_apply f a, cfc_apply g a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ 0 ≤ cfc (p := p) f a ↔ ∀ x ∈ spectrum R a, 0 ≤ f x
have rw : (∀ (a_1 : (↑(spectrum R a) : Type u_1)),
    LE.le (α := R) ((0 : (a : (↑(spectrum R a) : Type u_1)) → R) a_1 : R)
      (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
              C((↑(spectrum R a) : Type u_1), R) } :
            (a : (↑(spectrum R a) : Type u_1)) → R)
          a_1 :
        R)) ↔
  ∀ x ∈ spectrum R a, 0 ≤ f x
Tactic: rw [cfc_apply .., cfcHom_nonneg_iff, ContinuousMap.le_def]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (hypothesis)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
⊢ 0 ≤ a ↔ ∀ x ∈ spectrum R a, 0 ≤ x
have this : 0 ≤ cfc.{u_1, u_2} (R := R) (p := p) id a ↔ ∀ x ∈ spectrum R a, 0 ≤ id x
Tactic: have := cfc_nonneg_iff (id : R → R) a (by fun_prop) ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ IsStrictlyPositive (cfc (p := p) f a) ↔ ∀ x ∈ spectrum R a, 0 < f x
have rw : (∀ (x : (↑(spectrum R a) : Type u_1)),
    LT.lt (α := R) (0 : R)
      (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
              C((↑(spectrum R a) : Type u_1), R) } :
            (a : (↑(spectrum R a) : Type u_1)) → R)
          x :
        R)) ↔
  ∀ x ∈ spectrum R a, 0 < f x
Tactic: rw [cfc_apply .., cfcHom_isStrictlyPositive_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (hypothesis)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_14 : NonnegSpectrumClass R A
a : A
ha : p a
⊢ IsStrictlyPositive a ↔ ∀ x ∈ spectrum R a, 0 < x
have this : IsStrictlyPositive (cfc.{u_1, u_2} (R := R) (p := p) id a) ↔ ∀ x ∈ spectrum R a, 0 < id x
Tactic: have := cfc_isStrictlyPositive_iff (id : R → R) a (by fun_prop) ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, 0 ≤ f x
⊢ 0 ≤ cfc (p := p) f a
have pos : ∀ (hf : ContinuousOn f (spectrum R a)), 0 ≤ cfc (p := p) f a
Tactic: by_cases hf : ContinuousOn f (spectrum R a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, 0 ≤ f x
pos : ∀ (hf : ContinuousOn f (spectrum R a)), 0 ≤ cfc (p := p) f a
⊢ 0 ≤ cfc (p := p) f a
have neg : ∀ (hf : ¬ContinuousOn f (spectrum R a)), 0 ≤ cfc (p := p) f a
Tactic: by_cases hf : ContinuousOn f (spectrum R a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 0
⊢ cfc (p := p) f a ≤ 0
have pos : ∀ (hf : ContinuousOn f (spectrum R a)), cfc (p := p) f a ≤ 0
Tactic: by_cases hf : ContinuousOn f (spectrum R a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 0
pos : ∀ (hf : ContinuousOn f (spectrum R a)), cfc (p := p) f a ≤ 0
⊢ cfc (p := p) f a ≤ 0
have neg : ∀ (hf : ¬ContinuousOn f (spectrum R a)), cfc (p := p) f a ≤ 0
Tactic: by_cases hf : ContinuousOn f (spectrum R a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
a : A
h : ∀ x ∈ spectrum R a, x ≤ r
ha : p a
⊢ a ≤ (algebraMap R A : (a : R) → A) r
have rw : cfc.{u_1, u_2} (R := R) (p := p) id a ≤ (algebraMap R A : (a : R) → A) r
Tactic: rw [← cfc_id R a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : ContinuousSqrt R
inst_7 : StarOrderedRing R
inst_8 : TopologicalSpace A
inst_9 : Ring A
inst_10 : StarRing A
inst_11 : PartialOrder A
inst_12 : StarOrderedRing A
inst_13 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
a : A
h : ∀ x ∈ spectrum R a, r ≤ x
ha : p a
⊢ (algebraMap R A : (a : R) → A) r ≤ a
have rw : (algebraMap R A : (a : R) → A) r ≤ cfc.{u_1, u_2} (R := R) (p := p) id a
Tactic: rw [← cfc_id R a]