ι : Type ?u.93887
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l r : List α
i : ℕ
⊢ ∀ (h1 : i + 1 + length l < length (reverseAux (a :: l) r)) (h2 : i < length r),
    get (reverseAux (a :: l) r) { val := i + 1 + length l, isLt := h1 } = get r { val := i, isLt := h2 }
ι : Type ?u.93887
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l r : List α
i : ℕ
⊢ ∀ (h1 : i + length (a :: l) < length (reverseAux (a :: l) r)) (h2 : i < length r),
    get (reverseAux (a :: l) r) { val := i + length (a :: l), isLt := h1 } = get r { val := i, isLt := h2 }
rw [show i + length (a :: l) = i + 1 + length l from add_right_comm i (length l) 1]
no goals
ι : Type ?u.93887
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l r : List α
i : ℕ
⊢ ∀ (h1 : i + 1 + length l < length (reverseAux (a :: l) r)) (h2 : i < length r),
    get (reverseAux (a :: l) r) { val := i + 1 + length l, isLt := h1 } = get r { val := i, isLt := h2 }
exact fun h1 h2 => get_reverse_aux₁ l (a :: r) (i + 1) h1 (succ_lt_succ h2)