awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
h₁ :
  Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
    (closure[Unitization.instUniformSpace.toTopologicalSpace]
      ((⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
        (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
              NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
          Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)
⊢ ContinuousMapZero.id (σₙ 𝕜 a) ∈
    (↑(NonUnitalStarSubalgebra.comap (F := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ →⋆ₙₐ[𝕜] Unitization 𝕜 A)
          (cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha)
          (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A))) :
      Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
have refine_1 : Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 (Unitization 𝕜 A))
  (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A))
  (↑a : Unitization 𝕜 A)
Tactic: rw [SetLike.mem_coe, NonUnitalStarSubalgebra.mem_comap, cfcₙAux_id hp₁ a ha]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
h₁ :
  Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
    (closure[Unitization.instUniformSpace.toTopologicalSpace]
      ((⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
        (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
              NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
          Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)
⊢ IsClosed[Unitization.instUniformSpace.toTopologicalSpace]
    (Set.range (ι := A) (⇑(Unitization.inrNonUnitalStarAlgHom 𝕜 A) : (a : A) → Unitization 𝕜 A))
have h : Eq (α := Set (Unitization 𝕜 A))
  (Set.range (ι := A) (⇑(Unitization.inrNonUnitalStarAlgHom 𝕜 A) : (a : A) → Unitization 𝕜 A))
  (Set.preimage (β := 𝕜) (fun (x : Unitization 𝕜 A) ↦ x.toProd.1) {0})
Tactic: convert! IsClosed.preimage (Unitization.continuous_fst (𝕜 := 𝕜)) isClosed_singleton
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
h₁ :
  Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
    (closure[Unitization.instUniformSpace.toTopologicalSpace]
      ((⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
        (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
              NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
          Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)
h :
  Eq (α := Set (Unitization 𝕜 A))
    (Set.range (ι := A) (⇑(Unitization.inrNonUnitalStarAlgHom 𝕜 A) : (a : A) → Unitization 𝕜 A))
    (Set.preimage (β := 𝕜) (fun (x : Unitization 𝕜 A) ↦ x.toProd.1) {0})
⊢ IsClosed[Unitization.instUniformSpace.toTopologicalSpace]
    (Set.range (ι := A) (⇑(Unitization.inrNonUnitalStarAlgHom 𝕜 A) : (a : A) → Unitization 𝕜 A))
have refine_2 : 𝕜
Tactic: convert! IsClosed.preimage (Unitization.continuous_fst (𝕜 := 𝕜)) isClosed_singleton
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
inst_9 : CStarRing A
a : A
ha : p a
h : NonUnitalContinuousFunctionalCalculus 𝕜 A p := ⋯
⊢ Eq (α := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ →⋆ₙₐ[𝕜] Unitization 𝕜 A)
    (NonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom 𝕜 A) (cfcₙHom (p := p) ha)) (cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha)
have apply : IsScalarTower 𝕜 (Unitization 𝕜 A) (Unitization 𝕜 A)
Tactic: apply ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id _ _ _
    (Unitization.continuous_inr.comp <| cfcₙHom_continuous ha)
    (continuous_cfcₙAux hp₁ a ha)
    (by simp [cfcₙHom_id ha, cfcₙAux_id hp₁ a ha])
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
inst_9 : CStarRing A
a : A
ha : p a
h : NonUnitalContinuousFunctionalCalculus 𝕜 A p := ⋯
apply : IsScalarTower 𝕜 (Unitization 𝕜 A) (Unitization 𝕜 A)
⊢ Eq (α := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ →⋆ₙₐ[𝕜] Unitization 𝕜 A)
    (NonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom 𝕜 A) (cfcₙHom (p := p) ha)) (cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha)
have apply₁ : SMulCommClass 𝕜 (Unitization 𝕜 A) (Unitization 𝕜 A)
Tactic: apply ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id _ _ _
    (Unitization.continuous_inr.comp <| cfcₙHom_continuous ha)
    (continuous_cfcₙAux hp₁ a ha)
    (by simp [cfcₙHom_id ha, cfcₙAux_id hp₁ a ha])
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
inst_9 : CStarRing A
a : A
ha : p a
⊢ IsClosedEmbedding.{u_1, u_2} (X := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) (Y := A)
    (⇑(cfcₙHom (p := p) ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → A)
have apply : IsClosedEmbedding (X := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) (Y := Unitization 𝕜 A)
  (Unitization.inr ∘ (⇑(cfcₙHom (p := p) ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → A))
Tactic: apply isometry_inr (𝕜 := 𝕜) (A := A) |>.isClosedEmbedding |>.of_comp_iff.mp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
inst_9 : CStarRing A
a : A
ha : p a
⊢ IsClosedEmbedding (X := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) (Y := Unitization 𝕜 A)
    (Unitization.inr ∘ (⇑(cfcₙHom (p := p) ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → A))
have h : Eq (α := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ → Unitization 𝕜 A)
  (Unitization.inr ∘ (⇑(cfcₙHom (p := p) ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → A))
  (⇑(cfcₙAux (p := p) (p₁ := p₁) sorry a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A)
Tactic: convert! isClosedEmbedding_cfcₙAux hp₁ a ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
⊢ IsSelfAdjoint a ↔ IsStarNormal a ∧ QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)
have refine_1 : ∀ (ha : IsSelfAdjoint a) (x : ℂ) (hx : x ∈ σₙ ℂ a),
  (algebraMap ℝ ℂ : (a : ℝ) → ℂ) ((Complex.reCLM : (a : ℂ) → ℝ) x : ℝ) = x
Tactic: refine ⟨fun ha ↦ ⟨ha.isStarNormal, ⟨fun x hx ↦ ?_, Complex.ofReal_re⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
refine_1 :
  ∀ (ha : IsSelfAdjoint a) (x : ℂ) (hx : x ∈ σₙ ℂ a),
    (algebraMap ℝ ℂ : (a : ℝ) → ℂ) ((Complex.reCLM : (a : ℂ) → ℝ) x : ℝ) = x
⊢ IsSelfAdjoint a ↔ IsStarNormal a ∧ QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)
have refine_2 : IsStarNormal a ∧ QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ) → IsSelfAdjoint a
Tactic: refine ⟨fun ha ↦ ⟨ha.isStarNormal, ⟨fun x hx ↦ ?_, Complex.ofReal_re⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (hypothesis)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σₙ ℂ a
⊢ (algebraMap ℝ ℂ : (a : ℝ) → ℂ) ((Complex.reCLM : (a : ℂ) → ℝ) x : ℝ) = x
have this : Set.EqOn (fun (x : ℂ) ↦ star (id x)) id (σₙ ℂ a)
Tactic: have := eqOn_of_cfcₙ_eq_cfcₙ <|
      (cfcₙ_star (id : ℂ → ℂ) a).symm ▸ (cfcₙ_id ℂ a).symm ▸ ha.star_eq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)
⊢ star a = a
have refine_2 : star a = cfcₙ (R := ℂ) (p := IsStarNormal) id a
Tactic: nth_rw 2 [← cfcₙ_id ℂ a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)
⊢ star a = cfcₙ (R := ℂ) (p := IsStarNormal) id a
have refine_2 : cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ star x) a = cfcₙ (R := ℂ) (p := IsStarNormal) id a
Tactic: rw [← cfcₙ_star_id a (R := ℂ)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)
⊢ cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ star x) a = cfcₙ (R := ℂ) (p := IsStarNormal) id a
have refine_2 : ∀ (x : ℂ) (hx : x ∈ σₙ ℂ a), star x = id x
Tactic: refine cfcₙ_congr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)
x : ℂ
hx : x ∈ σₙ ℂ a
⊢ star x = id x
have refine_2 : ∀ (x : ℝ) (hx : Membership.mem (α := ℂ) (σₙ ℂ a) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x : ℂ)),
  Eq (α := ℂ) (star ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x) : ℂ) (id ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x) : ℂ)
Tactic: obtain ⟨x, -, rfl⟩ := ha₂.algebraMap_image.symm ▸ hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : IsScalarTower ℝ A A
inst_5 : SMulCommClass ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
⊢ ∃ (x : A),
    IsSelfAdjoint x ∧
      QuasispectrumRestricts (R := NNReal) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal) ∧ x * x = a
have right : QuasispectrumRestricts (R := NNReal) (S := ℝ) (cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a)
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal) ∧
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a = a
Tactic: use cfcₙ (√·) a, cfcₙ_predicate (√·) a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : IsScalarTower ℝ A A
inst_5 : SMulCommClass ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
⊢ QuasispectrumRestricts (R := NNReal) (S := ℝ) (cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal) ∧
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a = a
have right : QuasispectrumRestricts (R := NNReal) (S := ℝ) (cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a)
  (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : IsScalarTower ℝ A A
inst_5 : SMulCommClass ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
right :
  QuasispectrumRestricts (R := NNReal) (S := ℝ) (cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a)
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
⊢ QuasispectrumRestricts (R := NNReal) (S := ℝ) (cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal) ∧
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a = a
have right₁ : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : IsScalarTower ℝ A A
inst_5 : SMulCommClass ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a = a
have right : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = a
Tactic: rw [← cfcₙ_mul ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : IsScalarTower ℝ A A
inst_5 : SMulCommClass ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = a
have right : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a
Tactic: nth_rw 2 [← cfcₙ_id ℝ a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : IsScalarTower ℝ A A
inst_5 : SMulCommClass ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a
have apply : ∀ (x : ℝ) (hx : x ∈ σₙ ℝ a), √x * √x = id x
Tactic: apply cfcₙ_congr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : IsScalarTower ℝ A A
inst_5 : SMulCommClass ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
x : ℝ
hx : x ∈ σₙ ℝ a
⊢ √x * √x = id x
have rw : ∀ (ha₂ : ∀ x ∈ σₙ ℝ a, 0 ≤ x) (x : ℝ) (hx : x ∈ σₙ ℝ a), √x * √x = id x
Tactic: rw [QuasispectrumRestricts.nnreal_iff] at ha₂
Cleared hypotheses: ha₂, x, hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : IsScalarTower ℝ A A
inst_5 : SMulCommClass ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : ∀ x ∈ σₙ ℝ a, 0 ≤ x
x : ℝ
hx : x ∈ σₙ ℝ a
⊢ √x * √x = id x
have hx₁ : 0 ≤ x
Tactic: apply ha₂ x at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a : A
⊢ 0 ≤ a ↔
    IsSelfAdjoint a ∧ QuasispectrumRestricts (R := NNReal) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
have refine : IsSelfAdjoint a ∧ QuasispectrumRestricts (R := NNReal) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal) →
  0 ≤ a
Tactic: refine ⟨fun ha ↦ ⟨.of_nonneg ha, .nnreal_of_nonneg ha⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
⊢ 0 ≤ a
have obtain : ∀ (x : A) (hx : IsSelfAdjoint x) (ha₁ : IsSelfAdjoint (x * x))
  (ha₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) (x * x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)),
  0 ≤ x * x
Tactic: obtain ⟨x, hx, -, rfl⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts ha₁ ha₂
Cleared hypotheses: a, ha₁, ha₂
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
h : Commute a b
⊢ 0 ≤ a * b
have rw : IsSelfAdjoint (a * b) ∧
  QuasispectrumRestricts (R := NNReal) (S := ℝ) (a * b) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
Tactic: rw [nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
h : Commute a b
⊢ IsSelfAdjoint (a * b) ∧
    QuasispectrumRestricts (R := NNReal) (S := ℝ) (a * b) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
have refine : QuasispectrumRestricts (R := NNReal) (S := ℝ) (a * b) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
Tactic: refine ⟨ha.isSelfAdjoint.commute_iff hb.isSelfAdjoint |>.mp h, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
h : Commute a b
⊢ QuasispectrumRestricts (R := NNReal) (S := ℝ) (a * b) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
have hb₁ : IsSelfAdjoint b ∧ QuasispectrumRestricts (R := NNReal) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
Tactic: rw [nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts] at hb
Cleared hypotheses: hb, h