awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
l : List (List α)
hl : l.flatten ≠ []
hl' : l.getLast ⋯ ≠ []
⊢ l.flatten.getLast hl = (l.getLast ⋯).getLast hl'

Tactic:
(getLast_getLast_eq_getLast_flatten ..).symm

Premises used: List.getLast_getLast_eq_getLast_flatten, Eq.symm
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
h : Forall₂ R l₁ l₂
nil : Forall₂ S [] []
cons :
  ∀ {a : α} {b : β} {l₁ : List α} {l₂ : List β},
    R a b → Forall₂ R l₁ l₂ → Forall₂ S l₁ l₂ → Forall₂ S (a :: l₁) (b :: l₂)
⊢ Forall₂ S l₁ l₂

Tactic:
induction h
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
⊢ Forall₂ S [] []

Tactic:
constructor
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a : α
b : β
l₁_1 : List α
l₂_1 : List β
h : R a b
h_1 : Forall₂ R l₁_1 l₂_1
a_ih : Forall₂ S l₁_1 l₂_1
cons : S a b
cons₁ : Forall₂ S l₁_1 l₂_1
⊢ Forall₂ S (a :: l₁_1) (b :: l₂_1)

Tactic:
constructor
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a : α
b : β
l₁_1 : List α
l₂_1 : List β
h : R a b
h_1 : Forall₂ R l₁_1 l₂_1
a_ih : Forall₂ S l₁_1 l₂_1
⊢ S a b

Tactic:
solve_by_elim
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a : α
b : β
l₁_1 : List α
l₂_1 : List β
h : R a b
h_1 : Forall₂ R l₁_1 l₂_1
a_ih : Forall₂ S l₁_1 l₂_1
⊢ Forall₂ S l₁_1 l₂_1

Tactic:
solve_by_elim
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
Rₐ : α → α → Prop
⊢ Forall₂ Rₐ [] [] ↔ ∀ (x : α), Membership.mem (γ := List α) [] x → Rₐ x x

Tactic:
simp
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
Rₐ : α → α → Prop
a : α
l : List α
⊢ Forall₂ Rₐ (a :: l) (a :: l) ↔ ∀ (x : α), x ∈ a :: l → Rₐ x x

Tactic:
simp [@forall₂_same l]
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
Rₐ : α → α → Prop
inst : Std.Refl Rₐ
l : List α
⊢ Forall₂ Rₐ l l

Tactic:
forall₂_same.2 fun _ _ => refl _

Premises used: Iff.mpr, List.forall₂_same, refl
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
h : ∀ (a b : List α), Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b = (a = b)
⊢ Eq.{u_1 + 1} (α := List α → List α → Prop) (Forall₂ fun (x1 x2 : α) ↦ x1 = x2) Eq

Tactic:
funext a b
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
a b : List α
h : Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b ↔ a = b
⊢ Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b = (a = b)

Tactic:
apply propext

Premises used: propext
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
a b : List α
h : Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b → a = b
h₁ : a = b → Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b
⊢ Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b ↔ a = b

Tactic:
constructor
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
a b : List α
h : Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b
h₁ : Eq.{u_1 + 1} (α := List α) [] []
h₂ : ∀ {a b : α} {l₁ l₂ : List α}, a = b → Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) l₁ l₂ → l₁ = l₂ → a :: l₁ = b :: l₂
⊢ a = b

Tactic:
induction h
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
a b : List α
⊢ Eq.{u_1 + 1} (α := List α) [] []

Tactic:
rfl
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
a b : List α
a_1 b_1 : α
l₁ l₂ : List α
h : a_1 = b_1
h_1 : Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) l₁ l₂
a_ih : l₁ = l₂
⊢ a_1 :: l₁ = b_1 :: l₂

Tactic:
simp only [*]
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
a : List α
⊢ Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a a

Tactic:
forall₂_refl _

Premises used: List.forall₂_refl
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
a : List α
⊢ Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a a

Tactic:
exact forall₂_refl _

Premises used: List.forall₂_refl
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List β
H : Forall₂ R [] l
nil : Eq.{u_2 + 1} (α := List β) [] []
⊢ l = []

Tactic:
cases H
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ Eq.{u_2 + 1} (α := List β) [] []

Tactic:
rfl
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ Forall₂ R [] []

Tactic:
Forall₂.nil

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

Tactic:
exact Forall₂.nil

Premises used: List.Forall₂.nil
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
H : Forall₂ R l []
nil : Eq.{u_1 + 1} (α := List α) [] []
⊢ l = []

Tactic:
cases H
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ Eq.{u_1 + 1} (α := List α) [] []

Tactic:
rfl
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l : List α
u : List β
⊢ Forall₂ R (a :: l) u ↔ ∃ (b : β), ∃ (u' : List β), R a b ∧ Forall₂ R l u' ∧ u = b :: u'

Tactic:
Iff.intro
    (fun h =>
      match u, h with
      | b :: u', Forall₂.cons h₁ h₂ => ⟨b, u', h₁, h₂, rfl⟩)
    fun h =>
    match u, h with
    | _, ⟨_, _, h₁, h₂, rfl⟩ => Forall₂.cons h₁ h₂

Premises used: List.Forall₂.cons, Exists, List.cons, And, _private.0.List.forall₂_cons_left_iff.match_2, And.intro, _private.0.List.forall₂_cons_left_iff.match_1, Iff.intro, Exists.intro, List.Forall₂, Eq, rfl
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
b : β
l : List β
u : List α
⊢ Forall₂ R u (b :: l) ↔ ∃ (a : α), ∃ (u' : List α), R a b ∧ Forall₂ R u' l ∧ u = a :: u'

Tactic:
Iff.intro
    (fun h =>
      match u, h with
      | b :: u', Forall₂.cons h₁ h₂ => ⟨b, u', h₁, h₂, rfl⟩)
    fun h =>
    match u, h with
    | _, ⟨_, _, h₁, h₂, rfl⟩ => Forall₂.cons h₁ h₂

Premises used: List.Forall₂.cons, _private.0.List.forall₂_cons_right_iff.match_1, Exists, List.cons, And, _private.0.List.forall₂_cons_right_iff.match_2, And.intro, Iff.intro, Exists.intro, List.Forall₂, Eq, rfl
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Prop
u : List β
⊢ Forall₂ (fun (a : α) (b : β) ↦ p a ∧ R a b) [] u ↔
    (∀ (a : α), Membership.mem (γ := List α) [] a → p a) ∧ Forall₂ R [] u

Tactic:
simp only [forall₂_nil_left_iff, forall_prop_of_false not_mem_nil, imp_true_iff, true_and]

Premises used: List.forall₂_nil_left_iff, forall_prop_of_false, imp_true_iff, List.not_mem_nil, true_and
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Prop
a : α
l : List α
u : List β
simp :
  (p a ∧ ∃ (x : β), R a x ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ (x_1 : List β), Forall₂ R l x_1 ∧ u = x :: x_1) ↔
    p a ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ (b : β), R a b ∧ ∃ (x : List β), Forall₂ R l x ∧ u = b :: x
⊢ 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

Tactic:
simp only [forall₂_and_left l, forall₂_cons_left_iff, forall_mem_cons, and_assoc,
      exists_and_left]

Premises used: exists_and_left, List.forall_mem_cons, and_assoc, List.forall₂_cons_left_iff
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Prop
a : α
l : List α
u : List β
⊢ (p a ∧ ∃ (x : β), R a x ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ (x_1 : List β), Forall₂ R l x_1 ∧ u = x :: x_1) ↔
    p a ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ (b : β), R a b ∧ ∃ (x : List β), Forall₂ R l x ∧ u = b :: x

Tactic:
simp only [and_comm, and_assoc, ← exists_and_right]

Premises used: and_comm, exists_and_right, and_assoc
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → α
x : List β
⊢ Forall₂ R (map f []) x ↔ Forall₂ (fun (c : γ) (b : β) ↦ R (f c) b) [] x

Tactic:
simp only [map, forall₂_nil_left_iff]

Premises used: List.map, List.forall₂_nil_left_iff
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
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

Tactic:
simp only [map, forall₂_cons_left_iff, forall₂_map_left_iff]

Premises used: List.map, List.forall₂_cons_left_iff
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
x : List α
⊢ Forall₂ R x (map f []) ↔ Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) x []

Tactic:
simp only [map, forall₂_nil_right_iff]

Premises used: List.map, List.forall₂_nil_right_iff
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
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)

Tactic:
simp only [map, forall₂_cons_right_iff, forall₂_map_right_iff]

Premises used: List.map, List.forall₂_cons_right_iff
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
hr : LeftUnique R
⊢ LeftUnique (Forall₂ R)

Tactic:
@left_unique_forall₂' _ _ _ hr

Premises used: List.left_unique_forall₂', Relator.LeftUnique
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
hr : RightUnique R
⊢ RightUnique (Forall₂ R)

Tactic:
@right_unique_forall₂' _ _ _ hr

Premises used: Relator.RightUnique, List.right_unique_forall₂'
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
hr : BiUnique R
⊢ BiUnique (Forall₂ R)

Tactic:
⟨hr.left.forall₂, hr.right.forall₂⟩

Premises used: Relator.RightUnique.forall₂, Relator.LeftUnique.forall₂, And.right, And.left, And.intro, Relator.BiUnique
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
⊢ Forall₂ R l₁ l₂ ↔
    l₁.length = l₂.length ∧
      ∀ (i : ℕ) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
        R (l₁.get (⟨i, h₁⟩ : Fin l₁.length)) (l₂.get (⟨i, h₂⟩ : Fin l₂.length))

Tactic:
⟨fun h => ⟨h.length_eq, h.get⟩, fun h => forall₂_of_length_eq_of_get h.1 h.2⟩

Premises used: List.forall₂_of_length_eq_of_get, And.right, And.left, And.intro, Iff.intro, List.Forall₂.get, List.Forall₂.length_eq
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
b : β
l₁ : List α
l₂ : List β
h₁ : R a b
h₂ : Forall₂ R l₁ l₂
x : α
y : β
hx : (x, y) ∈ (a :: l₁).zip (b :: l₂)
⊢ (x, y) = (a, b) ∨ (x, y) ∈ zipWith Prod.mk l₁ l₂

Tactic:
rw [zip, zipWith, mem_cons] at hx

Premises used: List.zipWith, List.zip, List.mem_cons
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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

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

Tactic:
exact h₁
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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_1 : β
x_2 : α
h₃ : (x, y) ∈ zipWith Prod.mk l₁ l₂
h₁ : R x_2 x_1
⊢ R x y

Tactic:
forall₂_zip h₂ h₃
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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_1 : β
x_2 : α
h₃ : (x, y) ∈ zipWith Prod.mk l₁ l₂
h₁ : R x_2 x_1
⊢ R x y

Tactic:
exact forall₂_zip h₂ h₃
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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

Tactic:
match hx with
    | Or.inl rfl => exact h₁
    | Or.inr h₃ => exact forall₂_zip h₂ h₃
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : l₁.length = l₂.length ∧ ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
⊢ l₁.length = l₂.length

Tactic:
obtain ⟨h₁, h₂⟩ := h
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : l₁.length = l₂.length ∧ ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
h₁ : l₁.length = l₂.length
⊢ ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b

Tactic:
obtain ⟨h₁, h₂⟩ := h
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ : List β
h₁ : length.{u_1} (α := α) [] = l₂.length
h₂ : ∀ {a : α} {b : β}, Membership.mem (γ := List (α × β)) (zip [] l₂) (a, b) → R a b
nil :
  ∀ (h₁ : length.{u_1} (α := α) [] = length.{u_2} (α := β) [])
    (h₂ : ∀ {a : α} {b : β}, Membership.mem (γ := List (α × β)) (zip [] []) (a, b) → R a b), Forall₂ R [] []
⊢ Forall₂ R [] l₂

Tactic:
cases length_eq_zero_iff.1 h₁.symm

Premises used: Iff.mp, Eq.symm, List.length_eq_zero_iff
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
h₁ : length.{u_1} (α := α) [] = length.{u_2} (α := β) []
h₂ : ∀ {a : α} {b : β}, Membership.mem (γ := List (α × β)) (zip [] []) (a, b) → R a b
⊢ Forall₂ R [] []

Tactic:
constructor
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b), Forall₂ R l₁ l₂
l₂ : List β
h₁ : (a :: l₁).length = l₂.length
h₂ : ∀ {a_1 : α} {b : β}, (a_1, b) ∈ (a :: l₁).zip l₂ → R a_1 b
cons :
  ∀ (h₁ : (a :: l₁).length = length.{u_2} (α := β) [])
    (h₂ : ∀ {a_1 : α} {b : β}, Membership.mem (γ := List (α × β)) ((a :: l₁).zip []) (a_1, b) → R a_1 b),
    Forall₂ R (a :: l₁) []
cons₁ :
  ∀ (b : β) (l₂ : List β) (h₁ : (a :: l₁).length = (b :: l₂).length)
    (h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1), Forall₂ R (a :: l₁) (b :: l₂)
⊢ Forall₂ R (a :: l₁) l₂

Tactic:
rcases l₂ with - | ⟨b, l₂⟩
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b), Forall₂ R l₁ l₂
h₁ : (a :: l₁).length = length.{u_2} (α := β) []
h₂ : ∀ {a_1 : α} {b : β}, Membership.mem (γ := List (α × β)) ((a :: l₁).zip []) (a_1, b) → R a_1 b
⊢ Forall₂ R (a :: l₁) []

Tactic:
simp at h₁
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b), Forall₂ R l₁ l₂
b : β
l₂ : List β
h₁ : (a :: l₁).length = (b :: l₂).length
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
⊢ l₁.length = l₂.length

Tactic:
simp only [length_cons, succ.injEq] at h₁

Premises used: Nat.succ.injEq, List.length_cons
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b), Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
h₁ : l₁.length = l₂.length
⊢ (a, b) ∈ (a :: l₁).zip (b :: l₂)

Tactic:
simp [zip]

Premises used: List.zip
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b), Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_2 : α} {b_2 : β}, (a_2, b_2) ∈ (a :: l₁).zip (b :: l₂) → R a_2 b_2
h₁ : l₁.length = l₂.length
a_1 : α
b_1 : β
h : (a_1, b_1) ∈ l₁.zip l₂
simp : a_1 = a ∧ b_1 = b ∨ (a_1, b_1) ∈ zipWith Prod.mk l₁ l₂
⊢ (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂)

Tactic:
simp only [zip, zipWith, mem_cons, Prod.mk.injEq]

Premises used: List.zipWith, List.zip, Prod.mk.injEq, List.mem_cons
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b), Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_2 : α} {b_2 : β}, (a_2, b_2) ∈ (a :: l₁).zip (b :: l₂) → R a_2 b_2
h₁ : l₁.length = l₂.length
a_1 : α
b_1 : β
h : (a_1, b_1) ∈ l₁.zip l₂
h₃ : (a_1, b_1) ∈ zipWith Prod.mk l₁ l₂
⊢ a_1 = a ∧ b_1 = b ∨ (a_1, b_1) ∈ zipWith Prod.mk l₁ l₂

Tactic:
right
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b), Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_2 : α} {b_2 : β}, (a_2, b_2) ∈ (a :: l₁).zip (b :: l₂) → R a_2 b_2
h₁ : l₁.length = l₂.length
a_1 : α
b_1 : β
h : (a_1, b_1) ∈ l₁.zip l₂
⊢ (a_1, b_1) ∈ zipWith Prod.mk l₁ l₂

Tactic:
simpa [zip] using h

Premises used: List.zip
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b), Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
h₁ : l₁.length = l₂.length
⊢ Forall₂ R (a :: l₁) (b :: l₂)

Tactic:
exact Forall₂.cons (h₂ <| by simp [zip])
          (IH h₁ fun h => h₂ <| by
            simp only [zip, zipWith, mem_cons, Prod.mk.injEq]; right
            simpa [zip] using h)

Premises used: List.Forall₂.cons
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h₁ : l₁.length = l₂.length
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
nil :
  ∀ {l₂ : List β} (h₁ : length.{u_1} (α := α) [] = l₂.length)
    (h₂ : ∀ {a : α} {b : β}, Membership.mem (γ := List (α × β)) (zip [] l₂) (a, b) → R a b), Forall₂ R [] l₂
cons :
  ∀ (a : α) (l₁ : List α)
    (IH :
      ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b),
        Forall₂ R l₁ l₂)
    {l₂ : List β} (h₁ : (a :: l₁).length = l₂.length) (h₂ : ∀ {a_1 : α} {b : β}, (a_1, b) ∈ (a :: l₁).zip l₂ → R a_1 b),
    Forall₂ R (a :: l₁) l₂
⊢ Forall₂ R l₁ l₂

Tactic:
induction l₁ generalizing l₂ with
    | nil =>
      cases length_eq_zero_iff.1 h₁.symm
      constructor
    | cons a l₁ IH =>
      rcases l₂ with - | ⟨b, l₂⟩
      · simp at h₁
      · 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, mem_cons, Prod.mk.injEq]; right
            simpa [zip] using h)

Premises used: Nat.succ.injEq, List.length_cons, List.cons, Iff.mp, List.length_eq_zero_iff, List.nil
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
x : List α
x_1 : List β
h : Forall₂ R x x_1
⊢ Forall₂ R (take 0 x) (take 0 x_1)

Tactic:
simp only [Forall₂.nil, take]

Premises used: List.Forall₂.nil, List.take
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
n : ℕ
⊢ Forall₂ R (take (n + 1) []) (take (n + 1) [])

Tactic:
simp only [Forall₂.nil, take]

Premises used: List.Forall₂.nil, List.take
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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₂))

Tactic:
simp [And.intro h₁ h₂, forall₂_take n]

Premises used: And.intro
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
x : List α
x_1 : List β
h : Forall₂ R x x_1
⊢ Forall₂ R (drop 0 x) (drop 0 x_1)

Tactic:
simp only [drop, h]

Premises used: List.drop
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
n : ℕ
⊢ Forall₂ R (drop (n + 1) []) (drop (n + 1) [])

Tactic:
simp only [Forall₂.nil, drop]

Premises used: List.Forall₂.nil, List.drop
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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₂))

Tactic:
simp [And.intro h₁ h₂, forall₂_drop n]

Premises used: And.intro
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (take l₁.length l) (take l₁.length (l₁ ++ l₂))

Tactic:
have h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂)) :=
    forall₂_take (length l₁) h
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (take l₁.length l) (take l₁.length (l₁ ++ l₂))
rwa rwa₁ rwa₂ rwa₃ : ∀ (h' : Forall₂ R (take l₁.length l) l₁), Forall₂ R (take l₁.length l) l₁
⊢ Forall₂ R (take l₁.length l) l₁

Tactic:
rwa [take_left] at h'

Premises used: List.take_left
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (drop l₁.length l) (drop l₁.length (l₁ ++ l₂))

Tactic:
have h' : Forall₂ R (drop (length l₁) l) (drop (length l₁) (l₁ ++ l₂)) :=
    forall₂_drop (length l₁) h
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (drop l₁.length l) (drop l₁.length (l₁ ++ l₂))
rwa rwa₁ rwa₂ rwa₃ : ∀ (h' : Forall₂ R (drop l₁.length l) l₂), Forall₂ R (drop l₁.length l) l₂
⊢ Forall₂ R (drop l₁.length l) l₂

Tactic:
rwa [drop_left] at h'

Premises used: List.drop_left
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
hr : BiUnique R
a : α
b : β
h : R a b
⊢ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) a [] ↔ (fun (x1 : β) (x2 : List β) ↦ x1 ∈ x2) b []

Tactic:
simp only [not_mem_nil]

Premises used: List.not_mem_nil
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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
simp : a = a' ∨ a ∈ as ↔ b = b' ∨ b ∈ bs
⊢ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) a (a' :: as) ↔ (fun (x1 : β) (x2 : List β) ↦ x1 ∈ x2) b (b' :: bs)

Tactic:
simp only [mem_cons]

Premises used: List.mem_cons
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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

Tactic:
rel_or (rel_eq hr h h₁) (rel_mem hr h h₂)

Premises used: Relator.rel_or, Relator.rel_eq
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
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

Tactic:
exact rel_or (rel_eq hr h h₁) (rel_mem hr h h₂)

Premises used: Relator.rel_or, Relator.rel_eq
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
b : β
l₁ : List α
l₂ : List β
h₁ : R a b
h₂ : Forall₂ R l₁ l₂
simp : Forall₂ R (l₁.reverse ++ [a]) (l₂.reverse ++ [b])
⊢ Forall₂ R (a :: l₁).reverse (b :: l₂).reverse

Tactic:
simp only [reverse_cons]

Premises used: List.reverse_cons
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
b : β
l₁ : List α
l₂ : List β
h₁ : R a b
h₂ : Forall₂ R l₁ l₂
⊢ Forall₂ R (l₁.reverse ++ [a]) (l₂.reverse ++ [b])

Tactic:
rel_append (rel_reverse h₂) (Forall₂.cons h₁ Forall₂.nil)

Premises used: List.Forall₂.cons, List.Forall₂.nil, List.rel_append
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
b : β
l₁ : List α
l₂ : List β
h₁ : R a b
h₂ : Forall₂ R l₁ l₂
⊢ Forall₂ R (l₁.reverse ++ [a]) (l₂.reverse ++ [b])

Tactic:
exact rel_append (rel_reverse h₂) (Forall₂.cons h₁ Forall₂.nil)

Premises used: List.Forall₂.cons, List.Forall₂.nil, List.rel_append