Induction alternative name when using Quot.ind?

Stream: lean4

[François G. Dorais]

What is the induction alternative name when using Quot.ind? Leaving it blank works fine as in this snippet:

by induction q using Quot.ind with
| _ x => sorry

What should that blank be? mk doesn't work...

[Kyle Miller]

I believe the alternative names for the induction tactic come from the names of the arguments for the recursor. Quot.ind doesn't name the induction hypothesis however:

Quot.ind : ∀ {α : Sort u_1} {r : α → α → Prop} {β : Quot r → Prop}, (∀ (a : α), β (Quot.mk r a)) → ∀ (q : Quot r), β q

Judging by the case a heading for the tactic state at the sorry, it seems that Lean has decided to give it the name a (I wasn't able to figure out where this happens in the induction tactic though). So, this works:

induction q using Quot.ind with
| a x => exact sorry

[Kyle Miller]

Indeed:

def Quot.ind' {r : α → α → Prop} {β : Quot r → Prop}
  (mk : ∀ (a : α), β (Quot.mk r a)) : ∀ (q : Quot r), β q := Quot.ind mk

example (r : α → α → Prop) (q : Quot r) : q ≠ q :=
  by induction q using Quot.ind' with
  | mk x => exact sorry