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

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : List α
lb l' : List β
h : [].length = l'.length
this : l' = []
⊢ zipWith f ([] ++ la) (l' ++ lb) = zipWith f [] l' ++ zipWith f la lb

Tactic:
simp [this]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : List α
lb : List β
hl : α
tl : List α
ih : ∀ (l' : List β), tl.length = l'.length → zipWith f (tl ++ la) (l' ++ lb) = zipWith f tl l' ++ zipWith f la lb
l' : List β
h : (hl :: tl).length = l'.length
⊢ zipWith f (hl :: tl ++ la) (l' ++ lb) = zipWith f (hl :: tl) l' ++ zipWith f la lb

Tactic:
cases l' with
| nil => simp at h
| cons head tail =>
  simp only [length_cons, Nat.succ.injEq] at h
  simp [ih _ h]

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : List α
lb : List β
hl : α
tl : List α
ih : ∀ (l' : List β), tl.length = l'.length → zipWith f (tl ++ la) (l' ++ lb) = zipWith f tl l' ++ zipWith f la lb
head : β
tail : List β
h : (hl :: tl).length = (head :: tail).length
⊢ zipWith f (hl :: tl ++ la) (head :: tail ++ lb) = zipWith f (hl :: tl) (head :: tail) ++ zipWith f la lb

Tactic:
simp only [length_cons, Nat.succ.injEq] at h

Result:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : List α
lb : List β
hl : α
tl : List α
ih : ∀ (l' : List β), tl.length = l'.length → zipWith f (tl ++ la) (l' ++ lb) = zipWith f tl l' ++ zipWith f la lb
head : β
tail : List β
h : tl.length = tail.length
⊢ zipWith f (hl :: tl ++ la) (head :: tail ++ lb) = zipWith f (hl :: tl) (head :: tail) ++ zipWith f la lb

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

Tactic:
induction l generalizing l' with
| nil =>
  have : l' = [] := eq_nil_of_length_eq_zero (by simpa using h.symm)
  simp [this]
| cons hl tl ih =>
  cases l' with
  | nil => simp at h
  | cons head tail =>
    simp only [length_cons, Nat.succ.injEq] at h
    simp [ih _ h]

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : List α
lb : List β
hl : α
tl : List α
ih : ∀ (l' : List β), tl.length = l'.length → zipWith f (tl ++ la) (l' ++ lb) = zipWith f tl l' ++ zipWith f la lb
head : β
tail : List β
h : tl.length = tail.length
⊢ zipWith f (hl :: tl ++ la) (head :: tail ++ lb) = zipWith f (hl :: tl) (head :: tail) ++ zipWith f la lb

Tactic:
simp [ih _ h]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : List α
lb l' : List β
h : [].length = l'.length
⊢ zipWith f ([] ++ la) (l' ++ lb) = zipWith f [] l' ++ zipWith f la lb

Tactic:
have : l' = [] := eq_nil_of_length_eq_zero (by simpa using h.symm)

Result:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : List α
lb l' : List β
h : [].length = l'.length
this : l' = []
⊢ zipWith f ([] ++ la) (l' ++ lb) = zipWith f [] l' ++ zipWith f la lb

Proof state:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : List α
lb : List β
hl : α
tl : List α
ih : ∀ (l' : List β), tl.length = l'.length → zipWith f (tl ++ la) (l' ++ lb) = zipWith f tl l' ++ zipWith f la lb
h : (hl :: tl).length = [].length
⊢ zipWith f (hl :: tl ++ la) ([] ++ lb) = zipWith f (hl :: tl) [] ++ zipWith f la lb

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : List α
lb l' : List β
h : [].length = l'.length
⊢ l'.length = 0

Tactic:
simpa using h.symm

Result:
no goals