-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat} :
    (zipWithAll f as bs)[i]? = match as[i]?, bs[i]? with
      | none, none => .none | a?, b? => some (f a? b?)

Proof state:
case nil.cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
b : β
bs : List β
bih :
  ∀ {i : Nat},
    (zipWithAll f [] bs)[i]? =
      match [][i]?, bs[i]? with
      | none, none => none
      | a?, b? => some (f a? b?)
i : Nat
⊢ (zipWithAll f [] (b :: bs))[i]? =
    match [][i]?, (b :: bs)[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

Tactic:
cases i <;> simp_all

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
a : α
as : List α
aih :
  ∀ {bs : List β} {i : Nat},
    (zipWithAll f as bs)[i]? =
      match as[i]?, bs[i]? with
      | none, none => none
      | a?, b? => some (f a? b?)
i : Nat
b : β
bs : List β
⊢ (zipWithAll f (a :: as) (b :: bs))[i]? =
    match (a :: as)[i]?, (b :: bs)[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

Tactic:
cases i <;> simp_all

Result:
no goals

Proof state:
case nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
i : Nat
⊢ (zipWithAll f [] [])[i]? =
    match [][i]?, [][i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

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
⊢ (zipWithAll f as bs)[i]? =
    match as[i]?, bs[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

Tactic:
induction as generalizing bs i with
| nil => induction bs generalizing i with
  | nil => simp
  | cons b bs bih => cases i <;> simp_all
| cons a as aih => cases bs with
  | nil =>
    specialize @aih []
    cases i <;> simp_all
  | cons b bs => cases i <;> simp_all

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
a : α
as : List α
i : Nat
aih :
  ∀ {i : Nat},
    (zipWithAll f as [])[i]? =
      match as[i]?, [][i]? with
      | none, none => none
      | a?, b? => some (f a? b?)
⊢ (zipWithAll f (a :: as) [])[i]? =
    match (a :: as)[i]?, [][i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

Tactic:
cases i <;> simp_all

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
a : α
as : List α
aih :
  ∀ {bs : List β} {i : Nat},
    (zipWithAll f as bs)[i]? =
      match as[i]?, bs[i]? with
      | none, none => none
      | a?, b? => some (f a? b?)
i : Nat
⊢ (zipWithAll f (a :: as) [])[i]? =
    match (a :: as)[i]?, [][i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

Tactic:
specialize @aih []

Result:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
a : α
as : List α
i : Nat
aih :
  ∀ {i : Nat},
    (zipWithAll f as [])[i]? =
      match as[i]?, [][i]? with
      | none, none => none
      | a?, b? => some (f a? b?)
⊢ (zipWithAll f (a :: as) [])[i]? =
    match (a :: as)[i]?, [][i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
bs : List β
i : Nat
⊢ (zipWithAll f [] bs)[i]? =
    match [][i]?, bs[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

Tactic:
induction bs generalizing i with
| nil => simp
| cons b bs bih => cases i <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
a : α
as : List α
aih :
  ∀ {bs : List β} {i : Nat},
    (zipWithAll f as bs)[i]? =
      match as[i]?, bs[i]? with
      | none, none => none
      | a?, b? => some (f a? b?)
bs : List β
i : Nat
⊢ (zipWithAll f (a :: as) bs)[i]? =
    match (a :: as)[i]?, bs[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

Tactic:
cases bs with
| nil =>
specialize @aih []
cases i <;> simp_all
| cons b bs => cases i <;> simp_all

Result:
no goals