awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (splitBy r [])

Tactic:
isChain_nil

Premises used: List.isChain_nil, List.splitBy
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (splitBy r [])

Tactic:
exact isChain_nil

Premises used: List.isChain_nil
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
head : α
tail : List α
cons :
  ∀ (m : List α),
    Membership.mem (γ := Option (List α)) (head? []) m →
      ∃ (ha : m ≠ []), ∃ (hb : reverse [] ++ [head] ≠ []), r (m.getLast ha) ((reverse [] ++ [head]).head hb) = false
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (splitBy r (head :: tail))

Tactic:
apply isChain_getLast_head_splitByLoop _ not_mem_nil isChain_nil

Premises used: List.isChain_nil, _private.0.List.isChain_getLast_head_splitByLoop, List.not_mem_nil
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
nil :
  IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (splitBy r [])
cons :
  ∀ (head : α) (tail : List α),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy r (head :: tail))
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (splitBy r l)

Tactic:
cases l with
  | nil => exact isChain_nil
  | cons _ _ =>
    apply isChain_getLast_head_splitByLoop _ not_mem_nil isChain_nil
    rintro _ ⟨⟩

Premises used: List.isChain_nil, List.cons, _private.0.List.isChain_getLast_head_splitByLoop, List.not_mem_nil, List.nil
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
g : List α
a : α
h : IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ [a])
ha : ∀ (x : α), x ∈ m.head? → r ([a].getLast ⋯) x = false
nil : splitBy.loop r m a g [] = (g.reverse ++ [a]) :: splitBy r m
⊢ splitBy.loop r ([] ++ m) a g [] = (g.reverse ++ [a]) :: splitBy r m

Tactic:
rw [nil_append]

Premises used: List.nil_append
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
g : List α
a : α
h : IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ [a])
ha : ∀ (x : α), Membership.mem (γ := Option α) (head? []) x → r ([a].getLast ⋯) x = false
⊢ splitBy.loop r [] a g [] = (g.reverse ++ [a]) :: splitBy r []

Tactic:
simp [splitBy.loop]

Premises used: List.splitBy.loop
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
g : List α
a : α
h : IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ [a])
c : α
m : List α
ha : ∀ (x : α), x ∈ (c :: m).head? → r ([a].getLast ⋯) x = false
⊢ splitBy.loop r (c :: m) a g [] = (g.reverse ++ [a]) :: splitBy r (c :: m)

Tactic:
simp_all [splitBy.loop, splitByLoop_eq_append [_], splitBy]

Premises used: List.splitBy, List.cons, List.splitBy.loop, List.nil, _private.0.List.splitByLoop_eq_append
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
g : List α
a : α
h : IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ [a])
ha : ∀ (x : α), x ∈ m.head? → r ([a].getLast ⋯) x = false
nil :
  ∀ (ha : ∀ (x : α), Membership.mem (γ := Option α) (head? []) x → r ([a].getLast ⋯) x = false),
    splitBy.loop r [] a g [] = (g.reverse ++ [a]) :: splitBy r []
nil₁ :
  ∀ (c : α) (m : List α) (ha : ∀ (x : α), x ∈ (c :: m).head? → r ([a].getLast ⋯) x = false),
    splitBy.loop r (c :: m) a g [] = (g.reverse ++ [a]) :: splitBy r (c :: m)
⊢ splitBy.loop r m a g [] = (g.reverse ++ [a]) :: splitBy r m

Tactic:
cases m with
    | nil => simp [splitBy.loop]
    | cons c m => simp_all [splitBy.loop, splitByLoop_eq_append [_], splitBy]

Premises used: List.splitBy, List.cons, List.splitBy.loop, List.nil, _private.0.List.splitByLoop_eq_append
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {g : List α} {a : α} (h : IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ a :: l))
    (ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast ⋯) x = false),
    splitBy.loop r (l ++ m) a g [] = (g.reverse ++ a :: l) :: splitBy r m
g : List α
a : α
h : IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ a :: b :: l)
ha : ∀ (x : α), x ∈ m.head? → r ((a :: b :: l).getLast ⋯) x = false
⊢ splitBy.loop r (b :: l ++ m) a g [] = (g.reverse ++ a :: b :: l) :: splitBy r m

Tactic:
simp_all [splitBy.loop]

Premises used: List.splitBy.loop
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
l g : List α
a : α
h : IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ a :: l)
ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast ⋯) x = false
nil :
  ∀ {g : List α} {a : α} (h : IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ [a]))
    (ha : ∀ (x : α), x ∈ m.head? → r ([a].getLast ⋯) x = false),
    splitBy.loop r ([] ++ m) a g [] = (g.reverse ++ [a]) :: splitBy r m
cons :
  ∀ (b : α) (l : List α)
    (IH :
      ∀ {g : List α} {a : α} (h : IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ a :: l))
        (ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast ⋯) x = false),
        splitBy.loop r (l ++ m) a g [] = (g.reverse ++ a :: l) :: splitBy r m)
    {g : List α} {a : α} (h : IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ a :: b :: l))
    (ha : ∀ (x : α), x ∈ m.head? → r ((a :: b :: l).getLast ⋯) x = false),
    splitBy.loop r (b :: l ++ m) a g [] = (g.reverse ++ a :: b :: l) :: splitBy r m
⊢ splitBy.loop r (l ++ m) a g [] = (g.reverse ++ a :: l) :: splitBy r m

Tactic:
induction l generalizing a g with
  | nil =>
    rw [nil_append]
    cases m with
    | nil => simp [splitBy.loop]
    | cons c m => simp_all [splitBy.loop, splitByLoop_eq_append [_], splitBy]
  | cons b l IH => simp_all [splitBy.loop]

Premises used: List.splitBy, List.cons, List.splitBy.loop, List.nil_append, List.nil, _private.0.List.splitByLoop_eq_append
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
hn : Ne.{u_1 + 1} (α := List α) [] []
h : IsChain (fun (x y : α) ↦ r x y = true) []
⊢ splitBy r [] = [[]]

Tactic:
contradiction
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun (x y : α) ↦ r x y = true) (a :: l)
cons : (reverse [] ++ a :: l) :: splitBy r [] = [a :: (l ++ [])]
cons₁ : IsChain (fun (x y : α) ↦ r x y = true) (reverse [] ++ a :: l)
cons₂ : ∀ (x : α), Membership.mem (γ := Option α) (head? []) x → r ((a :: l).getLast ⋯) x = false
⊢ splitBy r (a :: l) = [a :: l]

Tactic:
rw [splitBy, ← append_nil l, splitByLoop_append]

Premises used: _private.0.List.splitByLoop_append, List.append_nil, List.splitBy
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun (x y : α) ↦ r x y = true) (a :: l)
⊢ (reverse [] ++ a :: l) :: splitBy r [] = [a :: (l ++ [])]

Tactic:
simp [h]
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun (x y : α) ↦ r x y = true) (a :: l)
⊢ IsChain (fun (x y : α) ↦ r x y = true) (reverse [] ++ a :: l)

Tactic:
simp [h]
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun (x y : α) ↦ r x y = true) (a :: l)
⊢ ∀ (x : α), Membership.mem (γ := Option α) (head? []) x → r ((a :: l).getLast ⋯) x = false

Tactic:
simp [h]
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
hn : l ≠ []
h : IsChain (fun (x y : α) ↦ r x y = true) l
nil : ∀ (hn : Ne.{u_1 + 1} (α := List α) [] []) (h : IsChain (fun (x y : α) ↦ r x y = true) []), splitBy r [] = [[]]
cons :
  ∀ (a : α) (l : List α) (hn : a :: l ≠ []) (h : IsChain (fun (x y : α) ↦ r x y = true) (a :: l)),
    splitBy r (a :: l) = [a :: l]
⊢ splitBy r l = [l]

Tactic:
cases l with
  | nil => contradiction
  | cons a l => rw [splitBy, ← append_nil l, splitByLoop_append] <;> simp [h]

Premises used: _private.0.List.splitByLoop_append, List.append_nil, List.splitBy, List.cons, List.nil
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
hn : Ne.{u_1 + 1} (α := List α) [] []
h : IsChain (fun (x y : α) ↦ r x y = true) []
ha : ∀ (x : α), x ∈ m.head? → r (getLast [] hn) x = false
⊢ splitBy r ([] ++ m) = [] :: splitBy r m

Tactic:
contradiction
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun (x y : α) ↦ r x y = true) (a :: l)
ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast hn) x = false
cons : (reverse [] ++ a :: l) :: splitBy r m = (a :: l) :: splitBy r m
⊢ splitBy r (a :: l ++ m) = (a :: l) :: splitBy r m

Tactic:
rw [cons_append, splitBy, splitByLoop_append h ha]

Premises used: _private.0.List.splitByLoop_append, List.splitBy, List.cons_append
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun (x y : α) ↦ r x y = true) (a :: l)
ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast hn) x = false
⊢ (reverse [] ++ a :: l) :: splitBy r m = (a :: l) :: splitBy r m

Tactic:
simp
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
l : List α
hn : l ≠ []
h : IsChain (fun (x y : α) ↦ r x y = true) l
ha : ∀ (x : α), x ∈ m.head? → r (l.getLast hn) x = false
nil :
  ∀ (hn : Ne.{u_1 + 1} (α := List α) [] []) (h : IsChain (fun (x y : α) ↦ r x y = true) [])
    (ha : ∀ (x : α), x ∈ m.head? → r (getLast [] hn) x = false), splitBy r ([] ++ m) = [] :: splitBy r m
cons :
  ∀ (a : α) (l : List α) (hn : a :: l ≠ []) (h : IsChain (fun (x y : α) ↦ r x y = true) (a :: l))
    (ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast hn) x = false), splitBy r (a :: l ++ m) = (a :: l) :: splitBy r m
⊢ splitBy r (l ++ m) = l :: splitBy r m

Tactic:
cases l with
  | nil => contradiction
  | cons a l => rw [cons_append, splitBy, splitByLoop_append h ha]; simp

Premises used: _private.0.List.splitByLoop_append, List.splitBy, List.cons, List.cons_append, List.nil
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
hn : ¬Membership.mem (γ := List (List α)) [] []
hc : ∀ (m : List α), Membership.mem (γ := List (List α)) [] m → IsChain (fun (x y : α) ↦ r x y = true) m
hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) []
⊢ splitBy r (flatten []) = []

Tactic:
rfl
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬[] ∈ a :: l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (a :: l)
⊢ ¬a = [] ∧ ¬[] ∈ l

Tactic:
rw [mem_cons, not_or, eq_comm] at hn

Premises used: eq_comm, not_or, List.mem_cons
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬[] ∈ a :: l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (a :: l)
hn₁ : ¬a = [] ∧ ¬[] ∈ l
⊢ ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m

Tactic:
rw [mem_cons, not_or, eq_comm] at hn

Premises used: eq_comm, not_or, List.mem_cons
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬[] ∈ a :: l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (a :: l)
hn₁ : ¬a = [] ∧ ¬[] ∈ l
hc₁ : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (a :: l)

Tactic:
rw [mem_cons, not_or, eq_comm] at hn

Premises used: eq_comm, not_or, List.mem_cons
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (a :: l)
cons : ∀ (x : α), x ∈ l.flatten.head? → r (a.getLast ⋯) x = false
⊢ splitBy r (a :: l).flatten = a :: l

Tactic:
rw [flatten_cons, splitBy_append_of_isChain hn.1 (hc _ mem_cons_self),
      IH hn.2 (fun m hm ↦ hc _ (mem_cons_of_mem a hm)) hc'.tail]

Premises used: _private.0.List.splitBy_append_of_isChain, List.mem_cons_of_mem, List.IsChain.tail, And.right, And.left, List.flatten_cons, List.mem_cons_self
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (a :: l)
y : α
hy : y ∈ l.flatten.head?
cons : r (a.getLast ⋯) (l.flatten.head ⋯) = false
⊢ r (a.getLast ⋯) y = false

Tactic:
rw [← head_of_mem_head? hy]

Premises used: List.head_of_mem_head?
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (a :: l)
y : α
hy : y ∈ l.flatten.head?
cons :
  ∀
    (hc' :
      (∀ (y : List α), y ∈ l.head? → ∃ (ha : a ≠ []), ∃ (hb : y ≠ []), r (a.getLast ha) (y.head hb) = false) ∧
        IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l)
    (y : α) (hy : y ∈ l.flatten.head?), r (a.getLast ⋯) (l.flatten.head ⋯) = false
⊢ r (a.getLast ⋯) (l.flatten.head ⋯) = false

Tactic:
rw [isChain_cons] at hc'

Premises used: List.isChain_cons
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' :
  (∀ (y : List α), y ∈ l.head? → ∃ (ha : a ≠ []), ∃ (hb : y ≠ []), r (a.getLast ha) (y.head hb) = false) ∧
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
y : α
hy : y ∈ l.flatten.head?
cons : ∀ (x : List α) (hx : x ∈ l), x ≠ [] → r (a.getLast ⋯) (l.flatten.head ⋯) = false
⊢ r (a.getLast ⋯) (l.flatten.head ⋯) = false

Tactic:
obtain ⟨x, hx, _⟩ := flatten_ne_nil_iff.1 (ne_nil_of_mem (mem_of_mem_head? hy))

Premises used: List.mem_of_mem_head?, List.flatten_ne_nil_iff, List.ne_nil_of_mem, Iff.mp
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' :
  (∀ (y : List α), y ∈ l.head? → ∃ (ha : a ≠ []), ∃ (hb : y ≠ []), r (a.getLast ha) (y.head hb) = false) ∧
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
y : α
hy : y ∈ l.flatten.head?
x : List α
hx : x ∈ l
right : x ≠ []
⊢ a ≠ []

Tactic:
obtain ⟨_, _, H⟩ := hc'.1 (l.head (ne_nil_of_mem hx)) (head_mem_head? _)

Premises used: List.head, List.ne_nil_of_mem, And.left, List.head_mem_head?
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' :
  (∀ (y : List α), y ∈ l.head? → ∃ (ha : a ≠ []), ∃ (hb : y ≠ []), r (a.getLast ha) (y.head hb) = false) ∧
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
y : α
hy : y ∈ l.flatten.head?
x : List α
hx : x ∈ l
right : x ≠ []
w : a ≠ []
⊢ l.head ⋯ ≠ []

Tactic:
obtain ⟨_, _, H⟩ := hc'.1 (l.head (ne_nil_of_mem hx)) (head_mem_head? _)

Premises used: List.head, List.ne_nil_of_mem, And.left, List.head_mem_head?
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' :
  (∀ (y : List α), y ∈ l.head? → ∃ (ha : a ≠ []), ∃ (hb : y ≠ []), r (a.getLast ha) (y.head hb) = false) ∧
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
y : α
hy : y ∈ l.flatten.head?
x : List α
hx : x ∈ l
right : x ≠ []
w : a ≠ []
w₁ : l.head ⋯ ≠ []
⊢ r (a.getLast w) ((l.head ⋯).head w₁) = false

Tactic:
obtain ⟨_, _, H⟩ := hc'.1 (l.head (ne_nil_of_mem hx)) (head_mem_head? _)

Premises used: List.head, List.ne_nil_of_mem, And.left, List.head_mem_head?
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' :
  (∀ (y : List α), y ∈ l.head? → ∃ (ha : a ≠ []), ∃ (hb : y ≠ []), r (a.getLast ha) (y.head hb) = false) ∧
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
y : α
hy : y ∈ l.flatten.head?
x : List α
hx : x ∈ l
right : x ≠ []
w : a ≠ []
w_1 : l.head ⋯ ≠ []
H : r (a.getLast w) ((l.head ⋯).head w_1) = false
cons : r (a.getLast ⋯) ((l.head ⋯).head w_1) = false
cons₁ : l.head ⋯ ≠ []
cons₂ : r (a.getLast ⋯) ((l.head ⋯).head w_1) = false
cons₃ : l.head ⋯ ≠ []
cons₄ : r (a.getLast ⋯) ((l.head ⋯).head w_1) = false
cons₅ : l.head ⋯ ≠ []
cons₆ : r (a.getLast ⋯) ((l.head ⋯).head w_1) = false
cons₇ : l.head ⋯ ≠ []
⊢ r (a.getLast ⋯) (l.flatten.head ⋯) = false

Tactic:
rwa [head_flatten_eq_head_head]

Premises used: List.head_flatten_eq_head_head
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List (List α)
hn : ¬[] ∈ l
hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
nil :
  ∀ (hn : ¬Membership.mem (γ := List (List α)) [] [])
    (hc : ∀ (m : List α), Membership.mem (γ := List (List α)) [] m → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) []),
    splitBy r (flatten []) = []
cons :
  ∀ (a : List α) (l : List (List α))
    (IH :
      ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
        (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
        splitBy r l.flatten = l)
    (hn : ¬[] ∈ a :: l) (hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' :
      IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (a :: l)),
    splitBy r (a :: l).flatten = a :: l
⊢ splitBy r l.flatten = l

Tactic:
induction l with
  | nil => rfl
  | cons a l IH =>
    rw [mem_cons, not_or, eq_comm] at hn
    rw [flatten_cons, splitBy_append_of_isChain hn.1 (hc _ mem_cons_self),
      IH hn.2 (fun m hm ↦ hc _ (mem_cons_of_mem a hm)) hc'.tail]
    intro y hy
    rw [← head_of_mem_head? hy]
    rw [isChain_cons] at hc'
    obtain ⟨x, hx, _⟩ := flatten_ne_nil_iff.1 (ne_nil_of_mem (mem_of_mem_head? hy))
    obtain ⟨_, _, H⟩ := hc'.1 (l.head (ne_nil_of_mem hx)) (head_mem_head? _)
    rwa [head_flatten_eq_head_head]

Premises used: eq_comm, not_or, List.cons, List.head_flatten_eq_head_head, List.isChain_cons, List.flatten_cons, List.mem_cons, List.nil
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
l : List (List α)
mp :
  splitBy r m = l →
    m = l.flatten ∧
      ¬[] ∈ l ∧
        (∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m) ∧
          IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
mpr :
  m = l.flatten ∧
      ¬[] ∈ l ∧
        (∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m) ∧
          IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l →
    splitBy r m = l
⊢ splitBy r m = l ↔
    m = l.flatten ∧
      ¬[] ∈ l ∧
        (∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m) ∧
          IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l

Tactic:
constructor
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
⊢ m = (splitBy r m).flatten ∧
    ¬[] ∈ splitBy r m ∧
      (∀ (m_1 : List α), m_1 ∈ splitBy r m → IsChain (fun (x y : α) ↦ r x y = true) m_1) ∧
        IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
          (splitBy r m)

Tactic:
⟨(flatten_splitBy r m).symm, nil_notMem_splitBy r m, fun _ ↦ isChain_of_mem_splitBy,
      isChain_getLast_head_splitBy r m⟩

Premises used: List.isChain_getLast_head_splitBy, List.isChain_of_mem_splitBy, List.nil_notMem_splitBy, And.intro, List.flatten_splitBy, Eq.symm