-- Mathlib/LinearAlgebra/Matrix/HermitianFunctionalCalculus.lean
lemma isClosedEmbedding_cfcAux : IsClosedEmbedding hA.cfcAux

Proof state:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf : ↑hA.cfcAux f = 0
⊢ f = 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] at hf
  replace hf := congr($(hf) * (eigenvectorUnitary hA : 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))

Result:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf : ↑hA.cfcAux f = 0
h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) = 0
⊢ f = 0

Proof state:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
⊢ IsClosedEmbedding ⇑hA.cfcAux

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 ↦ ?_

Result:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf : ↑hA.cfcAux f = 0
⊢ f = 0

Proof state:
case h.mk.intro
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf : ↑hA.cfcAux f = 0
h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) = diagonal fun x => 0
i : n
hx : hA.eigenvalues i ∈ spectrum ℝ A
⊢ f ⟨hA.eigenvalues i, hx⟩ = 0

Tactic:
have := (diagonal_eq_diagonal_iff).mp h2

Result:
case h.mk.intro
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf : ↑hA.cfcAux f = 0
h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) = diagonal fun x => 0
i : n
hx : hA.eigenvalues i ∈ spectrum ℝ A
this : ∀ (i : n), (RCLike.ofReal ∘ ⇑f ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) i = 0
⊢ f ⟨hA.eigenvalues i, hx⟩ = 0

Proof state:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ IsClosedEmbedding ⇑hA.cfcAux

Tactic:
have h0 : FiniteDimensional ℝ C(spectrum ℝ A, ℝ) :=
  FiniteDimensional.of_injective (ContinuousMap.coeFnLinearMap ℝ (M := ℝ)) DFunLike.coe_injective

Result:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
⊢ IsClosedEmbedding ⇑hA.cfcAux