awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C((↑(spectrum ℝ A) : Type), ℝ)
f : C((↑(spectrum ℝ A) : Type), ℝ)
hf :
  Eq (α := Matrix n n 𝕜)
    (((↑hA.cfcAux :
            [inst_3 :
                FunLike (C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) C((↑(spectrum ℝ A) : Type), ℝ)
                  (Matrix n n 𝕜)] →
              [SemilinearMapClass (C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (RingHom.id ℝ)
                    C((↑(spectrum ℝ A) : Type), ℝ) (Matrix n n 𝕜)] →
                C((↑(spectrum ℝ A) : Type), ℝ) →ₗ[ℝ] Matrix n n 𝕜) :
          (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)
        f :
      Matrix n n 𝕜)
    (0 : Matrix n n 𝕜)
h2 :
  Eq (α := Matrix n n 𝕜)
    (diagonal
      (RCLike.ofReal ∘
        Function.comp (β := (↑(spectrum ℝ A) : Type)) (⇑f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) fun (i : n) ↦
          Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) ⋯))
    0
x : (↑(spectrum ℝ A) : Type)
⊢ Eq (α := ℝ) ((f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) x : ℝ) (0 : ℝ)
have h : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ A),
  Eq (α := ℝ) ((f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) x hx) : ℝ)
    (0 : ℝ)
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C((↑(spectrum ℝ A) : Type), ℝ)
f : C((↑(spectrum ℝ A) : Type), ℝ)
hf :
  Eq (α := Matrix n n 𝕜)
    (((↑hA.cfcAux :
            [inst_3 :
                FunLike (C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) C((↑(spectrum ℝ A) : Type), ℝ)
                  (Matrix n n 𝕜)] →
              [SemilinearMapClass (C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (RingHom.id ℝ)
                    C((↑(spectrum ℝ A) : Type), ℝ) (Matrix n n 𝕜)] →
                C((↑(spectrum ℝ A) : Type), ℝ) →ₗ[ℝ] Matrix n n 𝕜) :
          (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)
        f :
      Matrix n n 𝕜)
    (0 : Matrix n n 𝕜)
h2 :
  Eq (α := Matrix n n 𝕜)
    (diagonal
      (RCLike.ofReal ∘
        Function.comp (β := (↑(spectrum ℝ A) : Type)) (⇑f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) fun (i : n) ↦
          Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) ⋯))
    0
x : ℝ
hx : x ∈ spectrum ℝ A
⊢ Eq (α := ℝ) ((f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) x hx) : ℝ)
    (0 : ℝ)
have h : ∀ (i : n) (hx : hA.eigenvalues i ∈ spectrum ℝ A),
  Eq (α := ℝ)
    ((f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) hx) :
      ℝ)
    (0 : ℝ)
Tactic: obtain ⟨i, rfl⟩ := hA.spectrum_real_eq_range_eigenvalues ▸ hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C((↑(spectrum ℝ A) : Type), ℝ)
f : C((↑(spectrum ℝ A) : Type), ℝ)
hf :
  Eq (α := Matrix n n 𝕜)
    (((↑hA.cfcAux :
            [inst_3 :
                FunLike (C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) C((↑(spectrum ℝ A) : Type), ℝ)
                  (Matrix n n 𝕜)] →
              [SemilinearMapClass (C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (RingHom.id ℝ)
                    C((↑(spectrum ℝ A) : Type), ℝ) (Matrix n n 𝕜)] →
                C((↑(spectrum ℝ A) : Type), ℝ) →ₗ[ℝ] Matrix n n 𝕜) :
          (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)
        f :
      Matrix n n 𝕜)
    (0 : Matrix n n 𝕜)
h2 :
  Eq (α := Matrix n n 𝕜)
    (diagonal
      (RCLike.ofReal ∘
        Function.comp (β := (↑(spectrum ℝ A) : Type)) (⇑f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) fun (i : n) ↦
          Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) ⋯))
    0
i : n
hx : hA.eigenvalues i ∈ spectrum ℝ A
⊢ Eq (α := ℝ)
    ((f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) hx) :
      ℝ)
    (0 : ℝ)
have h : ∀
  (h2 :
    Eq (α := Matrix n n 𝕜)
      (diagonal
        (RCLike.ofReal ∘
          Function.comp (β := (↑(spectrum ℝ A) : Type)) (⇑f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) fun (i : n) ↦
            Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) sorry))
      (diagonal fun (x : n) ↦ 0))
  (i : n) (hx : hA.eigenvalues i ∈ spectrum ℝ A),
  Eq (α := ℝ)
    ((f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) hx) :
      ℝ)
    (0 : ℝ)
Tactic: rw [← diagonal_zero] at h2
Cleared hypotheses: h2, i, hx
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (hypothesis)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C((↑(spectrum ℝ A) : Type), ℝ)
f : C((↑(spectrum ℝ A) : Type), ℝ)
hf :
  Eq (α := Matrix n n 𝕜)
    (((↑hA.cfcAux :
            [inst_3 :
                FunLike (C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) C((↑(spectrum ℝ A) : Type), ℝ)
                  (Matrix n n 𝕜)] →
              [SemilinearMapClass (C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (RingHom.id ℝ)
                    C((↑(spectrum ℝ A) : Type), ℝ) (Matrix n n 𝕜)] →
                C((↑(spectrum ℝ A) : Type), ℝ) →ₗ[ℝ] Matrix n n 𝕜) :
          (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)
        f :
      Matrix n n 𝕜)
    (0 : Matrix n n 𝕜)
h2 :
  Eq (α := Matrix n n 𝕜)
    (diagonal
      (RCLike.ofReal ∘
        Function.comp (β := (↑(spectrum ℝ A) : Type)) (⇑f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) fun (i : n) ↦
          Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) ⋯))
    (diagonal fun (x : n) ↦ 0)
i : n
hx : hA.eigenvalues i ∈ spectrum ℝ A
⊢ Eq (α := ℝ)
    ((f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) hx) :
      ℝ)
    (0 : ℝ)
have this : ∀ (i : n),
  Eq.{u_2 + 1} (α := 𝕜)
    ((RCLike.ofReal ∘
        Function.comp (β := (↑(spectrum ℝ A) : Type)) (⇑f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) fun (i : n) ↦
          Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) sorry)
      i)
    0
Tactic: have := diagonal_eq_diagonal_iff.mp h2
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [hA.spectral_theorem]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ (hA.cfcAux : (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)
      (ContinuousMap.restrict (spectrum ℝ A) (ContinuousMap.id ℝ)) =
    A
have conv_rhs : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: conv_rhs => rw [hA.spectral_theorem]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
inst_3 : Nontrivial (Matrix n n 𝕜)
a : Matrix n n 𝕜
ha : IsSelfAdjoint a
⊢ (spectrum ℝ a).Nonempty
have inl : ∀ (h : IsEmpty n), (spectrum ℝ a).Nonempty
Tactic: obtain (h | h) := isEmpty_or_nonempty n
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
inst_3 : Nontrivial (Matrix n n 𝕜)
a : Matrix n n 𝕜
ha : IsSelfAdjoint a
inl : ∀ (h : IsEmpty n), (spectrum ℝ a).Nonempty
⊢ (spectrum ℝ a).Nonempty
have inr : ∀ (h : Nonempty n), (spectrum ℝ a).Nonempty
Tactic: obtain (h | h) := isEmpty_or_nonempty n
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
inst_3 : Nontrivial (Matrix n n 𝕜)
a : Matrix n n 𝕜
ha : IsSelfAdjoint a
h : IsEmpty n
⊢ (spectrum ℝ a).Nonempty
have inl : ∀ (x y : Matrix n n 𝕜) (hxy : x ≠ y), (spectrum ℝ a).Nonempty
Tactic: obtain ⟨x, y, hxy⟩ := exists_pair_ne (Matrix n n 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (hypothesis)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : IsSelfAdjoint a
⊢ ∃ (φ : C((↑(spectrum ℝ a) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜),
    Continuous[_, instTopologicalSpaceMatrix] (⇑φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) ∧
      Function.Injective (α := C((↑(spectrum ℝ a) : Type), ℝ)) (β := Matrix n n 𝕜)
          (⇑φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) ∧
        (φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜)
              (ContinuousMap.restrict (spectrum ℝ a) (ContinuousMap.id ℝ)) =
            a ∧
          (∀ (f : C((↑(spectrum ℝ a) : Type), ℝ)),
              spectrum ℝ (A := Matrix n n 𝕜)
                  ((φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜) =
                Set.range (ι := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)) ∧
            ∀ (f : C((↑(spectrum ℝ a) : Type), ℝ)),
              IsSelfAdjoint (R := Matrix n n 𝕜)
                ((φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜)
have ha₁ : a.IsHermitian
Tactic: replace ha : IsHermitian a := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
⊢ ∃ (φ : C((↑(spectrum ℝ a) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜),
    Continuous[_, instTopologicalSpaceMatrix] (⇑φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) ∧
      Function.Injective (α := C((↑(spectrum ℝ a) : Type), ℝ)) (β := Matrix n n 𝕜)
          (⇑φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) ∧
        (φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜)
              (ContinuousMap.restrict (spectrum ℝ a) (ContinuousMap.id ℝ)) =
            a ∧
          (∀ (f : C((↑(spectrum ℝ a) : Type), ℝ)),
              spectrum ℝ (A := Matrix n n 𝕜)
                  ((φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜) =
                Set.range (ι := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)) ∧
            ∀ (f : C((↑(spectrum ℝ a) : Type), ℝ)),
              IsSelfAdjoint (R := Matrix n n 𝕜)
                ((φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜)
have refine : ∀ (f : C((↑(spectrum ℝ a) : Type), ℝ)),
  spectrum ℝ (A := Matrix n n 𝕜) ((ha.cfcAux : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜) =
    Set.range (ι := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
Tactic: refine ⟨ha.cfcAux, ha.isClosedEmbedding_cfcAux.continuous,
      ha.isClosedEmbedding_cfcAux.injective, ha.cfcAux_id, fun f ↦ ?map_spec,
      fun f ↦ ?hermitian⟩
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
refine :
  ∀ (f : C((↑(spectrum ℝ a) : Type), ℝ)),
    spectrum ℝ (A := Matrix n n 𝕜)
        ((ha.cfcAux : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜) =
      Set.range (ι := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
⊢ ∃ (φ : C((↑(spectrum ℝ a) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜),
    Continuous[_, instTopologicalSpaceMatrix] (⇑φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) ∧
      Function.Injective (α := C((↑(spectrum ℝ a) : Type), ℝ)) (β := Matrix n n 𝕜)
          (⇑φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) ∧
        (φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜)
              (ContinuousMap.restrict (spectrum ℝ a) (ContinuousMap.id ℝ)) =
            a ∧
          (∀ (f : C((↑(spectrum ℝ a) : Type), ℝ)),
              spectrum ℝ (A := Matrix n n 𝕜)
                  ((φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜) =
                Set.range (ι := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)) ∧
            ∀ (f : C((↑(spectrum ℝ a) : Type), ℝ)),
              IsSelfAdjoint (R := Matrix n n 𝕜)
                ((φ : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜)
have refine₁ : ∀ (f : C((↑(spectrum ℝ a) : Type), ℝ)),
  IsSelfAdjoint (R := Matrix n n 𝕜) ((ha.cfcAux : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜)
Tactic: refine ⟨ha.cfcAux, ha.isClosedEmbedding_cfcAux.continuous,
      ha.isClosedEmbedding_cfcAux.injective, ha.cfcAux_id, fun f ↦ ?map_spec,
      fun f ↦ ?hermitian⟩
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C((↑(spectrum ℝ a) : Type), ℝ)
⊢ spectrum ℝ (A := Matrix n n 𝕜) ((ha.cfcAux : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜) =
    Set.range (ι := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
have a₁ : spectrum ℝ (A := Matrix n n 𝕜) ((ha.cfcAux : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜) ⊆
  Set.range (ι := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
Tactic: apply Set.eq_of_subset_of_subset
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C((↑(spectrum ℝ a) : Type), ℝ)
a₁ :
  spectrum ℝ (A := Matrix n n 𝕜) ((ha.cfcAux : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜) ⊆
    Set.range (ι := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
⊢ spectrum ℝ (A := Matrix n n 𝕜) ((ha.cfcAux : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜) =
    Set.range (ι := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
have a₂ : Set.range (ι := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) ⊆
  spectrum ℝ (A := Matrix n n 𝕜) ((ha.cfcAux : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜)
Tactic: apply Set.eq_of_subset_of_subset
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C((↑(spectrum ℝ a) : Type), ℝ)
⊢ spectrum ℝ (A := Matrix n n 𝕜) ((ha.cfcAux : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜) ⊆
    Set.range (ι := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
have a₁ : spectrum ℝ (A := Matrix n n 𝕜) ((ha.cfcAux : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜) ⊆
  spectrum ℝ f
Tactic: rw [← ContinuousMap.spectrum_eq_range f]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C((↑(spectrum ℝ a) : Type), ℝ)
⊢ Set.range (ι := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) ⊆
    spectrum ℝ (A := Matrix n n 𝕜) ((ha.cfcAux : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜)
have a₁ : Set.range (ι := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) ⊆
  spectrum ℝ (A := Matrix n n 𝕜)
    (diagonal
      (RCLike.ofReal ∘
        Function.comp (β := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) fun (i : n) ↦
          Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues i) sorry))
Tactic: rw [cfcAux_apply, conjStarAlgAut_apply, Unitary.spectrum_star_right_conjugate]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C((↑(spectrum ℝ a) : Type), ℝ)
x : (↑(spectrum ℝ a) : Type)
⊢ Membership.mem (α := ℝ)
    (spectrum ℝ (A := Matrix n n 𝕜)
      (diagonal
        (RCLike.ofReal ∘
          Function.comp (β := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) fun (i : n) ↦
            Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues i) ⋯)))
    ((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) x : ℝ)
have a₁ : Membership.mem (α := 𝕜)
  (spectrum 𝕜 (A := Matrix n n 𝕜)
    (diagonal
      (RCLike.ofReal ∘
        Function.comp (β := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) fun (i : n) ↦
          Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues i) sorry)))
  ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) x : ℝ) : 𝕜)
Tactic: apply spectrum.of_algebraMap_mem 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C((↑(spectrum ℝ a) : Type), ℝ)
x : (↑(spectrum ℝ a) : Type)
⊢ Membership.mem (α := 𝕜)
    (spectrum 𝕜 (A := Matrix n n 𝕜)
      (diagonal
        (RCLike.ofReal ∘
          Function.comp (β := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) fun (i : n) ↦
            Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues i) ⋯)))
    ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) x : ℝ) : 𝕜)
have a₁ : ∃ (y : n),
  Eq (α := 𝕜)
    ((↑((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
            (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues y) sorry)) :
        𝕜) :
      𝕜)
    ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) x : ℝ) : 𝕜)
Tactic: simp only [Function.comp_apply, Set.mem_range, spectrum_diagonal]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C((↑(spectrum ℝ a) : Type), ℝ)
x : (↑(spectrum ℝ a) : Type)
⊢ ∃ (y : n),
    Eq (α := 𝕜)
      ((↑((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
              (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues y) ⋯)) :
          𝕜) :
        𝕜)
      ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) x : ℝ) : 𝕜)
have a₁ : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ a),
  ∃ (y : n),
    Eq (α := 𝕜)
      ((↑((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
              (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues y) sorry)) :
          𝕜) :
        𝕜)
      ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜)
          ((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) x hx) : ℝ) :
        𝕜)
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C((↑(spectrum ℝ a) : Type), ℝ)
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ ∃ (y : n),
    Eq (α := 𝕜)
      ((↑((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
              (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues y) ⋯)) :
          𝕜) :
        𝕜)
      ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜)
          ((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) x hx) : ℝ) :
        𝕜)
have a₁ : ∀ (i : n) (hx : ha.eigenvalues i ∈ spectrum ℝ a),
  ∃ (y : n),
    Eq (α := 𝕜)
      ((↑((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
              (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues y) sorry)) :
          𝕜) :
        𝕜)
      ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜)
          ((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
              (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues i) hx) :
            ℝ) :
        𝕜)
Tactic: obtain ⟨i, rfl⟩ := ha.spectrum_real_eq_range_eigenvalues ▸ hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C((↑(spectrum ℝ a) : Type), ℝ)
⊢ IsSelfAdjoint (R := Matrix n n 𝕜) ((ha.cfcAux : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜)
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [isSelfAdjoint_iff, cfcAux_apply, ← map_star]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C((↑(spectrum ℝ a) : Type), ℝ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [star_eq_conjTranspose, diagonal_conjTranspose]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C((↑(spectrum ℝ a) : Type), ℝ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : Eq (α := n → 𝕜)
  (star
    (RCLike.ofReal ∘
      Function.comp (β := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) fun (i : n) ↦
        Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues i) sorry))
  (RCLike.ofReal ∘
    Function.comp (β := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) fun (i : n) ↦
      Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues i) sorry)
Tactic: congr!
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (hypothesis)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
⊢ cfc (p := IsSelfAdjoint) f A = hA.cfc f
have hA' : IsSelfAdjoint A
Tactic: have hA' : IsSelfAdjoint A := hA
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (hypothesis)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
⊢ cfc (p := IsSelfAdjoint) f A = hA.cfc f
have this : Eq (α := C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (cfcHom (p := IsSelfAdjoint) hA') hA.cfcAux
Tactic: have := cfcHom_eq_of_continuous_of_map_id hA' hA.cfcAux hA.isClosedEmbedding_cfcAux.continuous
    hA.cfcAux_id