modifying let bindings via induction?

Stream: new members

[Paul Nelson]

In this example, induction' modifies the goal, but not the binding for y. Is there a way to get it to modify both, or some other way to "remember" in the subsequent case analysis that y is Sum.inl a in the first case and Sum.inr b in the second?

import Mathlib

example
  (e : γ ≃ α ⊕ β)
  (x : γ)
  : e x = e x := by
  let y := e x
  induction' e x with a b
  · sorry
  sorry

[Ruben Van de Velde]

Maybe induction' h : ..

[Paul Nelson]

perfect, thanks

[Richard Copley]

revert y before the induction' also does something that might be close to what you want.

[Ruben Van de Velde]

Though in that case you might use generalising y instead

[Paul Nelson]

OK I'll try those in a second. Maybe a related meta-question: is there some place where tactics like induction' are documented? I had tried #help tactic and looked briefly at Mathlib/Tactic/Cases.lean (and saw it in parts of MIL, but didn’t recall seeing the trick mentioned here). Or maybe the correct approach is to learn to read the self-documentation provided here by the source in Cases.lean?

[Ruben Van de Velde]

We used to have an overview like that for lean 3, but we haven't gotten around to rewriting it for lean 4, unfortunately

[Kevin Buzzard]

All tactics are documented "unofficially" here https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md but if you're a beginner and just want to know 25 or so common tactics then I just updated my course to use Lean 4 and my docs for tactics are here https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2024/Part_C/Part_C.html

[Winston Yin (尹維晨)]

Kevin Buzzard said:

All tactics are documented "unofficially" here https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md but if you're a beginner and just want to know 25 or so common tactics then I just updated my course to use Lean 4 and my docs for tactics are here https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2024/Part_C/Part_C.html

First time seeing either of these pages! They should definitely be featured more prominently / made official on the documentation site. I've been going back to the mathlib3 docs for tactic reference, wondering what could've changed in the mathlib4 version...