awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Matrix.Hermitian
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
b : OrthonormalBasis n 𝕜 E
this : FiniteDimensional 𝕜 E
h :
  ∀ (x y : E),
    inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A : E →ₗ[𝕜] E) : (a : E) → E) x) y =
      inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) Aᴴ : E →ₗ[𝕜] E) : (a : E) → E) x) y
⊢ A.IsHermitian

Tactic:
simpa using (LinearMap.ext fun x ↦ ext_inner_right _ (h x)).symm

Premises used: LinearMap.ext, ext_inner_right, Eq.symm
-- Module: Mathlib.Analysis.Matrix.Hermitian
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ LinearMap.IsSymmetric (𝕜 := 𝕜) (E := EuclideanSpace 𝕜 n)
      ((toEuclideanLin : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) A) ↔
    A.IsHermitian

Tactic:
isSymmetric_toLin_iff (EuclideanSpace.basisFun n 𝕜)

Premises used: Multiset.sum, Multiset.foldr, dotProduct, EuclideanSpace.basisFun, Matrix.isSymmetric_toLin_iff, Matrix.mulVec, Finset.sum
-- Module: Mathlib.Analysis.Matrix.Hermitian
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ A.IsHermitian ↔
    LinearMap.IsSymmetric (𝕜 := 𝕜) (E := EuclideanSpace 𝕜 n)
      ((toEuclideanLin : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) A)

Tactic:
isSymmetric_toEuclideanLin_iff.symm

Premises used: Matrix.isSymmetric_toEuclideanLin_iff, Iff.symm
-- Module: Mathlib.Analysis.Matrix.Hermitian
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
inst_1 : Fintype n
hA : A.IsHermitian
x : n → 𝕜
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (star x ⬝ᵥ A *ᵥ x) : ℝ) (0 : ℝ)

Tactic:
simpa [dotProduct_comm] using (isSymmetric_toEuclideanLin_iff.mpr hA).im_inner_self_apply _

Premises used: Iff.mpr, LinearMap.IsSymmetric.im_inner_self_apply, Matrix.isSymmetric_toEuclideanLin_iff, dotProduct_comm
-- Module: Mathlib.Analysis.Matrix.Hermitian
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
inst_1 : Fintype n
hA : A.IsHermitian
x : n → 𝕜
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (star x ⬝ᵥ A *ᵥ x) : ℝ) (0 : ℝ)

Tactic:
classical
  simpa [dotProduct_comm] using (isSymmetric_toEuclideanLin_iff.mpr hA).im_inner_self_apply _

Premises used: Iff.mpr, LinearMap.IsSymmetric.im_inner_self_apply, Matrix.isSymmetric_toEuclideanLin_iff, dotProduct_comm
-- Module: Mathlib.Analysis.Matrix.Hermitian
Goal:
n : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : RCLike 𝕜
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
b : OrthonormalBasis n 𝕜 E
rw :
  IsSymmetric.{u_2, u_3} (𝕜 := 𝕜) (E := E)
      ((Matrix.toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E)
        ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix n n 𝕜) f)) ↔
    IsSymmetric.{u_2, u_3} (𝕜 := 𝕜) (E := E) f
rw₁ rw₂ : IsSymmetric.{u_2, u_3} (𝕜 := 𝕜) (E := E) f ↔ IsSymmetric.{u_2, u_3} (𝕜 := 𝕜) (E := E) f
⊢ Matrix.IsHermitian.{u_2, u_1} (α := 𝕜) (n := n) ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix n n 𝕜) f) ↔
    IsSymmetric.{u_2, u_3} (𝕜 := 𝕜) (E := E) f

Tactic:
rw [← Matrix.isSymmetric_toLin_iff b, Matrix.toLin_toMatrix]

Premises used: Matrix.isSymmetric_toLin_iff, Matrix.toLin_toMatrix
-- 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:
simp [Pi.one_def, Function.comp_def]

Premises used: Function.comp_def, Pi.one_def
-- 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
f g : C((↑(spectrum ℝ A) : Type), ℝ)
simp : 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:
simp only [ContinuousMap.coe_mul, ← map_mul, diagonal_mul_diagonal, Function.comp_apply]

Premises used: map_mul, Function.comp_apply, Matrix.diagonal_mul_diagonal, ContinuousMap.coe_mul
-- 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
f g : C((↑(spectrum ℝ A) : Type), ℝ)
⊢ 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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [Pi.zero_def, Function.comp_def]

Premises used: Pi.zero_def, Function.comp_def
-- 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
f g : C((↑(spectrum ℝ A) : Type), ℝ)
simp : 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:
simp only [ContinuousMap.coe_add, ← map_add, diagonal_add, Function.comp_apply]

Premises used: map_add, ContinuousMap.coe_add, Matrix.diagonal_add, 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
r : ℝ
simp : 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:
simp only [Function.comp_def, algebraMap_apply, smul_eq_mul, mul_one]

Premises used: algebraMap_apply, Function.comp_def, smul_eq_mul, mul_one
-- 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
r : ℝ
rw :
  ((↑hA.eigenvectorUnitary : Matrix n n 𝕜) * diagonal fun (x : n) ↦ (↑r : 𝕜)) *
      star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) =
    HMul.hMul (β := Matrix n n 𝕜) (↑hA.eigenvectorUnitary : Matrix n n 𝕜)
        ((algebraMap ℝ (Matrix n n 𝕜) : (a : ℝ) → Matrix n n 𝕜) r : Matrix n n 𝕜) *
      star (↑hA.eigenvectorUnitary : Matrix n n 𝕜)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← mul_one (algebraMap _ _ _), ← coe_mul_star_self hA.eigenvectorUnitary,
      ← Algebra.left_comm, coe_star, ← mul_assoc, conjStarAlgAut_apply]

Premises used: Matrix.IsHermitian.eigenvectorUnitary, Algebra.algebraMap, mul_assoc, Unitary.coe_mul_star_self, Unitary.conjStarAlgAut_apply, Algebra.left_comm, mul_one, DFunLike.coe, Unitary.coe_star
-- 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
r : ℝ
⊢ ((↑hA.eigenvectorUnitary : Matrix n n 𝕜) * diagonal fun (x : n) ↦ (↑r : 𝕜)) *
      star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) =
    HMul.hMul (β := Matrix n n 𝕜) (↑hA.eigenvectorUnitary : Matrix n n 𝕜)
        ((algebraMap ℝ (Matrix n n 𝕜) : (a : ℝ) → Matrix n n 𝕜) r : Matrix n n 𝕜) *
      star (↑hA.eigenvectorUnitary : Matrix n n 𝕜)

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
f : C((↑(spectrum ℝ A) : Type), ℝ)
simp : 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:
simp only [star_trivial, ← map_star, star_eq_conjTranspose, diagonal_conjTranspose, Pi.star_def,
      Function.comp_apply, RCLike.star_def, RCLike.conj_ofReal]

Premises used: Matrix.star_eq_conjTranspose, RCLike.star_def, RCLike.conj_ofReal, StarHomClass.map_star, TrivialStar.star_trivial, Matrix.diagonal_conjTranspose, Pi.star_def, 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
f : C((↑(spectrum ℝ A) : Type), ℝ)
⊢ 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
⊢ FiniteDimensional ℝ C((↑(spectrum ℝ A) : Type), ℝ)

Tactic:
have h0 : FiniteDimensional ℝ C(spectrum ℝ A, ℝ) :=
    FiniteDimensional.of_injective (ContinuousMap.coeFnLinearMap ℝ (M := ℝ)) DFunLike.coe_injective
-- 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), ℝ)
⊢ IsClosedEmbedding (X := C((↑(spectrum ℝ A) : Type), ℝ)) (Y := Matrix n n 𝕜)
    (⇑hA.cfcAux : (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)

Tactic:
LinearMap.isClosedEmbedding_of_injective (𝕜 := ℝ) (E := C(spectrum ℝ A, ℝ))
    (F := Matrix n n 𝕜) (f := hA.cfcAux) <| LinearMap.ker_eq_bot'.mpr fun f hf ↦ ?_

Premises used: Iff.mpr, LinearMap.isClosedEmbedding_of_injective, LinearMap.ker_eq_bot'
-- 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), ℝ)
refine :
  ∀ (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 𝕜)),
    f = 0
⊢ IsClosedEmbedding (X := C((↑(spectrum ℝ A) : Type), ℝ)) (Y := Matrix n n 𝕜)
    (⇑hA.cfcAux : (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)

Tactic:
refine LinearMap.isClosedEmbedding_of_injective (𝕜 := ℝ) (E := C(spectrum ℝ A, ℝ))
    (F := Matrix n n 𝕜) (f := hA.cfcAux) <| LinearMap.ker_eq_bot'.mpr fun f hf ↦ ?_

Premises used: Iff.mpr, LinearMap.isClosedEmbedding_of_injective, LinearMap.ker_eq_bot'
-- 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 :
  (↑hA.eigenvectorUnitary : 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) ⋯) *
      star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) =
    0
⊢ (↑hA.eigenvectorUnitary : 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) ⋯) *
        star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
      (↑hA.eigenvectorUnitary : Matrix n n 𝕜) =
    0 * (↑hA.eigenvectorUnitary : Matrix n n 𝕜)

Tactic:
replace hf := congr($hf * (hA.eigenvectorUnitary : Matrix n n 𝕜))
-- 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 :
  (↑hA.eigenvectorUnitary : 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) ⋯) *
        star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
      (↑hA.eigenvectorUnitary : Matrix n n 𝕜) =
    0 * (↑hA.eigenvectorUnitary : Matrix n n 𝕜)
⊢ (↑hA.eigenvectorUnitary : 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

Tactic:
simp only [mul_assoc, SetLike.coe_mem, Unitary.star_mul_self_of_mem, mul_one, zero_mul] at hf

Premises used: SetLike.coe_mem, MulZeroClass.zero_mul, mul_assoc, Unitary.star_mul_self_of_mem, mul_one
-- 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 :
  (↑hA.eigenvectorUnitary : 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
⊢ 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

Tactic:
simpa [← mul_assoc] using congr((star hA.eigenvectorUnitary : Matrix n n 𝕜) * $hf)

Premises used: Matrix.IsHermitian.eigenvectorUnitary, mul_assoc, Subtype.val, Star.star
-- 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 𝕜)
⊢ 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

Tactic:
have h2 :
      diagonal (RCLike.ofReal ∘ f ∘ fun i ↦ ⟨hA.eigenvalues i, hA.eigenvalues_mem_spectrum_real i⟩)
        = (0 : Matrix n n 𝕜) := by
    simp only [LinearMap.coe_coe, cfcAux_apply, conjStarAlgAut_apply] at hf
    replace hf := congr($hf * (hA.eigenvectorUnitary : Matrix n n 𝕜))
    simp only [mul_assoc, SetLike.coe_mem, Unitary.star_mul_self_of_mem, mul_one, zero_mul] at hf
    simpa [← mul_assoc] using congr((star hA.eigenvectorUnitary : Matrix n n 𝕜) * $hf)
-- 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) ⋯))
    0
x : (↑(spectrum ℝ A) : Type)
h :
  ∀ (x : ℝ) (hx : x ∈ spectrum ℝ A),
    Eq (α := ℝ) ((f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) x hx) : ℝ)
      (0 : ℝ)
⊢ Eq (α := ℝ) ((f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) x : ℝ) (0 : ℝ)

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
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
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 : ℝ)
⊢ Eq (α := ℝ) ((f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) x hx) : ℝ)
    (0 : ℝ)

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
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
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) ⋯))
        (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 : ℝ)
⊢ 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

Premises used: Matrix.diagonal_zero
-- 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
⊢ ∀ (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

Tactic:
have := diagonal_eq_diagonal_iff.mp h2