meaning of `.symm`

Stream: new members

[Vasily Ilin]

I have state

z: ℂ
h1: ↑(z.re).re = z.re
h2: ↑(z.re).im = z.im
⊢ z.im = 0

and I used suggest, which suggested exact h2.symm. But what does .symm do? VSCode does not show me anything when I hover over h2.symm.

Also, is this the right stream for posting specific questions like this?

[Patrick Johnson]

docs#eq.symm

[Patrick Johnson]

h2.symm is eq.symm h2

[Kyle Miller]

Does anyone know why hover wouldn't work with dot notation in exact?

example (x y : ℕ) (h : x = y) : y = x := by exact h.symm -- hover over `symm`, see `h`
example (x y : ℕ) (h : x = y) : y = x := h.symm -- hover over `symm`, see `eq.symm`
example (x y : ℕ) (h : x = y) : y = x := by exact (eq.symm (eq.symm h.symm)) -- hover over first `eq.symm` see nothing, over second see `eq.symm`, over `h.symm` see `h`.

[Kevin Buzzard]

Does it work with unfold? The reason I ask is that IIRC right clicking on X in unfold X takes my poor students to the definition of unfold rather than the definition of X