awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x : Bool
heq : r a b = false
h_2 :
  ((a :: g).reverse :: gs).reverse ++ splitBy.loop r l b [] [] = gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]
⊢ splitBy.loop r l b [] ((a :: g).reverse :: gs) = gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
rw [IH]
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x : Bool
heq : r a b = false
rw : gs.reverse ++ ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] [])
| gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
rw [IH]
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x : Bool
heq : r a b = false
h_2 :
  ((a :: g).reverse :: gs).reverse ++ splitBy.loop r l b [] [] =
    gs.reverse ++ ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] [])
⊢ ((a :: g).reverse :: gs).reverse ++ splitBy.loop r l b [] [] = gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
conv_rhs => rw [IH]
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x : Bool
heq : r a b = false
⊢ ((a :: g).reverse :: gs).reverse ++ splitBy.loop r l b [] [] =
    gs.reverse ++ ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] [])

Tactic:
simp
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
gs : List (List α)
nil : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r [] a g gs = gs.reverse ++ splitBy.loop r [] a g []
cons :
  ∀ (b : α) (l : List α)
    (IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g [])
    {a : α} {g : List α} (gs : List (List α)),
    splitBy.loop r (b :: l) a g gs = gs.reverse ++ splitBy.loop r (b :: l) a g []
⊢ splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []

Tactic:
induction l generalizing a g gs with
  | nil => simp [splitBy.loop]
  | cons b l IH =>
    simp_rw [splitBy.loop]
    split <;> rw [IH]
    conv_rhs => rw [IH]
    simp

Premises used: List.cons, List.splitBy.loop, List.nil
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : α
g : List α
⊢ (splitBy.loop r [] a g []).flatten = g.reverse ++ [a]

Tactic:
simp [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 α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
cons :
  flatten
      (match (motive := Bool → List (List α)) r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => [(a :: g).reverse].reverse ++ splitBy.loop r l b [] []) =
    g.reverse ++ a :: b :: l
⊢ (splitBy.loop r (b :: l) a g []).flatten = g.reverse ++ a :: b :: l

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

Premises used: List.cons, List.splitBy.loop, List.nil, _private.0.List.splitByLoop_eq_append
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
h_1 : ∀ (x : Bool), r a b = true → (splitBy.loop r l b (a :: g) []).flatten = g.reverse ++ a :: b :: l
h_2 :
  ∀ (x : Bool),
    r a b = false → ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] []).flatten = g.reverse ++ a :: b :: l
⊢ flatten
      (match (motive := Bool → List (List α)) r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => [(a :: g).reverse].reverse ++ splitBy.loop r l b [] []) =
    g.reverse ++ a :: b :: l

Tactic:
split
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
x : Bool
heq : r a b = true
⊢ (splitBy.loop r l b (a :: g) []).flatten = g.reverse ++ a :: b :: l

Tactic:
simp [IH]
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
x : Bool
heq : r a b = false
⊢ ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] []).flatten = g.reverse ++ a :: b :: l

Tactic:
simp [IH]
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
nil : ∀ {a : α} {g : List α}, (splitBy.loop r [] a g []).flatten = g.reverse ++ [a]
cons :
  ∀ (b : α) (l : List α) (IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l) {a : α}
    {g : List α}, (splitBy.loop r (b :: l) a g []).flatten = g.reverse ++ a :: b :: l
⊢ (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l

Tactic:
induction l generalizing a g with
  | nil => simp [splitBy.loop]
  | cons b l IH =>
    rw [splitBy.loop, splitByLoop_eq_append [_]]
    split <;> simp [IH]

Premises used: List.cons, List.splitBy.loop, List.nil, _private.0.List.splitByLoop_eq_append
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
⊢ (splitBy r l).flatten = l

Tactic:
match l with
  | nil => rfl
  | cons _ _ => flatten_splitByLoop

Premises used: List.splitBy, _private.0.List.flatten_splitBy.match_1, Eq, _private.0.List.flatten_splitByLoop, rfl, List.flatten
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
⊢ (splitBy r l).flatten = l

Tactic:
have := flatten_splitBy r l
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
this : (splitBy r l).flatten = l
⊢ splitBy r l = [] ↔ l = []

Tactic:
⟨fun _ ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
this : (splitBy r l).flatten = l
refine_1 : splitBy r l = [] → l = []
refine_2 : l = [] → splitBy r l = []
⊢ splitBy r l = [] ↔ l = []

Tactic:
refine ⟨fun _ ↦ ?_, ?_⟩
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
this : (splitBy r l).flatten = l
h : splitBy r l = []
⊢ l = []

Tactic:
simp_all
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
this : (splitBy r l).flatten = l
⊢ l = [] → splitBy r l = []

Tactic:
simp_all
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
⊢ splitBy r l ≠ [] ↔ l ≠ []

Tactic:
splitBy_eq_nil.not

Premises used: Iff.not, List.splitBy_eq_nil
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : α
g : List α
⊢ ¬[] ∈ splitBy.loop r [] a g []

Tactic:
simp [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 α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
cons :
  ¬Membership.mem (γ := List (List α))
      (match (motive := Bool → List (List α)) r a b with
        | true => splitBy.loop r l b (a :: g) []
        | false => splitBy.loop r l b [] [(a :: g).reverse] :
        List (List α))
      []
⊢ ¬[] ∈ splitBy.loop r (b :: l) a g []

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 α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
h_1 : ∀ (x : Bool), r a b = true → ¬[] ∈ splitBy.loop r l b (a :: g) []
h_2 : ∀ (x : Bool), r a b = false → ¬[] ∈ splitBy.loop r l b [] [(a :: g).reverse]
⊢ ¬Membership.mem (γ := List (List α))
      (match (motive := Bool → List (List α)) r a b with
        | true => splitBy.loop r l b (a :: g) []
        | false => splitBy.loop r l b [] [(a :: g).reverse] :
        List (List α))
      []

Tactic:
split
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x : Bool
heq : r a b = true
⊢ ¬[] ∈ splitBy.loop r l b (a :: g) []

Tactic:
IH
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x : Bool
heq : r a b = true
⊢ ¬[] ∈ splitBy.loop r l b (a :: g) []

Tactic:
exact IH
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x : Bool
heq : r a b = false
h_2 : ¬([] ∈ [(a :: g).reverse].reverse ∨ [] ∈ splitBy.loop r l b [] [])
⊢ ¬[] ∈ splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
rw [splitByLoop_eq_append, mem_append]

Premises used: List.mem_append, _private.0.List.splitByLoop_eq_append
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x : Bool
heq : r a b = false
⊢ ¬([] ∈ [(a :: g).reverse].reverse ∨ [] ∈ splitBy.loop r l b [] [])

Tactic:
simpa using IH
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
nil : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r [] a g []
cons :
  ∀ (b : α) (l : List α) (IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []) {a : α} {g : List α},
    ¬[] ∈ splitBy.loop r (b :: l) a g []
⊢ ¬[] ∈ splitBy.loop r l a g []

Tactic:
induction l generalizing a g with
  | nil => simp [splitBy.loop]
  | cons b l IH =>
    rw [splitBy.loop]
    split
    · exact IH
    · rw [splitByLoop_eq_append, mem_append]
      simpa using IH

Premises used: List.cons, List.mem_append, List.splitBy.loop, List.nil, _private.0.List.splitByLoop_eq_append
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
⊢ ¬[] ∈ splitBy r l

Tactic:
match l with
  | nil => not_mem_nil
  | cons _ _ => nil_notMem_splitByLoop

Premises used: Membership.mem, List.splitBy, _private.0.List.nil_notMem_splitByLoop, _private.0.List.flatten_splitBy.match_1, Not, List.not_mem_nil, List.nil
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
l : List α
h : m ∈ splitBy r l
h_1 : m = []
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
hn : l ≠ []
⊢ ((splitBy r l).head ⋯).head ⋯ = l.head hn

Tactic:
simp [head_head_eq_head_flatten]

Premises used: List.head_head_eq_head_flatten
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
hn : l ≠ []
⊢ ((splitBy r l).getLast ⋯).getLast ⋯ = l.getLast hn

Tactic:
simp [getLast_getLast_eq_getLast_flatten]

Premises used: List.getLast_getLast_eq_getLast_flatten
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
h : m ∈ splitBy.loop r [] a g []
⊢ Membership.mem (γ := List (List α)) [] m ∨ m = (a :: g).reverse

Tactic:
rw [splitBy.loop, reverse_cons, mem_append, mem_reverse, mem_singleton] at h

Premises used: List.mem_reverse, List.mem_singleton, List.reverse_cons, List.mem_append, List.splitBy.loop
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
h : Membership.mem (γ := List (List α)) [] m ∨ m = (a :: g).reverse
nil : ∀ (hm : Membership.mem (γ := List (List α)) [] m), IsChain (fun (x y : α) ↦ r x y = true) m
nil₁ : IsChain (fun (x y : α) ↦ r x y = true) (a :: g).reverse
⊢ IsChain (fun (x y : α) ↦ r x y = true) m

Tactic:
obtain hm | rfl := h

Premises used: rfl
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
hm : Membership.mem (γ := List (List α)) [] m
⊢ IsChain (fun (x y : α) ↦ r x y = true) m

Tactic:
cases not_mem_nil hm

Premises used: List.not_mem_nil
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
nil : IsChain (fun (b a : α) ↦ r a b = true) (a :: g).reverse.reverse
⊢ IsChain (fun (x y : α) ↦ r x y = true) (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 α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
nil : IsChain (fun (b a : α) ↦ r a b = true) (a :: g)
⊢ IsChain (fun (b a : α) ↦ r a b = true) (a :: g).reverse.reverse

Tactic:
rw [reverse_reverse]

Premises used: List.reverse_reverse
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
⊢ IsChain (fun (b a : α) ↦ r a b = true) (a :: g)

Tactic:
isChain_cons.2 ⟨hga, hg⟩

Premises used: Iff.mpr, List.isChain_cons, And.intro
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
⊢ IsChain (fun (b a : α) ↦ r a b = true) (a :: g)

Tactic:
exact isChain_cons.2 ⟨hga, hg⟩

Premises used: Iff.mpr, List.isChain_cons, And.intro
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} (hga : ∀ (b : α), b ∈ g.head? → r b a = true) (hg : IsChain (fun (y x : α) ↦ r x y = true) g)
    (h : m ∈ splitBy.loop r l a g []), IsChain (fun (x y : α) ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
h : m ∈ splitBy.loop r (b :: l) a g []
⊢ Membership.mem (γ := List (List α))
    (match (motive := Bool → List (List α)) r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => splitBy.loop r l b [] [g.reverse ++ [a]] :
      List (List α))
    m

Tactic:
simp only [splitBy.loop, reverse_cons] at h

Premises used: List.reverse_cons, List.splitBy.loop
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} (hga : ∀ (b : α), b ∈ g.head? → r b a = true) (hg : IsChain (fun (y x : α) ↦ r x y = true) g)
    (h : m ∈ splitBy.loop r l a g []), IsChain (fun (x y : α) ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
h :
  Membership.mem (γ := List (List α))
    (match (motive := Bool → List (List α)) r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => splitBy.loop r l b [] [g.reverse ++ [a]] :
      List (List α))
    m
h_1 : ∀ (x : Bool), r a b = true → ∀ (h : m ∈ splitBy.loop r l b (a :: g) []), IsChain (fun (x y : α) ↦ r x y = true) m
h_2 :
  ∀ (x : Bool),
    r a b = false → ∀ (h : m ∈ splitBy.loop r l b [] [g.reverse ++ [a]]), IsChain (fun (x y : α) ↦ r x y = true) m
⊢ IsChain (fun (x y : α) ↦ r x y = true) m

Tactic:
split at h
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} (hga : ∀ (b : α), b ∈ g.head? → r b a = true) (hg : IsChain (fun (y x : α) ↦ r x y = true) g)
    (h : m ∈ splitBy.loop r l a g []), IsChain (fun (x y : α) ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
x : Bool
heq : r a b = true
h : m ∈ splitBy.loop r l b (a :: g) []
apply : ∀ (b_1 : α), b_1 ∈ (a :: g).head? → r b_1 b = true
⊢ IsChain (fun (x y : α) ↦ r x y = true) m

Tactic:
apply IH _ (isChain_cons.2 ⟨hga, hg⟩) h

Premises used: Iff.mpr, List.isChain_cons, And.intro
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} (hga : ∀ (b : α), b ∈ g.head? → r b a = true) (hg : IsChain (fun (y x : α) ↦ r x y = true) g)
    (h : m ∈ splitBy.loop r l a g []), IsChain (fun (x y : α) ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
x : Bool
heq : r a b = true
h : m ∈ splitBy.loop r l b (a :: g) []
⊢ ∀ (b_1 : α), b_1 ∈ (a :: g).head? → r b_1 b = true

Tactic:
grind
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} (hga : ∀ (b : α), b ∈ g.head? → r b a = true) (hg : IsChain (fun (y x : α) ↦ r x y = true) g)
    (h : m ∈ splitBy.loop r l a g []), IsChain (fun (x y : α) ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
x : Bool
heq : r a b = false
h : m ∈ splitBy.loop r l b [] [g.reverse ++ [a]]
⊢ m = g.reverse ++ [a] ∨ m ∈ splitBy.loop r l b [] []

Tactic:
rw [splitByLoop_eq_append, mem_append, reverse_singleton, mem_singleton] at h

Premises used: List.mem_singleton, List.reverse_singleton, List.mem_append, _private.0.List.splitByLoop_eq_append
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} (hga : ∀ (b : α), b ∈ g.head? → r b a = true) (hg : IsChain (fun (y x : α) ↦ r x y = true) g)
    (h : m ∈ splitBy.loop r l a g []), IsChain (fun (x y : α) ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
x : Bool
heq : r a b = false
h : m = g.reverse ++ [a] ∨ m ∈ splitBy.loop r l b [] []
h_2 :
  ∀
    (IH :
      ∀ {a_1 : α} {g_1 : List α} (hga : ∀ (b : α), b ∈ g_1.head? → r b a_1 = true)
        (hg : IsChain (fun (y x : α) ↦ r x y = true) g_1) (h : g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 []),
        IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ [a])),
    IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ [a])
h_2₁ : ∀ (hm : m ∈ splitBy.loop r l b [] []), IsChain (fun (x y : α) ↦ r x y = true) m
⊢ IsChain (fun (x y : α) ↦ r x y = true) m

Tactic:
obtain rfl | hm := h

Premises used: rfl
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
x : Bool
heq : r a b = false
IH :
  ∀ {a_1 : α} {g_1 : List α} (hga : ∀ (b : α), b ∈ g_1.head? → r b a_1 = true)
    (hg : IsChain (fun (y x : α) ↦ r x y = true) g_1) (h : g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 []),
    IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ [a])
h_2 : IsChain (fun (b a : α) ↦ r a b = true) (g.reverse ++ [a]).reverse
⊢ IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ [a])

Tactic:
apply List.isChain_reverse.1

Premises used: Iff.mp, List.isChain_reverse
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
x : Bool
heq : r a b = false
IH :
  ∀ {a_1 : α} {g_1 : List α} (hga : ∀ (b : α), b ∈ g_1.head? → r b a_1 = true)
    (hg : IsChain (fun (y x : α) ↦ r x y = true) g_1) (h : g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 []),
    IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ [a])
h_2 : IsChain (fun (b a : α) ↦ r a b = true) ([a] ++ g)
⊢ IsChain (fun (b a : α) ↦ r a b = true) (g.reverse ++ [a]).reverse

Tactic:
rw [reverse_append, reverse_cons, reverse_nil, nil_append, reverse_reverse]

Premises used: List.reverse_cons, List.reverse_reverse, List.nil_append, List.reverse_append, List.reverse_nil
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
x : Bool
heq : r a b = false
IH :
  ∀ {a_1 : α} {g_1 : List α} (hga : ∀ (b : α), b ∈ g_1.head? → r b a_1 = true)
    (hg : IsChain (fun (y x : α) ↦ r x y = true) g_1) (h : g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 []),
    IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ [a])
⊢ IsChain (fun (b a : α) ↦ r a b = true) ([a] ++ g)

Tactic:
isChain_cons.2 ⟨hga, hg⟩

Premises used: Iff.mpr, List.append, List.isChain_cons, And.intro
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
x : Bool
heq : r a b = false
IH :
  ∀ {a_1 : α} {g_1 : List α} (hga : ∀ (b : α), b ∈ g_1.head? → r b a_1 = true)
    (hg : IsChain (fun (y x : α) ↦ r x y = true) g_1) (h : g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 []),
    IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ [a])
⊢ IsChain (fun (b a : α) ↦ r a b = true) ([a] ++ g)

Tactic:
exact isChain_cons.2 ⟨hga, hg⟩

Premises used: Iff.mpr, List.isChain_cons, And.intro
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} (hga : ∀ (b : α), b ∈ g.head? → r b a = true) (hg : IsChain (fun (y x : α) ↦ r x y = true) g)
    (h : m ∈ splitBy.loop r l a g []), IsChain (fun (x y : α) ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
x : Bool
heq : r a b = false
hm : m ∈ splitBy.loop r l b [] []
⊢ IsChain (fun (x y : α) ↦ r x y = true) m

Tactic:
grind
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun (y x : α) ↦ r x y = true) g
h : m ∈ splitBy.loop r l a g []
nil :
  ∀ {a : α} {g : List α} (hga : ∀ (b : α), b ∈ g.head? → r b a = true) (hg : IsChain (fun (y x : α) ↦ r x y = true) g)
    (h : m ∈ splitBy.loop r [] a g []), IsChain (fun (x y : α) ↦ r x y = true) m
cons :
  ∀ (b : α) (l : List α)
    (IH :
      ∀ {a : α} {g : List α} (hga : ∀ (b : α), b ∈ g.head? → r b a = true)
        (hg : IsChain (fun (y x : α) ↦ r x y = true) g) (h : m ∈ splitBy.loop r l a g []),
        IsChain (fun (x y : α) ↦ r x y = true) m)
    {a : α} {g : List α} (hga : ∀ (b : α), b ∈ g.head? → r b a = true) (hg : IsChain (fun (y x : α) ↦ r x y = true) g)
    (h : m ∈ splitBy.loop r (b :: l) a g []), IsChain (fun (x y : α) ↦ r x y = true) m
⊢ IsChain (fun (x y : α) ↦ r x y = true) m

Tactic:
induction l generalizing a g with
  | nil =>
    rw [splitBy.loop, reverse_cons, mem_append, mem_reverse, mem_singleton] at h
    obtain hm | rfl := h
    · cases not_mem_nil hm
    · apply List.isChain_reverse.1
      rw [reverse_reverse]
      exact isChain_cons.2 ⟨hga, hg⟩
  | cons b l IH =>
    simp only [splitBy.loop, reverse_cons] at h
    split at h
    · apply IH _ (isChain_cons.2 ⟨hga, hg⟩) h
      grind
    · rw [splitByLoop_eq_append, mem_append, reverse_singleton, mem_singleton] at h
      obtain rfl | hm := h
      · apply List.isChain_reverse.1
        rw [reverse_append, reverse_cons, reverse_nil, nil_append, reverse_reverse]
        exact isChain_cons.2 ⟨hga, hg⟩
      · grind

Premises used: Iff.mpr, List.mem_reverse, List.mem_singleton, List.reverse_singleton, List.cons, List.reverse_cons, List.mem_append, List.reverse_reverse, List.splitBy.loop, List.isChain_cons, And.intro, List.nil_append, Iff.mp, List.reverse_append, List.reverse_nil, rfl, List.nil, _private.0.List.splitByLoop_eq_append, List.isChain_reverse
-- 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)
apply : ∀ (b : α), Membership.mem (γ := Option α) (head? []) b → r b a = true
apply₁ : IsChain (fun (y x : α) ↦ r x y = true) []
⊢ IsChain (fun (x y : α) ↦ r x y = true) m

Tactic:
apply isChain_of_mem_splitByLoop _ _ h

Premises used: _private.0.List.isChain_of_mem_splitByLoop