Theorem: List.get_ofFn (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Fin (length (ofFn f))
⊢ get (ofFn f) i = f (Fin.cast (_ : length (ofFn f) = n) i)
Tactic:
rcases i with ⟨i,hi⟩
State after:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi : i < length (ofFn f)
⊢ get (ofFn f) { val := i, isLt := hi } = f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi })

State before:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi : i < length (ofFn f)
⊢ get (ofFn f) { val := i, isLt := hi } = f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi })
Tactic:
dsimp [ofFn] at hi ⊢
State after:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi : i < length (Array.toList (Array.ofFn f))
⊢ get (Array.toList (Array.ofFn f)) { val := i, isLt := hi } =
    f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi })

State before:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi : i < length (Array.toList (Array.ofFn f))
⊢ get (Array.toList (Array.ofFn f)) { val := i, isLt := hi } =
    f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi })
Tactic:
simp only [get_of_eq (Array.toList_eq _), ← Array.getElem_eq_data_get]
State after:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi : i < length (Array.toList (Array.ofFn f))
⊢ (Array.ofFn f)[i] = f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi })

State before:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi : i < length (Array.toList (Array.ofFn f))
⊢ (Array.ofFn f)[i] = f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi })
Tactic:
conv at hi => rewrite [Array.toList_eq]
State after:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi✝ : i < length (Array.toList (Array.ofFn f))
hi : i < length (Array.ofFn f).data
⊢ (Array.ofFn f)[i] = f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi✝ })

State before:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi✝ : i < length (Array.toList (Array.ofFn f))
hi : i < length (Array.ofFn f).data
⊢ (Array.ofFn f)[i] = f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi✝ })
Tactic:
exact Array.getElem_ofFn f i hi
State after:
no goals