Is it idiomatic to explicitly unfold here?

Stream: new members

[Bbbbbbbbba]

Even though hxz ▸ hz on its own results in something defeq to the goal, having the expected type breaks the ▸ notation here.

import Mathlib

example (x z : ℕ) (hz : z + z + z + z + z = 20) (hxz : x = z) : x + x + x + x + x = 20 := by
  set y := x + x + x + x + x
  -- Some code that is made cleaner by this definition of y
  #check hxz ▸ hz -- Eq.symm hxz ▸ hz : x + x + x + x + x = 20
  -- rw [hxz] -- Tactic `rewrite` failed
  -- exact hxz ▸ hz -- invalid `▸` notation, expected result type of cast is  `y = 20`
  unfold y
  exact hxz ▸ hz

[Aaron Liu]

you can also set y := x + x + x + x + x with hy to get an hy you can use with rewriting

[Bbbbbbbbba]

True, but that feels a little more cumbersome than unfolding to me (if that is the only way I use that hypothesis)

[Ruben Van de Velde]

The triangle is very much "nice if it works, not worth digging into if it doesn't", in my opinion

[Snir Broshi]

You can smile

import Mathlib
example (x z : ℕ) (hz : z + z + z + z + z = 20) (hxz : x = z) : x + x + x + x + x = 20 := by
  set y := x + x + x + x + x
  exact (hxz ▸ hz :)

[Snir Broshi]

(#20436)

[Snir Broshi]

It's purpose is exactly to have no expected type