n m : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ ↑castSucc p
⊢ (if ↑castSucc (if h : ↑castSucc p < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n)) < ↑castSucc p then
      ↑castSucc (if h : ↑castSucc p < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n))
    else succ (if h : ↑castSucc p < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n))) =
    i
n m : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ ↑castSucc p
⊢ ↑(succAbove (↑castSucc p)) (predAbove p i) = i
dsimp [predAbove, succAbove]
case mk
n m : ℕ
i : Fin (n + 1)
p : ℕ
isLt✝ : p < n
h : i ≠ ↑castSucc { val := p, isLt := isLt✝ }
⊢ (if
        ↑castSucc
            (if h : ↑castSucc { val := p, isLt := isLt✝ } < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n)) <
          ↑castSucc { val := p, isLt := isLt✝ } then
      ↑castSucc (if h : ↑castSucc { val := p, isLt := isLt✝ } < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n))
    else succ (if h : ↑castSucc { val := p, isLt := isLt✝ } < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n))) =
    i
n m : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ ↑castSucc p
⊢ (if ↑castSucc (if h : ↑castSucc p < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n)) < ↑castSucc p then
      ↑castSucc (if h : ↑castSucc p < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n))
    else succ (if h : ↑castSucc p < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n))) =
    i
rcases p with ⟨p, _⟩
case mk.mk
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
⊢ (if
        ↑castSucc
            (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
              pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
            else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
          ↑castSucc { val := p, isLt := isLt✝¹ } then
      ↑castSucc
        (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))
    else
      succ
        (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))) =
    { val := i, isLt := isLt✝ }
case mk
n m : ℕ
i : Fin (n + 1)
p : ℕ
isLt✝ : p < n
h : i ≠ ↑castSucc { val := p, isLt := isLt✝ }
⊢ (if
        ↑castSucc
            (if h : ↑castSucc { val := p, isLt := isLt✝ } < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n)) <
          ↑castSucc { val := p, isLt := isLt✝ } then
      ↑castSucc (if h : ↑castSucc { val := p, isLt := isLt✝ } < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n))
    else succ (if h : ↑castSucc { val := p, isLt := isLt✝ } < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n))) =
    i
rcases i with ⟨i, _⟩
case mk.mk.inl
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ (if
        ↑castSucc
            (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
              pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
            else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
          ↑castSucc { val := p, isLt := isLt✝¹ } then
      ↑castSucc
        (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))
    else
      succ
        (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))) =
    { val := i, isLt := isLt✝ }

case mk.mk.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ (if
        ↑castSucc
            (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
              pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
            else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
          ↑castSucc { val := p, isLt := isLt✝¹ } then
      ↑castSucc
        (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))
    else
      succ
        (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))) =
    { val := i, isLt := isLt✝ }
case mk.mk
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
⊢ (if
        ↑castSucc
            (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
              pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
            else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
          ↑castSucc { val := p, isLt := isLt✝¹ } then
      ↑castSucc
        (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))
    else
      succ
        (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))) =
    { val := i, isLt := isLt✝ }
cases' lt_or_le i p with H H
case mk.mk.inl
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ (if
        ↑castSucc (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
          ↑castSucc { val := p, isLt := isLt✝¹ } then
      ↑castSucc (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))
    else succ (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))) =
    { val := i, isLt := isLt✝ }

case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
case mk.mk.inl
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ (if
        ↑castSucc
            (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
              pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
            else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
          ↑castSucc { val := p, isLt := isLt✝¹ } then
      ↑castSucc
        (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))
    else
      succ
        (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))) =
    { val := i, isLt := isLt✝ }
rw [dif_neg]
case mk.mk.inl
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ↑castSucc (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) = { val := i, isLt := isLt✝ }

case mk.mk.inl.hc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ↑castSucc (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
    ↑castSucc { val := p, isLt := isLt✝¹ }

case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }

case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
case mk.mk.inl
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ (if
        ↑castSucc (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
          ↑castSucc { val := p, isLt := isLt✝¹ } then
      ↑castSucc (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))
    else succ (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))) =
    { val := i, isLt := isLt✝ }

case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
rw [if_pos]
case mk.mk.inl.hc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ↑castSucc (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
    ↑castSucc { val := p, isLt := isLt✝¹ }

case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }

case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
case mk.mk.inl
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ↑castSucc (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) = { val := i, isLt := isLt✝ }

case mk.mk.inl.hc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ↑castSucc (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
    ↑castSucc { val := p, isLt := isLt✝¹ }

case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }

case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
rfl
case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }

case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
case mk.mk.inl.hc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ↑castSucc (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
    ↑castSucc { val := p, isLt := isLt✝¹ }

case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }

case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
exact H
case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ i ≤ p
case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }

case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
simp
no goals
case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ i ≤ p
apply le_of_lt H
case mk.mk.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ (if
        ↑castSucc (pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)) <
          ↑castSucc { val := p, isLt := isLt✝¹ } then
      ↑castSucc (pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0))
    else succ (pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0))) =
    { val := i, isLt := isLt✝ }

case mk.mk.inr.hc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
case mk.mk.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ (if
        ↑castSucc
            (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
              pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
            else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
          ↑castSucc { val := p, isLt := isLt✝¹ } then
      ↑castSucc
        (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))
    else
      succ
        (if h : ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))) =
    { val := i, isLt := isLt✝ }
rw [dif_pos]
case mk.mk.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ succ (pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)) = { val := i, isLt := isLt✝ }

case mk.mk.inr.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ ¬↑castSucc (pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)) <
      ↑castSucc { val := p, isLt := isLt✝¹ }

case mk.mk.inr.hc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }

case mk.mk.inr.hc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
case mk.mk.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ (if
        ↑castSucc (pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)) <
          ↑castSucc { val := p, isLt := isLt✝¹ } then
      ↑castSucc (pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0))
    else succ (pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0))) =
    { val := i, isLt := isLt✝ }

case mk.mk.inr.hc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
rw [if_neg]
no goals
case mk.mk.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ succ (pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)) = { val := i, isLt := isLt✝ }
simp
case mk.mk.inr.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ ↑castSucc { val := p, isLt := isLt✝¹ } ≤ ↑castSucc { val := Nat.pred i, isLt := (_ : Nat.pred i < Nat.pred (n + 1)) }
case mk.mk.inr.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ ¬↑castSucc (pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)) <
      ↑castSucc { val := p, isLt := isLt✝¹ }
simp only [pred, Fin.mk_lt_mk, not_lt]
no goals
case mk.mk.inr.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ ↑castSucc { val := p, isLt := isLt✝¹ } ≤ ↑castSucc { val := Nat.pred i, isLt := (_ : Nat.pred i < Nat.pred (n + 1)) }
exact Nat.le_pred_of_lt (h.symm.lt_of_le H)
no goals
case mk.mk.inr.hc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ ↑castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ ↑castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
exact lt_of_le_of_ne H h.symm