-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
    Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray

Proof state:
case cons.zero
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
⊢ (if p a = true then r ++ (a :: takeWhile p l).toArray else r) =
    r ++ (if p a = true then a :: takeWhile p l else []).toArray

Tactic:
split <;> simp

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
i : Nat
⊢ (if h : i + 1 < (a :: l).toArray.size then
      let a_1 := (a :: l).toArray[i + 1];
      if p a_1 = true then takeWhile.go p (a :: l).toArray (i + 1 + 1) (r.push a_1) else r
    else r) =
    r ++ (takeWhile p (drop (i + 1) (a :: l))).toArray

Tactic:
simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
  getElem_toArray, getElem_cons_succ, drop_succ_cons]

Result:
case cons.succ
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
i : Nat
⊢ (if h : i < l.length then if p l[i] = true then takeWhile.go p (a :: l).toArray (i + 1 + 1) (r.push l[i]) else r
    else r) =
    r ++ (takeWhile p (drop i l)).toArray

Proof state:
case cons.succ.isTrue
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
i : Nat
h₁ : i < l.length
⊢ (if p l[i] = true then takeWhile.go p (a :: l).toArray (i + 1 + 1) (r.push l[i]) else r) =
    r ++ (takeWhile p (drop i l)).toArray

Tactic:
rw [takeWhile_go_succ, ih]

Result:
case cons.succ.isTrue
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
i : Nat
h₁ : i < l.length
⊢ (if p l[i] = true then r.push l[i] ++ (takeWhile p (drop (i + 1) l)).toArray else r) =
    r ++ (takeWhile p (drop i l)).toArray

Proof state:
case cons.zero
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
⊢ (if h : 0 < (a :: l).toArray.size then
      let a_1 := (a :: l).toArray[0];
      if p a_1 = true then takeWhile.go p (a :: l).toArray (0 + 1) (r.push a_1) else r
    else r) =
    r ++ (takeWhile p (drop 0 (a :: l))).toArray

Tactic:
simp [takeWhile_go_succ, ih, takeWhile_cons]

Result:
case cons.zero
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
⊢ (if p a = true then r ++ (a :: takeWhile p l).toArray else r) =
    r ++ (if p a = true then a :: takeWhile p l else []).toArray

Proof state:
case cons.succ.isTrue
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
i : Nat
h₁ : i < l.length
⊢ (if p l[i] = true then r.push l[i] ++ (takeWhile p (drop (i + 1) l)).toArray else r) =
    r ++ (takeWhile p (drop i l)).toArray

Tactic:
rw [← getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons]

Result:
case cons.succ.isTrue
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
i : Nat
h₁ : i < l.length
⊢ (if p l[i] = true then r.push l[i] ++ (takeWhile p (drop (i + 1) l)).toArray else r) =
    r ++ (if p l[i] = true then l[i] :: takeWhile p (drop (i + 1) l) else []).toArray

Proof state:
case cons.succ.isFalse
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
i : Nat
h₁ : ¬i < l.length
⊢ r = r ++ (takeWhile p (drop i l)).toArray

Tactic:
simp_all [drop_eq_nil_of_le]

Result:
no goals

Proof state:
case cons.succ.isTrue
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
i : Nat
h₁ : i < l.length
⊢ (if p l[i] = true then r.push l[i] ++ (takeWhile p (drop (i + 1) l)).toArray else r) =
    r ++ (if p l[i] = true then l[i] :: takeWhile p (drop (i + 1) l) else []).toArray

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
i : Nat
⊢ takeWhile.go p (a :: l).toArray i r = r ++ (takeWhile p (drop i (a :: l))).toArray

Tactic:
rw [takeWhile.go]

Result:
case cons
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
i : Nat
⊢ (if h : i < (a :: l).toArray.size then
      let a_1 := (a :: l).toArray[i];
      if p a_1 = true then takeWhile.go p (a :: l).toArray (i + 1) (r.push a_1) else r
    else r) =
    r ++ (takeWhile p (drop i (a :: l))).toArray

Proof state:
case nil
α : Type u_1
p : α → Bool
r : Array α
i : Nat
⊢ takeWhile.go p #[] i r = r ++ (takeWhile p (drop i [])).toArray

Tactic:
simp [takeWhile.go]

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
i : Nat
⊢ (if h : i < l.length then if p l[i] = true then takeWhile.go p (a :: l).toArray (i + 1 + 1) (r.push l[i]) else r
    else r) =
    r ++ (takeWhile p (drop i l)).toArray

Tactic:
split <;> rename_i h₁

Result:
case cons.succ.isTrue
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
i : Nat
h₁ : i < l.length
⊢ (if p l[i] = true then takeWhile.go p (a :: l).toArray (i + 1 + 1) (r.push l[i]) else r) =
    r ++ (takeWhile p (drop i l)).toArray

case cons.succ.isFalse
α : Type u_1
p : α → Bool
a : α
l : List α
ih : ∀ {r : Array α} (i : Nat), takeWhile.go p l.toArray i r = r ++ (takeWhile p (drop i l)).toArray
r : Array α
i : Nat
h₁ : ¬i < l.length
⊢ r = r ++ (takeWhile p (drop i l)).toArray