awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 (α := Unitization 𝕜 A)
    ((NonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom 𝕜 A) (cfcₙHom (p := p) ha) :
          (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A)
        (ContinuousMapZero.id (σₙ 𝕜 a)) :
      Unitization 𝕜 A)
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A)
        (ContinuousMapZero.id (σₙ 𝕜 a)) :
      Unitization 𝕜 A)

Tactic:
simp [cfcₙHom_id ha, cfcₙAux_id hp₁ a ha]

Premises used: cfcₙHom_id, cfcₙAux_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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)
apply₁ : SMulCommClass 𝕜 (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)

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])

Premises used: ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id, continuous_cfcₙAux
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 := ⋯
⊢ IsScalarTower 𝕜 (Unitization 𝕜 A) (Unitization 𝕜 A)

Tactic:
infer_instance
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 := ⋯
⊢ SMulCommClass 𝕜 (Unitization 𝕜 A) (Unitization 𝕜 A)

Tactic:
infer_instance
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
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))
⊢ 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)

Tactic:
apply isometry_inr (𝕜 := 𝕜) (A := A) |>.isClosedEmbedding |>.of_comp_iff.mp

Premises used: Unitization.isometry_inr, Topology.IsClosedEmbedding.of_comp_iff, Isometry.isClosedEmbedding, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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)
    (⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A)

Tactic:
isClosedEmbedding_cfcₙAux hp₁ a ha

Premises used: isClosedEmbedding_cfcₙAux
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 :
  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₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 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))

Tactic:
convert! isClosedEmbedding_cfcₙAux hp₁ a ha

Premises used: isClosedEmbedding_cfcₙAux
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
⊢ 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₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A)

Tactic:
congrm (⇑$(inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux hp₁ a ha))
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 : ℂ) → ℝ)

Tactic:
⟨fun ha ↦ ⟨ha.isStarNormal, ⟨fun x hx ↦ ?_, Complex.ofReal_re⟩⟩, ?_⟩

Premises used: IsSelfAdjoint.isStarNormal, QuasispectrumRestricts.mk, And.intro, Iff.intro, Complex.ofReal_re
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
refine_2 : IsStarNormal a ∧ QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ) → IsSelfAdjoint a
⊢ IsSelfAdjoint a ↔ IsStarNormal a ∧ QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)

Tactic:
refine ⟨fun ha ↦ ⟨ha.isStarNormal, ⟨fun x hx ↦ ?_, Complex.ofReal_re⟩⟩, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
⊢ 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
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
this : Set.EqOn (fun (x : ℂ) ↦ star (id x)) id (σₙ ℂ a)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) x = x

Tactic:
simpa using this hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
this : Set.EqOn (fun (x : ℂ) ↦ star (id x)) id (σₙ ℂ a)
⊢ (algebraMap ℝ ℂ : (a : ℝ) → ℂ) ((Complex.reCLM : (a : ℂ) → ℝ) x : ℝ) = x

Tactic:
exact Complex.conj_eq_iff_re.mp (by simpa using this hx)

Premises used: Complex.conj_eq_iff_re, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 : ℂ) → ℝ)
refine_2 : star a = cfcₙ (R := ℂ) (p := IsStarNormal) id a
⊢ star a = a

Tactic:
nth_rw 2 [← cfcₙ_id ℂ a]

Premises used: cfcₙ_id, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 : ℂ) → ℝ)
refine_2 : cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ star x) a = cfcₙ (R := ℂ) (p := IsStarNormal) id a
⊢ star a = cfcₙ (R := ℂ) (p := IsStarNormal) id a

Tactic:
rw [← cfcₙ_star_id a (R := ℂ)]

Premises used: cfcₙ_star_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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

Tactic:
cfcₙ_congr fun x hx ↦ ?_

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 : ℂ) → ℝ)
refine_2 : ∀ (x : ℂ) (hx : x ∈ σₙ ℂ a), star x = id x
⊢ cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ star x) a = cfcₙ (R := ℂ) (p := IsStarNormal) id a

Tactic:
refine cfcₙ_congr fun x hx ↦ ?_

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
refine_2 :
  ∀ (x : ℝ) (hx : Membership.mem (α := ℂ) (σₙ ℂ a) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x : ℂ)),
    Eq (α := ℂ) (star ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x) : ℂ) (id ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x) : ℂ)
⊢ star x = id x

Tactic:
obtain ⟨x, -, rfl⟩ := ha₂.algebraMap_image.symm ▸ hx

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 : Membership.mem (α := ℂ) (σₙ ℂ a) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x : ℂ)
⊢ Eq (α := ℂ) (star ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x) : ℂ) (id ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x) : ℂ)

Tactic:
Complex.conj_ofReal _

Premises used: Complex.conj_ofReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 : Membership.mem (α := ℂ) (σₙ ℂ a) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x : ℂ)
⊢ Eq (α := ℂ) (star ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x) : ℂ) (id ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x) : ℂ)

Tactic:
exact Complex.conj_ofReal _

Premises used: Complex.conj_ofReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
⊢ QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)

Tactic:
isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts |>.mp ha |>.2

Premises used: isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, And.right, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 : QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)
inst_7 : IsStarNormal a
⊢ IsSelfAdjoint a

Tactic:
isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts.mpr ⟨‹_›, ha⟩

Premises used: Iff.mpr, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, And.intro
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
⊢ NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint

Tactic:
QuasispectrumRestricts.cfc (q := IsStarNormal) (p := IsSelfAdjoint) Complex.reCLM
    Complex.isometry_ofReal.isClosedEmbedding (.zero _)
    (fun _ ↦ isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts)

Premises used: Complex.isometry_ofReal, IsSelfAdjoint.zero, Isometry.isClosedEmbedding, QuasispectrumRestricts.cfc
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsSelfAdjoint a
⊢ SpectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)

Tactic:
ha.quasispectrumRestricts

Premises used: IsSelfAdjoint.quasispectrumRestricts
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
⊢ ContinuousFunctionalCalculus ℝ A IsSelfAdjoint

Tactic:
SpectrumRestricts.cfc (q := IsStarNormal) (p := IsSelfAdjoint) Complex.reCLM
    Complex.isometry_ofReal.isClosedEmbedding (.zero _)
    (fun _ ↦ isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts)

Premises used: Complex.isometry_ofReal, IsSelfAdjoint.zero, Isometry.isClosedEmbedding, SpectrumRestricts.cfc
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Algebra ℝ A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : Nontrivial A
a : A
ha : IsSelfAdjoint a
⊢ (σ ℝ a).Nonempty

Tactic:
ContinuousFunctionalCalculus.spectrum_nonempty a ha

Premises used: ContinuousFunctionalCalculus.spectrum_nonempty
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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) ∧
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a = a
⊢ ∃ (x : A),
    IsSelfAdjoint x ∧
      QuasispectrumRestricts (R := NNReal) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal) ∧ x * x = a

Tactic:
use cfcₙ (√·) a, cfcₙ_predicate (√·) a

Premises used: cfcₙ, cfcₙ_predicate, Real.sqrt
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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)
right₁ : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a = a
⊢ 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:
constructor
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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)

Tactic:
simpa only [QuasispectrumRestricts.nnreal_iff, cfcₙ_map_quasispectrum (√·) a,
      Set.mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
        using fun x _ ↦ Real.sqrt_nonneg x

Premises used: QuasispectrumRestricts.nnreal_iff, and_imp, Set.mem_image, forall_exists_index, Real.sqrt, Real.sqrt_nonneg, cfcₙ_map_quasispectrum, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x) a = a

Tactic:
rw [← cfcₙ_mul ..]

Premises used: cfcₙ_mul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = a

Tactic:
nth_rw 2 [← cfcₙ_id ℝ a]

Premises used: Real, cfcₙ_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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)
apply : ∀ (x : ℝ) (hx : x ∈ σₙ ℝ a), √x * √x = id x
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a

Tactic:
apply cfcₙ_congr fun x hx ↦ ?_

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
rw : ∀ (ha₂ : ∀ x ∈ σₙ ℝ a, 0 ≤ x) (x : ℝ) (hx : x ∈ σₙ ℝ a), √x * √x = id x
⊢ √x * √x = id x

Tactic:
rw [QuasispectrumRestricts.nnreal_iff] at ha₂

Premises used: QuasispectrumRestricts.nnreal_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
⊢ 0 ≤ x

Tactic:
apply ha₂ x at hx