-- 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:
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 ++ (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 ha : i < as.length then
  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]
else
  if hb : i < bs.length then
    simp only [Nat.not_lt] at ha
    rw [List.drop_eq_getElem_cons hb]
    rw [(drop_eq_nil_iff (l := as)).mpr (by omega), (drop_eq_nil_iff (l := as)).mpr (by omega)]
    simp only [nil_zipWithAll, map_drop, map_cons]
    rw [getElem?_eq_getElem hb]
    rw [getElem?_eq_none ha]
  else
    omega

Result:
no goals

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.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

Tactic:
simp only [getElem?_toArray, push_append_toArray]

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 ++ (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

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 (drop i as) (drop i bs)).toArray

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
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

Tactic:
simp only [zipWithAll_nil, map_drop, map_cons]

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]? :: drop (i + 1) (map (fun a => f (some a) none) as)).toArray =
    cs ++ (f (some as[i]) none :: drop (i + 1) (map (fun a => f (some a) none) as)).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]? :: drop (i + 1) (map (fun a => f (some a) none) as)).toArray =
    cs ++ (f (some as[i]) none :: drop (i + 1) (map (fun a => f (some a) none) as)).toArray

Tactic:
rw [getElem?_eq_getElem 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 (some as[i]) bs[i]? :: drop (i + 1) (map (fun a => f (some a) none) as)).toArray =
    cs ++ (f (some as[i]) none :: drop (i + 1) (map (fun a => f (some a) none) as)).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]? :: drop (i + 1) (map (fun b => f none (some b)) bs)).toArray =
    cs ++ (f none (some bs[i]) :: drop (i + 1) (map (fun b => f none (some b)) bs)).toArray

Tactic:
rw [getElem?_eq_getElem 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]? (some bs[i]) :: drop (i + 1) (map (fun b => f none (some b)) bs)).toArray =
    cs ++ (f none (some bs[i]) :: drop (i + 1) (map (fun b => f none (some b)) 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
hb : i < bs.length
ha : as.length ≤ i
⊢ as.length ≤ i + 1

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
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 (drop i as) (drop i bs)).toArray

Tactic:
simp only [Nat.not_lt] at 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
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

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
⊢ (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

Tactic:
rw [zipWithAll_go_toArray]

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
⊢ 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 γ
h : i < max as.length bs.length
hb : i < bs.length
ha : as.length ≤ i
⊢ as.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
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
  simp only [Nat.not_lt] at ha
  rw [List.drop_eq_getElem_cons hb]
  rw [(drop_eq_nil_iff (l := as)).mpr (by omega), (drop_eq_nil_iff (l := as)).mpr (by omega)]
  simp only [nil_zipWithAll, map_drop, map_cons]
  rw [getElem?_eq_getElem hb]
  rw [getElem?_eq_none ha]
else
  omega

Result:
no goals