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 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
pos : ∀ (hf0 : f 0 = 0), cfcₙ (p := p) f 0 = 0
⊢ cfcₙ (p := p) f 0 = 0
have neg : ∀ (hf0 : ¬f 0 = 0), cfcₙ (p := p) f 0 = 0
Tactic: by_cases hf0 : 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 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
hf0 : f 0 = 0
⊢ cfcₙ (p := p) f 0 = 0
have pos : cfcₙ (p := p) f 0 = cfcₙ.{u_1, u_2} (R := R) (p := p) 0 0
Tactic: nth_rw 2 [← cfcₙ_zero R 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 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
hf0 : f 0 = 0
⊢ cfcₙ (p := p) f 0 = cfcₙ.{u_1, u_2} (R := R) (p := p) 0 0
have pos : Set.EqOn f 0 (quasispectrum.{u_1, u_2} R (A := A) 0)
Tactic: apply cfcₙ_congr
-- 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 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
hf : ContinuousOn f_1 (σₙ R a_1)
hf0 : f_1 0 = 0
hg : ContinuousOn g (σₙ R a_1)
hg0 : g 0 = 0
ha : p a_1
f : R → R
a : A
⊢ Commute (star (cfcₙ (p := p) f a)) (cfcₙ (p := p) f a)
have refine : ∀ (x : ContinuousOn f (σₙ R a))
  (x_1 :
    Eq (α := R)
      (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry : C((↑(σₙ R a) : Type u_1), R) } :
            (a : (↑(σₙ R a) : Type u_1)) → R)
          0 :
        R)
      (0 : R))
  (x_2 : p a),
  (fun (x : A) ↦ Commute (star x) x)
    ((cfcₙHom (p := p) x_2 : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := x_1 :
        C((↑(σₙ R a) : Type u_1), R)₀ })
Tactic: refine cfcₙ_cases (fun x ↦ Commute (star x) x) _ _ (Commute.zero_right _) fun _ _ _ ↦ ?_
-- 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 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
hf : ContinuousOn f_1 (σₙ R a_1)
hf0 : f_1 0 = 0
hg : ContinuousOn g (σₙ R a_1)
hg0 : g 0 = 0
ha : p a_1
f : R → R
a : A
h : ContinuousOn f (σₙ R a)
h_1 :
  Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ : C((↑(σₙ R a) : Type u_1), R) } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        0 :
      R)
    (0 : R)
h_2 : p a
⊢ HMul.hMul (α := A) (β := A)
      (star
          ((cfcₙHom (p := p) h_2 : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
            { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := h_1 :
              C((↑(σₙ R a) : Type u_1), R)₀ }) :
        A)
      ((cfcₙHom (p := p) h_2 : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := h_1 :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A) =
    HMul.hMul (α := A) (β := A)
      ((cfcₙHom (p := p) h_2 : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := h_1 :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A)
      (star
          ((cfcₙHom (p := p) h_2 : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
            { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := h_1 :
              C((↑(σₙ R a) : Type u_1), R)₀ }) :
        A)
have rw : cfcₙ (p := p) (fun (x : R) ↦ star (f x) * f x) a = cfcₙ (p := p) (fun (x : R) ↦ f x * star (f x)) a
Tactic: rw [← cfcₙ_apply f a, ← cfcₙ_star, ← cfcₙ_mul .., ← cfcₙ_mul ..]
-- 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 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
hf : ContinuousOn f_1 (σₙ R a_1)
hf0 : f_1 0 = 0
hg : ContinuousOn g (σₙ R a_1)
hg0 : g 0 = 0
ha : p a_1
f : R → R
a : A
h : ContinuousOn f (σₙ R a)
h_1 :
  Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ : C((↑(σₙ R a) : Type u_1), R) } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        0 :
      R)
    (0 : R)
h_2 : p a
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x) * f x) a = cfcₙ (p := p) (fun (x : R) ↦ f x * star (f x)) a
have h : ∀ (x : R), star (f x) * f x = f x * star (f x)
Tactic: congr! 2
-- 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 : 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 g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
⊢ cfcₙ (p := p) (fun (x : R) ↦ f x - g x) a = cfcₙ (p := p) f a - cfcₙ (p := p) g a
have pos : ∀ (ha : p a), cfcₙ (p := p) (fun (x : R) ↦ f x - g x) 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 : 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 g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
pos : ∀ (ha : p a), cfcₙ (p := p) (fun (x : R) ↦ f x - g x) a = cfcₙ (p := p) f a - cfcₙ (p := p) g a
⊢ cfcₙ (p := p) (fun (x : R) ↦ f x - g x) a = cfcₙ (p := p) f a - cfcₙ (p := p) g a
have neg : ∀ (ha : ¬p a), cfcₙ (p := p) (fun (x : R) ↦ f x - g x) 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 : 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 g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
ha : p a
⊢ cfcₙ (p := p) (fun (x : R) ↦ f x - g x) a = cfcₙ (p := p) f a - cfcₙ (p := p) g a
have 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 - g x, continuous_toFun := sorry,
        map_zero' := sorry } :
    A)
  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      (HSub.hSub (α := C((↑(σₙ R a) : Type u_1), R)₀)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry :
          C((↑(σₙ R a) : Type u_1), R)₀ }
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := sorry, map_zero' := sorry :
          C((↑(σₙ R a) : Type u_1), R)₀ }) :
    A)
Tactic: rw [cfcₙ_apply f a, cfcₙ_apply g a, ← map_sub, cfcₙ_apply ..]
-- 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 : 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) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
have pos : ∀ (h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0), cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
Tactic: by_cases h : p a ∧ 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 : 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
pos : ∀ (h : p a ∧ ContinuousOn f (σₙ R a) ∧ 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
have neg : ∀ (h : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)), cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
Tactic: by_cases h : p a ∧ 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 : 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
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
have ha : p a
Tactic: obtain ⟨ha, hf, h0⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
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
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
have hf : ContinuousOn f (σₙ R a)
Tactic: obtain ⟨ha, hf, h0⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
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)
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
have h0 : f 0 = 0
Tactic: obtain ⟨ha, hf, h0⟩ := h
Cleared hypotheses: h
-- 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 : 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
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
have 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 := 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) f, continuous_toFun := sorry, map_zero' := sorry }) :
    A)
Tactic: rw [cfcₙ_apply f a, ← map_neg, cfcₙ_apply ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
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)
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
have h₁ : ¬p a ∨ ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
Tactic: simp only [not_and_or] at h
Cleared hypotheses: h
-- 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 : 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
⊢ 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 | h0) := h
Cleared hypotheses: h
-- 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 : 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
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
have neg₁ : ∀ (hf : ¬ContinuousOn f (σₙ R a)), cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
Tactic: obtain (ha | hf | h0) := h
Cleared hypotheses: h
-- 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 : 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
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
have neg₂ : ∀ (h0 : ¬f 0 = 0), cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
Tactic: obtain (ha | hf | h0) := h
Cleared hypotheses: h
-- 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 : 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)
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
have neg : ¬ContinuousOn (Y := R) (fun (x : R) ↦ -f x) (σₙ 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.NonUnital (goal)
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
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
have neg : ¬-f 0 = 0
Tactic: rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero, neg_zero]
-- 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 : 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
⊢ 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.NonUnital (goal)
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
⊢ cfcₙ (p := p) (fun (x : R) ↦ -x) a = -a
have rw : -cfcₙ (p := p) (fun (x : R) ↦ x) a = -a
Tactic: rw [cfcₙ_neg .., cfcₙ_id' R 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 : 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
⊢ cfcₙ (p := p) (fun (x : R) ↦ -x) a = -a
have rw₁ : -a = -a
Tactic: rw [cfcₙ_neg .., cfcₙ_id' R 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 : 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
⊢ 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.NonUnital (goal)
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)
⊢ 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.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)₀
⊢ 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 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
Tactic: constructor