Theorem: Array.ofFn_go_zero (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
f : Fin 0 → α
i : Nat
acc : Array α
⊢ ofFn.go f i acc = acc
Tactic:
unfold ofFn.go
State after:
α : Type u
f : Fin 0 → α
i : Nat
acc : Array α
⊢ (if h : i < 0 then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) = acc

State before:
α : Type u
f : Fin 0 → α
i : Nat
acc : Array α
⊢ (if h : i < 0 then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) = acc
Tactic:
exact dif_neg i.not_lt_zero
State after:
no goals