-- 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) bs)).toArray =
    cs ++ (zipWithAll f [] (bs[i] :: drop (i + 1) bs)).toArray

Tactic:
simp only [nil_zipWithAll, 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
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

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:
rw [List.drop_eq_getElem_cons ha, 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
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

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
⊢ 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 γ
⊢ zipWithAll.go f as.toArray bs.toArray i cs = cs ++ (zipWithAll f (drop i as) (drop i bs)).toArray

Tactic:
unfold zipWithAll.go

Result:
α : 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

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

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

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 [] []).toArray

Tactic:
simp

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

Tactic:
rw [getElem?_eq_none hb]

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]? (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

Tactic:
rw [getElem?_eq_none ha]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
x✝ : (_ : Nat) ×' Array γ
a✝¹ :
  ∀ (y : (_ : Nat) ×' Array γ),
    (invImage (fun x => PSigma.casesOn x fun i cs => max as.length bs.length - i) instWellFoundedRelationOfSizeOf).1 y
        x✝ →
      zipWithAll.go f as.toArray bs.toArray y.1 y.2 = y.2 ++ (zipWithAll f (drop y.1 as) (drop y.1 bs)).toArray
i : Nat
cs : Array γ
a✝ :
  ∀ (y : (_ : Nat) ×' Array γ),
    (invImage (fun x => PSigma.casesOn x fun i cs => max as.length bs.length - i) instWellFoundedRelationOfSizeOf).1 y
        ⟨i, cs⟩ →
      zipWithAll.go f as.toArray bs.toArray y.1 y.2 = y.2 ++ (zipWithAll f (drop y.1 as) (drop y.1 bs)).toArray
h✝ : i < max as.toArray.size bs.toArray.size
⊢ max as.length bs.length - (i + 1) < max as.length bs.length - i

Tactic:
decreasing_trivial_pre_omega

Result:
no goals