induction' leaves junk around

Stream: mathlib4

[Kevin Buzzard]

I just noticed this whilst in the process of rewriting NNG4 advanced addition world:

import Mathlib.Tactic.Cases

example (a b t : Nat) (h : a + t = b + t) : a = b := by
  induction t with
  | zero => sorry
  /-
  a b : ℕ
  h : a + Nat.zero = b + Nat.zero
  ⊢ a = b
  -/
  | succ n ih => sorry


example (a b t : Nat) (h : a + t = b + t) : a = b := by
  induction' t with d hd
  · sorry
  /-
  a b t : ℕ
  h✝ : a + t = b + t -- eh???
  h : a + Nat.zero = b + Nat.zero
  ⊢ a = b
  -/
  · sorry

The standard induction tactic tidies up after itself, but its variant induction' is leaving around a useless t and an inaccessible h✝ which mathematically shouldn't really be there anyway (you can't prove false but that's only because you don't know anything about t so it might be 0, giving you what you have already). In NNG4 the game infrastructure doesn't support all this 2d ASCII diagram => stuff, so our induction is like NNG3, it's Lean 4 induction'. Hence I'm getting all this junk too in NNG. There is also the same extra junk in the successor case.

In NNG3 I modified induction (with help from Rob) so that it changed all Nat.zeros to 0 after an induction call. Would it be hard to modify induction' so that it stopped leaving all this junk around? It's never useful (at least for nat) and it will cause confusion to users.