awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
rw : Forall₂ R l₁.reverse.reverse l₂.reverse.reverse
⊢ Forall₂ R l₁ l₂

Tactic:
rw [← reverse_reverse l₁, ← reverse_reverse l₂]

Premises used: List.reverse_reverse
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
⊢ Forall₂ R l₁.reverse.reverse l₂.reverse.reverse

Tactic:
rel_reverse h

Premises used: List.rel_reverse
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
⊢ Forall₂ R l₁.reverse.reverse l₂.reverse.reverse

Tactic:
exact rel_reverse h

Premises used: List.rel_reverse
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : α → β → Prop
P : γ → δ → Prop
⊢ (Forall₂ R ⇒ (R ⇒ Forall₂ P) ⇒ Forall₂ P) (swap (φ := fun (a : α → List γ) (a_1 : List α) ↦ List γ) flatMap)
    (swap (φ := fun (a : β → List δ) (a_1 : List β) ↦ List δ) flatMap)

Tactic:
fun _ _ h₁ _ _ h₂ => rel_flatten (rel_map (@h₂) h₁)

Premises used: List.rel_map, List.rel_flatten, Relator.LiftFun
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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
pos : ∀ (h : p a = true), Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
neg : ∀ (h : ¬p a = true), Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))

Tactic:
by_cases h : p a
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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 rwa rwa₁ rwa₂ rwa₃ : p a = true
⊢ q b = true

Tactic:
rwa [← hpq h₁]
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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

Tactic:
have : q b := by rwa [← hpq h₁]
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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))

Tactic:
simp only [filter_cons_of_pos h, filter_cons_of_pos this, forall₂_cons, h₁, true_and,
        rel_filter hpq h₂]

Premises used: List.filter_cons_of_pos, List.forall₂_cons, true_and
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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 rwa rwa₁ rwa₂ rwa₃ : ¬p a = true
⊢ ¬q b = true

Tactic:
rwa [← hpq h₁]
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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

Tactic:
have : ¬q b := by rwa [← hpq h₁]
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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))

Tactic:
simp only [filter_cons_of_neg h, filter_cons_of_neg this, rel_filter hpq h₂]

Premises used: List.filter_cons_of_neg
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : α → β → Prop
P : γ → δ → 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
rw :
  Forall₂ P
    (match (motive := Option γ → List γ) f a with
    | none => filterMap f as
    | some b => b :: filterMap f as)
    (match (motive := Option δ → List δ) g b with
    | none => filterMap g bs
    | some b => b :: filterMap g bs)
⊢ Forall₂ P (filterMap f (a :: as)) (filterMap g (b :: bs))

Tactic:
rw [filterMap_cons, filterMap_cons]

Premises used: List.filterMap_cons
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : α → β → Prop
P : γ → δ → 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 (motive := Option γ → List γ) f a with
    | none => filterMap f as
    | some b => b :: filterMap f as)
    (match (motive := Option δ → List δ) g b with
    | none => filterMap g bs
    | some b => b :: filterMap g bs)

Tactic:
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₂)

Premises used: List.Forall₂.cons, List.filterMap.match_1, List.cons, List, List.Forall₂, _private.0.List.rel_filterMap.match_2, List.filterMap
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : α → β → Prop
P : γ → δ → 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 (motive := Option γ → List γ) f a with
    | none => filterMap f as
    | some b => b :: filterMap f as)
    (match (motive := Option δ → List δ) g b with
    | none => filterMap g bs
    | some b => b :: filterMap g bs)

Tactic:
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₂)
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
mp : SublistForall₂ R l₁ l₂ → ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂
mpr : (∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂) → SublistForall₂ R l₁ l₂
⊢ SublistForall₂ R l₁ l₂ ↔ ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂

Tactic:
constructor
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ l : List β
⊢ ∃ (l_1 : List β), Forall₂ R [] l_1 ∧ l_1 <+ l

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

Premises used: List.Forall₂.nil, And.intro, Exists.intro, List.nil_sublist, List.nil
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ l : List β
⊢ ∃ (l_1 : List β), Forall₂ R [] l_1 ∧ l_1 <+ l

Tactic:
exact ⟨nil, Forall₂.nil, nil_sublist _⟩
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a : α
b : β
l1 : List α
l2 : List β
rab : R a b
h : SublistForall₂ R l1 l2
ih : ∃ (l : List β), Forall₂ R l1 l ∧ l <+ l2
mp : ∀ (l : List β) (hl1 : Forall₂ R l1 l) (hl2 : l <+ l2), ∃ (l : List β), Forall₂ R (a :: l1) l ∧ l <+ b :: l2
⊢ ∃ (l : List β), Forall₂ R (a :: l1) l ∧ l <+ b :: l2

Tactic:
obtain ⟨l, hl1, hl2⟩ := ih
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a : α
b : β
l1 : List α
l2 : List β
rab : R a b
h : SublistForall₂ R l1 l2
l : List β
hl1 : Forall₂ R l1 l
hl2 : l <+ l2
⊢ ∃ (l : List β), Forall₂ R (a :: l1) l ∧ l <+ b :: l2

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

Premises used: List.Forall₂.cons, List.Sublist.cons_cons, List.cons, And.intro, Exists.intro
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a : α
b : β
l1 : List α
l2 : List β
rab : R a b
h : SublistForall₂ R l1 l2
l : List β
hl1 : Forall₂ R l1 l
hl2 : l <+ l2
⊢ ∃ (l : List β), Forall₂ R (a :: l1) l ∧ l <+ b :: l2

Tactic:
exact ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a : β
l₁_1 : List α
l₂_1 : List β
h : SublistForall₂ R l₁_1 l₂_1
ih : ∃ (l : List β), Forall₂ R l₁_1 l ∧ l <+ l₂_1
mp : ∀ (l : List β) (hl1 : Forall₂ R l₁_1 l) (hl2 : l <+ l₂_1), ∃ (l : List β), Forall₂ R l₁_1 l ∧ l <+ a :: l₂_1
⊢ ∃ (l : List β), Forall₂ R l₁_1 l ∧ l <+ a :: l₂_1

Tactic:
obtain ⟨l, hl1, hl2⟩ := ih
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a : β
l₁_1 : List α
l₂_1 : List β
h : SublistForall₂ R l₁_1 l₂_1
l : List β
hl1 : Forall₂ R l₁_1 l
hl2 : l <+ l₂_1
⊢ ∃ (l : List β), Forall₂ R l₁_1 l ∧ l <+ a :: l₂_1

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

Premises used: And.intro, List.Sublist.trans, Exists.intro, List.Sublist.refl, List.Sublist.cons
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a : β
l₁_1 : List α
l₂_1 : List β
h : SublistForall₂ R l₁_1 l₂_1
l : List β
hl1 : Forall₂ R l₁_1 l
hl2 : l <+ l₂_1
⊢ ∃ (l : List β), Forall₂ R l₁_1 l ∧ l <+ a :: l₂_1

Tactic:
exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : SublistForall₂ R l₁ l₂
mp : ∀ {l : List β}, ∃ (l_1 : List β), Forall₂ R [] l_1 ∧ l_1 <+ l
mp₁ :
  ∀ {a : α} {b : β} {l1 : List α} {l2 : List β} (rab : R a b),
    SublistForall₂ R l1 l2 →
      ∀ (ih : ∃ (l : List β), Forall₂ R l1 l ∧ l <+ l2), ∃ (l : List β), Forall₂ R (a :: l1) l ∧ l <+ b :: l2
mp₂ :
  ∀ {a : β} {l₁ : List α} {l₂ : List β},
    SublistForall₂ R l₁ l₂ →
      ∀ (ih : ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂), ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ a :: l₂
⊢ ∃ (l : List β), 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 _))⟩

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂
mpr : ∀ (l : List β) (hl1 : Forall₂ R l₁ l) (hl2 : l <+ l₂), SublistForall₂ R l₁ l₂
⊢ SublistForall₂ R l₁ l₂

Tactic:
obtain ⟨l, hl1, hl2⟩ := h
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ l : List β
hl1 : Forall₂ R l₁ l
hl2 : l <+ l₂
mpr : ∀ {l₁ : List α} (hl1 : Forall₂ R l₁ l), SublistForall₂ R l₁ l₂
⊢ SublistForall₂ R l₁ l₂

Tactic:
revert l₁
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
mpr : SublistForall₂ R [] []
⊢ SublistForall₂ R l₁ []

Tactic:
rw [forall₂_nil_right_iff.1 hl1]

Premises used: Iff.mp, List.forall₂_nil_right_iff
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R [] []

Tactic:
SublistForall₂.nil

Premises used: List.SublistForall₂.nil
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R [] []

Tactic:
exact SublistForall₂.nil

Premises used: List.SublistForall₂.nil
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁_1 l₂_1 : List β
a : β
h : l₁_1 <+ l₂_1
ih : ∀ {l₁ : List α} (hl1 : Forall₂ R l₁ l₁_1), SublistForall₂ R l₁ l₂_1
l₁ : List α
hl1 : Forall₂ R l₁ l₁_1
⊢ SublistForall₂ R l₁ (a :: l₂_1)

Tactic:
SublistForall₂.cons_right (ih hl1)

Premises used: List.SublistForall₂.cons_right
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁_1 l₂_1 : List β
a : β
h : l₁_1 <+ l₂_1
ih : ∀ {l₁ : List α} (hl1 : Forall₂ R l₁ l₁_1), SublistForall₂ R l₁ l₂_1
l₁ : List α
hl1 : Forall₂ R l₁ l₁_1
⊢ SublistForall₂ R l₁ (a :: l₂_1)

Tactic:
exact SublistForall₂.cons_right (ih hl1)

Premises used: List.SublistForall₂.cons_right
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁_1 l₂_1 : List β
a : β
h : l₁_1 <+ l₂_1
ih : ∀ {l₁ : List α} (hl1 : Forall₂ R l₁ l₁_1), SublistForall₂ R l₁ l₂_1
l₁ : List α
hl1 : Forall₂ R l₁ (a :: l₁_1)
mpr : ∀ {a_1 : α} {l₁ : List α} (hr : R a_1 a) (hl : Forall₂ R l₁ l₁_1), SublistForall₂ R (a_1 :: l₁) (a :: l₂_1)
⊢ SublistForall₂ R l₁ (a :: l₂_1)

Tactic:
obtain - | ⟨hr, hl⟩ := hl1
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁ l₂_1 : List β
a : β
h : l₁ <+ l₂_1
ih : ∀ {l₁_2 : List α} (hl1 : Forall₂ R l₁_2 l₁), SublistForall₂ R l₁_2 l₂_1
a_1 : α
l₁_1 : List α
hr : R a_1 a
hl : Forall₂ R l₁_1 l₁
⊢ SublistForall₂ R (a_1 :: l₁_1) (a :: l₂_1)

Tactic:
SublistForall₂.cons hr (ih hl)

Premises used: List.SublistForall₂.cons
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁ l₂_1 : List β
a : β
h : l₁ <+ l₂_1
ih : ∀ {l₁_2 : List α} (hl1 : Forall₂ R l₁_2 l₁), SublistForall₂ R l₁_2 l₂_1
a_1 : α
l₁_1 : List α
hr : R a_1 a
hl : Forall₂ R l₁_1 l₁
⊢ SublistForall₂ R (a_1 :: l₁_1) (a :: l₂_1)

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

Premises used: List.SublistForall₂.cons
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
hl2 : l <+ l₂
mpr : ∀ {l₁ : List α} (hl1 : Forall₂ R l₁ []), SublistForall₂ R l₁ []
mpr₁ :
  ∀ {l₁ l₂ : List β} (a : β),
    l₁ <+ l₂ →
      ∀ (ih : ∀ {l₁_1 : List α} (hl1 : Forall₂ R l₁_1 l₁), SublistForall₂ R l₁_1 l₂) {l₁_1 : List α}
        (hl1 : Forall₂ R l₁_1 l₁), SublistForall₂ R l₁_1 (a :: l₂)
mpr₂ :
  ∀ {l₁ l₂ : List β} (a : β),
    l₁ <+ l₂ →
      ∀ (ih : ∀ {l₁_1 : List α} (hl1 : Forall₂ R l₁_1 l₁), SublistForall₂ R l₁_1 l₂) {l₁_1 : List α}
        (hl1 : Forall₂ R l₁_1 (a :: l₁)), SublistForall₂ R l₁_1 (a :: l₂)
⊢ ∀ {l₁ : List α} (hl1 : 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_cons _ _ ih =>
      intro l₁ hl1
      obtain - | ⟨hr, hl⟩ := hl1
      exact SublistForall₂.cons hr (ih hl)

Premises used: List.cons, List.SublistForall₂.nil
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst : Std.Refl Rₐ
⊢ Std.Refl (SublistForall₂ Rₐ)

Tactic:
⟨fun l => sublistForall₂_iff.2 ⟨l, forall₂_refl l, Sublist.refl l⟩⟩

Premises used: Iff.mpr, Std.Refl.mk, List.forall₂_refl, And.intro, List.sublistForall₂_iff, Exists.intro, List.Sublist.refl
-- Module: Mathlib.Data.List.Forall2
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 α
revert : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b c → SublistForall₂ Rₐ a c
⊢ SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b c → SublistForall₂ Rₐ a c

Tactic:
revert a b
-- Module: Mathlib.Data.List.Forall2
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 : List α
h1 : SublistForall₂ Rₐ a b
h2 : SublistForall₂ Rₐ b []
⊢ SublistForall₂ Rₐ a []

Tactic:
cases h2
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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 []

Tactic:
h1
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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 []

Tactic:
exact h1
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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)
cons : ∀ (h1 : SublistForall₂ Rₐ a []), SublistForall₂ Rₐ a (head :: tail)
cons₁ :
  ∀ {a₁ : α} {l₁ : List α} (h1 : SublistForall₂ Rₐ a (a₁ :: l₁)) (hbc : Rₐ a₁ head) (tbc : SublistForall₂ Rₐ l₁ tail),
    SublistForall₂ Rₐ a (head :: tail)
cons₂ : ∀ (btc : SublistForall₂ Rₐ b tail), SublistForall₂ Rₐ a (head :: tail)
⊢ SublistForall₂ Rₐ a (head :: tail)

Tactic:
obtain - | ⟨hbc, tbc⟩ | btc := h2
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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 []
cons : SublistForall₂ Rₐ [] (head :: tail)
⊢ SublistForall₂ Rₐ a (head :: tail)

Tactic:
cases h1
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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)

Tactic:
SublistForall₂.nil

Premises used: List.SublistForall₂.nil
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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)

Tactic:
exact SublistForall₂.nil

Premises used: List.SublistForall₂.nil
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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
cons : SublistForall₂ Rₐ [] (head :: tail)
cons₁ :
  ∀ {a₁_1 : α} {l₁_1 : List α} (hab : Rₐ a₁_1 a₁) (tab : SublistForall₂ Rₐ l₁_1 l₁),
    SublistForall₂ Rₐ (a₁_1 :: l₁_1) (head :: tail)
cons₂ : ∀ (atb : SublistForall₂ Rₐ a l₁), SublistForall₂ Rₐ a (head :: tail)
⊢ SublistForall₂ Rₐ a (head :: tail)

Tactic:
obtain - | ⟨hab, tab⟩ | atb := h1
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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)

Tactic:
SublistForall₂.nil

Premises used: List.SublistForall₂.nil
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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)

Tactic:
exact SublistForall₂.nil

Premises used: List.SublistForall₂.nil
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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₁_1 : α
l₁_1 : List α
hab : Rₐ a₁_1 a₁
tab : SublistForall₂ Rₐ l₁_1 l₁
⊢ SublistForall₂ Rₐ (a₁_1 :: l₁_1) (head :: tail)

Tactic:
SublistForall₂.cons (_root_.trans hab hbc) (ih _ _ tab tbc)

Premises used: List.SublistForall₂.cons, trans
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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₁_1 : α
l₁_1 : List α
hab : Rₐ a₁_1 a₁
tab : SublistForall₂ Rₐ l₁_1 l₁
⊢ SublistForall₂ Rₐ (a₁_1 :: l₁_1) (head :: tail)

Tactic:
exact SublistForall₂.cons (_root_.trans hab hbc) (ih _ _ tab tbc)

Premises used: List.SublistForall₂.cons, trans
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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)

Tactic:
SublistForall₂.cons_right (ih _ _ atb tbc)

Premises used: List.SublistForall₂.cons_right
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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)

Tactic:
exact SublistForall₂.cons_right (ih _ _ atb tbc)

Premises used: List.SublistForall₂.cons_right
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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)

Tactic:
SublistForall₂.cons_right (ih _ _ h1 btc)

Premises used: List.SublistForall₂.cons_right
-- Module: Mathlib.Data.List.Forall2
Goal:
α : 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)

Tactic:
exact SublistForall₂.cons_right (ih _ _ h1 btc)

Premises used: List.SublistForall₂.cons_right
-- Module: Mathlib.Data.List.Forall2
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 α
nil : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b [] → SublistForall₂ Rₐ a []
cons :
  ∀ (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)
⊢ ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b c → SublistForall₂ Rₐ a c

Tactic:
induction c with
    | nil =>
      rintro _ _ h1 h2
      cases h2
      exact h1
    | cons _ _ ih =>
      rintro a b h1 h2
      obtain - | ⟨hbc, tbc⟩ | btc := h2
      · cases h1
        exact SublistForall₂.nil
      · obtain - | ⟨hab, tab⟩ | atb := h1
        · exact SublistForall₂.nil
        · exact SublistForall₂.cons (_root_.trans hab hbc) (ih _ _ tab tbc)
        · exact SublistForall₂.cons_right (ih _ _ atb tbc)
      · exact SublistForall₂.cons_right (ih _ _ h1 btc)

Premises used: List.SublistForall₂.cons, List.SublistForall₂.nil