awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
toLinearMap : A₁ →ₗ[ℂ] A₂
map_cstarMatrix_nonneg' :
  ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁) (hM : 0 ≤ M),
    LE.le.{u_2} (α := CStarMatrix (Fin k) (Fin k) A₂) 0 (M.map (⇑toLinearMap : (a : A₁) → A₂))
toLinearMap_1 : A₁ →ₗ[ℂ] A₂
map_cstarMatrix_nonneg'_1 :
  ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁) (hM : 0 ≤ M),
    LE.le.{u_2} (α := CStarMatrix (Fin k) (Fin k) A₂) 0 (M.map (⇑toLinearMap_1 : (a : A₁) → A₂))
h :
  Eq (α := (a : A₁) → A₂)
    ((fun (f : A₁ →CP A₂) ↦ f.toFun) { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' })
    ((fun (f : A₁ →CP A₂) ↦ f.toFun)
      { toLinearMap := toLinearMap_1, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg'_1 })
mk : Eq (α := (a : A₁) → A₂) (⇑toLinearMap : (a : A₁) → A₂) (⇑toLinearMap_1 : (a : A₁) → A₂)
⊢ toLinearMap = toLinearMap_1

Tactic:
apply DFunLike.coe_injective'

Premises used: DFunLike.coe_injective'
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
toLinearMap : A₁ →ₗ[ℂ] A₂
map_cstarMatrix_nonneg' :
  ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁) (hM : 0 ≤ M),
    LE.le.{u_2} (α := CStarMatrix (Fin k) (Fin k) A₂) 0 (M.map (⇑toLinearMap : (a : A₁) → A₂))
toLinearMap_1 : A₁ →ₗ[ℂ] A₂
map_cstarMatrix_nonneg'_1 :
  ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁) (hM : 0 ≤ M),
    LE.le.{u_2} (α := CStarMatrix (Fin k) (Fin k) A₂) 0 (M.map (⇑toLinearMap_1 : (a : A₁) → A₂))
h :
  Eq (α := (a : A₁) → A₂)
    ((fun (f : A₁ →CP A₂) ↦ f.toFun) { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' })
    ((fun (f : A₁ →CP A₂) ↦ f.toFun)
      { toLinearMap := toLinearMap_1, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg'_1 })
⊢ Eq (α := (a : A₁) → A₂) (⇑toLinearMap : (a : A₁) → A₂) (⇑toLinearMap_1 : (a : A₁) → A₂)

Tactic:
h
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
toLinearMap : A₁ →ₗ[ℂ] A₂
map_cstarMatrix_nonneg' :
  ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁) (hM : 0 ≤ M),
    LE.le.{u_2} (α := CStarMatrix (Fin k) (Fin k) A₂) 0 (M.map (⇑toLinearMap : (a : A₁) → A₂))
toLinearMap_1 : A₁ →ₗ[ℂ] A₂
map_cstarMatrix_nonneg'_1 :
  ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁) (hM : 0 ≤ M),
    LE.le.{u_2} (α := CStarMatrix (Fin k) (Fin k) A₂) 0 (M.map (⇑toLinearMap_1 : (a : A₁) → A₂))
h :
  Eq (α := (a : A₁) → A₂)
    ((fun (f : A₁ →CP A₂) ↦ f.toFun) { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' })
    ((fun (f : A₁ →CP A₂) ↦ f.toFun)
      { toLinearMap := toLinearMap_1, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg'_1 })
⊢ Eq (α := (a : A₁) → A₂) (⇑toLinearMap : (a : A₁) → A₂) (⇑toLinearMap_1 : (a : A₁) → A₂)

Tactic:
exact h
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
n : Type u_3
inst_6 : Fintype n
φ : A₁ →CP A₂
M : CStarMatrix n n A₁
hM : 0 ≤ M
k : ℕ := Fintype.card n
e : n ≃ Fin (Fintype.card n) := Fintype.equivFinOfCardEq ⋯
simp :
  LE.le.{u_2} (α := CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂) 0
    (map.{0, 0, u_1, u_2} (A := A₁)
      ((reindexₐ ℂ A₁ e : (a : CStarMatrix n n A₁) → CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₁) M)
      (⇑φ : (a : A₁) → A₂))
⊢ LE.le.{u_2} (α := CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
    (0 : CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
    (((mapₗ
              (↑φ :
                [inst_7 : FunLike (A₁ →CP A₂) A₁ A₂] →
                  [SemilinearMapClass (A₁ →CP A₂) (RingHom.id ℂ) A₁ A₂] → A₁ →ₗ[ℂ] A₂) :
            LinearMap.{0, 0, u_1, u_2} (RingHom.id ℂ) (CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₁)
              (CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)) :
          (a : CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₁) →
            CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
        ((reindexₐ ℂ A₁ e : (a : CStarMatrix n n A₁) → CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₁)
          M) :
      CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)

Tactic:
simp only [mapₗ, LinearMap.coe_coe, LinearMap.coe_mk, AddHom.coe_mk]

Premises used: LinearMap.coe_mk, CStarMatrix.mapₗ, AddHom.coe_mk, LinearMap.coe_coe
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
n : Type u_3
inst_6 : Fintype n
φ : A₁ →CP A₂
M : CStarMatrix n n A₁
hM : 0 ≤ M
k : ℕ := Fintype.card n
e : n ≃ Fin (Fintype.card n) := Fintype.equivFinOfCardEq ⋯
⊢ LE.le.{u_2} (α := CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂) 0
    (map.{0, 0, u_1, u_2} (A := A₁)
      ((reindexₐ ℂ A₁ e : (a : CStarMatrix n n A₁) → CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₁) M)
      (⇑φ : (a : A₁) → A₂))

Tactic:
CompletelyPositiveMapClass.map_cstarMatrix_nonneg' _ k _ (map_nonneg _ hM)

Premises used: CompletelyPositiveMapClass.map_cstarMatrix_nonneg', map_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
n : Type u_3
inst_6 : Fintype n
φ : A₁ →CP A₂
M : CStarMatrix n n A₁
hM : 0 ≤ M
k : ℕ := Fintype.card n
e : n ≃ Fin (Fintype.card n) := Fintype.equivFinOfCardEq ⋯
⊢ LE.le.{u_2} (α := CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂) 0
    (map.{0, 0, u_1, u_2} (A := A₁)
      ((reindexₐ ℂ A₁ e : (a : CStarMatrix n n A₁) → CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₁) M)
      (⇑φ : (a : A₁) → A₂))

Tactic:
exact CompletelyPositiveMapClass.map_cstarMatrix_nonneg' _ k _ (map_nonneg _ hM)

Premises used: CompletelyPositiveMapClass.map_cstarMatrix_nonneg', map_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
n : Type u_3
inst_6 : Fintype n
φ : A₁ →CP A₂
M : CStarMatrix n n A₁
hM : 0 ≤ M
k : ℕ := Fintype.card n
e : n ≃ Fin (Fintype.card n) := Fintype.equivFinOfCardEq ⋯
⊢ LE.le.{u_2} (α := CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
    (0 : CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
    (((mapₗ
              (↑φ :
                [inst_7 : FunLike (A₁ →CP A₂) A₁ A₂] →
                  [SemilinearMapClass (A₁ →CP A₂) (RingHom.id ℂ) A₁ A₂] → A₁ →ₗ[ℂ] A₂) :
            LinearMap.{0, 0, u_1, u_2} (RingHom.id ℂ) (CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₁)
              (CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)) :
          (a : CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₁) →
            CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
        ((reindexₐ ℂ A₁ e : (a : CStarMatrix n n A₁) → CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₁)
          M) :
      CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)

Tactic:
have hmain : 0 ≤ (reindexₐ ℂ A₁ e M).mapₗ (φ : A₁ →ₗ[ℂ] A₂) := by
    simp only [mapₗ, LinearMap.coe_coe, LinearMap.coe_mk, AddHom.coe_mk]
    exact CompletelyPositiveMapClass.map_cstarMatrix_nonneg' _ k _ (map_nonneg _ hM)
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
n : Type u_3
inst_6 : Fintype n
φ : A₁ →CP A₂
M : CStarMatrix n n A₁
hM : 0 ≤ M
k : ℕ := Fintype.card n
e : n ≃ Fin (Fintype.card n) := Fintype.equivFinOfCardEq ⋯
hmain :
  LE.le.{u_2} (α := CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
    (0 : CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
    (((mapₗ
              (↑φ :
                [inst_7 : FunLike (A₁ →CP A₂) A₁ A₂] →
                  [SemilinearMapClass (A₁ →CP A₂) (RingHom.id ℂ) A₁ A₂] → A₁ →ₗ[ℂ] A₂) :
            LinearMap.{0, 0, u_1, u_2} (RingHom.id ℂ) (CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₁)
              (CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)) :
          (a : CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₁) →
            CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
        ((reindexₐ ℂ A₁ e : (a : CStarMatrix n n A₁) → CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₁)
          M) :
      CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
⊢ LE.le.{u_2} (α := CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
    (0 : CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
    ((reindexₐ ℂ A₂ e : (a : CStarMatrix n n A₂) → CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
        ((mapₗ
              (↑φ :
                [inst_7 : FunLike (A₁ →CP A₂) A₁ A₂] →
                  [SemilinearMapClass (A₁ →CP A₂) (RingHom.id ℂ) A₁ A₂] → A₁ →ₗ[ℂ] A₂) :
            (a : CStarMatrix n n A₁) → CStarMatrix n n A₂)
          M) :
      CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)

Tactic:
rw [← mapₗ_reindexₐ] at hmain

Premises used: CStarMatrix.mapₗ_reindexₐ
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
n : Type u_3
inst_6 : Fintype n
φ : A₁ →CP A₂
M : CStarMatrix n n A₁
hM : 0 ≤ M
k : ℕ := Fintype.card n
e : n ≃ Fin (Fintype.card n) := Fintype.equivFinOfCardEq ⋯
hmain :
  LE.le.{u_2} (α := CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
    (0 : CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
    ((reindexₐ ℂ A₂ e : (a : CStarMatrix n n A₂) → CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
        ((mapₗ
              (↑φ :
                [inst_7 : FunLike (A₁ →CP A₂) A₁ A₂] →
                  [SemilinearMapClass (A₁ →CP A₂) (RingHom.id ℂ) A₁ A₂] → A₁ →ₗ[ℂ] A₂) :
            (a : CStarMatrix n n A₁) → CStarMatrix n n A₂)
          M) :
      CStarMatrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) A₂)
⊢ LE.le (α := CStarMatrix n n A₂) 0 (M.map (⇑φ : (a : A₁) → A₂))

Tactic:
simpa [reindexₐ_symm] using map_nonneg (reindexₐ ℂ A₂ e).symm hmain

Premises used: CStarMatrix.reindexₐ_symm, CStarMatrix.reindexₐ, map_nonneg, StarAlgEquiv.symm, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
F : Type u_1
A₁ : Type u_2
A₂ : Type u_3
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
inst_6 : FunLike F A₁ A₂
inst_7 : NonUnitalAlgHomClass F ℂ A₁ A₂
inst_8 : StarHomClass F A₁ A₂
φ : F
k : ℕ
M : CStarMatrix (Fin k) (Fin k) A₁
hM : 0 ≤ M
change :
  LE.le.{u_3} (α := CStarMatrix (Fin k) (Fin k) A₂) (0 : CStarMatrix (Fin k) (Fin k) A₂)
    (((mapₙₐ (↑φ : A₁ →⋆ₙₐ[ℂ] A₂) :
            NonUnitalStarAlgHom.{0, u_2, u_3} ℂ (CStarMatrix (Fin k) (Fin k) A₁) (CStarMatrix (Fin k) (Fin k) A₂)) :
          (a : CStarMatrix (Fin k) (Fin k) A₁) → CStarMatrix (Fin k) (Fin k) A₂)
        M :
      CStarMatrix (Fin k) (Fin k) A₂)
⊢ LE.le.{u_3} (α := CStarMatrix (Fin k) (Fin k) A₂) 0 (M.map (⇑φ : (a : A₁) → A₂))

Tactic:
change 0 ≤ (mapₙₐ (φ : A₁ →⋆ₙₐ[ℂ] A₂)) M

Premises used: CStarMatrix.mapₙₐ, NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
F : Type u_1
A₁ : Type u_2
A₂ : Type u_3
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
inst_6 : FunLike F A₁ A₂
inst_7 : NonUnitalAlgHomClass F ℂ A₁ A₂
inst_8 : StarHomClass F A₁ A₂
φ : F
k : ℕ
M : CStarMatrix (Fin k) (Fin k) A₁
hM : 0 ≤ M
⊢ LE.le.{u_3} (α := CStarMatrix (Fin k) (Fin k) A₂) (0 : CStarMatrix (Fin k) (Fin k) A₂)
    (((mapₙₐ (↑φ : A₁ →⋆ₙₐ[ℂ] A₂) :
            NonUnitalStarAlgHom.{0, u_2, u_3} ℂ (CStarMatrix (Fin k) (Fin k) A₁) (CStarMatrix (Fin k) (Fin k) A₂)) :
          (a : CStarMatrix (Fin k) (Fin k) A₁) → CStarMatrix (Fin k) (Fin k) A₂)
        M :
      CStarMatrix (Fin k) (Fin k) A₂)

Tactic:
map_nonneg _ hM

Premises used: map_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
F : Type u_1
A₁ : Type u_2
A₂ : Type u_3
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
inst_6 : FunLike F A₁ A₂
inst_7 : NonUnitalAlgHomClass F ℂ A₁ A₂
inst_8 : StarHomClass F A₁ A₂
φ : F
k : ℕ
M : CStarMatrix (Fin k) (Fin k) A₁
hM : 0 ≤ M
⊢ LE.le.{u_3} (α := CStarMatrix (Fin k) (Fin k) A₂) (0 : CStarMatrix (Fin k) (Fin k) A₂)
    (((mapₙₐ (↑φ : A₁ →⋆ₙₐ[ℂ] A₂) :
            NonUnitalStarAlgHom.{0, u_2, u_3} ℂ (CStarMatrix (Fin k) (Fin k) A₁) (CStarMatrix (Fin k) (Fin k) A₂)) :
          (a : CStarMatrix (Fin k) (Fin k) A₁) → CStarMatrix (Fin k) (Fin k) A₂)
        M :
      CStarMatrix (Fin k) (Fin k) A₂)

Tactic:
exact map_nonneg _ hM

Premises used: map_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
x : A
φ : (↑(characterSpace ℂ ↥(elemental ℂ x)) : Type u_1)
⊢ Membership.mem (α := ℂ) (spectrum ℂ x)
    ((φ : (a : ↥(elemental ℂ x)) → ℂ)
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ x) x_1) x ⋯) :
      ℂ)

Tactic:
simpa only [StarSubalgebra.spectrum_eq (hS := isClosed ℂ x)
      (a := ⟨x, self_mem ℂ x⟩)] using AlgHom.apply_mem_spectrum φ ⟨x, self_mem ℂ x⟩

Premises used: AlgHom.apply_mem_spectrum, StarSubalgebra.spectrum_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
⊢ Continuous (X := (↑(characterSpace ℂ ↥(elemental ℂ x)) : Type u_1)) (characterSpaceToSpectrum x)

Tactic:
continuous_induced_rng.2
    (map_continuous <| gelfandTransform ℂ (elemental ℂ x) ⟨x, self_mem ℂ x⟩)

Premises used: Iff.mpr, Membership.mem, Subtype, StarAlgebra.elemental, Subtype.mk, StarAlgebra.elemental.self_mem, ContinuousMapClass.map_continuous, Complex, DFunLike.coe, WeakDual.gelfandTransform, continuous_induced_rng
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
⊢ Function.Bijective (α := (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)) (characterSpaceToSpectrum a)

Tactic:
⟨fun φ ψ h => starAlgHomClass_ext ℂ ?_ ?_ ?_, ?_⟩

Premises used: StarAlgebra.elemental.starAlgHomClass_ext, And.intro, Function.Bijective, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
refine_1 :
  ∀ (φ ψ : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1))
    (h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ),
    Continuous (X := ↥(elemental ℂ a)) (Y := ℂ) (⇑φ : (a : ↥(elemental ℂ a)) → ℂ)
refine_2 :
  ∀ (φ ψ : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1))
    (h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ),
    Continuous (X := ↥(elemental ℂ a)) (Y := ℂ) (⇑ψ : (a : ↥(elemental ℂ a)) → ℂ)
refine_3 :
  ∀ (φ ψ : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1))
    (h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ),
    Eq (α := ℂ)
      ((φ : (a : ↥(elemental ℂ a)) → ℂ)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯) :
        ℂ)
      ((ψ : (a : ↥(elemental ℂ a)) → ℂ)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯) :
        ℂ)
refine_4 : Function.Surjective (α := (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)) (characterSpaceToSpectrum a)
⊢ Function.Bijective (α := (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)) (characterSpaceToSpectrum a)

Tactic:
refine ⟨fun φ ψ h => starAlgHomClass_ext ℂ ?_ ?_ ?_, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
φ ψ : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Continuous (X := ↥(elemental ℂ a)) (Y := ℂ) (⇑φ : (a : ↥(elemental ℂ a)) → ℂ)

Tactic:
(map_continuous φ)

Premises used: ContinuousMapClass.map_continuous
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
φ ψ : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Continuous (X := ↥(elemental ℂ a)) (Y := ℂ) (⇑φ : (a : ↥(elemental ℂ a)) → ℂ)

Tactic:
exact (map_continuous φ)

Premises used: ContinuousMapClass.map_continuous
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
φ ψ : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Continuous (X := ↥(elemental ℂ a)) (Y := ℂ) (⇑ψ : (a : ↥(elemental ℂ a)) → ℂ)

Tactic:
(map_continuous ψ)

Premises used: ContinuousMapClass.map_continuous
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
φ ψ : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Continuous (X := ↥(elemental ℂ a)) (Y := ℂ) (⇑ψ : (a : ↥(elemental ℂ a)) → ℂ)

Tactic:
exact (map_continuous ψ)

Premises used: ContinuousMapClass.map_continuous
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
φ ψ : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Eq (α := ℂ)
    ((φ : (a : ↥(elemental ℂ a)) → ℂ)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯) :
      ℂ)
    ((ψ : (a : ↥(elemental ℂ a)) → ℂ)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯) :
      ℂ)

Tactic:
simpa only [characterSpaceToSpectrum, Subtype.mk_eq_mk,
      ContinuousMap.coe_mk] using h

Premises used: StarAlgebra.elemental.characterSpaceToSpectrum, ContinuousMap.coe_mk, Subtype.mk_eq_mk
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ z ∈
    spectrum ℂ (A := ↥(elemental ℂ a))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯)

Tactic:
have hz' := (StarSubalgebra.spectrum_eq (hS := isClosed ℂ a)
      (a := ⟨a, self_mem ℂ a⟩) ▸ hz)
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
z : ℂ
hz : z ∈ spectrum ℂ a
hz' :
  z ∈
    spectrum ℂ (A := ↥(elemental ℂ a))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯)
⊢ ∃ (f : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)),
    (f : (a : ↥(elemental ℂ a)) → ℂ)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯) =
      z

Tactic:
rw [CharacterSpace.mem_spectrum_iff_exists] at hz'

Premises used: WeakDual.CharacterSpace.mem_spectrum_iff_exists
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
z : ℂ
hz : z ∈ spectrum ℂ a
hz' :
  ∃ (f : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)),
    (f : (a : ↥(elemental ℂ a)) → ℂ)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯) =
      z
refine_4 :
  ∀ (φ : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1))
    (hz :
      Membership.mem (α := ℂ) (spectrum ℂ a)
        ((φ : (a : ↥(elemental ℂ a)) → ℂ)
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯) :
          ℂ)),
    ∃ (a_1 : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)),
      characterSpaceToSpectrum a a_1 =
        Subtype.mk (p := fun (x : ℂ) ↦ x ∈ spectrum ℂ a)
          ((φ : (a : ↥(elemental ℂ a)) → ℂ)
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯))
          hz
⊢ ∃ (a_1 : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)),
    characterSpaceToSpectrum a a_1 = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ spectrum ℂ a) z hz

Tactic:
obtain ⟨φ, rfl⟩ := hz'

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
φ : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)
hz :
  Membership.mem (α := ℂ) (spectrum ℂ a)
    ((φ : (a : ↥(elemental ℂ a)) → ℂ)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯) :
      ℂ)
⊢ ∃ (a_1 : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)),
    characterSpaceToSpectrum a a_1 =
      Subtype.mk (p := fun (x : ℂ) ↦ x ∈ spectrum ℂ a)
        ((φ : (a : ↥(elemental ℂ a)) → ℂ)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯))
        hz

Tactic:
⟨φ, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
φ : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)
hz :
  Membership.mem (α := ℂ) (spectrum ℂ a)
    ((φ : (a : ↥(elemental ℂ a)) → ℂ)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯) :
      ℂ)
⊢ ∃ (a_1 : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)),
    characterSpaceToSpectrum a a_1 =
      Subtype.mk (p := fun (x : ℂ) ↦ x ∈ spectrum ℂ a)
        ((φ : (a : ↥(elemental ℂ a)) → ℂ)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯))
        hz

Tactic:
exact ⟨φ, rfl⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
⊢ Eq (α := ↥(elemental ℂ a))
    ((continuousFunctionalCalculus a : (a_1 : C((↑(spectrum ℂ a) : Type), ℂ)) → ↥(elemental ℂ a))
        (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) :
      ↥(elemental ℂ a))
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a ⋯ : ↥(elemental ℂ a))

Tactic:
(gelfandStarTransform (elemental ℂ a)).symm_apply_apply _

Premises used: Set.Mem, setOf, ContinuousMap.comp, Membership.mem, Subtype, Function.surjInv, StarAlgebra.elemental, StarAlgEquiv.symm_apply_apply, gelfandStarTransform, Classical.choose, Complex