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

Proof state:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝³ : List α
toList✝² : List β
toList✝¹ : List α
toList✝ : List β
h : toList✝³.length = toList✝².length
⊢ zipWith f ({ toList := toList✝³ } ++ { toList := toList✝¹ }) ({ toList := toList✝² } ++ { toList := toList✝ }) =
    zipWith f { toList := toList✝³ } { toList := toList✝² } ++ zipWith f { toList := toList✝¹ } { toList := toList✝ }

Tactic:
simp [List.zipWith_append, h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l la : Array α
l' lb : Array β
h : l.size = l'.size
⊢ zipWith f (l ++ la) (l' ++ lb) = zipWith f l l' ++ zipWith f la lb

Tactic:
cases l

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

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

Tactic:
cases l'

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : Array α
lb : Array β
toList✝¹ : List α
toList✝ : List β
h : { toList := toList✝¹ }.size = { toList := toList✝ }.size
⊢ zipWith f ({ toList := toList✝¹ } ++ la) ({ toList := toList✝ } ++ lb) =
    zipWith f { toList := toList✝¹ } { toList := toList✝ } ++ zipWith f la lb

Proof state:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝³ : List α
toList✝² : List β
h : { toList := toList✝³ }.size = { toList := toList✝² }.size
toList✝¹ : List α
toList✝ : List β
⊢ zipWith f ({ toList := toList✝³ } ++ { toList := toList✝¹ }) ({ toList := toList✝² } ++ { toList := toList✝ }) =
    zipWith f { toList := toList✝³ } { toList := toList✝² } ++ zipWith f { toList := toList✝¹ } { toList := toList✝ }

Tactic:
simp at h

Result:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝³ : List α
toList✝² : List β
toList✝¹ : List α
toList✝ : List β
h : toList✝³.length = toList✝².length
⊢ zipWith f ({ toList := toList✝³ } ++ { toList := toList✝¹ }) ({ toList := toList✝² } ++ { toList := toList✝ }) =
    zipWith f { toList := toList✝³ } { toList := toList✝² } ++ zipWith f { toList := toList✝¹ } { toList := toList✝ }

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
lb : Array β
toList✝² : List α
toList✝¹ : List β
h : { toList := toList✝² }.size = { toList := toList✝¹ }.size
toList✝ : List α
⊢ zipWith f ({ toList := toList✝² } ++ { toList := toList✝ }) ({ toList := toList✝¹ } ++ lb) =
    zipWith f { toList := toList✝² } { toList := toList✝¹ } ++ zipWith f { toList := toList✝ } lb

Tactic:
cases lb

Result:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝³ : List α
toList✝² : List β
h : { toList := toList✝³ }.size = { toList := toList✝² }.size
toList✝¹ : List α
toList✝ : List β
⊢ zipWith f ({ toList := toList✝³ } ++ { toList := toList✝¹ }) ({ toList := toList✝² } ++ { toList := toList✝ }) =
    zipWith f { toList := toList✝³ } { toList := toList✝² } ++ zipWith f { toList := toList✝¹ } { toList := toList✝ }

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : Array α
lb : Array β
toList✝¹ : List α
toList✝ : List β
h : { toList := toList✝¹ }.size = { toList := toList✝ }.size
⊢ zipWith f ({ toList := toList✝¹ } ++ la) ({ toList := toList✝ } ++ lb) =
    zipWith f { toList := toList✝¹ } { toList := toList✝ } ++ zipWith f la lb

Tactic:
cases la

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
lb : Array β
toList✝² : List α
toList✝¹ : List β
h : { toList := toList✝² }.size = { toList := toList✝¹ }.size
toList✝ : List α
⊢ zipWith f ({ toList := toList✝² } ++ { toList := toList✝ }) ({ toList := toList✝¹ } ++ lb) =
    zipWith f { toList := toList✝² } { toList := toList✝¹ } ++ zipWith f { toList := toList✝ } lb