Theorem: List.zipWith_fst (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
hl : length l₁ ≤ length l₂
⊢ zipWith (fun a b => a) l₁ l₂ = l₁
Tactic:
erw [← List.map_uncurry_zip_eq_zipWith, List.map_fst_zip]
State after:
case a
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
hl : length l₁ ≤ length l₂
⊢ length l₁ ≤ length l₂

State before:
case a
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
hl : length l₁ ≤ length l₂
⊢ length l₁ ≤ length l₂
Tactic:
exact hl
State after:
no goals