awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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
⊢ 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
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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
⊢ 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.NonUnital (goal)
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
⊢ 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.NonUnital (goal)
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
have 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 := sorry, map_zero' := sorry } :
    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 := sorry, map_zero' := sorry } :
    A)
Tactic: rw [cfcₙ_apply f a, cfcₙ_apply g a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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
⊢ 0 ≤ cfcₙ (p := p) f a ↔ ∀ x ∈ σₙ R a, 0 ≤ f x
have 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 := sorry, map_zero' := sorry } :
            (a : (↑(σₙ R a) : Type u_1)) → R)
          x :
        R)) ↔
  ∀ x ∈ σₙ R a, 0 ≤ f x
Tactic: rw [cfcₙ_apply .., cfcₙHom_nonneg_iff, ContinuousMapZero.le_def]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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
⊢ (∀ (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
have simp : (∀ (a_1 : R) (b : a_1 ∈ σₙ R a),
    (0 : (a : (↑(σₙ R a) : Type u_1)) → R) (Subtype.mk (p := fun (a_2 : R) ↦ a_2 ∈ σₙ R a) a_1 b) ≤ f a_1) ↔
  ∀ x ∈ σₙ R a, 0 ≤ f x
Tactic: simp only [ContinuousMapZero.coe_mk, ContinuousMap.coe_mk, Set.restrict_apply, Subtype.forall]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
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
⊢ 0 ≤ a ↔ ∀ x ∈ σₙ R a, 0 ≤ x
have this : 0 ≤ cfcₙ.{u_1, u_2} (R := R) (p := p) id a ↔ ∀ x ∈ σₙ R a, 0 ≤ id x
Tactic: have := cfcₙ_nonneg_iff (id : R → R) a (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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 : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
⊢ 0 ≤ cfcₙ (p := p) f a
have pos : ∀ (hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0), 0 ≤ cfcₙ (p := p) f a
Tactic: by_cases hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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 : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
pos : ∀ (hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0), 0 ≤ cfcₙ (p := p) f a
⊢ 0 ≤ cfcₙ (p := p) f a
have neg : ∀ (hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)), 0 ≤ cfcₙ (p := p) f a
Tactic: by_cases hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
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 : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ 0 ≤ cfcₙ (p := p) f a
have h₁ : ContinuousOn f (σₙ R a)
Tactic: obtain ⟨h₁, h₂⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
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 : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
h₁ : ContinuousOn f (σₙ R a)
⊢ 0 ≤ cfcₙ (p := p) f a
have h₂ : f 0 = 0
Tactic: obtain ⟨h₁, h₂⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
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 : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ 0 ≤ cfcₙ (p := p) f a
have hf₁ : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
Tactic: simp only [not_and_or] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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 : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
⊢ 0 ≤ cfcₙ (p := p) f a
have neg : ∀ (hf : ¬ContinuousOn f (σₙ R a)), 0 ≤ cfcₙ (p := p) f a
Tactic: obtain (hf | hf) := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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 : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
neg : ∀ (hf : ¬ContinuousOn f (σₙ R a)), 0 ≤ cfcₙ (p := p) f a
⊢ 0 ≤ cfcₙ (p := p) f a
have neg₁ : ∀ (hf : ¬f 0 = 0), 0 ≤ cfcₙ (p := p) f a
Tactic: obtain (hf | hf) := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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 : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
⊢ cfcₙ (p := p) f a ≤ 0
have pos : ∀ (hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0), cfcₙ (p := p) f a ≤ 0
Tactic: by_cases hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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 : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
pos : ∀ (hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0), cfcₙ (p := p) f a ≤ 0
⊢ cfcₙ (p := p) f a ≤ 0
have neg : ∀ (hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)), cfcₙ (p := p) f a ≤ 0
Tactic: by_cases hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
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 : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ cfcₙ (p := p) f a ≤ 0
have h₁ : ContinuousOn f (σₙ R a)
Tactic: obtain ⟨h₁, h₂⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
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 : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
h₁ : ContinuousOn f (σₙ R a)
⊢ cfcₙ (p := p) f a ≤ 0
have h₂ : f 0 = 0
Tactic: obtain ⟨h₁, h₂⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
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 : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ cfcₙ (p := p) f a ≤ 0
have hf₁ : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
Tactic: simp only [not_and_or] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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 : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
⊢ cfcₙ (p := p) f a ≤ 0
have neg : ∀ (hf : ¬ContinuousOn f (σₙ R a)), cfcₙ (p := p) f a ≤ 0
Tactic: obtain (hf | hf) := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
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 : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
neg : ∀ (hf : ¬ContinuousOn f (σₙ R a)), cfcₙ (p := p) f a ≤ 0
⊢ cfcₙ (p := p) f a ≤ 0
have neg₁ : ∀ (hf : ¬f 0 = 0), cfcₙ (p := p) f a ≤ 0
Tactic: obtain (hf | hf) := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalRing 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 g : C((↑(σₙ R a) : Type u_1), R)₀
⊢ 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) ↔
    f ≤ g
have rw : 0 ≤
    HSub.hSub (α := A) (β := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A)
      ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A) ↔
  f ≤ g
Tactic: rw [← sub_nonneg, ← map_sub, cfcₙHom_nonneg_iff, sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalRing 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 g : C((↑(σₙ R a) : Type u_1), R)₀
rw :
  0 ≤
      HSub.hSub (α := A) (β := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A)
        ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A) ↔
    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) ↔
    f ≤ g
have rw₁ : LE.le.{u_2} (α := A) (0 : A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) (g - f) : A) ↔ f ≤ g
Tactic: rw [← sub_nonneg, ← map_sub, cfcₙHom_nonneg_iff, sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalRing 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 g : C((↑(σₙ R a) : Type u_1), R)₀
rw :
  0 ≤
      HSub.hSub (α := A) (β := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) g : A)
        ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A) ↔
    f ≤ g
rw₁ : LE.le.{u_2} (α := A) (0 : A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) (g - f) : A) ↔ 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) ↔
    f ≤ g
have rw₂ : 0 ≤ g - f ↔ f ≤ g
Tactic: rw [← sub_nonneg, ← map_sub, cfcₙHom_nonneg_iff, sub_nonneg]