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

State before:
n✝ n : Nat
i : (Fin.iota n).Index
⊢ i.val.iotaFind = i
Tactic:
induction n with
| zero => contradiction
| succ n H =>
  match i with
  | .head => rfl
  | .tail (i : List.Index ((Fin.iota n).map Fin.succ)) =>
    calc
    _ = iotaFind (List.Index.val (.tail i : List.Index (Fin.iota (n+1)))) := rfl
    _ = iotaFind (List.Index.val i) := by rw [List.Index.val_tail]
    _ = iotaFind (List.Index.val (List.Index.map Fin.succ (List.Index.unmap Fin.succ i))) := by rw [List.Index.map_unmap]
    _ = iotaFind (Fin.succ (List.Index.val (List.Index.unmap Fin.succ i))) := by rw [List.Index.val_map]
    _ = .tail (List.Index.map Fin.succ (iotaFind (List.Index.val (List.Index.unmap Fin.succ i)))) := by rw [iotaFind_succ]
    _ = .tail (List.Index.map Fin.succ (List.Index.unmap Fin.succ i)) := by rw [H]
    _ = .tail i := by rw [List.Index.map_unmap]
State after:
no goals

State before:
case zero
n : Nat
i : (Fin.iota 0).Index
⊢ i.val.iotaFind = i
Tactic:
contradiction
State after:
no goals

State before:
case succ
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i : (Fin.iota (n + 1)).Index
⊢ i.val.iotaFind = i
Tactic:
match i with
| .head => rfl
| .tail (i : List.Index ((Fin.iota n).map Fin.succ)) =>
  calc
  _ = iotaFind (List.Index.val (.tail i : List.Index (Fin.iota (n+1)))) := rfl
  _ = iotaFind (List.Index.val i) := by rw [List.Index.val_tail]
  _ = iotaFind (List.Index.val (List.Index.map Fin.succ (List.Index.unmap Fin.succ i))) := by rw [List.Index.map_unmap]
  _ = iotaFind (Fin.succ (List.Index.val (List.Index.unmap Fin.succ i))) := by rw [List.Index.val_map]
  _ = .tail (List.Index.map Fin.succ (iotaFind (List.Index.val (List.Index.unmap Fin.succ i)))) := by rw [iotaFind_succ]
  _ = .tail (List.Index.map Fin.succ (List.Index.unmap Fin.succ i)) := by rw [H]
  _ = .tail i := by rw [List.Index.map_unmap]
State after:
no goals

State before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i : (Fin.iota (n + 1)).Index
⊢ List.Index.head.val.iotaFind = List.Index.head
Tactic:
rfl
State after:
no goals

State before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ i.tail.val.iotaFind = i.tail
Tactic:
calc
_ = iotaFind (List.Index.val (.tail i : List.Index (Fin.iota (n+1)))) := rfl
_ = iotaFind (List.Index.val i) := by rw [List.Index.val_tail]
_ = iotaFind (List.Index.val (List.Index.map Fin.succ (List.Index.unmap Fin.succ i))) := by rw [List.Index.map_unmap]
_ = iotaFind (Fin.succ (List.Index.val (List.Index.unmap Fin.succ i))) := by rw [List.Index.val_map]
_ = .tail (List.Index.map Fin.succ (iotaFind (List.Index.val (List.Index.unmap Fin.succ i)))) := by rw [iotaFind_succ]
_ = .tail (List.Index.map Fin.succ (List.Index.unmap Fin.succ i)) := by rw [H]
_ = .tail i := by rw [List.Index.map_unmap]
State after:
no goals

State before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ i.tail.val.iotaFind = i.val.iotaFind
Tactic:
rw [List.Index.val_tail]
State after:
no goals

State before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ i.val.iotaFind = (List.Index.map succ (List.Index.unmap succ i)).val.iotaFind
Tactic:
rw [List.Index.map_unmap]
State after:
no goals

State before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ (List.Index.map succ (List.Index.unmap succ i)).val.iotaFind = (List.Index.unmap succ i).val.succ.iotaFind
Tactic:
rw [List.Index.val_map]
State after:
no goals

State before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ (List.Index.unmap succ i).val.succ.iotaFind = (List.Index.map succ (List.Index.unmap succ i).val.iotaFind).tail
Tactic:
rw [iotaFind_succ]
State after:
no goals

State before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ (List.Index.map succ (List.Index.unmap succ i).val.iotaFind).tail =
    (List.Index.map succ (List.Index.unmap succ i)).tail
Tactic:
rw [H]
State after:
no goals

State before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ (List.Index.map succ (List.Index.unmap succ i)).tail = i.tail
Tactic:
rw [List.Index.map_unmap]
State after:
no goals