Tactic generalize failed result is not type correct

Stream: lean4

[Arnav Sabharwal]

I was trying to expand the definition of the non-inductive Fin2 type, using the PFin2 type defined below to match on it. However, as I was doing so, I encountered the following error, which I was unable to understand. Here is an MWE:

import Mathlib

open Nat

universe u

/-- An alternate definition of `fin n` defined as an inductive type instead of a subtype of `Nat`. -/
inductive PFin2 : Nat → Type u
  /- `0` as a member of `fin (succ n)` (`fin 0` is empty) -/
  | fz {n} : PFin2 (succ n)
  | /-- `n` as a member of `fin (succ n)` -/
  fs {n} : PFin2 n → PFin2 (succ n)
  deriving DecidableEq

def func: (i : Fin2 2) → Type u
  | Fin2.fz => PFin2 1
  | Fin2.fs Fin2.fz => PFin2 1

def sample1 : (x : Fin2 2) → (x_1 : func x) → Nat
  | Fin2.fz, x => 0
  | Fin2.fs y, x => 0

def sample2 : (x : Fin2 2) → (x_1 : func x) → Nat
  | Fin2.fz, x => 0
  | Fin2.fs y, x => 0

def ofFin2 : Fin2 n → PFin2 n
  | .fz   => .fz
  | .fs i => .fs <| ofFin2 i

def toFin2 : PFin2 n → Fin2 n
  | .fz   => .fz
  | .fs i => .fs <| toFin2 i

@[simp]
theorem ofFin2_toFin2_iso {i : Fin2 n} :
  (toFin2 <| ofFin2 i) = i :=
by
  induction i
  . rfl
  . simp [ofFin2, toFin2, *]

example : sample1 = sample2 := by {
  apply funext
  intro x
  apply funext
  rw [← (@ofFin2_toFin2_iso 2 x)]
  intro x_1
  -- fails with result is not type correct error
  -- cases (ofFin2 x)
}

Assistance would really help, thanks!

[Kevin Buzzard]

Does

  generalize ofFin2 x = g at *
  cases g

do what you're looking for?

[Arnav Sabharwal]

Yes, thank you!

[Arnav Sabharwal]

What are we doing differently when mentioned substitution is made? A clarification would really help in reasoning about future issues of this form, thanks!

[Kevin Buzzard]

If I have some number n in a proof, and then can I suddenly decide to do induction on n^2+3? I'm not really entirely sure what this means. Is the inductive step supposed to be something like "if it's true when n^2+3=7 then it's true for n^2+3=8"? But n^2+3 can't ever be 8. Similarly, "it's true for n^2+3=6" is a vacuous statement so can't possibly help for the case n^2+3=7.

I feel like what you're doing here is a bit similar. You are trying to do induction on something which isn't a bare variable. Sure you can split into cases for ofFin2 x but that's not really doing induction on something (which is what cases is doing under the hood).