no goals
α : Type u_2
β : Type ?u.51699
m : Type ?u.51702
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : IsROrC α
inst✝ : IsROrC β
A : Matrix n n α
h : IsHermitian A
i : n
⊢ ↑(↑re (A i i)) = A i i
rw [← conj_eq_iff_re, ← star_def, ← conjTranspose_apply, h.eq]