[Merged by Bors] - fix(Tactic/Cases): fix context for induction'

[joneugster]

Adding a test case for induction' that failed and fixing it: induction' a would accidentally leave a and variables depending on a in context.

---

This is the example that's been added to the test cases:

example (a b : ℕ) (h : a + b = a) : b = 0 := by
  induction' a with d hd
  · sorry
  · -- bad context:
    -- a b: ℕ
    -- h✝: a + b = a
    -- d: ℕ
    -- hd: d + b = d → b = 0
    -- h: Nat.succ d + b = Nat.succ d
    -- ⊢ b = 0
    sorry

See Zulip thread

[semorrison]

bors d+

[bors]

✌️ joneugster can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[joneugster]

bors r+

[bors]

Build failed:

• Build

[semorrison]

@joneugster do you want to merge master, and see if there is a problem, and then send it to bors again?

[joneugster]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style