Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
⊢ (if (if ↑k < if ↑j < ↑i then ↑i - 1 else ↑i then ↑k else ↑k + 1) < if ↑j < ↑i then ↑j else ↑j + 1 then
      if ↑k < if ↑j < ↑i then ↑i - 1 else ↑i then ↑k else ↑k + 1
    else (if ↑k < if ↑j < ↑i then ↑i - 1 else ↑i then ↑k else ↑k + 1) + 1) =
    if (if ↑k < ↑j then ↑k else ↑k + 1) < ↑i then if ↑k < ↑j then ↑k else ↑k + 1
    else (if ↑k < ↑j then ↑k else ↑k + 1) + 1

Tactic:
split_ifs

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ↑j < ↑i
h✝² : ↑k < ↑i - 1
h✝¹ : ↑k < ↑j
h✝ : ↑k < ↑i
⊢ ↑k = ↑k

case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ↑j < ↑i
h✝² : ↑k < ↑i - 1
h✝¹ : ↑k < ↑j
h✝ : ¬↑k < ↑i
⊢ ↑k = ↑k + 1

case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ↑j < ↑i
h✝² : ↑k < ↑i - 1
h✝¹ : ¬↑k < ↑j
h✝ : ↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1

case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ↑j < ↑i
h✝² : ↑k < ↑i - 1
h✝¹ : ¬↑k < ↑j
h✝ : ¬↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1 + 1

case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ↑k + 1 < ↑j
h✝¹ : ↑k < ↑j
h✝ : ↑k < ↑i
⊢ ↑k + 1 = ↑k

case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ↑k + 1 < ↑j
h✝¹ : ↑k < ↑j
h✝ : ¬↑k < ↑i
⊢ ↑k + 1 = ↑k + 1

case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ↑k + 1 < ↑j
h✝¹ : ¬↑k < ↑j
h✝ : ↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1

case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ↑k + 1 < ↑j
h✝¹ : ¬↑k < ↑j
h✝ : ¬↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1 + 1

case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ¬↑k + 1 < ↑j
h✝¹ : ↑k < ↑j
h✝ : ↑k < ↑i
⊢ ↑k + 1 + 1 = ↑k

case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ¬↑k + 1 < ↑j
h✝¹ : ↑k < ↑j
h✝ : ¬↑k < ↑i
⊢ ↑k + 1 + 1 = ↑k + 1

case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ¬↑k + 1 < ↑j
h✝¹ : ¬↑k < ↑j
h✝ : ↑k + 1 < ↑i
⊢ ↑k + 1 + 1 = ↑k + 1

case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ¬↑k + 1 < ↑j
h✝¹ : ¬↑k < ↑j
h✝ : ¬↑k + 1 < ↑i
⊢ ↑k + 1 + 1 = ↑k + 1 + 1

case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ¬↑j < ↑i
h✝² : ↑k < ↑i
h✝¹ : ↑k < ↑j + 1
h✝ : ↑k < ↑j
⊢ ↑k = ↑k

case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ↑k < ↑i
h✝² : ↑k < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ↑k + 1 < ↑i
⊢ ↑k = ↑k + 1

case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ↑k < ↑i
h✝² : ↑k < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ¬↑k + 1 < ↑i
⊢ ↑k = ↑k + 1 + 1

case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ¬↑j < ↑i
h✝² : ↑k < ↑i
h✝¹ : ¬↑k < ↑j + 1
h✝ : ↑k < ↑j
⊢ ↑k + 1 = ↑k

case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ↑k < ↑i
h✝² : ¬↑k < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1

case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ↑k < ↑i
h✝² : ¬↑k < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ¬↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1 + 1

case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ¬↑j < ↑i
h✝² : ¬↑k < ↑i
h✝¹ : ↑k + 1 < ↑j + 1
h✝ : ↑k < ↑j
⊢ ↑k + 1 = ↑k + 1

case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ¬↑k < ↑i
h✝² : ↑k + 1 < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1

case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ¬↑k < ↑i
h✝² : ↑k + 1 < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ¬↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1 + 1

case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ¬↑j < ↑i
h✝² : ¬↑k < ↑i
h✝¹ : ¬↑k + 1 < ↑j + 1
h✝ : ↑k < ↑j
⊢ ↑k + 1 + 1 = ↑k + 1

case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ¬↑k < ↑i
h✝² : ¬↑k + 1 < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ↑k + 1 < ↑i
⊢ ↑k + 1 + 1 = ↑k + 1

case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ¬↑k < ↑i
h✝² : ¬↑k + 1 < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ¬↑k + 1 < ↑i
⊢ ↑k + 1 + 1 = ↑k + 1 + 1