Rewriting modulo let

Stream: lean4

[Wojciech Nawrocki]

Is there a reasonable way to do "rewriting modulo let"? That is, I want something like rw but which would also try to unify modulo the let-reduction rule (zeta). I have found a custom simp config to kind of work, but it still seems to do a bit more than I want it to (i.e. just rewriting). Btw, this is for use in a tactic so I cannot easily do all the things that I could in this particular interactive proof.

def f (n : Nat) := n + 1
example (k : Nat) : let x := 10; f x = k := by
  have : f 10 = 11 := rfl
  /- tactic 'rewrite' failed, did not find instance of the pattern in the target expression
    f 10 -/
  -- rw (config := { transparency := .all }) [this]
  simp (config := {
    zeta := true
    eta := false
    beta := false
    iota := false
    proj := false
    decide := false
  }) only [this]
  /- k : Nat
  this : f 10 = 11
  ⊢ 11 = k -/
  trace_state

[Leonardo de Moura]

If you intro x, you can use rw.

def f (n : Nat) := n + 1
example (k : Nat) : let x := 10; f x = k := by
  intro x
  have : f 10 = 11 := rfl
  rw [this]

[François G. Dorais]

I did not know that! Thanks!

At the risk of letting the wrong thing in... should letIn be a pattern? https://media4.giphy.com/media/PA5pAhOp5Y2Qg/giphy.gif?cid=c623cb35q728p49kdltp3pafce2i7qwepc8ch4izndkg6nbi&rid=giphy.gif&ct=g

[Wojciech Nawrocki]

Leonardo de Moura said:

If you intro x, you can use rw.

def f (n : Nat) := n + 1
example (k : Nat) : let x := 10; f x = k := by
  intro x
  have : f 10 = 11 := rfl
  rw [this]

Unfortunately this is one of the things I cannot do :) Thelet actually appears in an equality in a hypothesis. I.e. the goal state has

h : let x := 10; f x = k

[Leonardo de Moura]

@Wojciech Nawrocki I added two new features to conv mode. I hope they are helpful for your example.
See https://github.com/leanprover/lean4/blob/master/RELEASES.md

[Leonardo de Moura]

Example: conv at h => zeta; rw [this]