awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
nil : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, [] = l₁ ++ a :: b :: l₂ → R a b) → IsChain R []
singleton : ∀ (x : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, [x] = l₁ ++ a :: b :: l₂ → R a b) → IsChain R [x]
cons_cons :
  ∀ (head head' : α) (tail : List α),
    ((∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail) →
      ∀
        (ih :
          ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)),
        (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b) →
          IsChain R (head :: head' :: tail)
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b) → IsChain R l

Tactic:
induction l using twoStepInduction with
  | nil | singleton => grind
  | cons_cons head head' tail _ ih =>
    refine fun h ↦ isChain_cons_cons.mpr ⟨h (nil_append _).symm, ih _ fun ⦃a b l₁ l₂⦄ eq => ?_⟩
    apply h
    rw [eq, cons_append]

Premises used: List.head, List.tail, Singleton.singleton, List.cons_append, List.nil
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b) → IsChain R l

Tactic:
induction l using twoStepInduction with
  | nil | singleton => grind
  | cons_cons head head' tail _ ih =>
    refine fun h ↦ isChain_cons_cons.mpr ⟨h (nil_append _).symm, ih _ fun ⦃a b l₁ l₂⦄ eq => ?_⟩
    apply h
    rw [eq, cons_append]

Premises used: List.head, List.tail, Singleton.singleton, List.cons_append, List.nil
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
nil : IsChain R [] ↔ Forall₂ R (dropLast []) (tail [])
singleton : ∀ (x : α), IsChain R [x] ↔ Forall₂ R [x].dropLast [x].tail
cons_cons :
  ∀ (x y : α) (xs : List α),
    (IsChain R xs ↔ Forall₂ R xs.dropLast xs.tail) →
      (∀ (y : α), IsChain R (y :: xs) ↔ Forall₂ R (y :: xs).dropLast (y :: xs).tail) →
        (IsChain R (x :: y :: xs) ↔ Forall₂ R (x :: y :: xs).dropLast (x :: y :: xs).tail)
⊢ IsChain R l ↔ Forall₂ R l.dropLast l.tail

Tactic:
induction l using twoStepInduction
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
⊢ IsChain R [] ↔ Forall₂ R (dropLast []) (tail [])

Tactic:
simp_all
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
x : α
⊢ IsChain R [x] ↔ Forall₂ R [x].dropLast [x].tail

Tactic:
simp_all
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
x y : α
xs : List α
h : IsChain R xs ↔ Forall₂ R xs.dropLast xs.tail
h_1 : ∀ (y : α), IsChain R (y :: xs) ↔ Forall₂ R (y :: xs).dropLast (y :: xs).tail
⊢ IsChain R (x :: y :: xs) ↔ Forall₂ R (x :: y :: xs).dropLast (x :: y :: xs).tail

Tactic:
simp_all
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
a : α
nil : IsChain R [a] ↔ Eq.{u + 1} (α := List α) [] [] ∨ Forall₂ R (a :: dropLast []) []
cons :
  ∀ (head : α) (tail : List α),
    IsChain R (a :: head :: tail) ↔ head :: tail = [] ∨ Forall₂ R (a :: (head :: tail).dropLast) (head :: tail)
⊢ IsChain R (a :: l) ↔ l = [] ∨ Forall₂ R (a :: l.dropLast) l

Tactic:
cases l
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
a : α
⊢ IsChain R [a] ↔ Eq.{u + 1} (α := List α) [] [] ∨ Forall₂ R (a :: dropLast []) []

Tactic:
simp [isChain_iff_forall₂]

Premises used: List.isChain_iff_forall₂
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
a head : α
tail : List α
⊢ IsChain R (a :: head :: tail) ↔ head :: tail = [] ∨ Forall₂ R (a :: (head :: tail).dropLast) (head :: tail)

Tactic:
simp [isChain_iff_forall₂]

Premises used: List.isChain_iff_forall₂
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
a b : α
simp_rw : Forall₂ R (a :: l ++ [b]).dropLast (a :: l ++ [b]).tail ↔ Forall₂ R (a :: l) (l ++ [b])
simp_rw₁ : Forall₂ R (a :: l) (a :: l ++ [b]).tail ↔ Forall₂ R (a :: l) (l ++ [b])
simp_rw₂ : Forall₂ R (a :: l) (a :: (l ++ [b])).tail ↔ Forall₂ R (a :: l) (l ++ [b])
⊢ IsChain R (a :: l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b])

Tactic:
simp_rw [isChain_iff_forall₂, dropLast_concat, cons_append, tail_cons]

Premises used: List.isChain_iff_forall₂, List.tail_cons, List.dropLast_concat, List.cons_append
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
R : α → α → Prop
f : β → α
l : List β
nil : IsChain R (map f []) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) []
singleton : ∀ (x : β), IsChain R (map f [x]) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) [x]
cons_cons :
  ∀ (x y : β) (xs : List β),
    (IsChain R (map f xs) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) xs) →
      (∀ (y : β), IsChain R (map f (y :: xs)) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) (y :: xs)) →
        (IsChain R (map f (x :: y :: xs)) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) (x :: y :: xs))
⊢ IsChain R (map f l) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) l

Tactic:
induction l using twoStepInduction
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
R : α → α → Prop
f : β → α
⊢ IsChain R (map f []) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) []

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
R : α → α → Prop
f : β → α
x : β
⊢ IsChain R (map f [x]) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) [x]

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
R : α → α → Prop
f : β → α
x y : β
xs : List β
h : IsChain R (map f xs) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) xs
h_1 : ∀ (y : β), IsChain R (map f (y :: xs)) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) (y :: xs)
⊢ IsChain R (map f (x :: y :: xs)) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) (x :: y :: xs)

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
f : α → β
H : ∀ (a b : α), S (f a) (f b) → R a b
l : List α
p : IsChain S (map f l)
⊢ IsChain R l

Tactic:
((isChain_map f).1 p).imp H

Premises used: List.isChain_map, Iff.mp, List.IsChain.imp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
f : α → β
H : ∀ (a b : α), R a b → S (f a) (f b)
l : List α
p : IsChain R l
⊢ IsChain S (map f l)

Tactic:
(isChain_map f).2 <| p.imp H

Premises used: Iff.mpr, List.isChain_map, List.IsChain.imp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
R : α → α → Prop
f : β → α
l : List β
b : β
⊢ IsChain R (f b :: map f l) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) (b :: l)

Tactic:
isChain_map f (l := b :: l)

Premises used: List.map, List.isChain_map
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
R : α → α → Prop
a : α
S : β → β → Prop
f : α → β
H : ∀ (a b : α), S (f a) (f b) → R a b
l : List α
p : IsChain S (f a :: map f l)
⊢ IsChain R (a :: l)

Tactic:
((isChain_cons_map f).1 p).imp H

Premises used: List.isChain_cons_map, Iff.mp, List.IsChain.imp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
R : α → α → Prop
a : α
S : β → β → Prop
f : α → β
H : ∀ (a b : α), R a b → S (f a) (f b)
l : List α
p : IsChain R (a :: l)
⊢ IsChain S (f a :: map f l)

Tactic:
(isChain_cons_map f).2 <| p.imp H

Premises used: Iff.mpr, List.isChain_cons_map, List.IsChain.imp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
nil :
  ∀ (hl : ∀ (a : α), Membership.mem (γ := List α) [] a → p a),
    IsChain S (pmap (P := p) f [] hl) ↔ IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) []
singleton :
  ∀ (x : α) (hl : ∀ (a : α), a ∈ [x] → p a),
    IsChain S (pmap (P := p) f [x] hl) ↔ IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) [x]
cons_cons :
  ∀ (x y : α) (xs : List α),
    (∀ (hl : ∀ (a : α), a ∈ xs → p a),
        IsChain S (pmap (P := p) f xs hl) ↔
          IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) xs) →
      (∀ (y : α) (hl : ∀ (a : α), a ∈ y :: xs → p a),
          IsChain S (pmap (P := p) f (y :: xs) hl) ↔
            IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) (y :: xs)) →
        ∀ (hl : ∀ (a : α), a ∈ x :: y :: xs → p a),
          IsChain S (pmap (P := p) f (x :: y :: xs) hl) ↔
            IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) (x :: y :: xs)
⊢ IsChain S (pmap (P := p) f l hl) ↔ IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) l

Tactic:
induction l using twoStepInduction
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
hl : ∀ (a : α), Membership.mem (γ := List α) [] a → p a
⊢ IsChain S (pmap (P := p) f [] hl) ↔ IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) []

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
x : α
hl : ∀ (a : α), a ∈ [x] → p a
⊢ IsChain S (pmap (P := p) f [x] hl) ↔ IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) [x]

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
x y : α
xs : List α
h :
  ∀ (hl : ∀ (a : α), a ∈ xs → p a),
    IsChain S (pmap (P := p) f xs hl) ↔ IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) xs
h_1 :
  ∀ (y : α) (hl : ∀ (a : α), a ∈ y :: xs → p a),
    IsChain S (pmap (P := p) f (y :: xs) hl) ↔
      IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) (y :: xs)
hl : ∀ (a : α), a ∈ x :: y :: xs → p a
⊢ IsChain S (pmap (P := p) f (x :: y :: xs) hl) ↔
    IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) (x :: y :: xs)

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
l : List α
hl₁ : IsChain R l
hl₂ : ∀ (a : α), a ∈ l → p a
⊢ ∀ (a b : α), a ∈ l → b ∈ l → R a b → ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁ : ∀ (a : α), a ∈ l → p a
hl₂ : IsChain S (pmap (P := p) f l hl₁)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
⊢ ∀ ⦃a b : α⦄, (∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) → R a b

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
l : List β
hl : ∀ (b : β), b ∈ l → p b
a : β
ha : p a
⊢ ∀ (a_1 : β), a_1 ∈ a :: l → p a_1

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
l : List α
a : α
ha : p a
hl₁ : IsChain R (a :: l)
hl₂ : ∀ (a : α), a ∈ l → p a
⊢ ∀ (a_1 b : α), a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → ∃ (ha : p a_1), ∃ (hb : p b), S (f a_1 ha) (f b hb)

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁ : ∀ (a : α), a ∈ l → p a
a : α
ha : p a
hl₂ : IsChain S (f a ha :: pmap (P := p) f l hl₁)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
⊢ ∀ ⦃a b : α⦄, (∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) → R a b

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
inst : Trans R R R
hl : IsChain R l₂
h : l₁ <+ l₂
rw : ∀ (hl : Pairwise R l₂) (h : l₁ <+ l₂), Pairwise R l₁
⊢ IsChain R l₁

Tactic:
rw [isChain_iff_pairwise] at hl ⊢

Premises used: List.isChain_iff_pairwise
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
inst : Trans R R R
hl : Pairwise R l₂
h : l₁ <+ l₂
⊢ Pairwise R l₁

Tactic:
hl.sublist h

Premises used: List.Pairwise.sublist
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
inst : Trans R R R
hl : Pairwise R l₂
h : l₁ <+ l₂
⊢ Pairwise R l₁

Tactic:
exact hl.sublist h

Premises used: List.Pairwise.sublist
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
a b : α
inst : Trans R R R
hl : IsChain R (a :: l)
hb : b ∈ l
⊢ Pairwise R (a :: l)

Tactic:
rw [isChain_iff_pairwise] at hl

Premises used: List.isChain_iff_pairwise
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
a b : α
inst : Trans R R R
hl : IsChain R (a :: l)
hb : b ∈ l
hl₁ : Pairwise R (a :: l)
⊢ b ∈ l

Tactic:
rw [isChain_iff_pairwise] at hl

Premises used: List.isChain_iff_pairwise
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
a b : α
inst : Trans R R R
hl : Pairwise R (a :: l)
hb : b ∈ l
⊢ R a b

Tactic:
rel_of_pairwise_cons hl hb

Premises used: List.rel_of_pairwise_cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
a b : α
inst : Trans R R R
hl : Pairwise R (a :: l)
hb : b ∈ l
⊢ R a b

Tactic:
exact rel_of_pairwise_cons hl hb

Premises used: List.rel_of_pairwise_cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
h : IsChain R l
⊢ IsChain R l.tail

Tactic:
grind +splitIndPred
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
x y : α
l : List α
h : IsChain R (x :: y :: l)
⊢ R x y

Tactic:
List.rel_of_isChain_cons_cons h

Premises used: List.rel_of_isChain_cons_cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
x : α
l : List α
h : IsChain R (x :: l)
y : α
hy : y ∈ l.head?
⊢ IsChain R (x :: y :: l.tail)

Tactic:
rw [← cons_head?_tail hy] at h

Premises used: List.cons_head?_tail
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
x : α
l : List α
h : IsChain R (x :: l)
y : α
hy : y ∈ l.head?
h₁ : IsChain R (x :: y :: l.tail)
⊢ y ∈ l.head?

Tactic:
rw [← cons_head?_tail hy] at h

Premises used: List.cons_head?_tail
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
x : α
l : List α
y : α
h : IsChain R (x :: y :: l.tail)
hy : y ∈ l.head?
⊢ R x y

Tactic:
h.rel_head

Premises used: List.IsChain.rel_head
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
x : α
l : List α
y : α
h : IsChain R (x :: y :: l.tail)
hy : y ∈ l.head?
⊢ R x y

Tactic:
exact h.rel_head

Premises used: List.IsChain.rel_head
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
x : α
l : List α
l_ne_nil : l ≠ []
hl : IsChain R l
h : R x (l.head l_ne_nil)
⊢ IsChain R (x :: l)

Tactic:
grind +splitIndPred
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
x : α
l : List α
⊢ IsChain R (x :: l) ↔ (∀ (y : α), y ∈ l.head? → R x y) ∧ IsChain R l

Tactic:
⟨fun h => ⟨h.rel_head?, h.tail⟩, fun ⟨h₁, h₂⟩ => h₂.cons h₁⟩

Premises used: List.IsChain.rel_head?, List.IsChain, List.IsChain.cons, _private.0.List.isChain_cons.match_1, List.IsChain.tail, List.cons, And.intro, Iff.intro
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
⊢ IsChain R ([] ++ l) ↔
    IsChain R [] ∧
      IsChain R l ∧ ∀ (x : α), Membership.mem (γ := Option α) (getLast? []) x → ∀ (y : α), y ∈ l.head? → R x y

Tactic:
simp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
a : α
l : List α
⊢ IsChain R ([a] ++ l) ↔ IsChain R [a] ∧ IsChain R l ∧ ∀ (x : α), x ∈ [a].getLast? → ∀ (y : α), y ∈ l.head? → R x y

Tactic:
simp [isChain_cons, and_comm]

Premises used: and_comm, List.isChain_cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
a b : α
l₁ l₂ : List α
rw :
  (R a b ∧ IsChain R (b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
    R a b ∧
      IsChain R (b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y
⊢ IsChain R (a :: b :: l₁ ++ l₂) ↔
    IsChain R (a :: b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y

Tactic:
rw [cons_append, cons_append, isChain_cons_cons, isChain_cons_cons,
      ← cons_append, isChain_append, and_assoc]

Premises used: List.isChain_cons_cons, and_assoc, List.cons_append
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ (R a b ∧ IsChain R (b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
    R a b ∧
      IsChain R (b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y

Tactic:
simp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
h₁ : IsChain R l₁
h₂ : IsChain R l₂
h : ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y
⊢ IsChain R (l₁ ++ l₂)

Tactic:
isChain_append.2 ⟨h₁, h₂, h⟩

Premises used: Iff.mpr, List.isChain_append, And.intro
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
h : IsChain R (l₁ ++ l₂)
⊢ IsChain R l₁

Tactic:
(isChain_append.1 h).1

Premises used: List.isChain_append, And.left, Iff.mp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
h : IsChain R (l₁ ++ l₂)
⊢ IsChain R l₂

Tactic:
(isChain_append.1 h).2.1

Premises used: List.isChain_append, And.right, And.left, Iff.mp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l l₁ : List α
h : IsChain R l
h' : l₁ <:+: l
rcases : ∀ (l₂ l₃ : List α) (h : IsChain R (l₂ ++ l₁ ++ l₃)), IsChain R l₁
⊢ IsChain R l₁

Tactic:
rcases h' with ⟨l₂, l₃, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ l₃ : List α
h : IsChain R (l₂ ++ l₁ ++ l₃)
⊢ IsChain R l₁

Tactic:
h.left_of_append.right_of_append

Premises used: List.IsChain.left_of_append, List.IsChain.right_of_append
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ l₃ : List α
h : IsChain R (l₂ ++ l₁ ++ l₃)
⊢ IsChain R l₁

Tactic:
exact h.left_of_append.right_of_append

Premises used: List.IsChain.left_of_append, List.IsChain.right_of_append
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l l₁ : List α
h : IsChain R l
h' : l₁ <:+ l
⊢ IsChain R l₁

Tactic:
h.infix h'.isInfix

Premises used: List.IsChain.infix, List.IsSuffix.isInfix
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l l₁ : List α
h : IsChain R l
h' : l₁ <+: l
⊢ IsChain R l₁

Tactic:
h.infix h'.isInfix

Premises used: List.IsChain.infix, List.IsPrefix.isInfix
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
h : IsChain R l
n : ℕ
⊢ IsChain R (List.drop n l)

Tactic:
h.suffix (drop_suffix _ _)

Premises used: List.drop_suffix, List.IsChain.suffix
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
h : IsChain R l
⊢ IsChain R l.dropLast

Tactic:
h.prefix l.dropLast_prefix

Premises used: List.IsChain.prefix, List.dropLast_prefix
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
h : IsChain R l
n : ℕ
⊢ IsChain R (List.take n l)

Tactic:
h.prefix (take_prefix _ _)

Premises used: List.take_prefix, List.IsChain.prefix
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
x y : α
h : ∀ {z : α}, R x z → R y z
l : List α
hl : IsChain R (x :: l)
⊢ IsChain R (y :: l)

Tactic:
IsChain.cons_of_imp @h hl

Premises used: List.IsChain.cons_of_imp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
⊢ ∀ {l : List α}, IsChain R l ↔ ∀ (i : Fin l.length.pred), R (l.get (Fin.cast ⋯ i.castSucc)) (l.get (Fin.cast ⋯ i.succ))

Tactic:
simp [isChain_iff_getElem, Fin.forall_iff, Nat.lt_sub_iff_add_lt]

Premises used: Nat.lt_sub_iff_add_lt, Fin.forall_iff, List.isChain_iff_getElem
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
a : α
l : List α
⊢ IsChain R (a :: l) ↔ ∀ (i : Fin l.length), R ((a :: l).get i.castSucc) ((a :: l).get i.succ)

Tactic:
simp only [isChain_iff_getElem, length_cons, Fin.forall_iff, Nat.add_lt_add_iff_right,
    getElem_cons_succ, Fin.castSucc_mk, get_eq_getElem, Fin.succ_mk]

Premises used: List.length_cons, List.get_eq_getElem, Fin.succ_mk, Fin.forall_iff, List.isChain_iff_getElem, Nat.add_lt_add_iff_right, Fin.castSucc_mk, List.getElem_cons_succ
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
h : ¬IsChain R l
⊢ ∃ (n : ℕ),
    ∃ (h : n + 1 < l.length),
      ¬R (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯)
          (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (n + 1) h)

Tactic:
simp_all [isChain_iff_getElem]

Premises used: List.isChain_iff_getElem
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
⊢ IsChain R (reverse []) ↔ IsChain (fun (a b : α) ↦ R b a) []

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
a : α
⊢ IsChain R [a].reverse ↔ IsChain (fun (a b : α) ↦ R b a) [a]

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun (a b : α) ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (y :: l)
cons_cons : IsChain R (a :: b :: l).reverse ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₁ : IsChain R ((b :: l).reverse ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₂ : IsChain R (l.reverse ++ [b] ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₃ : IsChain R (l.reverse ++ ([b] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₄ : IsChain R (l.reverse ++ b :: ([] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₅ : IsChain R (l.reverse ++ [b, a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₆ : IsChain R (l.reverse ++ [b]) ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₇ : IsChain R (b :: l).reverse ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₈ :
  IsChain (fun (a b : α) ↦ R b a) (b :: l) ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₉ :
  IsChain R [b, a] ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₁₀ cons_cons₁₁ :
  R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
⊢ IsChain R (a :: b :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (a :: b :: l)

Tactic:
rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      isChain_split, ← reverse_cons, IH2, and_comm, isChain_pair]

Premises used: List.isChain_pair, List.append_assoc, and_comm, List.isChain_cons_cons, List.reverse_cons, List.isChain_split, List.nil_append, List.cons_append
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
nil : IsChain R (reverse []) ↔ IsChain (fun (a b : α) ↦ R b a) []
singleton : ∀ (a : α), IsChain R [a].reverse ↔ IsChain (fun (a b : α) ↦ R b a) [a]
cons_cons :
  ∀ (a b : α) (l : List α) (IH : IsChain R l.reverse ↔ IsChain (fun (a b : α) ↦ R b a) l)
    (IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (y :: l)),
    IsChain R (a :: b :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (a :: b :: l)
⊢ IsChain R l.reverse ↔ IsChain (fun (a b : α) ↦ R b a) l

Tactic:
induction l using twoStepInduction with
  | nil => grind
  | singleton a => grind
  | cons_cons a b l IH IH2 =>
    rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      isChain_split, ← reverse_cons, IH2, and_comm, isChain_pair]

Premises used: List.isChain_pair, List.append_assoc, and_comm, List.isChain_cons_cons, List.reverse_cons, List.isChain_split, List.nil_append, Singleton.singleton, List.cons_append, List.nil
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ l₃ : List α
h₁ : IsChain R (l₁ ++ l₂)
h₂ : IsChain R (l₂ ++ l₃)
hn : l₂ ≠ []
⊢ ∀ (x : α), x ∈ (l₁ ++ l₂).getLast? → ∀ (y : α), y ∈ l₃.head? → R x y

Tactic:
simpa only [getLast?_append_of_ne_nil _ hn] using (isChain_append.1 h₂).2.2

Premises used: List.isChain_append, List.getLast?_append_of_ne_nil, And.right, Iff.mp