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

State before:
n✝ n : Nat
i : Fin n
⊢ i.iotaFind.val = i
Tactic:
induction n with
| zero => cases i; contradiction
| succ n H =>
  match i with
  | ⟨0,_⟩ => rfl
  | ⟨i+1,hi⟩ =>
    apply Fin.eq
    open List.Index in rw [iotaFind, val_tail, val_map, H, Fin.succ]
State after:
no goals

State before:
case zero
n : Nat
i : Fin 0
⊢ i.iotaFind.val = i
Tactic:
cases i
State after:
case zero.mk
n val✝ : Nat
isLt✝ : val✝ < 0
⊢ ⟨val✝, isLt✝⟩.iotaFind.val = ⟨val✝, isLt✝⟩

State before:
case zero.mk
n val✝ : Nat
isLt✝ : val✝ < 0
⊢ ⟨val✝, isLt✝⟩.iotaFind.val = ⟨val✝, isLt✝⟩
Tactic:
contradiction
State after:
no goals

State before:
case succ
n✝ n : Nat
H : ∀ (i : Fin n), i.iotaFind.val = i
i : Fin (n + 1)
⊢ i.iotaFind.val = i
Tactic:
match i with
| ⟨0,_⟩ => rfl
| ⟨i+1,hi⟩ =>
  apply Fin.eq
  open List.Index in rw [iotaFind, val_tail, val_map, H, Fin.succ]
State after:
no goals

State before:
n✝ n : Nat
H : ∀ (i : Fin n), i.iotaFind.val = i
i : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ⟨0, isLt✝⟩.iotaFind.val = ⟨0, isLt✝⟩
Tactic:
rfl
State after:
no goals

State before:
n✝ n : Nat
H : ∀ (i : Fin n), i.iotaFind.val = i
i✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
⊢ ⟨i + 1, hi⟩.iotaFind.val = ⟨i + 1, hi⟩
Tactic:
apply Fin.eq
State after:
case a
n✝ n : Nat
H : ∀ (i : Fin n), i.iotaFind.val = i
i✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
⊢ ↑⟨i + 1, hi⟩.iotaFind.val = ↑⟨i + 1, hi⟩

State before:
case a
n✝ n : Nat
H : ∀ (i : Fin n), i.iotaFind.val = i
i✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
⊢ ↑⟨i + 1, hi⟩.iotaFind.val = ↑⟨i + 1, hi⟩
Tactic:
open List.Index in rw [iotaFind, val_tail, val_map, H, Fin.succ]
State after:
no goals

State before:
case a
n✝ n : Nat
H : ∀ (i : Fin n), i.iotaFind.val = i
i✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
⊢ ↑⟨i + 1, hi⟩.iotaFind.val = ↑⟨i + 1, hi⟩
Tactic:
rw [iotaFind, val_tail, val_map, H, Fin.succ]
State after:
no goals