-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → Option β → γ) (i : Nat) (cs : Array γ) :
    zipWithAll.go f as.toArray bs.toArray i cs = cs ++ (List.zipWithAll f (as.drop i) (bs.drop i)).toArray

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : i < max as.length bs.length
hb : i < bs.length
ha : as.length ≤ i
⊢ cs ++ (f as[i]? bs[i]? :: zipWithAll f (drop (i + 1) as) (drop (i + 1) bs)).toArray =
    cs ++ (zipWithAll f (drop i as) (drop i bs)).toArray

Tactic:
rw [List.drop_eq_getElem_cons hb]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : i < max as.length bs.length
hb : i < bs.length
ha : as.length ≤ i
⊢ cs ++ (f as[i]? bs[i]? :: zipWithAll f (drop (i + 1) as) (drop (i + 1) bs)).toArray =
    cs ++ (zipWithAll f (drop i as) (bs[i] :: drop (i + 1) bs)).toArray

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : max as.length bs.length ≤ i
⊢ bs.length ≤ i

Tactic:
omega

Result:
no goals

Proof state:
case isFalse
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : max as.length bs.length ≤ i
⊢ cs = cs ++ (zipWithAll f (drop i as) (drop i bs)).toArray

Tactic:
rw [drop_eq_nil_of_le (by omega), drop_eq_nil_of_le (by omega)]

Result:
case isFalse
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : max as.length bs.length ≤ i
⊢ cs = cs ++ (zipWithAll f [] []).toArray

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : i < max as.length bs.length
ha : i < as.length
hb : bs.length ≤ i
⊢ cs ++ (f as[i]? bs[i]? :: zipWithAll f (drop (i + 1) as) (drop (i + 1) bs)).toArray =
    cs ++ (zipWithAll f (drop i as) (drop i bs)).toArray

Tactic:
rw [List.drop_eq_getElem_cons ha]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : i < max as.length bs.length
ha : i < as.length
hb : bs.length ≤ i
⊢ cs ++ (f as[i]? bs[i]? :: zipWithAll f (drop (i + 1) as) (drop (i + 1) bs)).toArray =
    cs ++ (zipWithAll f (as[i] :: drop (i + 1) as) (drop i bs)).toArray

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : i < max as.length bs.length
ha : i < as.length
hb : bs.length ≤ i
⊢ bs.length ≤ i

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : i < max as.length bs.length
hb : i < bs.length
ha : as.length ≤ i
⊢ cs ++ (f as[i]? bs[i]? :: zipWithAll f (drop (i + 1) as) (drop (i + 1) bs)).toArray =
    cs ++ (zipWithAll f (drop i as) (bs[i] :: drop (i + 1) bs)).toArray

Tactic:
rw [(drop_eq_nil_iff (l := as)).mpr (by omega), (drop_eq_nil_iff (l := as)).mpr (by omega)]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : i < max as.length bs.length
hb : i < bs.length
ha : as.length ≤ i
⊢ cs ++ (f as[i]? bs[i]? :: zipWithAll f [] (drop (i + 1) bs)).toArray =
    cs ++ (zipWithAll f [] (bs[i] :: drop (i + 1) bs)).toArray

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : i < max as.length bs.length
ha : i < as.length
hb : i < bs.length
⊢ cs ++ (f as[i]? bs[i]? :: zipWithAll f (drop (i + 1) as) (drop (i + 1) bs)).toArray =
    cs ++ (zipWithAll f (as[i] :: drop (i + 1) as) (bs[i] :: drop (i + 1) bs)).toArray

Tactic:
simp only [ha, hb, getElem?_eq_getElem, zipWithAll_cons_cons]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : i < max as.length bs.length
ha : i < as.length
hb : bs.length ≤ i
⊢ cs ++ (f as[i]? bs[i]? :: zipWithAll f (drop (i + 1) as) (drop (i + 1) bs)).toArray =
    cs ++ (zipWithAll f (as[i] :: drop (i + 1) as) (drop i bs)).toArray

Tactic:
rw [(drop_eq_nil_iff (l := bs)).mpr (by omega), (drop_eq_nil_iff (l := bs)).mpr (by omega)]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : i < max as.length bs.length
ha : i < as.length
hb : bs.length ≤ i
⊢ cs ++ (f as[i]? bs[i]? :: zipWithAll f (drop (i + 1) as) []).toArray =
    cs ++ (zipWithAll f (as[i] :: drop (i + 1) as) []).toArray

Proof state:
case isTrue
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : i < max as.toArray.size bs.toArray.size
⊢ cs.push (f as.toArray[i]? bs.toArray[i]?) ++ (zipWithAll f (drop (i + 1) as) (drop (i + 1) bs)).toArray =
    cs ++ (zipWithAll f (drop i as) (drop i bs)).toArray

Tactic:
simp at h

Result:
case isTrue
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : i < max as.length bs.length
⊢ cs.push (f as.toArray[i]? bs.toArray[i]?) ++ (zipWithAll f (drop (i + 1) as) (drop (i + 1) bs)).toArray =
    cs ++ (zipWithAll f (drop i as) (drop i bs)).toArray

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
⊢ (if i < max as.toArray.size bs.toArray.size then
      let a := as.toArray[i]?;
      let b := bs.toArray[i]?;
      zipWithAll.go f as.toArray bs.toArray (i + 1) (cs.push (f a b))
    else cs) =
    cs ++ (zipWithAll f (drop i as) (drop i bs)).toArray

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : i < max as.toArray.size bs.toArray.size
⊢ (let a := as.toArray[i]?;
    let b := bs.toArray[i]?;
    zipWithAll.go f as.toArray bs.toArray (i + 1) (cs.push (f a b))) =
    cs ++ (zipWithAll f (drop i as) (drop i bs)).toArray

case isFalse
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : ¬i < max as.toArray.size bs.toArray.size
⊢ cs = cs ++ (zipWithAll f (drop i as) (drop i bs)).toArray

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : i < max as.length bs.length
ha : i < as.length
⊢ cs ++ (f as[i]? bs[i]? :: zipWithAll f (drop (i + 1) as) (drop (i + 1) bs)).toArray =
    cs ++ (zipWithAll f (drop i as) (drop i bs)).toArray

Tactic:
if hb : i < bs.length then
  rw [List.drop_eq_getElem_cons ha, List.drop_eq_getElem_cons hb]
  simp only [ha, hb, getElem?_eq_getElem, zipWithAll_cons_cons]
else
  simp only [Nat.not_lt] at hb
  rw [List.drop_eq_getElem_cons ha]
  rw [(drop_eq_nil_iff (l := bs)).mpr (by omega), (drop_eq_nil_iff (l := bs)).mpr (by omega)]
  simp only [zipWithAll_nil, map_drop, map_cons]
  rw [getElem?_eq_getElem ha]
  rw [getElem?_eq_none hb]

Result:
no goals

Proof state:
case isFalse
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : ¬i < max as.toArray.size bs.toArray.size
⊢ cs = cs ++ (zipWithAll f (drop i as) (drop i bs)).toArray

Tactic:
simp only [size_toArray, Nat.not_lt] at h

Result:
case isFalse
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
i : Nat
cs : Array γ
h : max as.length bs.length ≤ i
⊢ cs = cs ++ (zipWithAll f (drop i as) (drop i bs)).toArray