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
a : A
ha : p a
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)
⊢ 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 neg : ∀ (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)
-- 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
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)
have pos : ∀ (f_zero : f 0 = 0),
  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_zero : 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
ha : p a
f_cont : ContinuousOn f (σₙ R a)
pos :
  ∀ (f_zero : f 0 = 0),
    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)
⊢ 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 neg : ∀ (f_zero : ¬f 0 = 0),
  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_zero : 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
ha : p a
f_cont : ContinuousOn f (σₙ R a)
f_zero : f 0 = 0
⊢ 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 : 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) f, continuous_toFun := sorry, map_zero' := sorry } :
    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) :
    A)
Tactic: rw [cfcₙ_apply f a, mkD_of_continuousOn f_cont f_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
ha : p a
f_cont : ContinuousOn f (σₙ R a)
f_zero : f 0 = 0
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) f, continuous_toFun := ⋯, map_zero' := ⋯ } :
      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) :
      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₁ : 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) 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' := f_zero } :
    A)
Tactic: rw [cfcₙ_apply f a, mkD_of_continuousOn f_cont f_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
ha : p a
f_cont : ContinuousOn f (σₙ R a)
f_zero : ¬f 0 = 0
⊢ 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 neg : (σₙ R a).restrict (π := fun (a : R) ↦ R) f 0 ≠ 0
Tactic: rw [cfcₙ_apply_of_not_map_zero a f_zero, mkD_of_not_zero, map_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
ha : p a
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)
have neg : Eq.{u_2 + 1} (α := A) (0 : 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) :
    A)
Tactic: rw [cfcₙ_apply_of_not_continuousOn a f_cont, mkD_of_not_continuousOn f_cont, map_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
ha : p a
f_cont : ¬ContinuousOn f (σₙ R a)
neg :
  Eq.{u_2 + 1} (α := A) (0 : 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) :
      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 neg₁ : Eq.{u_2 + 1} (α := A) (0 : A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) 0 : A)
Tactic: rw [cfcₙ_apply_of_not_continuousOn a f_cont, mkD_of_not_continuousOn f_cont, map_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
ha : p a
f_cont : ¬ContinuousOn f (σₙ R a)
neg :
  Eq.{u_2 + 1} (α := A) (0 : 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) :
      A)
neg₁ : Eq.{u_2 + 1} (α := A) (0 : A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) 0 : 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 neg₂ : Eq.{u_2 + 1} (α := A) 0 0
Tactic: rw [cfcₙ_apply_of_not_continuousOn a f_cont, mkD_of_not_continuousOn f_cont, map_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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      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))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
⊢ P (cfcₙ (p := p) f a)
have pos : ∀ (h : ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a), P (cfcₙ (p := p) f a)
Tactic: by_cases h : ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ 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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      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))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
pos : ∀ (h : ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a), P (cfcₙ (p := p) f a)
⊢ P (cfcₙ (p := p) f a)
have neg : ∀ (h : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a)), P (cfcₙ (p := p) f a)
Tactic: by_cases h : ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ 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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      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))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
h : ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a
⊢ P (cfcₙ (p := p) f a)
have pos : P
  ((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 })
Tactic: rw [cfcₙ_apply f a h.1 h.2.1 h.2.2]
-- 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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      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))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
h : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a)
⊢ P (cfcₙ (p := p) f a)
have h₁ : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0 ∨ ¬p a
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      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))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
h : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0 ∨ ¬p a
⊢ P (cfcₙ (p := p) f a)
have neg : ∀ (h : ¬ContinuousOn f (σₙ R a)), P (cfcₙ (p := p) f a)
Tactic: obtain (h | h | h) := 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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      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))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
h : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0 ∨ ¬p a
neg : ∀ (h : ¬ContinuousOn f (σₙ R a)), P (cfcₙ (p := p) f a)
⊢ P (cfcₙ (p := p) f a)
have neg₁ : ∀ (h : ¬f 0 = 0), P (cfcₙ (p := p) f a)
Tactic: obtain (h | h | h) := 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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a))
    (h0 :
      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))
    (ha : p a),
    P
      ((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' := h0 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
h : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0 ∨ ¬p a
neg : ∀ (h : ¬ContinuousOn f (σₙ R a)), P (cfcₙ (p := p) f a)
neg₁ : ∀ (h : ¬f 0 = 0), P (cfcₙ (p := p) f a)
⊢ P (cfcₙ (p := p) f a)
have neg₂ : ∀ (h : ¬p a), P (cfcₙ (p := p) f a)
Tactic: obtain (h | h | h) := 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 g : R → R
a : A
⊢ Commute (cfcₙ (p := p) f a) (cfcₙ (p := p) g a)
have refine : ∀ (hf : ContinuousOn f (σₙ R a))
  (hf0 :
    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))
  (ha : p a),
  (fun (x : A) ↦ Commute x (cfcₙ (p := p) g 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 :
        C((↑(σₙ R a) : Type u_1), R)₀ })
Tactic: refine cfcₙ_cases (fun x ↦ Commute x (cfcₙ g a)) a f (by simp) fun hf hf0 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 g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 :
  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)
ha : p a
⊢ (fun (x : A) ↦ Commute x (cfcₙ (p := p) g 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 := ⋯, map_zero' := hf0 :
        C((↑(σₙ R a) : Type u_1), R)₀ })
have refine : ∀ (hg : ContinuousOn g (σₙ R a))
  (hg0 :
    Eq (α := R)
      (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := sorry : C((↑(σₙ R a) : Type u_1), R) } :
            (a : (↑(σₙ R a) : Type u_1)) → R)
          0 :
        R)
      (0 : R))
  (x : p a),
  (fun (x : A) ↦
      Commute
        ((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 :
            C((↑(σₙ R a) : Type u_1), R)₀ })
        x)
    ((cfcₙHom (p := p) x : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := sorry, map_zero' := hg0 :
        C((↑(σₙ R a) : Type u_1), R)₀ })
Tactic: refine cfcₙ_cases (fun x ↦ Commute _ x) a g (by simp) fun 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
f g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
⊢ cfcₙ (p := p) f a = cfcₙ (p := p) g a
have pos : ∀ (h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0), cfcₙ (p := p) f a = cfcₙ (p := p) g a
Tactic: by_cases h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 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 g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
pos : ∀ (h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0), cfcₙ (p := p) f a = cfcₙ (p := p) g a
⊢ cfcₙ (p := p) f a = cfcₙ (p := p) g a
have neg : ∀ (h : ¬(p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0)), cfcₙ (p := p) f a = cfcₙ (p := p) g a
Tactic: by_cases h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0