n✝ m n : ℕ
C : Fin (n + 1) → Sort u_1
h0 : C (last n)
hs : (i : Fin n) → C (succ i) → C (↑castSucc i)
⊢ (if hi : last n = last n then _root_.cast (_ : C (last n) = C (last n)) h0
    else
      let j := { val := ↑(last n), isLt := (_ : ↑(last n) < n) };
      let_fun x := (_ : n - ↑(last n) < n + 1 - ↑(last n));
      let_fun hi := (_ : last n = ↑castSucc j);
      _root_.cast (_ : C (↑castSucc j) = C (last n)) (hs j (reverseInduction h0 hs (succ j)))) =
    h0
n✝ m n : ℕ
C : Fin (n + 1) → Sort u_1
h0 : C (last n)
hs : (i : Fin n) → C (succ i) → C (↑castSucc i)
⊢ reverseInduction h0 hs (last n) = h0
rw [reverseInduction]
no goals
n✝ m n : ℕ
C : Fin (n + 1) → Sort u_1
h0 : C (last n)
hs : (i : Fin n) → C (succ i) → C (↑castSucc i)
⊢ (if hi : last n = last n then _root_.cast (_ : C (last n) = C (last n)) h0
    else
      let j := { val := ↑(last n), isLt := (_ : ↑(last n) < n) };
      let_fun x := (_ : n - ↑(last n) < n + 1 - ↑(last n));
      let_fun hi := (_ : last n = ↑castSucc j);
      _root_.cast (_ : C (↑castSucc j) = C (last n)) (hs j (reverseInduction h0 hs (succ j)))) =
    h0
simp