case mp
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : SublistForall₂ R l₁ l₂
⊢ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ l₂
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
⊢ SublistForall₂ R l₁ l₂ ↔ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
constructor <;> intro h
case mp.nil
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ l✝ : List β
⊢ ∃ l, Forall₂ R [] l ∧ l <+ l✝

case mp.cons
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
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

case mp.cons_right
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
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
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : SublistForall₂ R l₁ l₂
⊢ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
induction' h with _ a b l1 l2 rab _ ih b l1 l2 _ ih
no goals
case mp.nil
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ l✝ : List β
⊢ ∃ l, Forall₂ R [] l ∧ l <+ l✝
exact ⟨nil, Forall₂.nil, nil_sublist _⟩
case mp.cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
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
case mp.cons
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
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
obtain ⟨l, hl1, hl2⟩ := ih
no goals
case mp.cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
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
refine' ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩
case mp.cons_right.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
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
case mp.cons_right
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
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
obtain ⟨l, hl1, hl2⟩ := ih
no goals
case mp.cons_right.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
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
exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ l : List β
hl1 : Forall₂ R l₁ l
hl2 : l <+ l₂
⊢ SublistForall₂ R l₁ l₂
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ l₂
obtain ⟨l, hl1, hl2⟩ := h
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l : List β
hl2 : l <+ l₂
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ l → SublistForall₂ R l₁ l₂
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ l : List β
hl1 : Forall₂ R l₁ l
hl2 : l <+ l₂
⊢ SublistForall₂ R l₁ l₂
revert l₁
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R l₁ []

case mpr.intro.intro.cons
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
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₂✝)

case mpr.intro.intro.cons₂
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
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₂✝)
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l : List β
hl2 : l <+ l₂
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ l → SublistForall₂ R l₁ l₂
induction' hl2 with _ _ _ _ ih _ _ _ _ ih <;> intro l₁ hl1
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R [] []
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R l₁ []
rw [forall₂_nil_right_iff.1 hl1]
no goals
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R [] []
exact SublistForall₂.nil
no goals
case mpr.intro.intro.cons
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
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₂✝)
exact SublistForall₂.cons_right (ih hl1)
case mpr.intro.intro.cons₂.cons
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
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₂✝)
case mpr.intro.intro.cons₂
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
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₂✝)
cases' hl1 with _ _ _ _ hr hl _
no goals
case mpr.intro.intro.cons₂.cons
α : Type u_1
β : Type u_2
γ : Type ?u.158809
δ : Type ?u.158812
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₂✝)
exact SublistForall₂.cons hr (ih hl)