case intro
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h₁ : length l₁ = length l₂
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b
⊢ Forall₂ R l₁ l₂
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : length l₁ = length l₂ ∧ ∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b
⊢ Forall₂ R l₁ l₂
cases' h with h₁ h₂
case intro.nil
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂✝ : List β
h₁✝ : length l₁ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂✝ → R a b
l₂ : List β
h₁ : length [] = length l₂
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ zip [] l₂ → R a b
⊢ Forall₂ R [] l₂

case intro.cons
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
l₂ : List β
h₁ : length (a :: l₁) = length l₂
h₂ : ∀ {a_1 : α} {b : β}, (a_1, b) ∈ zip (a :: l₁) l₂ → R a_1 b
⊢ Forall₂ R (a :: l₁) l₂
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h₁ : length l₁ = length l₂
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b
⊢ Forall₂ R l₁ l₂
induction' l₁ with a l₁ IH generalizing l₂
case intro.nil.refl
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h₁✝ : length l₁ = length l₂
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b
h₁ : length [] = length []
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ zip [] [] → R a b
⊢ Forall₂ R [] []
case intro.nil
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂✝ : List β
h₁✝ : length l₁ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂✝ → R a b
l₂ : List β
h₁ : length [] = length l₂
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ zip [] l₂ → R a b
⊢ Forall₂ R [] l₂
cases length_eq_zero.1 h₁.symm
no goals
case intro.nil.refl
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h₁✝ : length l₁ = length l₂
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b
h₁ : length [] = length []
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ zip [] [] → R a b
⊢ Forall₂ R [] []
constructor
case intro.cons.nil
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂ : List β
h₁✝ : length l₁✝ = length l₂
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
h₁ : length (a :: l₁) = length []
h₂ : ∀ {a_1 : α} {b : β}, (a_1, b) ∈ zip (a :: l₁) [] → R a_1 b
⊢ Forall₂ R (a :: l₁) []

case intro.cons.cons
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₁ : length (a :: l₁) = length (b :: l₂)
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
⊢ Forall₂ R (a :: l₁) (b :: l₂)
case intro.cons
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
l₂ : List β
h₁ : length (a :: l₁) = length l₂
h₂ : ∀ {a_1 : α} {b : β}, (a_1, b) ∈ zip (a :: l₁) l₂ → R a_1 b
⊢ Forall₂ R (a :: l₁) l₂
cases' l₂ with b l₂
case intro.cons.cons
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₁ : length (a :: l₁) = length (b :: l₂)
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
⊢ Forall₂ R (a :: l₁) (b :: l₂)
case intro.cons.nil
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂ : List β
h₁✝ : length l₁✝ = length l₂
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
h₁ : length (a :: l₁) = length []
h₂ : ∀ {a_1 : α} {b : β}, (a_1, b) ∈ zip (a :: l₁) [] → R a_1 b
⊢ Forall₂ R (a :: l₁) []

case intro.cons.cons
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₁ : length (a :: l₁) = length (b :: l₂)
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
⊢ Forall₂ R (a :: l₁) (b :: l₂)
. simp at h₁
no goals
case intro.cons.cons
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₁ : length (a :: l₁) = length (b :: l₂)
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
⊢ Forall₂ R (a :: l₁) (b :: l₂)
. simp only [length_cons, succ.injEq] at h₁
  exact Forall₂.cons (h₂ <| by simp [zip])
    (IH h₁ <| fun h => h₂ <| by
      simp only [zip, zipWith, find?, mem_cons, Prod.mk.injEq]; right
      simpa [zip] using h)
no goals
case intro.cons.nil
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂ : List β
h₁✝ : length l₁✝ = length l₂
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
h₁ : length (a :: l₁) = length []
h₂ : ∀ {a_1 : α} {b : β}, (a_1, b) ∈ zip (a :: l₁) [] → R a_1 b
⊢ Forall₂ R (a :: l₁) []
simp at h₁
case intro.cons.cons
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
h₁ : length l₁ = length l₂
⊢ Forall₂ R (a :: l₁) (b :: l₂)
case intro.cons.cons
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₁ : length (a :: l₁) = length (b :: l₂)
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
⊢ Forall₂ R (a :: l₁) (b :: l₂)
simp only [length_cons, succ.injEq] at h₁
no goals
case intro.cons.cons
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
h₁ : length l₁ = length l₂
⊢ Forall₂ R (a :: l₁) (b :: l₂)
exact Forall₂.cons (h₂ <| by simp [zip])
  (IH h₁ <| fun h => h₂ <| by
    simp only [zip, zipWith, find?, mem_cons, Prod.mk.injEq]; right
    simpa [zip] using h)
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
h₁ : length l₁ = length l₂
⊢ (a, b) ∈ zip (a :: l₁) (b :: l₂)
simp [zip]
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
h₁ : length l₁ = length l₂
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ zip l₁ l₂
⊢ a✝ = a ∧ b✝ = b ∨ (a✝, b✝) ∈ zipWith Prod.mk l₁ l₂
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
h₁ : length l₁ = length l₂
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ zip l₁ l₂
⊢ (a✝, b✝) ∈ zip (a :: l₁) (b :: l₂)
simp only [zip, zipWith, find?, mem_cons, Prod.mk.injEq]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
h₁ : length l₁ = length l₂
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ zip l₁ l₂
⊢ (a✝, b✝) ∈ zipWith Prod.mk l₁ l₂
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
h₁ : length l₁ = length l₂
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ zip l₁ l₂
⊢ a✝ = a ∧ b✝ = b ∨ (a✝, b✝) ∈ zipWith Prod.mk l₁ l₂
right
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.40478
δ : Type ?u.40481
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
h₁ : length l₁ = length l₂
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ zip l₁ l₂
⊢ (a✝, b✝) ∈ zipWith Prod.mk l₁ l₂
simpa [zip] using h