why does `rewrite at` create a new variable?

Stream: new members

[Yannick Seurin]

In the following example, why does tactic rw at create a new variable? I've never encountered this behavior before.
(NB: replacing the line rw [this] at b with simp only [nfoldProd] at b works, i.e., it yields b : β without creating a new variable; but curiously, simp only [zero_add] at b also creates a new variable.)

import Mathlib

def nfoldProd.{u} (α : Type u) : ℕ → Type u
  | 0     => PUnit
  | 1     => α
  | n + 2 => α × nfoldProd α (n + 1)

def nfoldMap.{u,v} {α : Type u} {β : Type v} (f : α → β) : (n : ℕ) → nfoldProd α n → nfoldProd β n
  | 0, _       => PUnit.unit
  | 1, x       => f x
  | n + 2, (x, xs) => (f x, nfoldMap f (n + 1) xs)

#eval nfoldMap (· + 1) 3 (7, (8, (9 : ℕ))) -- (8, 9, 10)

variable {α β : Type} {f : α → β}

theorem Function.bijective_nfold (n : ℕ) (hf : Function.Bijective f) :
    Function.Bijective (nfoldMap f n) := by
  apply (Function.bijective_iff_existsUnique (nfoldMap f n)).mpr
  intro b
  cases n with
    | zero =>
      simp only [nfoldMap]
      exact existsUnique_eq
    | succ n =>
      induction' n with n ih
      · simp only [Nat.reduceAdd, nfoldProd, nfoldMap] at *
        have : nfoldProd β (0 + 1) = β := rfl
        rw [this] at b -- creates b✝ : nfoldProd β (0 + 1) and replaces b by b✝ in the goal
        sorry
      sorry

[Aaron Liu]

It's because of b occurs in the goal and you rewrite it's type there's a change the goal will not typecheck anymore, so to be safe it gets duplicated. The reason simp doesn't do this sometimes is probably that it keeps track of if the transformation is defeq (if actually only dsimp would have done the same thing) and since everything is definitional it knows it doesn't have to make a new variable.

[Yannick Seurin]

Thanks Aaron. So are you saying that any time one does a rw [...] at h and h appears in the goal, this will happen?

[Aaron Liu]

yes, that's correct

[Aaron Liu]

and not just the goal, but anywhere

[Aaron Liu]

so it could be because it's used in the type of another hypothesis, or in the value of a local let-decl

[Yannick Seurin]

OK, thanks! I don't think I've seen this explained anywhere, might be worth an addition to rewrite documentation.

[Aaron Liu]

It's not specific to rewrite, there's a function docs#Lean.MVarId.replaceLocalDecl and all the tactics that use this function in their implementation will show the same behavior