awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
refine_1 :
  LE.le (α := Filter (CStarMatrix m n A)) (cobounded (CStarMatrix m n A))
    (Filter.comap (β := Matrix m n A) (⇑(Equiv.symm ofMatrix) : (a : CStarMatrix m n A) → Matrix m n A)
      (cobounded (Matrix m n A)))
⊢ Eq (α := Filter (CStarMatrix m n A)) (cobounded (CStarMatrix m n A))
    (Filter.comap (β := Matrix m n A) (⇑(Equiv.symm ofMatrix) : (a : CStarMatrix m n A) → Matrix m n A)
      (cobounded (Matrix m n A)))
have refine_2 : LE.le (α := Filter (CStarMatrix m n A))
  (Filter.comap (β := Matrix m n A) (⇑(Equiv.symm ofMatrix) : (a : CStarMatrix m n A) → Matrix m n A)
    (cobounded (Matrix m n A)))
  (cobounded (CStarMatrix m n A))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (hypothesis)
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
⊢ Eq (α := Filter (CStarMatrix m n A)) (cobounded (CStarMatrix m n A)) (cobounded ((i : m) → n → A))
have this : Eq (α := Filter (CStarMatrix m n A)) (cobounded (CStarMatrix m n A))
  (Filter.comap (β := Matrix m n A) (⇑(Equiv.symm ofMatrix) : (a : CStarMatrix m n A) → Matrix m n A)
    (cobounded (Matrix m n A)))
Tactic: have : cobounded (CStarMatrix m n A) = Filter.comap ofMatrix.symm (cobounded _) := by
    refine le_antisymm ?_ ?_
    · exact antilipschitzWith_toMatrixAux.tendsto_cobounded.le_comap
    · exact lipschitzWith_toMatrixAux.comap_cobounded_le
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
x x_1 : CStarMatrix n n A
⊢ ‖x * x_1‖ ≤ ‖x‖ * ‖x_1‖
have simpa : ‖HMul.hMul (α := (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) (β := (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)
      ((toCLMNonUnitalAlgHom : (a : CStarMatrix n n A) → (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) x :
        (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)
      ((toCLMNonUnitalAlgHom : (a : CStarMatrix n n A) → (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) x_1 :
        (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)‖ ≤
  norm (E := (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)
      ((toCLMNonUnitalAlgHom : (a : CStarMatrix n n A) → (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) x :
        (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) *
    norm (E := (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)
      ((toCLMNonUnitalAlgHom : (a : CStarMatrix n n A) → (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) x_1 :
        (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)
Tactic: simpa only [norm_def', map_mul] using norm_mul_le _ _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap (goal)
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₂
f g : A₁ →CP A₂
h : Eq (α := (a : A₁) → A₂) ((fun (f : A₁ →CP A₂) ↦ f.toFun) f) ((fun (f : A₁ →CP A₂) ↦ f.toFun) g)
⊢ f = g
have mk : ∀ (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₂)))
  (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) g)),
  { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' : A₁ →CP A₂ } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap (goal)
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₂
g : A₁ →CP 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₂))
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) g)
⊢ { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' : A₁ →CP A₂ } = g
have mk : ∀ (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 })),
  { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' : A₁ →CP A₂ } =
    { toLinearMap := toLinearMap_1, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap (goal)
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 })
⊢ { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' : A₁ →CP A₂ } =
    { toLinearMap := toLinearMap_1, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg'_1 }
have mk : toLinearMap = toLinearMap_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap (goal)
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 })
⊢ toLinearMap = toLinearMap_1
have mk : Eq (α := (a : A₁) → A₂) (⇑toLinearMap : (a : A₁) → A₂) (⇑toLinearMap_1 : (a : A₁) → A₂)
Tactic: apply DFunLike.coe_injective'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap (goal)
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₂)
have 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₂))
Tactic: simp only [mapₗ, LinearMap.coe_coe, LinearMap.coe_mk, AddHom.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap (hypothesis)
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 (α := CStarMatrix n n A₂) 0 (M.map (⇑φ : (a : A₁) → A₂))
have 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₂)
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)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap (hypothesis)
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 (α := CStarMatrix n n A₂) 0 (M.map (⇑φ : (a : A₁) → A₂))
have 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₂)
Tactic: rw [← mapₗ_reindexₐ] at hmain
Cleared hypotheses: hmain
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap (goal)
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 (M.map (⇑φ : (a : A₁) → A₂))
have 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₂)
Tactic: change 0 ≤ (mapₙₐ (φ : A₁ →⋆ₙₐ[ℂ] A₂)) M
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
⊢ Function.Bijective (α := (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)) (characterSpaceToSpectrum a)
have refine_1 : ∀ (φ ψ : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1))
  (h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ),
  Continuous (X := ↥(elemental ℂ a)) (Y := ℂ) (⇑φ : (a : ↥(elemental ℂ a)) → ℂ)
Tactic: refine ⟨fun φ ψ h => starAlgHomClass_ext ℂ ?_ ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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)) → ℂ)
⊢ Function.Bijective (α := (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)) (characterSpaceToSpectrum a)
have refine_2 : ∀ (φ ψ : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1))
  (h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ),
  Continuous (X := ↥(elemental ℂ a)) (Y := ℂ) (⇑ψ : (a : ↥(elemental ℂ a)) → ℂ)
Tactic: refine ⟨fun φ ψ h => starAlgHomClass_ext ℂ ?_ ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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)) → ℂ)
⊢ Function.Bijective (α := (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)) (characterSpaceToSpectrum a)
have 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 sorry) :
      ℂ)
    ((ψ : (a : ↥(elemental ℂ a)) → ℂ)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a sorry) :
      ℂ)
Tactic: refine ⟨fun φ ψ h => starAlgHomClass_ext ℂ ?_ ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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 ⋯) :
        ℂ)
⊢ Function.Bijective (α := (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)) (characterSpaceToSpectrum a)
have refine_4 : Function.Surjective (α := (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)) (characterSpaceToSpectrum a)
Tactic: refine ⟨fun φ ψ h => starAlgHomClass_ext ℂ ?_ ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ ∃ (a_1 : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)),
    characterSpaceToSpectrum a a_1 = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ spectrum ℂ a) z hz
have hz' : z ∈
  spectrum ℂ (A := ↥(elemental ℂ a))
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra ℂ A) (elemental ℂ a) x) a sorry)
Tactic: have hz' := (StarSubalgebra.spectrum_eq (hS := isClosed ℂ a)
      (a := ⟨a, self_mem ℂ a⟩) ▸ hz)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
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 ⋯)
⊢ ∃ (a_1 : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)),
    characterSpaceToSpectrum a a_1 = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ spectrum ℂ a) z hz
have 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 sorry) =
    z
Tactic: rw [CharacterSpace.mem_spectrum_iff_exists] at hz'
Cleared hypotheses: hz'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ ∃ (a_1 : (↑(characterSpace ℂ ↥(elemental ℂ a)) : Type u_1)),
    characterSpaceToSpectrum a a_1 = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ spectrum ℂ a) z hz
have 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 sorry) :
        ℂ)),
  ∃ (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 sorry))
        hz
Tactic: obtain ⟨φ, rfl⟩ := hz'
Cleared hypotheses: z, hz, hz'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ ∃ (φ : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] A),
    Continuous (X := C((↑(spectrum ℂ a) : Type), ℂ)) (Y := A) (⇑φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) ∧
      Function.Injective (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
          (⇑φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) ∧
        (φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) =
            a ∧
          (∀ (f : C((↑(spectrum ℂ a) : Type), ℂ)),
              spectrum ℂ (A := A) ((φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) f : A) =
                Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)) ∧
            ∀ (f : C((↑(spectrum ℂ a) : Type), ℂ)),
              IsStarNormal (R := A) ((φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) f : A)
have this : Isometry (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
  (⇑(StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
        (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a))) :
    (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
Tactic: have : Isometry ((StarAlgebra.elemental ℂ a).subtype.comp <| continuousFunctionalCalculus a :
        C(spectrum ℂ a, ℂ) →⋆ₐ[ℂ] A) :=
      isometry_subtype_coe.comp <| StarAlgEquiv.isometry (continuousFunctionalCalculus a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
this :
  Isometry (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
    (⇑(StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
          (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a))) :
      (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
⊢ ∃ (φ : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] A),
    Continuous (X := C((↑(spectrum ℂ a) : Type), ℂ)) (Y := A) (⇑φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) ∧
      Function.Injective (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
          (⇑φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) ∧
        (φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) =
            a ∧
          (∀ (f : C((↑(spectrum ℂ a) : Type), ℂ)),
              spectrum ℂ (A := A) ((φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) f : A) =
                Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)) ∧
            ∀ (f : C((↑(spectrum ℂ a) : Type), ℂ)),
              IsStarNormal (R := A) ((φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) f : A)
have refine : (StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
        (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)) :
      (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
    (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) =
  a
Tactic: refine ⟨_, this.continuous, this.injective, ?hom_id, ?hom_map_spectrum, ?predicate_hom⟩