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

case mk.mk.inl.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁ : { val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) }
h₂ : ¬{ val := p, isLt := (_ : p < Nat.succ n) } < { val := i, isLt := (_ : i < Nat.succ n) }
⊢ castLT { val := i, isLt := (_ : i < Nat.succ n) } (_ : ↑{ val := i, isLt := (_ : i < Nat.succ n) } < n) =
    { val := i, isLt := isLt✝ }

case mk.mk.inr.inl
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁ : ¬{ val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) }
h₃ : { val := p, isLt := (_ : p < Nat.succ n) } < { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
⊢ pred { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
      (_ : { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } ≠ 0) =
    { val := i, isLt := isLt✝ }

case mk.mk.inr.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁ : ¬{ val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) }
h₃ : ¬{ val := p, isLt := (_ : p < Nat.succ n) } < { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
⊢ castLT { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
      (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } < n) =
    { val := i, isLt := isLt✝ }
case mk.mk
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
⊢ (if h :
        { val := p, isLt := (_ : p < Nat.succ n) } <
          if { val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) } then
            { val := i, isLt := (_ : i < Nat.succ n) }
          else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } then
      pred
        (if { val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) } then
          { val := i, isLt := (_ : i < Nat.succ n) }
        else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) })
        (_ :
          (if { val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) } then
              { val := i, isLt := (_ : i < Nat.succ n) }
            else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }) ≠
            0)
    else
      castLT
        (if { val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) } then
          { val := i, isLt := (_ : i < Nat.succ n) }
        else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) })
        (_ :
          ↑(if { val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) } then
                { val := i, isLt := (_ : i < Nat.succ n) }
              else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }) <
            n)) =
    { val := i, isLt := isLt✝ }
split_ifs with h₁ h₂ h₃
case mk.mk.inl.inl
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁✝ : { val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) }
h₂✝ : { val := p, isLt := (_ : p < Nat.succ n) } < { val := i, isLt := (_ : i < Nat.succ n) }
h₁ : i < p
h₂ : p < i
⊢ pred { val := i, isLt := (_ : i < Nat.succ n) } (_ : { val := i, isLt := (_ : i < Nat.succ n) } ≠ 0) =
    { val := i, isLt := isLt✝ }
case mk.mk.inl.inl
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁ : { val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) }
h₂ : { val := p, isLt := (_ : p < Nat.succ n) } < { val := i, isLt := (_ : i < Nat.succ n) }
⊢ pred { val := i, isLt := (_ : i < Nat.succ n) } (_ : { val := i, isLt := (_ : i < Nat.succ n) } ≠ 0) =
    { val := i, isLt := isLt✝ }
simp only [← val_fin_lt, not_lt] at h₁ h₂
no goals
case mk.mk.inl.inl
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁✝ : { val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) }
h₂✝ : { val := p, isLt := (_ : p < Nat.succ n) } < { val := i, isLt := (_ : i < Nat.succ n) }
h₁ : i < p
h₂ : p < i
⊢ pred { val := i, isLt := (_ : i < Nat.succ n) } (_ : { val := i, isLt := (_ : i < Nat.succ n) } ≠ 0) =
    { val := i, isLt := isLt✝ }
exact (lt_le_antisymm h₁ (le_of_lt h₂)).elim
no goals
case mk.mk.inl.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁ : { val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) }
h₂ : ¬{ val := p, isLt := (_ : p < Nat.succ n) } < { val := i, isLt := (_ : i < Nat.succ n) }
⊢ castLT { val := i, isLt := (_ : i < Nat.succ n) } (_ : ↑{ val := i, isLt := (_ : i < Nat.succ n) } < n) =
    { val := i, isLt := isLt✝ }
rfl
no goals
case mk.mk.inr.inl
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁ : ¬{ val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) }
h₃ : { val := p, isLt := (_ : p < Nat.succ n) } < { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
⊢ pred { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
      (_ : { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } ≠ 0) =
    { val := i, isLt := isLt✝ }
rfl
case mk.mk.inr.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁✝ : ¬{ val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) }
h₃✝ : ¬{ val := p, isLt := (_ : p < Nat.succ n) } < { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
h₁ : p ≤ i
h₃ : i + 1 ≤ p
⊢ castLT { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
      (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } < n) =
    { val := i, isLt := isLt✝ }
case mk.mk.inr.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁ : ¬{ val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) }
h₃ : ¬{ val := p, isLt := (_ : p < Nat.succ n) } < { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
⊢ castLT { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
      (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } < n) =
    { val := i, isLt := isLt✝ }
simp only [← val_fin_lt, not_lt] at h₁ h₃
no goals
case mk.mk.inr.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁✝ : ¬{ val := i, isLt := (_ : i < Nat.succ n) } < { val := p, isLt := (_ : p < Nat.succ n) }
h₃✝ : ¬{ val := p, isLt := (_ : p < Nat.succ n) } < { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
h₁ : p ≤ i
h₃ : i + 1 ≤ p
⊢ castLT { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
      (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } < n) =
    { val := i, isLt := isLt✝ }
contradiction