Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

Tactic:
<;>

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