awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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
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) ⋯)
        i)
      0
⊢ Eq (α := ℝ)
    ((f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) hx) :
      ℝ)
    (0 : ℝ)

Tactic:
RCLike.ofReal_eq_zero.mp (this i)

Premises used: RCLike.ofReal_eq_zero, Iff.mp
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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
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) ⋯)
        i)
      0
⊢ Eq (α := ℝ)
    ((f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) hx) :
      ℝ)
    (0 : ℝ)

Tactic:
exact RCLike.ofReal_eq_zero.mp (this i)

Premises used: RCLike.ofReal_eq_zero, Iff.mp
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [hA.spectral_theorem]

Premises used: Matrix.IsHermitian.spectral_theorem
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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
conv_rhs : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (hA.cfcAux : (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)
      (ContinuousMap.restrict (spectrum ℝ A) (ContinuousMap.id ℝ)) =
    A

Tactic:
conv_rhs => rw [hA.spectral_theorem]

Premises used: Matrix.IsHermitian.spectral_theorem
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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)

Tactic:
rfl
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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
inr : ∀ (h : Nonempty n), (spectrum ℝ a).Nonempty
⊢ (spectrum ℝ a).Nonempty

Tactic:
obtain (h | h) := isEmpty_or_nonempty n

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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
inl : ∀ (x y : Matrix n n 𝕜) (hxy : x ≠ y), (spectrum ℝ a).Nonempty
⊢ (spectrum ℝ a).Nonempty

Tactic:
obtain ⟨x, y, hxy⟩ := exists_pair_ne (Matrix n n 𝕜)

Premises used: Matrix, exists_pair_ne
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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
x y : Matrix n n 𝕜
hxy : x ≠ y
⊢ (spectrum ℝ a).Nonempty

Tactic:
False.elim <| Matrix.of.symm.injective.ne hxy <| Subsingleton.elim _ _

Premises used: False.elim, Matrix.of, Function.Injective.ne, Equiv.injective, Equiv.symm, Subsingleton.elim
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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
x y : Matrix n n 𝕜
hxy : x ≠ y
⊢ (spectrum ℝ a).Nonempty

Tactic:
exact False.elim <| Matrix.of.symm.injective.ne hxy <| Subsingleton.elim _ _

Premises used: False.elim, Matrix.of, Function.Injective.ne, Equiv.injective, Equiv.symm, Subsingleton.elim
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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 : Nonempty n
⊢ (spectrum ℝ a).Nonempty

Tactic:
spectrum_real_eq_range_eigenvalues ha ▸ Set.range_nonempty _

Premises used: Eq.rec, Set.range_nonempty, Matrix.IsHermitian.spectrum_real_eq_range_eigenvalues, Eq.symm
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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 : Nonempty n
⊢ (spectrum ℝ a).Nonempty

Tactic:
exact spectrum_real_eq_range_eigenvalues ha ▸ Set.range_nonempty _
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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
⊢ a.IsHermitian

Tactic:
replace ha : IsHermitian a := ha
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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 𝕜)

Tactic:
⟨ha.cfcAux, ha.isClosedEmbedding_cfcAux.continuous,
      ha.isClosedEmbedding_cfcAux.injective, ha.cfcAux_id, fun f ↦ ?map_spec,
      fun f ↦ ?hermitian⟩

Premises used: Matrix.IsHermitian.isClosedEmbedding_cfcAux, Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsClosedEmbedding.continuous, And.intro, Topology.IsEmbedding.injective, Matrix.IsHermitian.cfcAux_id, Exists.intro, Matrix.IsHermitian.cfcAux
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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)) → ℝ)
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 𝕜)
⊢ ∃ (φ : 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 𝕜)

Tactic:
refine ⟨ha.cfcAux, ha.isClosedEmbedding_cfcAux.continuous,
      ha.isClosedEmbedding_cfcAux.injective, ha.cfcAux_id, fun f ↦ ?map_spec,
      fun f ↦ ?hermitian⟩
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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)) → ℝ)
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 𝕜)
⊢ 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

Premises used: Set.eq_of_subset_of_subset
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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 𝕜) ⊆
    spectrum ℝ f
⊢ 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:
rw [← ContinuousMap.spectrum_eq_range f]

Premises used: ContinuousMap.spectrum_eq_range
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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 𝕜) ⊆
    spectrum ℝ f

Tactic:
apply AlgHom.spectrum_apply_subset

Premises used: AlgHom.spectrum_apply_subset
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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₁ :
  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) ⋯))
⊢ 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:
rw [cfcAux_apply, conjStarAlgAut_apply, Unitary.spectrum_star_right_conjugate]

Premises used: Unitary.spectrum_star_right_conjugate, Matrix.IsHermitian.cfcAux_apply, Unitary.conjStarAlgAut_apply
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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)
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) ⋯)))
    ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) x : ℝ) : 𝕜)
⊢ 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 : ℝ)

Tactic:
apply spectrum.of_algebraMap_mem 𝕜

Premises used: spectrum.of_algebraMap_mem
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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)
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)) → ℝ) x : ℝ) : 𝕜)
⊢ 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 : ℝ) : 𝕜)

Tactic:
simp only [Function.comp_apply, Set.mem_range, spectrum_diagonal]

Premises used: Set.mem_range, spectrum_diagonal, Function.comp_apply
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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)
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) ⋯)) :
            𝕜) :
          𝕜)
        ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜)
            ((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) x hx) : ℝ) :
          𝕜)
⊢ ∃ (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 : ℝ) : 𝕜)

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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
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) ⋯)) :
            𝕜) :
          𝕜)
        ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜)
            ((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues i) hx) :
              ℝ) :
          𝕜)
⊢ ∃ (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) : ℝ) :
        𝕜)

Tactic:
obtain ⟨i, rfl⟩ := ha.spectrum_real_eq_range_eigenvalues ▸ hx

Premises used: rfl
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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), ℝ)
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) ⋯)) :
          𝕜) :
        𝕜)
      ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜)
          ((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
              (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues i) hx) :
            ℝ) :
        𝕜)

Tactic:
⟨i, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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), ℝ)
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) ⋯)) :
          𝕜) :
        𝕜)
      ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜)
          ((f : (a : (↑(spectrum ℝ a) : Type)) → ℝ)
              (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues i) hx) :
            ℝ) :
        𝕜)

Tactic:
exact ⟨i, rfl⟩
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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)) → ℝ)

Tactic:
case map_spec =>
      apply Set.eq_of_subset_of_subset
      · rw [← ContinuousMap.spectrum_eq_range f]
        apply AlgHom.spectrum_apply_subset
      · rw [cfcAux_apply, conjStarAlgAut_apply, Unitary.spectrum_star_right_conjugate]
        rintro - ⟨x, rfl⟩
        apply spectrum.of_algebraMap_mem 𝕜
        simp only [Function.comp_apply, Set.mem_range, spectrum_diagonal]
        obtain ⟨x, hx⟩ := x
        obtain ⟨i, rfl⟩ := ha.spectrum_real_eq_range_eigenvalues ▸ hx
        exact ⟨i, rfl⟩

Premises used: Set.mem_range, spectrum_diagonal, Unitary.spectrum_star_right_conjugate, Matrix.IsHermitian.cfcAux_apply, Unitary.conjStarAlgAut_apply, AlgHom.spectrum_apply_subset, ContinuousMap.spectrum_eq_range, Function.comp_apply, spectrum.of_algebraMap_mem, Set.eq_of_subset_of_subset, rfl
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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), ℝ)
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ IsSelfAdjoint (R := Matrix n n 𝕜) ((ha.cfcAux : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → Matrix n n 𝕜) f : Matrix n n 𝕜)

Tactic:
simp only [isSelfAdjoint_iff, cfcAux_apply, ← map_star]

Premises used: StarHomClass.map_star, Matrix.IsHermitian.cfcAux_apply, isSelfAdjoint_iff
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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), ℝ)
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [star_eq_conjTranspose, diagonal_conjTranspose]

Premises used: Matrix.star_eq_conjTranspose, Matrix.diagonal_conjTranspose
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
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), ℝ)
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) ⋯))
    (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) ⋯)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
congr!