Theorem: LoVe.length_zip (LoVe/Lectures/LoVe05_FunctionalProgramming_Demo.lean)

State before:
α β : Type
xs : List α
ys : List β
⊢ length (zip xs ys) = min (length xs) (length ys)
Tactic:
induction xs generalizing ys with
| nil           => simp [min, length]
| cons x xs' ih =>
  cases ys with
  | nil        => rfl
  | cons y ys' => simp [zip, length, ih ys', min_add_add]
State after:
no goals

State before:
case nil
α β : Type
ys : List β
⊢ length (zip [] ys) = min (length []) (length ys)
Tactic:
simp [min, length]
State after:
no goals

State before:
case cons
α β : Type
x : α
xs' : List α
ih : ∀ (ys : List β), length (zip xs' ys) = min (length xs') (length ys)
ys : List β
⊢ length (zip (x :: xs') ys) = min (length (x :: xs')) (length ys)
Tactic:
cases ys with
| nil        => rfl
| cons y ys' => simp [zip, length, ih ys', min_add_add]
State after:
no goals

State before:
case cons.nil
α β : Type
x : α
xs' : List α
ih : ∀ (ys : List β), length (zip xs' ys) = min (length xs') (length ys)
⊢ length (zip (x :: xs') []) = min (length (x :: xs')) (length [])
Tactic:
rfl
State after:
no goals

State before:
case cons.cons
α β : Type
x : α
xs' : List α
ih : ∀ (ys : List β), length (zip xs' ys) = min (length xs') (length ys)
y : β
ys' : List β
⊢ length (zip (x :: xs') (y :: ys')) = min (length (x :: xs')) (length (y :: ys'))
Tactic:
simp [zip, length, ih ys', min_add_add]
State after:
no goals