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