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

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

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

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

State before:
case inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rcases lt_or_le (castSucc k) i with (hik | hik)
State after:
case inl.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : k.castSucc < i
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)

case inl.inr
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : i ≤ k.castSucc
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)

State before:
case inl.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : k.castSucc < i
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
have H := (castSucc_lt_iff_succ_le.mp
(castSucc_lt_castSucc_iff.mpr hik)).trans_lt hij
State after:
case inl.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : k.castSucc < i
H : k.castSucc.succ < j
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)

State before:
case inl.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : k.castSucc < i
H : k.castSucc.succ < j
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rw [succAbove_of_castSucc_lt _ _ hik, succAbove_of_succ_le _ _ H.le,
succAbove_of_castSucc_lt _ k ((lt_pred_iff _).mpr H), succAbove_castSucc_of_lt _ _ hik]
State after:
no goals

State before:
case inl.inr
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : i ≤ k.castSucc
⊢ i.castSucc.succAbove ((j.pred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rw [succAbove_of_le_castSucc _ _ hik,
succAbove_castSucc_of_le, ← succ_succAbove_succ, succ_pred]
State after:
case inl.inr.h
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : i ≤ k.castSucc
⊢ i ≤ (j.pred ⋯).succAbove k

State before:
case inl.inr.h
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : i.castSucc < j
hik : i ≤ k.castSucc
⊢ i ≤ (j.pred ⋯).succAbove k
Tactic:
exact hik.trans (castSucc_le_succAbove _ _)
State after:
no goals

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

State before:
case inr
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rcases lt_or_le i (succ k) with (hik | hik)
State after:
case inr.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : i < k.succ
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)

case inr.inr
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : k.succ ≤ i
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)

State before:
case inr.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : i < k.succ
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
have H := ((hij.trans_lt (castSucc_lt_castSucc_iff.mpr hik)))
State after:
case inr.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : i < k.succ
H : j < k.succ.castSucc
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)

State before:
case inr.inl
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : i < k.succ
H : j < k.succ.castSucc
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rw [succAbove_of_lt_succ _ _ hik, succAbove_of_le_castSucc _ _ H.le,
succAbove_of_lt_succ _ k ((castPred_lt_iff _).mpr H), succAbove_succ_of_lt _ _ hik]
State after:
no goals

State before:
case inr.inr
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : k.succ ≤ i
⊢ i.succ.succAbove ((j.castPred ⋯).succAbove k) = j.succAbove (i.succAbove k)
Tactic:
rw [succAbove_of_succ_le _ _ hik, succAbove_succ_of_le,
← castSucc_succAbove_castSucc, castSucc_castPred]
State after:
case inr.inr.h
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : k.succ ≤ i
⊢ (j.castPred ⋯).succAbove k ≤ i

State before:
case inr.inr.h
m : ℕ
i : Fin (m + 1)
k : Fin m
j : Fin (m + 2)
hij : j ≤ i.castSucc
hik : k.succ ≤ i
⊢ (j.castPred ⋯).succAbove k ≤ i
Tactic:
exact (succAbove_le_succ _ _).trans hik
State after:
no goals