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
ha : p a
hf : ∀ (i : ι), ContinuousOn (f i) (σₙ R a)
hf0 : ∀ (i : ι), f i 0 = 0
⊢ Eq (α := (i : ι) → A) (fun (i : ι) ↦ cfcₙ (p := p) (f i) a) fun (i : ι) ↦
    (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f i), continuous_toFun := ⋯, map_zero' := ⋯ }
have h : ∀ (i : ι),
  cfcₙ (p := p) (f i) a =
    (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f i), continuous_toFun := sorry, map_zero' := sorry }
Tactic: ext i
-- 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 ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ cfcₙ (p := p) f a = 0
have rw : Eq.{u_2 + 1} (α := A)
  (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
    (cfcₙHom (p := p) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry }
  else 0)
  0
Tactic: rw [cfcₙ_def, dif_neg ha]
-- 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 ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
      (cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }
    else 0)
    0
⊢ cfcₙ (p := p) f a = 0
have rw₁ : Eq.{u_2 + 1} (α := A) 0 0
Tactic: rw [cfcₙ_def, dif_neg ha]
-- 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
⊢ cfcₙ (p := p) f a = 0
have rw : Eq.{u_2 + 1} (α := A)
  (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
    (cfcₙHom (p := p) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry }
  else 0)
  0
Tactic: rw [cfcₙ_def, dif_neg (not_and_of_not_left _ ha)]
-- 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
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
      (cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }
    else 0)
    0
⊢ cfcₙ (p := p) f a = 0
have rw₁ : Eq.{u_2 + 1} (α := A) 0 0
Tactic: rw [cfcₙ_def, dif_neg (not_and_of_not_left _ ha)]
-- 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) f a = 0
have rw : Eq.{u_2 + 1} (α := A)
  (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
    (cfcₙHom (p := p) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry }
  else 0)
  0
Tactic: rw [cfcₙ_def, dif_neg (not_and_of_not_right _ (not_and_of_not_left _ 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
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
      (cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }
    else 0)
    0
⊢ cfcₙ (p := p) f a = 0
have rw₁ : Eq.{u_2 + 1} (α := A) 0 0
Tactic: rw [cfcₙ_def, dif_neg (not_and_of_not_right _ (not_and_of_not_left _ 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
f : R → R
a : A
hf : ¬f 0 = 0
⊢ cfcₙ (p := p) f a = 0
have rw : Eq.{u_2 + 1} (α := A)
  (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
    (cfcₙHom (p := p) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry }
  else 0)
  0
Tactic: rw [cfcₙ_def, dif_neg (not_and_of_not_right _ (not_and_of_not_right _ 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
f : R → R
a : A
hf : ¬f 0 = 0
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
      (cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }
    else 0)
    0
⊢ cfcₙ (p := p) f a = 0
have rw₁ : Eq.{u_2 + 1} (α := A) 0 0
Tactic: rw [cfcₙ_def, dif_neg (not_and_of_not_right _ (not_and_of_not_right _ 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
a : A
g : R → R
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
⊢ (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) =
    (σₙ R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
        (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
have h : ∀ (x : (↑(σₙ R a) : Type u_1)),
  (f : (a : (↑(σₙ R a) : Type u_1)) → R) x =
    (σₙ R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
        (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
      x
Tactic: ext
-- 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
a : A
g : R → R
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
⊢ (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f =
    cfcₙ (p := p)
      (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
        (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
      a
have h : (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) =
  (σₙ R a).restrict (π := fun (a : R) ↦ R)
    (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
      (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
Tactic: have h : f = (σₙ R a).restrict (Function.extend Subtype.val f g) := by
    ext; simp
-- 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
a : A
g : R → R
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
h :
  (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) =
    (σₙ R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
        (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
⊢ (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f =
    cfcₙ (p := p)
      (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
        (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
      a
have hg : ContinuousOn
  (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
    (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
  (σₙ R a)
Tactic: have hg : ContinuousOn (Function.extend Subtype.val f g) (σₙ R a) :=
    continuousOn_iff_continuous_restrict.mpr <| h ▸ map_continuous f
-- 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
a : A
g : R → R
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
h :
  (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) =
    (σₙ R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
        (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
hg :
  ContinuousOn
    (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
      (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
    (σₙ R a)
⊢ Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
      (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g 0 =
    0
have rw : Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) 0 : R) ((↑0 : R) : R)
Tactic: rw [← quasispectrum.coe_zero (R := R) a, Subtype.val_injective.extend_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 : 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
a : A
g : R → R
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
h :
  (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) =
    (σₙ R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
        (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
hg :
  ContinuousOn
    (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
      (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
    (σₙ R a)
⊢ (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f =
    cfcₙ (p := p)
      (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
        (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
      a
have hg0 : Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
    (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g 0 =
  0
Tactic: have hg0 : (Function.extend Subtype.val f g) 0 = 0 := by
    rw [← quasispectrum.coe_zero (R := R) a, Subtype.val_injective.extend_apply]
    exact map_zero f
-- 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
a : A
g : R → R
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
h :
  (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) =
    (σₙ R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
        (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
hg :
  ContinuousOn
    (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
      (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
    (σₙ R a)
hg0 :
  Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
      (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g 0 =
    0
⊢ (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f =
    cfcₙ (p := p)
      (Function.extend (α := { x : R // x ∈ σₙ R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ σₙ R a))
        (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) g)
      a
have generalize : ∀ (f' : R → R) (h : (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) = (σₙ R a).restrict (π := fun (a : R) ↦ R) f')
  (hg : ContinuousOn f' (σₙ R a)) (hg0 : f' 0 = 0),
  (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f = cfcₙ (p := p) f' a
Tactic: generalize Function.extend Subtype.val f g = f' at *
Cleared hypotheses: h, hg, hg0
-- 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
a : A
g : R → R
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
f' : R → R
h : (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R) = (σₙ R a).restrict (π := fun (a : R) ↦ R) f'
hg : ContinuousOn f' (σₙ R a)
hg0 : f' 0 = 0
⊢ (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f = cfcₙ (p := p) f' a
have rw : Eq.{u_2 + 1} (α := 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)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f', continuous_toFun := sorry, map_zero' := sorry } :
    A)
Tactic: rw [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 : 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
a : A
f : R → R
ha : p a
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
⊢ cfcₙ (p := p) f a =
    ((cfcₙL (p := p) ha : C((↑(σₙ R a) : Type u_1), R)₀ →L[R] A) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := hf0 }
have rw : Eq.{u_2 + 1} (α := A)
  (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
      (cfcₙHom (p := p) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry }
    else 0 :
    A)
  (((cfcₙL (p := p) ha : C((↑(σₙ R a) : Type u_1), R)₀ →L[R] A) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := hf0 } :
    A)
Tactic: rw [cfcₙ_def, dif_pos ⟨ha, hf, hf0⟩, cfcₙL_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 : 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
a : A
f : R → R
ha : p a
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
        (cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }
      else 0 :
      A)
    (((cfcₙL (p := p) ha : C((↑(σₙ R a) : Type u_1), R)₀ →L[R] A) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := hf0 } :
      A)
⊢ cfcₙ (p := p) f a =
    ((cfcₙL (p := p) ha : C((↑(σₙ R a) : Type u_1), R)₀ →L[R] A) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := hf0 }
have rw₁ : Eq.{u_2 + 1} (α := A)
  ((cfcₙHom (p := p) sorry : (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ₙL (p := p) ha : C((↑(σₙ R a) : Type u_1), R)₀ →L[R] A) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := hf0 } :
    A)
Tactic: rw [cfcₙ_def, dif_pos ⟨ha, hf, hf0⟩, cfcₙL_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 : 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
a : A
f : R → R
ha : p a
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
        (cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }
      else 0 :
      A)
    (((cfcₙL (p := p) ha : C((↑(σₙ R a) : Type u_1), R)₀ →L[R] A) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := hf0 } :
      A)
rw₁ :
  Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ } :
      A)
    (((cfcₙL (p := p) ha : C((↑(σₙ R a) : Type u_1), R)₀ →L[R] A) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := hf0 } :
      A)
⊢ cfcₙ (p := p) f a =
    ((cfcₙL (p := p) ha : C((↑(σₙ R a) : Type u_1), R)₀ →L[R] A) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := hf0 }
have rw₂ : Eq.{u_2 + 1} (α := A)
  ((cfcₙHom (p := p) sorry : (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) f, continuous_toFun := sorry, map_zero' := hf0 } :
    A)
Tactic: rw [cfcₙ_def, dif_pos ⟨ha, hf, hf0⟩, cfcₙL_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 : 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
⊢ cfcₙ (p := p) f a =
    (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) (mkD ((σₙ R a).restrict (π := fun (a : R) ↦ R) f) 0)
have pos : ∀ (f_cont : ContinuousOn f (σₙ R a)),
  cfcₙ (p := p) f a =
    (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) (mkD ((σₙ R a).restrict (π := fun (a : R) ↦ R) f) 0)
Tactic: by_cases f_cont : ContinuousOn f (quasispectrum R a)