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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (σₙ R a)
⊢ cfcₙ.{u_1, u_2} (R := R) (p := p) (∑ i ∈ s, f i) a = ∑ i ∈ s, cfcₙ (p := p) (f i) a
have pos : cfcₙ.{u_1, u_2} (R := R) (p := p) (∑ i : ↥s, f (↑i : ι)) a = ∑ i : ↥s, cfcₙ (p := p) (f (↑i : ι)) a
Tactic: rw [← sum_coe_sort s, ← sum_coe_sort s]
-- 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (σₙ R a)
⊢ cfcₙ.{u_1, u_2} (R := R) (p := p) (∑ i : ↥s, f (↑i : ι)) a = ∑ i : ↥s, cfcₙ (p := p) (f (↑i : ι)) 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) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := sorry,
        map_zero' := sorry } :
    A)
  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      (∑ x : ↥s,
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := sorry, map_zero' := sorry }) :
    A)
Tactic: rw [cfcₙ_apply_pi _ a ha (fun ⟨i, hi⟩ => hf i hi), ← map_sum, cfcₙ_apply _ a 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 : 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (σₙ R a)
⊢ 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) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := ⋯,
          map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (∑ x : ↥s,
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯, map_zero' := ⋯ }) :
      A)
have pos : Eq (α := C((↑(σₙ R a) : Type u_1), R)₀)
  { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := sorry, map_zero' := sorry }
  (∑ x : ↥s, { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := sorry, map_zero' := sorry })
Tactic: congr 1
-- 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (σₙ R a)
⊢ Eq (α := C((↑(σₙ R a) : Type u_1), R)₀)
    { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := ⋯, map_zero' := ⋯ }
    (∑ x : ↥s,
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯, map_zero' := ⋯ })
have pos : ∀ (x : (↑(σₙ R a) : Type u_1)),
  Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := sorry,
            map_zero' := sorry } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        x :
      R)
    ((∑ x : ↥s,
            { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := sorry, map_zero' := sorry } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        x :
      R)
Tactic: ext
-- 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
S : Type u_3
inst_12 : SMulZeroClass S R
inst_13 : ContinuousConstSMul S R
inst_14 : SMulZeroClass S A
inst_15 : IsScalarTower S R A
inst_16 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
⊢ cfcₙ (p := p) (fun (x : R) ↦ s • f x) a = s • cfcₙ (p := p) f a
have pos : ∀ (ha : p a), cfcₙ (p := p) (fun (x : R) ↦ s • f x) a = s • cfcₙ (p := p) f 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 : 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
S : Type u_3
inst_12 : SMulZeroClass S R
inst_13 : ContinuousConstSMul S R
inst_14 : SMulZeroClass S A
inst_15 : IsScalarTower S R A
inst_16 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
pos : ∀ (ha : p a), cfcₙ (p := p) (fun (x : R) ↦ s • f x) a = s • cfcₙ (p := p) f a
⊢ cfcₙ (p := p) (fun (x : R) ↦ s • f x) a = s • cfcₙ (p := p) f a
have neg : ∀ (ha : ¬p a), cfcₙ (p := p) (fun (x : R) ↦ s • f x) a = s • cfcₙ (p := p) f 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 : 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
S : Type u_3
inst_12 : SMulZeroClass S R
inst_13 : ContinuousConstSMul S R
inst_14 : SMulZeroClass S A
inst_15 : IsScalarTower S R A
inst_16 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ cfcₙ (p := p) (fun (x : R) ↦ s • f x) a = s • cfcₙ (p := p) f a
have pos : (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) ↦ s • f x, continuous_toFun := sorry, map_zero' := sorry } =
  HSMul.hSMul (β := A) s
    ((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 :
          C((↑(σₙ R a) : Type u_1), R)₀ } :
      A)
Tactic: rw [cfcₙ_apply f a, cfcₙ_apply _ 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 : 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
S : Type u_3
inst_12 : SMulZeroClass S R
inst_13 : ContinuousConstSMul S R
inst_14 : SMulZeroClass S A
inst_15 : IsScalarTower S R A
inst_16 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p 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) ↦ s • f x, continuous_toFun := ⋯,
        map_zero' := ⋯ } =
    HSMul.hSMul (β := A) s
      ((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' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A)
have pos : (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
    { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (HSMul.hSMul (β := R) s 1 • f), continuous_toFun := sorry,
      map_zero' := sorry } =
  HSMul.hSMul (β := A) (HSMul.hSMul (β := R) s 1)
    ((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 :
          C((↑(σₙ R a) : Type u_1), R)₀ } :
      A)
Tactic: simp_rw [← Pi.smul_def, ← smul_one_smul R s _]
-- 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
S : Type u_3
inst_12 : SMulZeroClass S R
inst_13 : ContinuousConstSMul S R
inst_14 : SMulZeroClass S A
inst_15 : IsScalarTower S R A
inst_16 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (HSMul.hSMul (β := R) s 1 • f), continuous_toFun := ⋯,
        map_zero' := ⋯ } =
    HSMul.hSMul (β := A) (HSMul.hSMul (β := R) s 1)
      ((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' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        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) (HSMul.hSMul (β := R) s 1 • f), continuous_toFun := sorry,
        map_zero' := sorry } :
    A)
  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      (HSMul.hSMul (β := C((↑(σₙ R a) : Type u_1), R)₀) (HSMul.hSMul (β := R) s 1)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry :
          C((↑(σₙ R a) : Type u_1), R)₀ }) :
    A)
Tactic: rw [← map_smul]
-- 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
a : A
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
have pos : ∀ (h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0), cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (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 : 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
a : A
pos :
  ∀ (h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0), cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
have neg : ∀ (h : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)),
  cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (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 : 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
a : A
h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (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 : 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
a : A
h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0
ha : p a
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (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 : 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
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) ↦ star (f x)) a = star (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 : 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
a : A
ha : p a
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (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) ↦ star (f x), continuous_toFun := sorry,
        map_zero' := sorry } :
    A)
  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      (star { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry }) :
    A)
Tactic: rw [cfcₙ_apply f a, ← map_star, cfcₙ_apply _ a]
-- 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 : 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
a : A
h : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (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 : 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
a : A
h : ¬p a ∨ ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
have neg : ∀ (ha : ¬p a), cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (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 : 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
a : A
h : ¬p a ∨ ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
neg : ∀ (ha : ¬p a), cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
have neg₁ : ∀ (hf : ¬ContinuousOn f (σₙ R a)), cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (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 : 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
a : A
h : ¬p a ∨ ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
neg : ∀ (ha : ¬p a), cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
neg₁ : ∀ (hf : ¬ContinuousOn f (σₙ R a)), cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
have neg₂ : ∀ (h0 : ¬f 0 = 0), cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (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 : 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
a : A
hf : ¬ContinuousOn f (σₙ R a)
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
have neg : ¬ContinuousOn (Y := R) (fun (x : R) ↦ star (f x)) (σₙ R a)
Tactic: rw [cfcₙ_apply_of_not_continuousOn a hf, cfcₙ_apply_of_not_continuousOn, star_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 : 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
a : A
h0 : ¬f 0 = 0
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x)) a = star (cfcₙ (p := p) f a)
have neg : ¬star (f 0) = 0
Tactic: rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero, star_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 : 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
S : Type u_3
inst_12 : SMulZeroClass S R
inst_13 : ContinuousConstSMul S R
inst_14 : SMulZeroClass S A
inst_15 : IsScalarTower S R A
inst_16 : IsScalarTower S R (R → R)
s : S
a : A
ha : p a
⊢ cfcₙ (p := p) (fun (x : R) ↦ s • x) a = s • a
have rw : s • cfcₙ (p := p) (fun (x : R) ↦ x) a = s • a
Tactic: rw [cfcₙ_smul s _ a, 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 : 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
S : Type u_3
inst_12 : SMulZeroClass S R
inst_13 : ContinuousConstSMul S R
inst_14 : SMulZeroClass S A
inst_15 : IsScalarTower S R A
inst_16 : IsScalarTower S R (R → R)
s : S
a : A
ha : p a
rw : s • cfcₙ (p := p) (fun (x : R) ↦ x) a = s • a
⊢ cfcₙ (p := p) (fun (x : R) ↦ s • x) a = s • a
have rw₁ : s • a = s • a
Tactic: rw [cfcₙ_smul s _ a, cfcₙ_id' R a]