induction using additional relation

Stream: Is there code for X?

[Antoine Chambert-Loir]

I had something of the following form to prove:

example (α : Type*) (deg : α → ℕ∞) (motive : α → ℕ∞ → Prop) (a : α) :
    motive a (deg a) := by

My first attempt has been to use induction on ℕ∞ to split into the two possible cases,
⊤, or coe n, as follows, but that failed, it loses the relation between deg a and the specific case.

example (α : Type*) (deg : α → ℕ∞) (motive : α → ℕ∞ → Prop) (a : α) :
    motive a (deg a) := by
  induction deg a with
  -- loses the relation between `deg a` and `⊤` or `n`
  | top => sorry
  | coe n => sorry

The same issue actually happens for

example (α : Type*) (deg : α → ℕ) (motive : α → ℕ → Prop) (a : α) :
    motive a (deg a) := by
  induction deg a with
  -- loses the relation between `deg a` and `0` or `n`
  | zero => sorry
  | succ n h => sorry

The following worked, but there should be a more idiomatic way to do it, certainly using generalizing but I couldn't make it work.

example (α : Type*) (deg : α → ℕ∞) (motive : α → ℕ∞ → Prop) (a : α) :
    motive a (deg a) := by
  suffices ∀ n a, deg a = n → motive a n by
    exact this (deg a) a (refl _)
  intro n
  induction n with
  | top => sorry
  | coe n => sorry

[Riccardo Brasca]

Can you write explicitly your assumptions? I mean, those that make the lemma provable.

[Aaron Liu]

does induction hn : deg a with work

[Antoine Chambert-Loir]

Yes, it does! Thanks!

[Antoine Chambert-Loir]

For Riccardo, unfortunately, not. α is the SpecialLinearGroup K V (for some finite dimensional K-vector space V), deg is the transvection degree, the minimal number required to write an element as a product of transvections, and motive is the assertion finrank K V ≤ deg e + finrank K e.fixedSubmodule, where e.fixedSubmodule is the eigenspace for the eigenvalue 1.

[Riccardo Brasca]

It' s a bit annoying that it doesn't work with match or a similar syntax :(

[Riccardo Brasca]

It's actually the same syntax

example (α : Type*) (deg : α → ℕ∞) (motive : α → ℕ∞ → Prop) (a : α) (h : motive a ⊤) :
    motive a (deg a) := by
  match d : deg a with
  | ⊤ => exact h
  | some A =>
    sorry