Theorem: Fin.succAbove_succAbove_predAbove (Controlbits/Fin.lean)

State before:
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
⊢ (j.succAbove i).succAbove (i.predAbove j) = j
Tactic:
rcases lt_or_le (castSucc i) j with (h | h)
State after:
case inl
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : i.castSucc < j
⊢ (j.succAbove i).succAbove (i.predAbove j) = j

case inr
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : j ≤ i.castSucc
⊢ (j.succAbove i).succAbove (i.predAbove j) = j

State before:
case inl
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : i.castSucc < j
⊢ (j.succAbove i).succAbove (i.predAbove j) = j
Tactic:
rw [succAbove_of_castSucc_lt _ _ h, predAbove_of_castSucc_lt _ _ h,
succAbove_castSucc_of_le, succ_pred]
State after:
case inl.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : i.castSucc < j
⊢ i ≤ j.pred ⋯

State before:
case inl.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : i.castSucc < j
⊢ i ≤ j.pred ⋯
Tactic:
rw [le_pred_iff, ← castSucc_lt_iff_succ_le]
State after:
case inl.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : i.castSucc < j
⊢ i.castSucc < j

State before:
case inl.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : i.castSucc < j
⊢ i.castSucc < j
Tactic:
exact h
State after:
no goals

State before:
case inr
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : j ≤ i.castSucc
⊢ (j.succAbove i).succAbove (i.predAbove j) = j
Tactic:
rw [succAbove_of_le_castSucc _ _ h, predAbove_of_le_castSucc _ _ h,
succAbove_succ_of_le, castSucc_castPred]
State after:
case inr.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : j ≤ i.castSucc
⊢ j.castPred ⋯ ≤ i

State before:
case inr.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : j ≤ i.castSucc
⊢ j.castPred ⋯ ≤ i
Tactic:
rw [castPred_le_iff]
State after:
case inr.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : j ≤ i.castSucc
⊢ j ≤ i.castSucc

State before:
case inr.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : j ≤ i.castSucc
⊢ j ≤ i.castSucc
Tactic:
exact h
State after:
no goals