Theorem: Pos.toInd_ofInd (GMLInit/Data/Pos.lean)

State before:
n : Pos.asInd
⊢ (Pos.ofInd n).toInd = n
Tactic:
induction n with
| one => rfl
| succ n ih =>
  rw [ofInd_succ]
  rw [toInd_succ]
  rw [ih]
State after:
no goals

State before:
case one

⊢ (Pos.ofInd asInd.one).toInd = asInd.one
Tactic:
rfl
State after:
no goals

State before:
case succ
n : Pos.asInd
ih : (Pos.ofInd n).toInd = n
⊢ (Pos.ofInd n.succ).toInd = n.succ
Tactic:
rw [ofInd_succ]
State after:
case succ
n : Pos.asInd
ih : (Pos.ofInd n).toInd = n
⊢ (Pos.ofInd n + 1).toInd = n.succ

State before:
case succ
n : Pos.asInd
ih : (Pos.ofInd n).toInd = n
⊢ (Pos.ofInd n + 1).toInd = n.succ
Tactic:
rw [toInd_succ]
State after:
case succ
n : Pos.asInd
ih : (Pos.ofInd n).toInd = n
⊢ (Pos.ofInd n).toInd.succ = n.succ

State before:
case succ
n : Pos.asInd
ih : (Pos.ofInd n).toInd = n
⊢ (Pos.ofInd n).toInd.succ = n.succ
Tactic:
rw [ih]
State after:
no goals