Accessing inductive hypothesis after using <;>

Stream: lean4

[Joey Eremondi]

I often write tactic code that looks like this:

induction x <;> intros a b <;> try aesop

If I have a large number of cases, usually aesop can knock a bunch of them out and then I'll manually provide proofs for the hard cases.

The problem I'm having is that in the remaining cases, the inductive hypothesis is in the context greyed out, and I can't refer to it directly because it has some machine-generated name.

I'm wondering, is there a way to either (1) access these unnamed/machine-named variables, or (2) manually give a name to the inductive hypothesis, when I'm using induction in a chain of tactics to try to automate as many cases as possible?

[Kyle Miller]

(1) yes, the rename_i tactic or the next ... => focusing block (or case ... => if you want to refer to a case by name). (2) yes, you can use the structured induction tactic, with syntax induction x with | case1 ... => ... | case2 ... => .... You can even write induction x with intros a b; try aesop | case1 .... => ... to try to knock out cases first. I could dig up references for these later.

[Mario Carneiro]

import Aesop
inductive Foo
  | a (x y : Nat)
  | b (x y : Nat)
  | c (x y : Nat)

example (u : Foo) : ∀ a b : Bool, ∃ x y, u = Foo.a x y := by
  induction u with intros a b <;> try aesop; done
  | b x y => sorry
  | c x y => sorry

example (u : Foo) : ∀ a b : Bool, ∃ x y, u = Foo.a x y := by
  induction u <;> intros a b <;> try aesop; done
  case b x y => sorry
  case c x y => sorry

[Joey Eremondi]

Ah, that works great, thanks both!