no goals
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
⊢ size (ofFn.go f i acc) = size acc + (n - i)
if hin : i < n then
  unfold ofFn.go
  have : 1 + (n - (i + 1)) = n - i :=
    Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
  rw [dif_pos hin, size_ofFn_go f (i+1), size_push, Nat.add_assoc, this]
else
  have : n - i = 0 := Nat.sub_eq_zero_of_le (Nat.le_of_not_lt hin)
  unfold ofFn.go
  simp [hin, this]
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : i < n
⊢ size (if h : i < n then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) = size acc + (n - i)
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : i < n
⊢ size (ofFn.go f i acc) = size acc + (n - i)
unfold ofFn.go
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : i < n
this : 1 + (n - (i + 1)) = n - i
⊢ size (if h : i < n then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) = size acc + (n - i)
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : i < n
⊢ size (if h : i < n then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) = size acc + (n - i)
have : 1 + (n - (i + 1)) = n - i :=
  Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
no goals
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : i < n
this : 1 + (n - (i + 1)) = n - i
⊢ size (if h : i < n then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) = size acc + (n - i)
rw [dif_pos hin, size_ofFn_go f (i+1), size_push, Nat.add_assoc, this]
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : ¬i < n
this : n - i = 0
⊢ size (ofFn.go f i acc) = size acc + (n - i)
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : ¬i < n
⊢ size (ofFn.go f i acc) = size acc + (n - i)
have : n - i = 0 := Nat.sub_eq_zero_of_le (Nat.le_of_not_lt hin)
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : ¬i < n
this : n - i = 0
⊢ size (if h : i < n then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) = size acc + (n - i)
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : ¬i < n
this : n - i = 0
⊢ size (ofFn.go f i acc) = size acc + (n - i)
unfold ofFn.go
no goals
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : ¬i < n
this : n - i = 0
⊢ size (if h : i < n then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) = size acc + (n - i)
simp [hin, this]