term mode `set`

Stream: new members

[Horatiu Cheval]

Is there an equivalent idiom to the set tactic for term mode in order to easily get definitional equations for local let bindings?
I am basically looking for a term mode equivalent of this.

example : {x : ℕ // x ≤ 42} :=
begin
  set x : ℕ := 3 with h,
end

I can of course always obtain h : x = 3 from a term mode let x := 3.

example : {x : ℕ // x ≤ 42} :=
  let x := 3 in
  ⟨x, begin
    have h : x = 3 := rfl,
  end⟩

But is there an option where I don't have to restate the x = 3 equality and then prove it trivially?

[Yakov Pechersky]

As far as I know, no. You can do a term mode "have" as well right after but it would involve stating the tautology. The set tactic just wraps all of this together for you.

[Eric Wieser]

(λ x (h : x = 3), sorry) _ rfl perhaps?

[Eric Wieser]

Which saves you writing 3 twice at least