[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : α
b : β
l₁ : List α
l₂ : List β
h : Forall₂ R (a :: l₁) (b :: l₂)
⊢ R a b ∧ Forall₂ R l₁ l₂
[PROOFSTEP]
cases' h with h₁ h₂
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : α
b : β
l₁ : List α
l₂ : List β
a✝¹ : R a b
a✝ : Forall₂ R l₁ l₂
⊢ R a b ∧ Forall₂ R l₁ l₂
[PROOFSTEP]
constructor
[GOAL]
case cons.left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : α
b : β
l₁ : List α
l₂ : List β
a✝¹ : R a b
a✝ : Forall₂ R l₁ l₂
⊢ R a b
[PROOFSTEP]
assumption
[GOAL]
case cons.right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : α
b : β
l₁ : List α
l₂ : List β
a✝¹ : R a b
a✝ : Forall₂ R l₁ l₂
⊢ Forall₂ R l₁ l₂
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
h : Forall₂ R l₁ l₂
⊢ Forall₂ S l₁ l₂
[PROOFSTEP]
induction h
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
⊢ Forall₂ S [] []
[PROOFSTEP]
constructor
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ Forall₂ S (a✝² :: l₁✝) (b✝ :: l₂✝)
[PROOFSTEP]
constructor
[GOAL]
case cons.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ S a✝² b✝
[PROOFSTEP]
solve_by_elim
[GOAL]
case cons.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ Forall₂ S l₁✝ l₂✝
[PROOFSTEP]
solve_by_elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
⊢ Forall₂ Rₐ [] [] ↔ ∀ (x : α), x ∈ [] → Rₐ x x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : α
l : List α
⊢ Forall₂ Rₐ (a :: l) (a :: l) ↔ ∀ (x : α), x ∈ a :: l → Rₐ x x
[PROOFSTEP]
simp [@forall₂_same l]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
⊢ (Forall₂ fun x x_1 => x = x_1) = Eq
[PROOFSTEP]
funext a b
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a b = (a = b)
[PROOFSTEP]
apply propext
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a b ↔ a = b
[PROOFSTEP]
constructor
[GOAL]
case h.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a b → a = b
[PROOFSTEP]
intro h
[GOAL]
case h.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
h : Forall₂ (fun x x_1 => x = x_1) a b
⊢ a = b
[PROOFSTEP]
induction h
[GOAL]
case h.h.a.mp.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ [] = []
[PROOFSTEP]
rfl
[GOAL]
case h.h.a.mp.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
a✝² b✝ : α
l₁✝ l₂✝ : List α
a✝¹ : a✝² = b✝
a✝ : Forall₂ (fun x x_1 => x = x_1) l₁✝ l₂✝
a_ih✝ : l₁✝ = l₂✝
⊢ a✝² :: l₁✝ = b✝ :: l₂✝
[PROOFSTEP]
simp only [*]
[GOAL]
case h.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ a = b → Forall₂ (fun x x_1 => x = x_1) a b
[PROOFSTEP]
rintro rfl
[GOAL]
case h.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a a
[PROOFSTEP]
exact forall₂_refl _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List β
H : Forall₂ R [] l
⊢ l = []
[PROOFSTEP]
cases H
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
⊢ [] = []
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List β
⊢ l = [] → Forall₂ R [] l
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
⊢ Forall₂ R [] []
[PROOFSTEP]
exact Forall₂.nil
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
H : Forall₂ R l []
⊢ l = []
[PROOFSTEP]
cases H
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
⊢ [] = []
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
⊢ l = [] → Forall₂ R l []
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
⊢ Forall₂ R [] []
[PROOFSTEP]
exact Forall₂.nil
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Prop
u : List β
⊢ Forall₂ (fun a b => p a ∧ R a b) [] u ↔ (∀ (a : α), a ∈ [] → p a) ∧ Forall₂ R [] u
[PROOFSTEP]
simp only [forall₂_nil_left_iff, forall_prop_of_false (not_mem_nil _), imp_true_iff, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Prop
a : α
l : List α
u : List β
⊢ Forall₂ (fun a b => p a ∧ R a b) (a :: l) u ↔ (∀ (a_1 : α), a_1 ∈ a :: l → p a_1) ∧ Forall₂ R (a :: l) u
[PROOFSTEP]
simp only [forall₂_and_left l, forall₂_cons_left_iff, forall_mem_cons, and_assoc, @and_comm _ (p a),
  @and_left_comm _ (p a), exists_and_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Prop
a : α
l : List α
u : List β
⊢ (p a ∧ ∃ x, R a x ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ x_1, Forall₂ R l x_1 ∧ u = x :: x_1) ↔
    p a ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ b, R a b ∧ ∃ x, Forall₂ R l x ∧ u = b :: x
[PROOFSTEP]
simp only [and_comm, and_assoc, and_left_comm, ← exists_and_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : γ → α
x✝ : List β
⊢ Forall₂ R (map f []) x✝ ↔ Forall₂ (fun c b => R (f c) b) [] x✝
[PROOFSTEP]
simp only [map, forall₂_nil_left_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : γ → α
a : γ
l : List γ
x✝ : List β
⊢ Forall₂ R (map f (a :: l)) x✝ ↔ Forall₂ (fun c b => R (f c) b) (a :: l) x✝
[PROOFSTEP]
simp only [map, forall₂_cons_left_iff, forall₂_map_left_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : γ → β
x✝ : List α
⊢ Forall₂ R x✝ (map f []) ↔ Forall₂ (fun a c => R a (f c)) x✝ []
[PROOFSTEP]
simp only [map, forall₂_nil_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : γ → β
x✝ : List α
b : γ
u : List γ
⊢ Forall₂ R x✝ (map f (b :: u)) ↔ Forall₂ (fun a c => R a (f c)) x✝ (b :: u)
[PROOFSTEP]
simp only [map, forall₂_cons_right_iff, forall₂_map_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) ∈ zip (a✝ :: l₁✝) (b✝ :: l₂✝)
⊢ R x y
[PROOFSTEP]
rw [zip, zipWith, mem_cons] at hx 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
⊢ R x y
[PROOFSTEP]
match hx with
| Or.inl rfl => exact h₁
| Or.inr h₃ => exact forall₂_zip h₂ h₃
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
h₁ : R x y
⊢ R x y
[PROOFSTEP]
exact h₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
x✝¹ : β
x✝ : α
h₃ : (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
h₁ : R x✝ x✝¹
⊢ R x y
[PROOFSTEP]
exact forall₂_zip h₂ h₃
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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₂
[PROOFSTEP]
cases' h with h₁ h₂
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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₂
[PROOFSTEP]
induction' l₁ with a l₁ IH generalizing l₂
[GOAL]
case intro.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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₂
[PROOFSTEP]
cases length_eq_zero.1 h₁.symm
[GOAL]
case intro.nil.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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 [] []
[PROOFSTEP]
constructor
[GOAL]
case intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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₂
[PROOFSTEP]
cases' l₂ with b l₂
[GOAL]
case intro.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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₁) []
[PROOFSTEP]
simp at h₁ 
[GOAL]
case intro.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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₂)
[PROOFSTEP]
simp only [length_cons, succ.injEq] at h₁ 
[GOAL]
case intro.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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₂)
[PROOFSTEP]
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)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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₂)
[PROOFSTEP]
simp [zip]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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₂)
[PROOFSTEP]
simp only [zip, zipWith, find?, mem_cons, Prod.mk.injEq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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₂
[PROOFSTEP]
right
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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₂
[PROOFSTEP]
simpa [zip] using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
x✝² : List α
x✝¹ : List β
x✝ : Forall₂ R x✝² x✝¹
⊢ Forall₂ R (take 0 x✝²) (take 0 x✝¹)
[PROOFSTEP]
simp only [Forall₂.nil, take]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
n✝ : ℕ
⊢ Forall₂ R (take (n✝ + 1) []) (take (n✝ + 1) [])
[PROOFSTEP]
simp only [Forall₂.nil, take]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
n : ℕ
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (take (n + 1) (a✝ :: l₁✝)) (take (n + 1) (b✝ :: l₂✝))
[PROOFSTEP]
simp [And.intro h₁ h₂, forall₂_take n]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
x✝¹ : List α
x✝ : List β
h : Forall₂ R x✝¹ x✝
⊢ Forall₂ R (drop 0 x✝¹) (drop 0 x✝)
[PROOFSTEP]
simp only [drop, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
n✝ : ℕ
⊢ Forall₂ R (drop (n✝ + 1) []) (drop (n✝ + 1) [])
[PROOFSTEP]
simp only [Forall₂.nil, drop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
n : ℕ
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (drop (n + 1) (a✝ :: l₁✝)) (drop (n + 1) (b✝ :: l₂✝))
[PROOFSTEP]
simp [And.intro h₁ h₂, forall₂_drop n]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (take (length l₁) l) l₁
[PROOFSTEP]
have h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂)) := forall₂_take (length l₁) h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂))
⊢ Forall₂ R (take (length l₁) l) l₁
[PROOFSTEP]
rwa [take_left] at h' 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (drop (length l₁) l) l₂
[PROOFSTEP]
have h' : Forall₂ R (drop (length l₁) l) (drop (length l₁) (l₁ ++ l₂)) := forall₂_drop (length l₁) h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (drop (length l₁) l) (drop (length l₁) (l₁ ++ l₂))
⊢ Forall₂ R (drop (length l₁) l) l₂
[PROOFSTEP]
rwa [drop_left] at h' 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
hr : BiUnique R
a : α
b : β
x✝ : R a b
⊢ (fun x x_1 => x ∈ x_1) a [] ↔ (fun x x_1 => x ∈ x_1) b []
[PROOFSTEP]
simp only [not_mem_nil]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ (fun x x_1 => x ∈ x_1) a (a' :: as) ↔ (fun x x_1 => x ∈ x_1) b (b' :: bs)
[PROOFSTEP]
simp only [mem_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ a = a' ∨ a ∈ as ↔ b = b' ∨ b ∈ bs
[PROOFSTEP]
exact rel_or (rel_eq hr h h₁) (rel_mem hr h h₂)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (reverse (a✝ :: l₁✝)) (reverse (b✝ :: l₂✝))
[PROOFSTEP]
simp only [reverse_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (reverse l₁✝ ++ [a✝]) (reverse l₂✝ ++ [b✝])
[PROOFSTEP]
exact rel_append (rel_reverse h₂) (Forall₂.cons h₁ Forall₂.nil)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R (reverse l₁) (reverse l₂)
⊢ Forall₂ R l₁ l₂
[PROOFSTEP]
rw [← reverse_reverse l₁, ← reverse_reverse l₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R (reverse l₁) (reverse l₂)
⊢ Forall₂ R (reverse (reverse l₁)) (reverse (reverse l₂))
[PROOFSTEP]
exact rel_reverse h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : (R ⇒ fun x x_1 => x ↔ x_1) (fun x => p x = true) fun x => q x = true
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
[PROOFSTEP]
dsimp [LiftFun] at hpq 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
[PROOFSTEP]
by_cases h : p a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
[PROOFSTEP]
have : q b := by rwa [← hpq h₁]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
⊢ q b = true
[PROOFSTEP]
rwa [← hpq h₁]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
this : q b = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
[PROOFSTEP]
simp only [filter_cons_of_pos _ h, filter_cons_of_pos _ this, forall₂_cons, h₁, true_and_iff, rel_filter hpq h₂]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
[PROOFSTEP]
have : ¬q b := by rwa [← hpq h₁]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
⊢ ¬q b = true
[PROOFSTEP]
rwa [← hpq h₁]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
this : ¬q b = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
[PROOFSTEP]
simp only [filter_cons_of_neg _ h, filter_cons_of_neg _ this, rel_filter hpq h₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P (filterMap f (a :: as)) (filterMap g (b :: bs))
[PROOFSTEP]
rw [filterMap_cons, filterMap_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P
    (match f a with
    | none => filterMap f as
    | some b => b :: filterMap f as)
    (match g b with
    | none => filterMap g bs
    | some b => b :: filterMap g bs)
[PROOFSTEP]
exact
  match f a, g b, hfg h₁ with
  | _, _, Option.Rel.none => rel_filterMap (@hfg) h₂
  | _, _, Option.Rel.some h => Forall₂.cons h (rel_filterMap (@hfg) h₂)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
⊢ SublistForall₂ R l₁ l₂ ↔ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
⊢ SublistForall₂ R l₁ l₂ → ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ l₂) → SublistForall₂ R l₁ l₂
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : SublistForall₂ R l₁ l₂
⊢ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
[PROOFSTEP]
induction' h with _ a b l1 l2 rab _ ih b l1 l2 _ ih
[GOAL]
case mp.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ l✝ : List β
⊢ ∃ l, Forall₂ R [] l ∧ l <+ l✝
[PROOFSTEP]
exact ⟨nil, Forall₂.nil, nil_sublist _⟩
[GOAL]
case mp.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
a : α
b : β
l1 : List α
l2 : List β
rab : R a b
a✝ : SublistForall₂ R l1 l2
ih : ∃ l, Forall₂ R l1 l ∧ l <+ l2
⊢ ∃ l, Forall₂ R (a :: l1) l ∧ l <+ b :: l2
[PROOFSTEP]
obtain ⟨l, hl1, hl2⟩ := ih
[GOAL]
case mp.cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
a : α
b : β
l1 : List α
l2 : List β
rab : R a b
a✝ : SublistForall₂ R l1 l2
l : List β
hl1 : Forall₂ R l1 l
hl2 : l <+ l2
⊢ ∃ l, Forall₂ R (a :: l1) l ∧ l <+ b :: l2
[PROOFSTEP]
refine' ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩
[GOAL]
case mp.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
b : β
l1 : List α
l2 : List β
a✝ : SublistForall₂ R l1 l2
ih : ∃ l, Forall₂ R l1 l ∧ l <+ l2
⊢ ∃ l, Forall₂ R l1 l ∧ l <+ b :: l2
[PROOFSTEP]
obtain ⟨l, hl1, hl2⟩ := ih
[GOAL]
case mp.cons_right.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
b : β
l1 : List α
l2 : List β
a✝ : SublistForall₂ R l1 l2
l : List β
hl1 : Forall₂ R l1 l
hl2 : l <+ l2
⊢ ∃ l, Forall₂ R l1 l ∧ l <+ b :: l2
[PROOFSTEP]
exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ l₂
[PROOFSTEP]
obtain ⟨l, hl1, hl2⟩ := h
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ l : List β
hl1 : Forall₂ R l₁ l
hl2 : l <+ l₂
⊢ SublistForall₂ R l₁ l₂
[PROOFSTEP]
revert l₁
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l : List β
hl2 : l <+ l₂
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ l → SublistForall₂ R l₁ l₂
[PROOFSTEP]
induction' hl2 with _ _ _ _ ih _ _ _ _ ih
[GOAL]
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l : List β
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ [] → SublistForall₂ R l₁ []
[PROOFSTEP]
intro l₁ hl1
[GOAL]
case mpr.intro.intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ (a✝¹ :: l₂✝)
[PROOFSTEP]
intro l₁ hl1
[GOAL]
case mpr.intro.intro.cons₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ (a✝¹ :: l₁✝) → SublistForall₂ R l₁ (a✝¹ :: l₂✝)
[PROOFSTEP]
intro l₁ hl1
[GOAL]
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R l₁ []
[PROOFSTEP]
rw [forall₂_nil_right_iff.1 hl1]
[GOAL]
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R [] []
[PROOFSTEP]
exact SublistForall₂.nil
[GOAL]
case mpr.intro.intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
l₁ : List α
hl1 : Forall₂ R l₁ l₁✝
⊢ SublistForall₂ R l₁ (a✝¹ :: l₂✝)
[PROOFSTEP]
exact SublistForall₂.cons_right (ih hl1)
[GOAL]
case mpr.intro.intro.cons₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
l₁ : List α
hl1 : Forall₂ R l₁ (a✝¹ :: l₁✝)
⊢ SublistForall₂ R l₁ (a✝¹ :: l₂✝)
[PROOFSTEP]
cases' hl1 with _ _ _ _ hr hl _
[GOAL]
case mpr.intro.intro.cons₂.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l l₁✝¹ l₂✝ : List β
a✝² : β
a✝¹ : l₁✝¹ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝¹ → SublistForall₂ R l₁ l₂✝
a✝ : α
l₁✝ : List α
hr : R a✝ a✝²
hl : Forall₂ R l₁✝ l₁✝¹
⊢ SublistForall₂ R (a✝ :: l₁✝) (a✝² :: l₂✝)
[PROOFSTEP]
exact SublistForall₂.cons hr (ih hl)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
a b c : List α
⊢ SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b c → SublistForall₂ Rₐ a c
[PROOFSTEP]
revert a b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
c : List α
⊢ ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b c → SublistForall₂ Rₐ a c
[PROOFSTEP]
induction' c with _ _ ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
⊢ ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b [] → SublistForall₂ Rₐ a []
[PROOFSTEP]
rintro _ _ h1 h2
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
a✝ b✝ : List α
h1 : SublistForall₂ Rₐ a✝ b✝
h2 : SublistForall₂ Rₐ b✝ []
⊢ SublistForall₂ Rₐ a✝ []
[PROOFSTEP]
cases h2
[GOAL]
case nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
a✝ : List α
h1 : SublistForall₂ Rₐ a✝ []
⊢ SublistForall₂ Rₐ a✝ []
[PROOFSTEP]
exact h1
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
⊢ ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b (head✝ :: tail✝) → SublistForall₂ Rₐ a (head✝ :: tail✝)
[PROOFSTEP]
rintro a b h1 h2
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a b : List α
h1 : SublistForall₂ Rₐ a b
h2 : SublistForall₂ Rₐ b (head✝ :: tail✝)
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
[PROOFSTEP]
cases' h2 with _ _ _ _ _ hbc tbc _ _ y1 btc
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
h1 : SublistForall₂ Rₐ a []
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
[PROOFSTEP]
cases h1
[GOAL]
case cons.nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
⊢ SublistForall₂ Rₐ [] (head✝ :: tail✝)
[PROOFSTEP]
exact SublistForall₂.nil
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
a₁✝ : α
l₁✝ : List α
h1 : SublistForall₂ Rₐ a (a₁✝ :: l₁✝)
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
[PROOFSTEP]
cases' h1 with _ _ _ _ _ hab tab _ _ _ atb
[GOAL]
case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a₁✝ : α
l₁✝ : List α
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
⊢ SublistForall₂ Rₐ [] (head✝ :: tail✝)
[PROOFSTEP]
exact SublistForall₂.nil
[GOAL]
case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a₁✝¹ : α
l₁✝¹ : List α
hbc : Rₐ a₁✝¹ head✝
tbc : SublistForall₂ Rₐ l₁✝¹ tail✝
a₁✝ : α
l₁✝ : List α
hab : Rₐ a₁✝ a₁✝¹
tab : SublistForall₂ Rₐ l₁✝ l₁✝¹
⊢ SublistForall₂ Rₐ (a₁✝ :: l₁✝) (head✝ :: tail✝)
[PROOFSTEP]
exact SublistForall₂.cons (_root_.trans hab hbc) (ih _ _ tab tbc)
[GOAL]
case cons.cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
a₁✝ : α
l₁✝ : List α
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
atb : SublistForall₂ Rₐ a l₁✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
[PROOFSTEP]
exact SublistForall₂.cons_right (ih _ _ atb tbc)
[GOAL]
case cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a b : List α
h1 : SublistForall₂ Rₐ a b
btc : SublistForall₂ Rₐ b tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
[PROOFSTEP]
exact SublistForall₂.cons_right (ih _ _ h1 btc)
