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

State before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
⊢ length (ofFn f) = n
Tactic:
dsimp [ofFn]
State after:
α : Type u
β : Type v
n : Nat
f : Fin n → α
⊢ length (Array.toList (Array.ofFn f)) = n

State before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
⊢ length (Array.toList (Array.ofFn f)) = n
Tactic:
rewrite [Array.toList_eq]
State after:
α : Type u
β : Type v
n : Nat
f : Fin n → α
⊢ length (Array.ofFn f).data = n

State before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
⊢ length (Array.ofFn f).data = n
Tactic:
show (Array.ofFn f).size = n
State after:
α : Type u
β : Type v
n : Nat
f : Fin n → α
⊢ Array.size (Array.ofFn f) = n

State before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
⊢ Array.size (Array.ofFn f) = n
Tactic:
exact Array.size_ofFn f
State after:
no goals