Theorem: List.zipWith_snd (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 => b) l₁ l₂ = l₂
Tactic:
erw [← List.map_uncurry_zip_eq_zipWith, List.map_snd_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