rw [dif_neg n.lt_irrefl]
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ push acc (f { val := n, isLt := (_ : n < Nat.succ n) }) =
    push
      (if h : n < n then
        if h_1 : n + 1 < n then
          if h_2 : n + 1 + 1 < n then
            ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1 + 1 + 1)
              (push
                (push
                  (push acc
                    (f
                      { val := ↑{ val := n, isLt := (_ : n < n) },
                        isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) }))
                  (f
                    { val := ↑{ val := n + 1, isLt := (_ : n + 1 < n) },
                      isLt := (_ : ↑{ val := n + 1, isLt := (_ : n + 1 < n) } < Nat.succ n) }))
                (f
                  { val := ↑{ val := n + 1 + 1, isLt := h_2 },
                    isLt := (_ : ↑{ val := n + 1 + 1, isLt := h_2 } < Nat.succ n) }))
          else
            push
              (push acc
                (f
                  { val := ↑{ val := n, isLt := (_ : n < n) },
                    isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) }))
              (f
                { val := ↑{ val := n + 1, isLt := (_ : n + 1 < n) },
                  isLt := (_ : ↑{ val := n + 1, isLt := (_ : n + 1 < n) } < Nat.succ n) })
        else
          push acc
            (f
              { val := ↑{ val := n, isLt := (_ : n < n) },
                isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) })
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
no goals