How to rewrite local definition?

Stream: new members

[Jakub Nowak]

How can I rewrite local definition? I know I can use subst, but this will remove the definition and it will replace it in all hypotheses and goal. But subst sometimes doesn't work, and sometimes I don't want to replace with the definition in all hypotheses and goal. How can I do that?

example : Nat :=
  let n := 1
  by
    have h₁ : n + 1 = 2 := by rfl
    have h₂ : n + 2 = 3 := by rfl
    -- That's what I want to get:
    replace h₁ : 1 + 1 = 2 := by rfl

[Aaron Liu]

You can rw [rewritingTheorm] at hypothesisName

[Jakub Nowak]

Yeah, but in this case, it's not a theorem of the form h : a = b, but a local definition a := b. And rw [n] at h₁ doesn't work.

[Eric Paul]

Here are two ways to do it.

The first way is to have Lean automatically add a theorem that says n = 1 and then you rewrite with it. The second is to use unfold.

example : Nat :=
  let (eq := h) n := 1
  by
    have h₁ : n + 1 = 2 := by rfl
    have h₂ : n + 2 = 3 := by rfl
    rw [h] at h₁

example : Nat :=
  let n := 1
  by
    have h₁ : n + 1 = 2 := by rfl
    have h₂ : n + 2 = 3 := by rfl
    unfold n at h₁

[Matt Diamond]

you can also write set n := 1 with h within the tactic block to get an equality lemma

[Ruben Van de Velde]

Or simp [n] at h

[Aaron Liu]

maybe simp only [n] at h

[Matt Diamond]

non-terminal simps aren't so great though... simp only [n] or simp_rw [n] might be cleaner, though it's also a heavy hammer and might simplify too much

[Aaron Liu]

better make that simp (config := Lean.Meta.Simp.neutralConfig) only [n, -eq_self] at h so you don't simplify too much

[Jakub Nowak]

Thanks everyone!
In my case I'm proving something about a function I wrote, and the value came from there, so I can't use set and I don't want to change to add unused equality lemma in my function.
unfold does exactly what I want. Haven't though about it, cause I only used it for unfolding definition of a function.

[Jakub Nowak]

Btw, if I ever wanted to contribute to mathlib, is there some policy about using non-terminal simp?

[Aaron Liu]

the policy is "don't do that" since simp can change behavior if new simp theorems are added and break your proof which now someone else has to spend time fixing

[Jakub Nowak]

Yeah, I'm aware. But what about simp only? I've noticed that simp only [] also sometimes does something, so is it ok to use it, or not?

[Aaron Liu]

simp only is fine since adding new simp lemmas won't change what it does