awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (hypothesis)
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 ≠ []), ∃ (hb : (a :: g).reverse ++ [b] ≠ []), r (m.getLast ha) (((a :: g).reverse ++ [b]).head hb) = false
have ha : m ≠ []
Tactic: obtain ⟨ha, _, H⟩ := hga m hm
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (hypothesis)
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 ≠ []
⊢ ∃ (ha : m ≠ []), ∃ (hb : (a :: g).reverse ++ [b] ≠ []), r (m.getLast ha) (((a :: g).reverse ++ [b]).head hb) = false
have w : g.reverse ++ [a] ≠ []
Tactic: obtain ⟨ha, _, H⟩ := hga m hm
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (hypothesis)
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] ≠ []
⊢ ∃ (ha : m ≠ []), ∃ (hb : (a :: g).reverse ++ [b] ≠ []), r (m.getLast ha) (((a :: g).reverse ++ [b]).head hb) = false
have H : r (m.getLast ha) ((g.reverse ++ [a]).head w) = false
Tactic: obtain ⟨ha, _, H⟩ := hga m hm
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
have h_1 : r (m.getLast ha) (((a :: g).reverse ++ [b]).head sorry) = false
Tactic: refine ⟨ha, append_ne_nil_of_right_ne_nil _ (cons_ne_nil _ _), ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ r (m.getLast ha) (((a :: g).reverse ++ [b]).head ⋯) = false
have h_1 : r (m.getLast ha) ((g.reverse ++ [a] ++ [b]).head sorry) = false
Tactic: rwa [reverse_cons, head_append_of_ne_nil]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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 (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (splitBy.loop r l b [] ((a :: g).reverse :: gs))
have h_2 : ¬[] ∈ (a :: g).reverse :: gs
Tactic: apply IH
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ 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))
have h_2₁ : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
  ((a :: g).reverse :: gs)
Tactic: apply IH
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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)
⊢ 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))
have h_2₂ : ∀ (m : List α),
  m ∈ ((a :: g).reverse :: gs).head? →
    ∃ (ha : m ≠ []), ∃ (hb : reverse [] ++ [b] ≠ []), r (m.getLast ha) ((reverse [] ++ [b]).head hb) = false
Tactic: apply IH
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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)
    ((a :: g).reverse :: gs)
have h_2 : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
  ((g.reverse ++ [a]) :: gs)
Tactic: rw [reverse_cons]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (splitBy.loop r l a g gs)
have 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)
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
Cleared hypotheses: l, a, g, gs, hgs', hgs, hga
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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)
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (splitBy.loop r l a g gs)
have 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)
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
Cleared hypotheses: l, a, g, gs, hgs', hgs, hga
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
head : α
tail : List α
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (splitBy r (head :: tail))
have cons : ∀ (m : List α),
  Membership.mem (γ := Option (List α)) (head? []) m →
    ∃ (ha : m ≠ []), ∃ (hb : reverse [] ++ [head] ≠ []), r (m.getLast ha) ((reverse [] ++ [head]).head hb) = false
Tactic: apply isChain_getLast_head_splitByLoop _ not_mem_nil isChain_nil
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l : List α
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (splitBy r l)
have nil : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (splitBy r [])
Tactic: cases l with
  | nil => exact isChain_nil
  | cons _ _ =>
    apply isChain_getLast_head_splitByLoop _ not_mem_nil isChain_nil
    rintro _ ⟨⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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 [])
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (splitBy r l)
have 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))
Tactic: cases l with
  | nil => exact isChain_nil
  | cons _ _ =>
    apply isChain_getLast_head_splitByLoop _ not_mem_nil isChain_nil
    rintro _ ⟨⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ splitBy.loop r ([] ++ m) a g [] = (g.reverse ++ [a]) :: splitBy r m
have nil : splitBy.loop r m a g [] = (g.reverse ++ [a]) :: splitBy r m
Tactic: rw [nil_append]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ splitBy.loop r m a g [] = (g.reverse ++ [a]) :: splitBy r m
have nil : ∀ (ha : ∀ (x : α), Membership.mem (γ := Option α) (head? []) x → r ([a].getLast sorry) x = false),
  splitBy.loop r [] a g [] = (g.reverse ++ [a]) :: splitBy r []
Tactic: cases m with
    | nil => simp [splitBy.loop]
    | cons c m => simp_all [splitBy.loop, splitByLoop_eq_append [_], splitBy]
Cleared hypotheses: m, ha
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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 []
⊢ splitBy.loop r m a g [] = (g.reverse ++ [a]) :: splitBy r m
have nil₁ : ∀ (c : α) (m : List α) (ha : ∀ (x : α), x ∈ (c :: m).head? → r ([a].getLast sorry) x = false),
  splitBy.loop r (c :: m) a g [] = (g.reverse ++ [a]) :: splitBy r (c :: m)
Tactic: cases m with
    | nil => simp [splitBy.loop]
    | cons c m => simp_all [splitBy.loop, splitByLoop_eq_append [_], splitBy]
Cleared hypotheses: m, ha
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ splitBy.loop r (l ++ m) a g [] = (g.reverse ++ a :: l) :: splitBy r m
have nil : ∀ {g : List α} {a : α} (h : IsChain (fun (x y : α) ↦ r x y = true) (g.reverse ++ [a]))
  (ha : ∀ (x : α), x ∈ m.head? → r ([a].getLast sorry) x = false),
  splitBy.loop r ([] ++ m) a g [] = (g.reverse ++ [a]) :: 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]
Cleared hypotheses: l, g, a, h, ha
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ splitBy.loop r (l ++ m) a g [] = (g.reverse ++ a :: l) :: splitBy r m
have 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 sorry) 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 sorry) x = false),
  splitBy.loop r (b :: l ++ m) a g [] = (g.reverse ++ a :: b :: 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]
Cleared hypotheses: l, g, a, h, ha
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun (x y : α) ↦ r x y = true) (a :: l)
⊢ splitBy r (a :: l) = [a :: l]
have cons : (reverse [] ++ a :: l) :: splitBy r [] = [a :: (l ++ [])]
Tactic: rw [splitBy, ← append_nil l, splitByLoop_append]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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 ++ [])]
⊢ splitBy r (a :: l) = [a :: l]
have cons₁ : IsChain (fun (x y : α) ↦ r x y = true) (reverse [] ++ a :: l)
Tactic: rw [splitBy, ← append_nil l, splitByLoop_append]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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)
⊢ splitBy r (a :: l) = [a :: l]
have cons₂ : ∀ (x : α), Membership.mem (γ := Option α) (head? []) x → r ((a :: l).getLast sorry) x = false
Tactic: rw [splitBy, ← append_nil l, splitByLoop_append]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l : List α
hn : l ≠ []
h : IsChain (fun (x y : α) ↦ r x y = true) l
⊢ splitBy r l = [l]
have nil : ∀ (hn : Ne.{u_1 + 1} (α := List α) [] []) (h : IsChain (fun (x y : α) ↦ r x y = true) []), splitBy r [] = [[]]
Tactic: cases l with
  | nil => contradiction
  | cons a l => rw [splitBy, ← append_nil l, splitByLoop_append] <;> simp [h]
Cleared hypotheses: l, hn, h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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 [] = [[]]
⊢ splitBy r l = [l]
have cons : ∀ (a : α) (l : List α) (hn : a :: l ≠ []) (h : IsChain (fun (x y : α) ↦ r x y = true) (a :: l)),
  splitBy r (a :: l) = [a :: l]
Tactic: cases l with
  | nil => contradiction
  | cons a l => rw [splitBy, ← append_nil l, splitByLoop_append] <;> simp [h]
Cleared hypotheses: l, hn, h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ splitBy r (a :: l ++ m) = (a :: l) :: splitBy r m
have cons : (reverse [] ++ a :: l) :: splitBy r m = (a :: l) :: splitBy r m
Tactic: rw [cons_append, splitBy, splitByLoop_append h ha]