awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
l_1 : List α
h_1 : m ∈ splitBy r l_1
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ ∀ (b : α), Membership.mem (γ := Option α) (head? []) b → r b a = true

Tactic:
simp
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
l_1 : List α
h_1 : m ∈ splitBy r l_1
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ IsChain (fun (y x : α) ↦ r x y = true) []

Tactic:
simp
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
l : List α
h : m ∈ splitBy r l
⊢ IsChain (fun (x y : α) ↦ r x y = true) m

Tactic:
match l, h with
  | a::l, h => apply isChain_of_mem_splitByLoop _ _ h <;> simp
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
nil :
  IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (gs.reverse ++ [(a :: g).reverse])
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (splitBy.loop r [] a g gs)

Tactic:
rw [splitBy.loop, reverse_cons]

Premises used: List.reverse_cons, List.splitBy.loop
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
nil :
  IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (gs.reverse ++ [(a :: g).reverse]).reverse
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (gs.reverse ++ [(a :: g).reverse])

Tactic:
apply List.isChain_reverse.1

Premises used: Iff.mp, List.isChain_reverse
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
⊢ IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (gs.reverse ++ [(a :: g).reverse]).reverse

Tactic:
simpa using isChain_cons.2 ⟨hga, hgs⟩

Premises used: Iff.mpr, List.isChain_cons, And.intro
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
cons :
  IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (match (motive := Bool → List (List α)) r a b with
    | true => splitBy.loop r l b (a :: g) gs
    | false => splitBy.loop r l b [] ((a :: g).reverse :: gs))
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (splitBy.loop r (b :: l) a g gs)

Tactic:
rw [splitBy.loop]

Premises used: List.splitBy.loop
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
h_1 :
  ∀ (x : Bool),
    r a b = true →
      IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
        (splitBy.loop r l b (a :: g) gs)
h_2 :
  ∀ (x : Bool),
    r a b = false →
      IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
        (splitBy.loop r l b [] ((a :: g).reverse :: gs))
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (match (motive := Bool → List (List α)) r a b with
    | true => splitBy.loop r l b (a :: g) gs
    | false => splitBy.loop r l b [] ((a :: g).reverse :: gs))

Tactic:
split
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x : Bool
heq : r a b = true
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (splitBy.loop r l b (a :: g) gs)

Tactic:
IH hgs' hgs fun m hm ↦ ?_
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x : Bool
heq : r a b = true
h_1 :
  ∀ (m : List α) (hm : m ∈ gs.head?),
    ∃ (ha : m ≠ []), ∃ (hb : (a :: g).reverse ++ [b] ≠ []), r (m.getLast ha) (((a :: g).reverse ++ [b]).head hb) = false
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (splitBy.loop r l b (a :: g) gs)

Tactic:
refine IH hgs' hgs fun m hm ↦ ?_
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x : Bool
heq : r a b = true
m : List α
hm : m ∈ gs.head?
⊢ m ≠ []

Tactic:
obtain ⟨ha, _, H⟩ := hga m hm
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x : Bool
heq : r a b = true
m : List α
hm : m ∈ gs.head?
ha : m ≠ []
⊢ g.reverse ++ [a] ≠ []

Tactic:
obtain ⟨ha, _, H⟩ := hga m hm
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x : Bool
heq : r a b = true
m : List α
hm : m ∈ gs.head?
ha : m ≠ []
w : g.reverse ++ [a] ≠ []
⊢ r (m.getLast ha) ((g.reverse ++ [a]).head w) = false

Tactic:
obtain ⟨ha, _, H⟩ := hga m hm
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x : Bool
heq : r a b = true
m : List α
hm : m ∈ gs.head?
ha : m ≠ []
w : g.reverse ++ [a] ≠ []
H : r (m.getLast ha) ((g.reverse ++ [a]).head w) = false
⊢ ∃ (ha : m ≠ []), ∃ (hb : (a :: g).reverse ++ [b] ≠ []), r (m.getLast ha) (((a :: g).reverse ++ [b]).head hb) = false

Tactic:
⟨ha, append_ne_nil_of_right_ne_nil _ (cons_ne_nil _ _), ?_⟩

Premises used: List.cons_ne_nil, Exists.intro, List.append_ne_nil_of_right_ne_nil
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x : Bool
heq : r a b = true
m : List α
hm : m ∈ gs.head?
ha : m ≠ []
w : g.reverse ++ [a] ≠ []
H : r (m.getLast ha) ((g.reverse ++ [a]).head w) = false
h_1 : r (m.getLast ha) (((a :: g).reverse ++ [b]).head ⋯) = false
⊢ ∃ (ha : m ≠ []), ∃ (hb : (a :: g).reverse ++ [b] ≠ []), r (m.getLast ha) (((a :: g).reverse ++ [b]).head hb) = false

Tactic:
refine ⟨ha, append_ne_nil_of_right_ne_nil _ (cons_ne_nil _ _), ?_⟩
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x : Bool
heq : r a b = true
m : List α
hm : m ∈ gs.head?
ha : m ≠ []
w : g.reverse ++ [a] ≠ []
H : r (m.getLast ha) ((g.reverse ++ [a]).head w) = false
h_1 : r (m.getLast ha) ((g.reverse ++ [a] ++ [b]).head ⋯) = false
h_1₁ : r (m.getLast ha) ((g.reverse ++ [a]).head w) = false
h_1₂ : g.reverse ++ [a] ≠ []
h_1₃ : r (m.getLast ha) ((g.reverse ++ [a]).head w) = false
h_1₄ : g.reverse ++ [a] ≠ []
h_1₅ : r (m.getLast ha) ((g.reverse ++ [a]).head w) = false
h_1₆ : g.reverse ++ [a] ≠ []
h_1₇ : r (m.getLast ha) ((g.reverse ++ [a]).head w) = false
h_1₈ : g.reverse ++ [a] ≠ []
⊢ r (m.getLast ha) (((a :: g).reverse ++ [b]).head ⋯) = false

Tactic:
rwa [reverse_cons, head_append_of_ne_nil]

Premises used: List.head_append_of_ne_nil, List.reverse_cons
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x : Bool
heq : r a b = false
h_2 : ¬[] ∈ (a :: g).reverse :: gs
h_2₁ :
  IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    ((a :: g).reverse :: gs)
h_2₂ :
  ∀ (m : List α),
    m ∈ ((a :: g).reverse :: gs).head? →
      ∃ (ha : m ≠ []), ∃ (hb : reverse [] ++ [b] ≠ []), r (m.getLast ha) ((reverse [] ++ [b]).head hb) = false
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (splitBy.loop r l b [] ((a :: g).reverse :: gs))

Tactic:
apply IH
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x : Bool
heq : r a b = false
⊢ ¬[] ∈ (a :: g).reverse :: gs

Tactic:
simpa using hgs'
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x : Bool
heq : r a b = false
h_2 :
  IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    ((g.reverse ++ [a]) :: gs)
⊢ IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    ((a :: g).reverse :: gs)

Tactic:
rw [reverse_cons]

Premises used: List.reverse_cons
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x : Bool
heq : r a b = false
⊢ IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    ((g.reverse ++ [a]) :: gs)

Tactic:
apply isChain_cons.2 ⟨hga, hgs⟩

Premises used: Iff.mpr, List.isChain_cons, And.intro
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x : Bool
heq : r a b = false
⊢ ∀ (m : List α),
    m ∈ ((a :: g).reverse :: gs).head? →
      ∃ (ha : m ≠ []), ∃ (hb : reverse [] ++ [b] ≠ []), r (m.getLast ha) ((reverse [] ++ [b]).head hb) = false

Tactic:
simpa
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs
hga :
  ∀ (m : List α),
    m ∈ gs.head? →
      ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
nil :
  ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r [] a g gs)
cons :
  ∀ (b : α) (l : List α)
    (IH :
      ∀ {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
        (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
        (hga :
          ∀ (m : List α),
            m ∈ gs.head? →
              ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
        IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
          (splitBy.loop r l a g gs))
    {a : α} {g : List α} {gs : List (List α)} (hgs' : ¬[] ∈ gs)
    (hgs : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs)
    (hga :
      ∀ (m : List α),
        m ∈ gs.head? →
          ∃ (ha : m ≠ []), ∃ (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false),
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
      (splitBy.loop r (b :: l) a g gs)
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (splitBy.loop r l a g gs)

Tactic:
induction l generalizing a g gs with
  | nil =>
    rw [splitBy.loop, reverse_cons]
    apply List.isChain_reverse.1
    simpa using isChain_cons.2 ⟨hga, hgs⟩
  | cons b l IH =>
    rw [splitBy.loop]
    split
    · refine IH hgs' hgs fun m hm ↦ ?_
      obtain ⟨ha, _, H⟩ := hga m hm
      refine ⟨ha, append_ne_nil_of_right_ne_nil _ (cons_ne_nil _ _), ?_⟩
      rwa [reverse_cons, head_append_of_ne_nil]
    · apply IH
      · simpa using hgs'
      · rw [reverse_cons]
        apply isChain_cons.2 ⟨hga, hgs⟩
      · simpa

Premises used: Iff.mpr, List.head_append_of_ne_nil, List.cons, List.reverse_cons, List.splitBy.loop, List.isChain_cons, And.intro, Iff.mp, List.nil, List.isChain_reverse