ι : Type ?u.476103
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : Option α → β → γ
a : α
as : List α
b : β
bs : List β
h : length bs ≤ length as
this : (fun a b => flip f a (some b)) = flip fun a b => f (some a) b
⊢ map₂Right f as bs = zipWith (fun a b => f (some a) b) as bs
ι : Type ?u.476103
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : Option α → β → γ
a : α
as : List α
b : β
bs : List β
h : length bs ≤ length as
⊢ map₂Right f as bs = zipWith (fun a b => f (some a) b) as bs
have : (fun a b => flip f a (some b)) = flip fun a b => f (some a) b := rfl
no goals
ι : Type ?u.476103
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : Option α → β → γ
a : α
as : List α
b : β
bs : List β
h : length bs ≤ length as
this : (fun a b => flip f a (some b)) = flip fun a b => f (some a) b
⊢ map₂Right f as bs = zipWith (fun a b => f (some a) b) as bs
simp only [map₂Right, map₂Left_eq_zipWith, zipWith_flip, *]