-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zip_append {l₁ : Vector α n} {l₂ : Vector β n} {r₁ : Vector α m} {r₂ : Vector β m} :
    zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂

Proof state:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
r₁ : Array α
r₂ : Array β
h' : r₂.size = r₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ } ++ { toArray := r₁, size_toArray := ⋯ }).zip
      ({ toArray := l₂, size_toArray := h } ++ { toArray := r₂, size_toArray := h' }) =
    { toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h } ++
      { toArray := r₁, size_toArray := ⋯ }.zip { toArray := r₂, size_toArray := h' }

Tactic:
simp [Array.zip_append, h, h']

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
m : Nat
r₁ : Vector α m
r₂ : Vector β m
l₁ : Array α
l₂ : Vector β l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ } ++ r₁).zip (l₂ ++ r₂) = { toArray := l₁, size_toArray := ⋯ }.zip l₂ ++ r₁.zip r₂

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

Result:
case mk.mk
α : Type u_1
β : Type u_2
m : Nat
r₁ : Vector α m
r₂ : Vector β m
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ } ++ r₁).zip ({ toArray := l₂, size_toArray := h } ++ r₂) =
    { toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h } ++ r₁.zip r₂

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
m : Nat
r₁ : Vector α m
r₂ : Vector β m
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ } ++ r₁).zip ({ toArray := l₂, size_toArray := h } ++ r₂) =
    { toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h } ++ r₁.zip r₂

Tactic:
rcases r₁ with ⟨r₁, rfl⟩

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
r₁ : Array α
r₂ : Vector β r₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ } ++ { toArray := r₁, size_toArray := ⋯ }).zip
      ({ toArray := l₂, size_toArray := h } ++ r₂) =
    { toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h } ++
      { toArray := r₁, size_toArray := ⋯ }.zip r₂

Proof state:
α : Type u_1
n : Nat
β : Type u_2
m : Nat
l₁ : Vector α n
l₂ : Vector β n
r₁ : Vector α m
r₂ : Vector β m
⊢ (l₁ ++ r₁).zip (l₂ ++ r₂) = l₁.zip l₂ ++ r₁.zip r₂

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
m : Nat
r₁ : Vector α m
r₂ : Vector β m
l₁ : Array α
l₂ : Vector β l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ } ++ r₁).zip (l₂ ++ r₂) = { toArray := l₁, size_toArray := ⋯ }.zip l₂ ++ r₁.zip r₂

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
r₁ : Array α
r₂ : Vector β r₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ } ++ { toArray := r₁, size_toArray := ⋯ }).zip
      ({ toArray := l₂, size_toArray := h } ++ r₂) =
    { toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h } ++
      { toArray := r₁, size_toArray := ⋯ }.zip r₂

Tactic:
rcases r₂ with ⟨r₂, h'⟩

Result:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
r₁ : Array α
r₂ : Array β
h' : r₂.size = r₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ } ++ { toArray := r₁, size_toArray := ⋯ }).zip
      ({ toArray := l₂, size_toArray := h } ++ { toArray := r₂, size_toArray := h' }) =
    { toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h } ++
      { toArray := r₁, size_toArray := ⋯ }.zip { toArray := r₂, size_toArray := h' }