α : Type u
β : Type u_1
γ : Type ?u.20405
δ : Type ?u.20408
ε : Type ?u.20411
r₁ : List α
l₂ r₂ : List β
h : length [] = length l₂
⊢ zip ([] ++ r₁) ([] ++ r₂) = zip [] [] ++ zip r₁ r₂
α : Type u
β : Type u_1
γ : Type ?u.20405
δ : Type ?u.20408
ε : Type ?u.20411
r₁ : List α
l₂ r₂ : List β
h : length [] = length l₂
⊢ zip ([] ++ r₁) (l₂ ++ r₂) = zip [] l₂ ++ zip r₁ r₂
simp only [eq_nil_of_length_eq_zero h.symm]
no goals
α : Type u
β : Type u_1
γ : Type ?u.20405
δ : Type ?u.20408
ε : Type ?u.20411
r₁ : List α
l₂ r₂ : List β
h : length [] = length l₂
⊢ zip ([] ++ r₁) ([] ++ r₂) = zip [] [] ++ zip r₁ r₂
rfl
α : Type u
β : Type u_1
γ : Type ?u.20405
δ : Type ?u.20408
ε : Type ?u.20411
l₁ r₁ : List α
r₂ : List β
h : length l₁ = length []
⊢ zip ([] ++ r₁) ([] ++ r₂) = zip [] [] ++ zip r₁ r₂
α : Type u
β : Type u_1
γ : Type ?u.20405
δ : Type ?u.20408
ε : Type ?u.20411
l₁ r₁ : List α
r₂ : List β
h : length l₁ = length []
⊢ zip (l₁ ++ r₁) ([] ++ r₂) = zip l₁ [] ++ zip r₁ r₂
simp only [eq_nil_of_length_eq_zero h]
no goals
α : Type u
β : Type u_1
γ : Type ?u.20405
δ : Type ?u.20408
ε : Type ?u.20411
l₁ r₁ : List α
r₂ : List β
h : length l₁ = length []
⊢ zip ([] ++ r₁) ([] ++ r₂) = zip [] [] ++ zip r₁ r₂
rfl
no goals
α : Type u
β : Type u_1
γ : Type ?u.20405
δ : Type ?u.20408
ε : Type ?u.20411
a : α
l₁ r₁ : List α
b : β
l₂ r₂ : List β
h : length (a :: l₁) = length (b :: l₂)
⊢ zip (a :: l₁ ++ r₁) (b :: l₂ ++ r₂) = zip (a :: l₁) (b :: l₂) ++ zip r₁ r₂
simp only [cons_append, zip_cons_cons, zip_append (succ.inj h)]