awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
inst : BEq ι
inst_1 : LawfulBEq ι
a : ι
l : List ι
IH :
  ∀ {i : ℕ} (hi : i < l.length),
    l.erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l i hi) ~ l.eraseIdx i
n : ℕ
hi : n + 1 < (a :: l).length
⊢ (a :: l).erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) (a :: l) (n + 1) hi) ~
    (a :: l).eraseIdx (n + 1)

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
inst : BEq ι
inst_1 : LawfulBEq ι
a : ι
l : List ι
IH :
  ∀ {i : ℕ} (hi : i < l.length),
    l.erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l i hi) ~ l.eraseIdx i
i : ℕ
hi : i < (a :: l).length
cons :
  ∀ (hi : 0 < (a :: l).length),
    (a :: l).erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) (a :: l) 0 hi) ~ (a :: l).eraseIdx 0
cons₁ :
  ∀ (n : ℕ) (hi : n + 1 < (a :: l).length),
    (a :: l).erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) (a :: l) (n + 1) hi) ~
      (a :: l).eraseIdx (n + 1)
⊢ (a :: l).erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) (a :: l) i hi) ~ (a :: l).eraseIdx i

Tactic:
cases i with grind
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
inst : BEq ι
inst_1 : LawfulBEq ι
l : List ι
i : ℕ
hi : i < l.length
nil :
  ∀ {i : ℕ} (hi : i < length.{u_1} (α := ι) []),
    List.erase [] (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) [] i hi) ~ eraseIdx [] i
cons :
  ∀ (a : ι) (l : List ι)
    (IH :
      ∀ {i : ℕ} (hi : i < l.length),
        l.erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l i hi) ~ l.eraseIdx i)
    {i : ℕ} (hi : i < (a :: l).length),
    (a :: l).erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) (a :: l) i hi) ~ (a :: l).eraseIdx i
⊢ l.erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l i hi) ~ l.eraseIdx i

Tactic:
induction l generalizing i with
  | nil => simp
  | cons a l IH => cases i with grind

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
l : List ι
i : ℕ
h : i < l.length
⊢ (l.eraseIdx i).length + 1 = l.length

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
finj : Injective f
l₁ l₂ : List α
⊢ map f (l₁.diff l₂) = (map f l₁).diff (map f l₂)

Tactic:
simp only [diff_eq_foldl, foldl_map, map_foldl_erase finj]

Premises used: List.diff_eq_foldl, List.map_foldl_erase, List.foldl_map
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Prop
inst : DecidablePred p
l : List α
hp : ∃ (a : α), a ∈ l ∧ p a
⊢ choose p l hp ∈ l ∧ p (choose p l hp)

Tactic:
(chooseX p l hp).property

Premises used: List.choose, List.chooseX, Subtype.property
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Prop
inst : DecidablePred p
l : List α
hp : ∃ (a : α), a ∈ l ∧ p a
⊢ choose p l hp ∈ l

Tactic:
(choose_spec _ _ _).1

Premises used: And.left, List.choose_spec
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Prop
inst : DecidablePred p
l : List α
hp : ∃ (a : α), a ∈ l ∧ p a
⊢ p (choose p l hp)

Tactic:
(choose_spec _ _ _).2

Premises used: And.right, List.choose_spec
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Prop
ys : List α
⊢ Forall p ([] ++ ys) ↔ Forall p [] ∧ Forall p ys

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Prop
ys : List α
head : α
tail : List α
⊢ Forall p (head :: tail ++ ys) ↔ Forall p (head :: tail) ∧ Forall p ys

Tactic:
simp [forall_append, and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Prop
x : α
l : List α
rw : Forall p (x :: l) ↔ p x ∧ ∀ (x : α), x ∈ l → p x
rw₁ : p x ∧ Forall p l ↔ p x ∧ ∀ (x : α), x ∈ l → p x
rw₂ rw₃ : (p x ∧ ∀ (x : α), x ∈ l → p x) ↔ p x ∧ ∀ (x : α), x ∈ l → p x
⊢ Forall p (x :: l) ↔ ∀ (x_1 : α), x_1 ∈ x :: l → p x_1

Tactic:
rw [forall_mem_cons, forall_cons, forall_iff_forall_mem]

Premises used: List.forall_cons, List.forall_mem_cons
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
simp : p x → Forall p l → q x ∧ Forall q l
⊢ Forall p (x :: l) → Forall q (x :: l)

Tactic:
simp only [forall_cons, and_imp]

Premises used: and_imp, List.forall_cons
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
rw : p x ∧ Forall p l → q x ∧ Forall q l
⊢ p x → Forall p l → q x ∧ Forall q l

Tactic:
rw [← and_imp]

Premises used: and_imp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x ∧ Forall p l → q x ∧ Forall q l

Tactic:
And.imp (h x) (Forall.imp h)

Premises used: And.imp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x ∧ Forall p l → q x ∧ Forall q l

Tactic:
exact And.imp (h x) (Forall.imp h)

Premises used: And.imp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
nil : Forall p (map f []) ↔ Forall (p ∘ f) []
cons :
  ∀ (head : α) (tail : List α),
    (Forall p (map f tail) ↔ Forall (p ∘ f) tail) → (Forall p (map f (head :: tail)) ↔ Forall (p ∘ f) (head :: tail))
⊢ Forall p (map f l) ↔ Forall (p ∘ f) l

Tactic:
induction l
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
⊢ Forall p (map f []) ↔ Forall (p ∘ f) []

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
head : α
tail : List α
tail_ih : Forall p (map f tail) ↔ Forall (p ∘ f) tail
⊢ Forall p (map f (head :: tail)) ↔ Forall (p ∘ f) (head :: tail)

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
i : Fin l.attach.length
⊢ (↑(l.attach.get i) : α) = l.get ⟨(↑i : ℕ), ⋯⟩

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
simp : ∀ ⦃a : β⦄, (∃ (a_1 : α), ∃ (h : a_1 ∈ s), f a_1 ⋯ = a) → (∃ (a_2 : α), ∃ (h : a_2 ∈ t), f a_2 ⋯ = a) → False
⊢ (pmap (P := p) f s hs).Disjoint (pmap (P := p) f t ht)

Tactic:
simp only [Disjoint, mem_pmap]

Premises used: List.Disjoint, List.mem_pmap
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
a : α
ha : a ∈ s
a' : α
ha' : a' ∈ t
ha'' : f a' ⋯ = f a ⋯
apply : a ∈ t
⊢ False

Tactic:
apply h ha
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
a : α
ha : a ∈ s
a' : α
ha' : a' ∈ t
ha'' : f a' ⋯ = f a ⋯
rwa rwa₁ rwa₂ rwa₃ : a' ∈ t
⊢ a ∈ t

Tactic:
rwa [hf a a' (hs a ha) (ht a' ha') ha''.symm]

Premises used: Eq.symm
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t : List α
hf : Injective f
h : s.Disjoint t
rw :
  Disjoint.{v} (α := β) (pmap (P := fun (x : α) ↦ True) (fun (a : α) (x : True) ↦ f a) s ⋯)
    (pmap (P := fun (x : α) ↦ True) (fun (a : α) (x : True) ↦ f a) t ⋯)
⊢ (map f s).Disjoint (map f t)

Tactic:
rw [← pmap_eq_map (fun _ _ ↦ trivial), ← pmap_eq_map (fun _ _ ↦ trivial)]

Premises used: trivial, List.pmap_eq_map
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t : List α
hf : Injective f
h : s.Disjoint t
⊢ Disjoint.{v} (α := β) (pmap (P := fun (x : α) ↦ True) (fun (a : α) (x : True) ↦ f a) s ⋯)
    (pmap (P := fun (x : α) ↦ True) (fun (a : α) (x : True) ↦ f a) t ⋯)

Tactic:
disjoint_pmap _ _ (fun _ _ _ _ h' ↦ hf h') h

Premises used: List.disjoint_pmap
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t : List α
hf : Injective f
h : s.Disjoint t
⊢ Disjoint.{v} (α := β) (pmap (P := fun (x : α) ↦ True) (fun (a : α) (x : True) ↦ f a) s ⋯)
    (pmap (P := fun (x : α) ↦ True) (fun (a : α) (x : True) ↦ f a) t ⋯)

Tactic:
exact disjoint_pmap _ _ (fun _ _ _ _ h' ↦ hf h') h

Premises used: List.disjoint_pmap
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t : List α
h : (List.map f s).Disjoint (List.map f t)
⊢ s.Disjoint t

Tactic:
fun _a has hat ↦
  h (mem_map_of_mem has) (mem_map_of_mem hat)

Premises used: List.Disjoint, List.mem_map_of_mem
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t : List α
hf : Injective f
⊢ (List.map f s).Disjoint (List.map f t) ↔ s.Disjoint t

Tactic:
⟨fun h ↦ h.of_map, fun h ↦ h.map hf⟩

Premises used: List.Disjoint.of_map, Iff.intro, List.Disjoint.map
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
simp_rw : (∀ ⦃a : α⦄, a ∈ l₁ → ¬a ∈ l) ↔ ∀ ⦃a : α⦄, a ∈ l₂ → ¬a ∈ l
⊢ l.Disjoint l₁ ↔ l.Disjoint l₂

Tactic:
simp_rw [List.disjoint_right, p.mem_iff]

Premises used: List.disjoint_right, List.Perm.mem_iff
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
⊢ l₁.reverse.Disjoint l₂ ↔ l₁.Disjoint l₂

Tactic:
reverse_perm _ |>.disjoint_left

Premises used: List.Perm.disjoint_left, List.reverse_perm
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
⊢ l₁.Disjoint l₂.reverse ↔ l₁.Disjoint l₂

Tactic:
reverse_perm _ |>.disjoint_right

Premises used: List.Perm.disjoint_right, List.reverse_perm
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
f : α → β
a : α
h : Membership.mem (γ := List α) [] a
⊢ lookup a (map (fun (x : α) ↦ (x, f x)) []) = some (f a)

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
f : α → β
a head : α
tail : List α
tail_ih : ∀ (h : a ∈ tail), lookup a (map (fun (x : α) ↦ (x, f x)) tail) = some (f a)
h : a ∈ head :: tail
⊢ lookup a (map (fun (x : α) ↦ (x, f x)) (head :: tail)) = some (f a)

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
f : α → β
a : α
as : List α
h : a ∈ as
nil : ∀ (h : Membership.mem (γ := List α) [] a), lookup a (map (fun (x : α) ↦ (x, f x)) []) = some (f a)
cons :
  ∀ (head : α) (tail : List α),
    (∀ (h : a ∈ tail), lookup a (map (fun (x : α) ↦ (x, f x)) tail) = some (f a)) →
      ∀ (h : a ∈ head :: tail), lookup a (map (fun (x : α) ↦ (x, f x)) (head :: tail)) = some (f a)
⊢ lookup a (map (fun (x : α) ↦ (x, f x)) as) = some (f a)

Tactic:
induction as with grind
-- Module: Mathlib.Data.List.Basic
Goal:
a : ℕ
⊢ range' a 0 0 = replicate 0 a

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
a b : ℕ
ih : range' a b 0 = replicate b a
⊢ range' a (b + 1) 0 = replicate (b + 1) a

Tactic:
simp [range'_succ, ih, replicate_succ]

Premises used: List.replicate_succ, List.range'_succ
-- Module: Mathlib.Data.List.Basic
Goal:
a b : ℕ
zero : range' a 0 0 = replicate 0 a
succ : ∀ (b : ℕ) (ih : range' a b 0 = replicate b a), range' a (b + 1) 0 = replicate (b + 1) a
⊢ range' a b 0 = replicate b a

Tactic:
induction b with
  | zero => simp
  | succ b ih => simp [range'_succ, ih, replicate_succ]

Premises used: List.replicate_succ, Nat.zero, Nat.succ, List.range'_succ
-- Module: Mathlib.Data.List.Basic
Goal:
a b s x : ℕ
hx : x ∈ range' a b s
obtain : ∀ (i : ℕ), i < b → ∀ (hx : a + s * i ∈ range' a b s), a ≤ a + s * i
⊢ a ≤ x

Tactic:
obtain ⟨i, _, rfl⟩ := List.mem_range'.mp hx

Premises used: List.mem_range', Iff.mp, rfl
-- Module: Mathlib.Data.List.Basic
Goal:
a b s i : ℕ
left : i < b
hx : a + s * i ∈ range' a b s
⊢ a ≤ a + s * i

Tactic:
le_add_right a (s * i)

Premises used: HMul.hMul, Nat.le_add_right
-- Module: Mathlib.Data.List.Basic
Goal:
a b s i : ℕ
left : i < b
hx : a + s * i ∈ range' a b s
⊢ a ≤ a + s * i

Tactic:
exact le_add_right a (s * i)

Premises used: HMul.hMul, Nat.le_add_right
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
⊢ IsChain R []

Tactic:
.nil

Premises used: List.IsChain.nil
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
a : α
⊢ IsChain R [a]

Tactic:
.singleton _

Premises used: List.IsChain.singleton
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
a : α
l : List α
simp :
  (l = [] ∨ ∃ (a_1 : α), ∃ (b : α), R a_1 b ∧ ∃ (x : List α), IsChain R (b :: x) ∧ a = a_1 ∧ l = b :: x) ↔
    l = [] ∨ ∃ (b : α), R a b ∧ ∃ (x : List α), IsChain R (b :: x) ∧ l = b :: x
⊢ (a :: l = [] ∨
      (∃ (a_1 : α), a :: l = [a_1]) ∨
        ∃ (a_1 : α), ∃ (b : α), ∃ (l_1 : List α), R a_1 b ∧ IsChain R (b :: l_1) ∧ a :: l = a_1 :: b :: l_1) ↔
    l = [] ∨ ∃ (b : α), ∃ (l' : List α), R a b ∧ IsChain R (b :: l') ∧ l = b :: l'

Tactic:
simp only [cons_ne_nil, List.cons_eq_cons, exists_and_right,
      exists_eq', true_and, exists_and_left, false_or]

Premises used: exists_and_left, false_or, exists_and_right, exists_eq', List.cons_ne_nil, List.cons_eq_cons, true_and
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
a : α
l : List α
⊢ (l = [] ∨ ∃ (a_1 : α), ∃ (b : α), R a_1 b ∧ ∃ (x : List α), IsChain R (b :: x) ∧ a = a_1 ∧ l = b :: x) ↔
    l = [] ∨ ∃ (b : α), R a b ∧ ∃ (x : List α), IsChain R (b :: x) ∧ l = b :: x

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R S : α → α → Prop
l : List α
H : ∀ (a b : α), Membership.mem (γ := List α) [] a → Membership.mem (γ := List α) (tail []) b → R a b → S a b
⊢ IsChain S []

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R S : α → α → Prop
l : List α
a : α
H : ∀ (a_1 b : α), a_1 ∈ [a] → b ∈ [a].tail → R a_1 b → S a_1 b
⊢ IsChain S [a]

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R S : α → α → Prop
l : List α
a b : α
l_1 : List α
hr : R a b
h : IsChain R (b :: l_1)
h_ih : ∀ (H : ∀ (a b_1 : α), a ∈ b :: l_1 → b_1 ∈ (b :: l_1).tail → R a b_1 → S a b_1), IsChain S (b :: l_1)
H : ∀ (a_1 b_1 : α), a_1 ∈ a :: b :: l_1 → b_1 ∈ (a :: b :: l_1).tail → R a_1 b_1 → S a_1 b_1
⊢ IsChain S (a :: b :: l_1)

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R S : α → α → Prop
l : List α
H : ∀ (a b : α), a ∈ l → b ∈ l.tail → R a b → S a b
p : IsChain R l
nil :
  ∀ (H : ∀ (a b : α), Membership.mem (γ := List α) [] a → Membership.mem (γ := List α) (tail []) b → R a b → S a b),
    IsChain S []
singleton : ∀ (a : α) (H : ∀ (a_1 b : α), a_1 ∈ [a] → b ∈ [a].tail → R a_1 b → S a_1 b), IsChain S [a]
cons_cons :
  ∀ {a b : α} {l : List α},
    R a b →
      IsChain R (b :: l) →
        (∀ (H : ∀ (a b_1 : α), a ∈ b :: l → b_1 ∈ (b :: l).tail → R a b_1 → S a b_1), IsChain S (b :: l)) →
          ∀ (H : ∀ (a_1 b_1 : α), a_1 ∈ a :: b :: l → b_1 ∈ (a :: b :: l).tail → R a_1 b_1 → S a_1 b_1),
            IsChain S (a :: b :: l)
⊢ IsChain S l

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

Tactic:
p.imp_of_mem_tail_imp (H · · · <| mem_of_mem_tail ·)

Premises used: List.IsChain.imp_of_mem_tail_imp, List.mem_of_mem_tail
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R S : α → α → Prop
H : ∀ (a b : α), R a b ↔ S a b
l : List α
⊢ IsChain R l ↔ IsChain S l

Tactic:
⟨IsChain.imp fun a b => (H a b).1, IsChain.imp fun a b => (H a b).2⟩

Premises used: Iff.mpr, Iff.intro, Iff.mp, List.IsChain.imp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R S : α → α → Prop
l : List α
H : ∀ (a b : α), a ∈ l → b ∈ l → (R a b ↔ S a b)
⊢ IsChain R l ↔ IsChain S l

Tactic:
⟨IsChain.imp_of_mem_imp (Iff.mp <| H · · · ·), IsChain.imp_of_mem_imp (Iff.mpr <| H · · · ·)⟩

Premises used: Iff.mpr, Iff.intro, Iff.mp, List.IsChain.imp_of_mem_imp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R S : α → α → Prop
l : List α
H : ∀ (a b : α), a ∈ l → b ∈ l.tail → (R a b ↔ S a b)
⊢ IsChain R l ↔ IsChain S l

Tactic:
⟨IsChain.imp_of_mem_tail_imp (Iff.mp <| H · · · ·),
  IsChain.imp_of_mem_tail_imp (Iff.mpr <| H · · · ·)⟩

Premises used: Iff.mpr, List.IsChain.imp_of_mem_tail_imp, Iff.intro, Iff.mp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
⊢ ∀ (a b : α), a ∈ l → b ∈ l → (R a b ↔ a ∈ l ∧ b ∈ l ∧ R a b)

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
⊢ ∀ (a b : α), a ∈ l → b ∈ l.tail → (R a b ↔ a ∈ l ∧ b ∈ l.tail ∧ R a b)

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
x y : α
⊢ IsChain R [x, y] ↔ R x y

Tactic:
simp only [IsChain.singleton, isChain_cons_cons, and_true]

Premises used: and_true, List.IsChain.singleton, List.isChain_cons_cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
a b : α
l : List α
⊢ [] ++ [a, b] ++ l = a :: b :: l

Tactic:
simp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
a b : α
l : List α
x x_1 : α
h : [x, x_1] <:+: b :: l
⊢ [a] ++ b :: l ++ [] = a :: b :: l

Tactic:
simp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
c : α
l₂ : List α
⊢ IsChain R ([] ++ c :: l₂) ↔ IsChain R ([] ++ [c]) ∧ IsChain R (c :: l₂)

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
c x : α
l₂ : List α
⊢ IsChain R ([x] ++ c :: l₂) ↔ IsChain R ([x] ++ [c]) ∧ IsChain R (c :: l₂)

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
c x y : α
xs : List α
h : ∀ {l₂ : List α}, IsChain R (xs ++ c :: l₂) ↔ IsChain R (xs ++ [c]) ∧ IsChain R (c :: l₂)
h_1 : ∀ (y : α) {l₂ : List α}, IsChain R (y :: xs ++ c :: l₂) ↔ IsChain R (y :: xs ++ [c]) ∧ IsChain R (c :: l₂)
l₂ : List α
⊢ IsChain R (x :: y :: xs ++ c :: l₂) ↔ IsChain R (x :: y :: xs ++ [c]) ∧ IsChain R (c :: l₂)

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
c : α
l₁ l₂ : List α
nil : ∀ {l₂ : List α}, IsChain R ([] ++ c :: l₂) ↔ IsChain R ([] ++ [c]) ∧ IsChain R (c :: l₂)
singleton : ∀ (x : α) {l₂ : List α}, IsChain R ([x] ++ c :: l₂) ↔ IsChain R ([x] ++ [c]) ∧ IsChain R (c :: l₂)
cons_cons :
  ∀ (x y : α) (xs : List α),
    (∀ {l₂ : List α}, IsChain R (xs ++ c :: l₂) ↔ IsChain R (xs ++ [c]) ∧ IsChain R (c :: l₂)) →
      (∀ (y : α) {l₂ : List α}, IsChain R (y :: xs ++ c :: l₂) ↔ IsChain R (y :: xs ++ [c]) ∧ IsChain R (c :: l₂)) →
        ∀ {l₂ : List α}, IsChain R (x :: y :: xs ++ c :: l₂) ↔ IsChain R (x :: y :: xs ++ [c]) ∧ IsChain R (c :: l₂)
⊢ IsChain R (l₁ ++ c :: l₂) ↔ IsChain R (l₁ ++ [c]) ∧ IsChain R (c :: l₂)

Tactic:
induction l₁ using twoStepInduction generalizing l₂ with grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
b c : α
l₁ l₂ : List α
rw : IsChain R (l₁ ++ [b]) ∧ IsChain R (b :: c :: l₂) ↔ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂)
rw₁ rw₂ : IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂) ↔ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂)
⊢ IsChain R (l₁ ++ b :: c :: l₂) ↔ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂)

Tactic:
rw [isChain_split, isChain_cons_cons]

Premises used: List.isChain_cons_cons, List.isChain_split
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
a b c : α
l₁ l₂ : List α
rw :
  IsChain R (a :: (l₁ ++ [b])) ∧ IsChain R (b :: c :: l₂) ↔ IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂)
rw₁ rw₂ :
  IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂) ↔
    IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂)
⊢ IsChain R (a :: (l₁ ++ b :: c :: l₂)) ↔ IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂)

Tactic:
rw [isChain_cons_split, isChain_cons_cons]

Premises used: List.isChain_cons_split, List.isChain_cons_cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
⊢ IsChain R l ↔ ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b

Tactic:
⟨fun h _ _ _ _ eq => (isChain_append_cons_cons.mp (eq ▸ h)).2.1, ?_⟩

Premises used: And.right, And.left, Iff.intro, Iff.mp, List.isChain_append_cons_cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
refine : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b) → IsChain R l
⊢ IsChain R l ↔ ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b

Tactic:
refine ⟨fun h _ _ _ _ eq => (isChain_append_cons_cons.mp (eq ▸ h)).2.1, ?_⟩
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, [] = l₁ ++ a :: b :: l₂ → R a b) → IsChain R []

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
x : α
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, [x] = l₁ ++ a :: b :: l₂ → R a b) → IsChain R [x]

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
head head' : α
tail : List α
h : (∀ ⦃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)

Tactic:
fun h ↦ isChain_cons_cons.mpr ⟨h (nil_append _).symm, ih _ fun ⦃a b l₁ l₂⦄ eq => ?_⟩

Premises used: Iff.mpr, List.cons, List.isChain_cons_cons, And.intro, List.nil_append, Eq.symm
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
head head' : α
tail : List α
h : (∀ ⦃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)
cons_cons :
  ∀ (h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b) ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄
    (eq : head' :: tail = l₁ ++ a :: b :: l₂), R a b
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (head :: head' :: tail)

Tactic:
refine fun h ↦ isChain_cons_cons.mpr ⟨h (nil_append _).symm, ih _ fun ⦃a b l₁ l₂⦄ eq => ?_⟩

Premises used: Iff.mpr, List.isChain_cons_cons, And.intro
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
head head' : α
tail : List α
h_1 : (∀ ⦃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)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
cons_cons : head :: head' :: tail = head :: l₁ ++ a :: b :: l₂
cons_cons₁ cons_cons₂ : List α
⊢ R a b

Tactic:
apply h
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
head head' : α
tail : List α
h_1 : (∀ ⦃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)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
cons_cons : head :: (l₁ ++ a :: b :: l₂) = head :: l₁ ++ a :: b :: l₂
cons_cons₁ : head :: (l₁ ++ a :: b :: l₂) = head :: (l₁ ++ a :: b :: l₂)
rw : α
rw₁ : List α
cons_cons₂ : head :: (l₁ ++ a :: b :: l₂) = head :: (l₁ ++ a :: b :: l₂)
rw₂ : α
rw₃ : List α
⊢ head :: head' :: tail = head :: l₁ ++ a :: b :: l₂

Tactic:
rw [eq, cons_append]

Premises used: List.cons_append