-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Iterate.lean
theorem hIterateFrom_elim {P : Nat → Sort _}(Q : ∀(i : Nat), P i → Prop)
    {n  : Nat}
    (f : ∀(i : Fin n), P i.val → P (i.val+1))
    {i : Nat} (ubnd : i ≤ n)
    (s : P i)
    (init : Q i s)
    (step : ∀(k : Fin n) (s : P k.val), Q k.val s → Q (k.val+1) (f k s)) :
    Q n (hIterateFrom P f i ubnd s)

Proof state:
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
j : Nat
p : i + j = n
⊢ Q n (hIterateFrom P f i ubnd s)

Tactic:
induction j generalizing i ubnd init with
| zero =>
  unfold hIterateFrom
  have g : ¬ (i < n) := by simp at p; simp [p]
  have r : Q n (_root_.cast (congrArg P p) s) :=
    @Eq.rec Nat i (fun k eq => Q k (_root_.cast (congrArg P eq) s)) init n p
  simp only [g, r, dite_false]
| succ j inv =>
  unfold hIterateFrom
  have d : Nat.succ i + j = n := by simp [Nat.succ_add]; exact p
  have g : i < n := Nat.le.intro d
  simp only [g]
  exact inv _ _ (step ⟨i,g⟩ s init) d

Result:
no goals

Proof state:
case zero
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + 0 = n
g : ¬i < n
r : Q n (cast ⋯ s)
⊢ Q n
    (if g : i < n then hIterateFrom P f (i + 1) g (f ⟨i, g⟩ s)
    else
      let_fun p := ⋯;
      cast ⋯ s)

Tactic:
simp only [g, r, dite_false]

Result:
no goals

Proof state:
case succ
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
j : Nat
inv : ∀ {i : Nat} (ubnd : i ≤ n) (s : P i), Q i s → i + j = n → Q n (hIterateFrom P f i ubnd s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + (j + 1) = n
⊢ Q n
    (if g : i < n then hIterateFrom P f (i + 1) g (f ⟨i, g⟩ s)
    else
      let_fun p := ⋯;
      cast ⋯ s)

Tactic:
have d : Nat.succ i + j = n := by simp [Nat.succ_add]; exact p

Result:
case succ
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
j : Nat
inv : ∀ {i : Nat} (ubnd : i ≤ n) (s : P i), Q i s → i + j = n → Q n (hIterateFrom P f i ubnd s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + (j + 1) = n
d : i.succ + j = n
⊢ Q n
    (if g : i < n then hIterateFrom P f (i + 1) g (f ⟨i, g⟩ s)
    else
      let_fun p := ⋯;
      cast ⋯ s)

Proof state:
case succ
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
j : Nat
inv : ∀ {i : Nat} (ubnd : i ≤ n) (s : P i), Q i s → i + j = n → Q n (hIterateFrom P f i ubnd s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + (j + 1) = n
d : i.succ + j = n
g : i < n
⊢ Q n (if h : True then hIterateFrom P f (i + 1) ⋯ (f ⟨i, ⋯⟩ s) else cast ⋯ s)

Tactic:
exact inv _ _ (step ⟨i,g⟩ s init) d

Result:
no goals

Proof state:
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
⊢ Q n (hIterateFrom P f i ubnd s)

Tactic:
let ⟨j, p⟩ := Nat.le.dest ubnd

Result:
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
j : Nat
p : i + j = n
⊢ Q n (hIterateFrom P f i ubnd s)