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

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

State before:
case one

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

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

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

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