-- Mathlib/Data/List/Forall2.lean
theorem sublistForall₂_iff {l₁ : List α} {l₂ : List β} :
    SublistForall₂ R l₁ l₂ ↔ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

Proof state:
case mpr
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ l₂

Tactic:
obtain ⟨l, hl1, hl2⟩ := h

Result:
case mpr.intro.intro
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ l : List β
hl1 : Forall₂ R l₁ l
hl2 : l <+ l₂
⊢ SublistForall₂ R l₁ l₂

Proof state:
case mp.cons_right
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a✝¹ : β
l₁✝ : List α
l₂✝ : List β
a✝ : SublistForall₂ R l₁✝ l₂✝
ih : ∃ l, Forall₂ R l₁✝ l ∧ l <+ l₂✝
⊢ ∃ l, Forall₂ R l₁✝ l ∧ l <+ a✝¹ :: l₂✝

Tactic:
obtain ⟨l, hl1, hl2⟩ := ih

Result:
case mp.cons_right.intro.intro
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a✝¹ : β
l₁✝ : List α
l₂✝ : List β
a✝ : SublistForall₂ R l₁✝ l₂✝
l : List β
hl1 : Forall₂ R l₁✝ l
hl2 : l <+ l₂✝
⊢ ∃ l, Forall₂ R l₁✝ l ∧ l <+ a✝¹ :: l₂✝

Proof state:
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ [] → SublistForall₂ R l₁ []

Tactic:
intro l₁ hl1

Result:
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R l₁ []

Proof state:
case mpr.intro.intro.cons₂
α : Type u_1
β : Type u_2
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₂✝)

Tactic:
obtain - | ⟨hr, hl⟩ := hl1

Result:
case mpr.intro.intro.cons₂.cons
α : Type u_1
β : Type u_2
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₂✝)

Proof state:
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R [] []

Tactic:
exact SublistForall₂.nil

Result:
no goals

Proof state:
case mp.nil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ l✝ : List β
⊢ ∃ l, Forall₂ R [] l ∧ l <+ l✝

Tactic:
exact ⟨nil, Forall₂.nil, nil_sublist _⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : SublistForall₂ R l₁ l₂
⊢ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

Tactic:
induction h with
| nil => exact ⟨nil, Forall₂.nil, nil_sublist _⟩
| @cons a b l1 l2 rab _ ih =>
  obtain ⟨l, hl1, hl2⟩ := ih
  exact ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩
| cons_right _ ih =>
  obtain ⟨l, hl1, hl2⟩ := ih
  exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩

Result:
no goals

Proof state:
case mp.cons.intro.intro
α : Type u_1
β : Type u_2
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

Tactic:
exact ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩

Result:
no goals

Proof state:
case mpr.intro.intro.cons₂
α : Type u_1
β : Type u_2
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₂✝)

Tactic:
intro l₁ hl1

Result:
case mpr.intro.intro.cons₂
α : Type u_1
β : Type u_2
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₂✝)

Proof state:
case mp.cons
α : Type u_1
β : Type u_2
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

Tactic:
obtain ⟨l, hl1, hl2⟩ := ih

Result:
case mp.cons.intro.intro
α : Type u_1
β : Type u_2
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

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
⊢ SublistForall₂ R l₁ l₂ ↔ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u_1
β : Type u_2
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
R : α → β → Prop
l₁ : List α
l₂ : List β
h : ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ l₂

Proof state:
case mpr.intro.intro.cons
α : Type u_1
β : Type u_2
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₂✝)

Tactic:
exact SublistForall₂.cons_right (ih hl1)

Result:
no goals

Proof state:
case mpr.intro.intro.cons₂.cons
α : Type u_1
β : Type u_2
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₂✝)

Tactic:
exact SublistForall₂.cons hr (ih hl)

Result:
no goals

Proof state:
case mpr.intro.intro.cons
α : Type u_1
β : Type u_2
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₂✝)

Tactic:
intro l₁ hl1

Result:
case mpr.intro.intro.cons
α : Type u_1
β : Type u_2
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₂✝)

Proof state:
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R l₁ []

Tactic:
rw [forall₂_nil_right_iff.1 hl1]

Result:
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R [] []

Proof state:
case mp.cons_right.intro.intro
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a✝¹ : β
l₁✝ : List α
l₂✝ : List β
a✝ : SublistForall₂ R l₁✝ l₂✝
l : List β
hl1 : Forall₂ R l₁✝ l
hl2 : l <+ l₂✝
⊢ ∃ l, Forall₂ R l₁✝ l ∧ l <+ a✝¹ :: l₂✝

Tactic:
exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩

Result:
no goals

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ l : List β
hl1 : Forall₂ R l₁ l
hl2 : l <+ l₂
⊢ SublistForall₂ R l₁ l₂

Tactic:
revert l₁

Result:
case mpr.intro.intro
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
hl2 : l <+ l₂
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ l → SublistForall₂ R l₁ l₂

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
hl2 : l <+ l₂
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ l → SublistForall₂ R l₁ l₂

Tactic:
induction hl2 with
| slnil =>
  intro l₁ hl1
  rw [forall₂_nil_right_iff.1 hl1]
  exact SublistForall₂.nil
| cons _ _ ih => intro l₁ hl1; exact SublistForall₂.cons_right (ih hl1)
| cons₂ _ _ ih =>
  intro l₁ hl1
  obtain - | ⟨hr, hl⟩ := hl1
  exact SublistForall₂.cons hr (ih hl)

Result:
no goals