rw a binding in tactic mode

Stream: new members

[ROCKY KAMEN-RUBIO]

How do I tell lean to replace a value with its binding? It seems like neither unfold nor rewrite work here.

Degenerate example for the sake of the mwe.

example : tt :=
begin
have x := 1,
have hx : x = 1,
{
  --how do I do this?
  sorry},
exact rfl,
end

[Kenny Lau]

have forgets definition, so you're out of luck

[Bryan Gin-ge Chen]

You want to use let instead of have to set the value of x.

[Kenny Lau]

you might want to use generalize

[Kenny Lau]

example : tt :=
begin
  let x := 1,
  have hx : x = 1 := rfl,
  exact rfl,
end

example : tt :=
begin
  generalize hx : 1 = x,
  exact rfl,
end

[Kevin Buzzard]

tt is a term not a type, so example : tt is a bit weird. I suspect lean is coercing it to true, which is a type