ι : Type ?u.477219
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
as✝ : List α
b : β
bs✝ : List β
as : List α
bs : List β
⊢ zipWithLeft Prod.mk as bs = (zipWithLeft' Prod.mk as bs).fst
ι : Type ?u.477219
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
as✝ : List α
b : β
bs✝ : List β
as : List α
bs : List β
⊢ zipLeft as bs = (zipLeft' as bs).fst
rw [zipLeft, zipLeft']
no goals
ι : Type ?u.477219
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
as✝ : List α
b : β
bs✝ : List β
as : List α
bs : List β
⊢ zipWithLeft Prod.mk as bs = (zipWithLeft' Prod.mk as bs).fst
cases as with
| nil => rfl
| cons _ atl =>
  cases bs with
  | nil => rfl
  | cons _ btl => rw [zipWithLeft, zipWithLeft', cons_inj]; exact @zipLeft_eq_zipLeft' atl btl
no goals
case nil
ι : Type ?u.477219
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
as : List α
b : β
bs✝ bs : List β
⊢ zipWithLeft Prod.mk [] bs = (zipWithLeft' Prod.mk [] bs).fst
rfl
no goals
case cons
ι : Type ?u.477219
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
as : List α
b : β
bs✝ bs : List β
head✝ : α
atl : List α
⊢ zipWithLeft Prod.mk (head✝ :: atl) bs = (zipWithLeft' Prod.mk (head✝ :: atl) bs).fst
cases bs with
| nil => rfl
| cons _ btl => rw [zipWithLeft, zipWithLeft', cons_inj]; exact @zipLeft_eq_zipLeft' atl btl
no goals
case cons.nil
ι : Type ?u.477219
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
as : List α
b : β
bs : List β
head✝ : α
atl : List α
⊢ zipWithLeft Prod.mk (head✝ :: atl) [] = (zipWithLeft' Prod.mk (head✝ :: atl) []).fst
rfl
case cons.cons
ι : Type ?u.477219
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
as : List α
b : β
bs : List β
head✝¹ : α
atl : List α
head✝ : β
btl : List β
⊢ zipWithLeft Prod.mk atl btl = (zipWithLeft' Prod.mk atl btl).fst
case cons.cons
ι : Type ?u.477219
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
as : List α
b : β
bs : List β
head✝¹ : α
atl : List α
head✝ : β
btl : List β
⊢ zipWithLeft Prod.mk (head✝¹ :: atl) (head✝ :: btl) = (zipWithLeft' Prod.mk (head✝¹ :: atl) (head✝ :: btl)).fst
rw [zipWithLeft, zipWithLeft', cons_inj]
no goals
case cons.cons
ι : Type ?u.477219
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
as : List α
b : β
bs : List β
head✝¹ : α
atl : List α
head✝ : β
btl : List β
⊢ zipWithLeft Prod.mk atl btl = (zipWithLeft' Prod.mk atl btl).fst
exact @zipLeft_eq_zipLeft' atl btl