-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zipWith_append (f : α → β → γ)
    (l : Vector α n) (la : Vector α m) (l' : Vector β n) (lb : Vector β m) :
    zipWith f (l ++ la) (l' ++ lb) = zipWith f l l' ++ zipWith f la lb

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
m : Nat
f : α → β → γ
la : Vector α m
lb : Vector β m
l : Array α
l' : Array β
h : l'.size = l.size
⊢ zipWith f ({ toArray := l, size_toArray := ⋯ } ++ la) ({ toArray := l', size_toArray := h } ++ lb) =
    zipWith f { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h } ++ zipWith f la lb

Tactic:
rcases la with ⟨la, rfl⟩

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : Array α
l' : Array β
h : l'.size = l.size
la : Array α
lb : Vector β la.size
⊢ zipWith f ({ toArray := l, size_toArray := ⋯ } ++ { toArray := la, size_toArray := ⋯ })
      ({ toArray := l', size_toArray := h } ++ lb) =
    zipWith f { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h } ++
      zipWith f { toArray := la, size_toArray := ⋯ } lb

Proof state:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : Array α
l' : Array β
h : l'.size = l.size
la : Array α
lb : Array β
h' : lb.size = la.size
⊢ zipWith f ({ toArray := l, size_toArray := ⋯ } ++ { toArray := la, size_toArray := ⋯ })
      ({ toArray := l', size_toArray := h } ++ { toArray := lb, size_toArray := h' }) =
    zipWith f { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h } ++
      zipWith f { toArray := la, size_toArray := ⋯ } { toArray := lb, size_toArray := h' }

Tactic:
simp [Array.zipWith_append, *]

Result:
no goals

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : Array α
l' : Array β
h : l'.size = l.size
la : Array α
lb : Vector β la.size
⊢ zipWith f ({ toArray := l, size_toArray := ⋯ } ++ { toArray := la, size_toArray := ⋯ })
      ({ toArray := l', size_toArray := h } ++ lb) =
    zipWith f { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h } ++
      zipWith f { toArray := la, size_toArray := ⋯ } lb

Tactic:
rcases lb with ⟨lb, h'⟩

Result:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : Array α
l' : Array β
h : l'.size = l.size
la : Array α
lb : Array β
h' : lb.size = la.size
⊢ zipWith f ({ toArray := l, size_toArray := ⋯ } ++ { toArray := la, size_toArray := ⋯ })
      ({ toArray := l', size_toArray := h } ++ { toArray := lb, size_toArray := h' }) =
    zipWith f { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h } ++
      zipWith f { toArray := la, size_toArray := ⋯ } { toArray := lb, size_toArray := h' }

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n m : Nat
f : α → β → γ
l : Vector α n
la : Vector α m
l' : Vector β n
lb : Vector β m
⊢ zipWith f (l ++ la) (l' ++ lb) = zipWith f l l' ++ zipWith f la lb

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
m : Nat
f : α → β → γ
la : Vector α m
lb : Vector β m
l : Array α
l' : Vector β l.size
⊢ zipWith f ({ toArray := l, size_toArray := ⋯ } ++ la) (l' ++ lb) =
    zipWith f { toArray := l, size_toArray := ⋯ } l' ++ zipWith f la lb

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
m : Nat
f : α → β → γ
la : Vector α m
lb : Vector β m
l : Array α
l' : Vector β l.size
⊢ zipWith f ({ toArray := l, size_toArray := ⋯ } ++ la) (l' ++ lb) =
    zipWith f { toArray := l, size_toArray := ⋯ } l' ++ zipWith f la lb

Tactic:
rcases l' with ⟨l', h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
m : Nat
f : α → β → γ
la : Vector α m
lb : Vector β m
l : Array α
l' : Array β
h : l'.size = l.size
⊢ zipWith f ({ toArray := l, size_toArray := ⋯ } ++ la) ({ toArray := l', size_toArray := h } ++ lb) =
    zipWith f { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h } ++ zipWith f la lb