Theorem: Fin.iotaFind_succ (GMLInit/Data/Fin/Basic.lean)

State before:
n✝ n : Nat
i : Fin n
⊢ i.succ.iotaFind = (List.Index.map succ i.iotaFind).tail
Tactic:
cases i
State after:
case mk
n✝ n val✝ : Nat
isLt✝ : val✝ < n
⊢ ⟨val✝, isLt✝⟩.succ.iotaFind = (List.Index.map succ ⟨val✝, isLt✝⟩.iotaFind).tail

State before:
case mk
n✝ n val✝ : Nat
isLt✝ : val✝ < n
⊢ ⟨val✝, isLt✝⟩.succ.iotaFind = (List.Index.map succ ⟨val✝, isLt✝⟩.iotaFind).tail
Tactic:
rfl
State after:
no goals