awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
⊢ ¬[] ∈ splitBy.loop r (b :: l) a g []
have 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 α))
    []
Tactic: rw [splitBy.loop]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
⊢ ¬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 α))
      []
have h_1 : ∀ (x : Bool), r a b = true → ¬[] ∈ splitBy.loop r l b (a :: g) []
Tactic: split
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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) []
⊢ ¬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 α))
      []
have h_2 : ∀ (x : Bool), r a b = false → ¬[] ∈ splitBy.loop r l b [] [(a :: g).reverse]
Tactic: split
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ ¬[] ∈ splitBy.loop r l b [] [(a :: g).reverse]
have h_2 : ¬([] ∈ [(a :: g).reverse].reverse ∨ [] ∈ splitBy.loop r l b [] [])
Tactic: rw [splitByLoop_eq_append, mem_append]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
⊢ ¬[] ∈ splitBy.loop r l a g []
have nil : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r [] 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
Cleared hypotheses: l, a, g
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
nil : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r [] a g []
⊢ ¬[] ∈ splitBy.loop r l a g []
have cons : ∀ (b : α) (l : List α) (IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []) {a : α} {g : List α},
  ¬[] ∈ splitBy.loop r (b :: 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
Cleared hypotheses: l, a, g
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (hypothesis)
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 []
⊢ IsChain (fun (x y : α) ↦ r x y = true) m
have h₁ : Membership.mem (γ := List (List α)) [] m ∨ m = (a :: g).reverse
Tactic: rw [splitBy.loop, reverse_cons, mem_append, mem_reverse, mem_singleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ IsChain (fun (x y : α) ↦ r x y = true) m
have nil : ∀ (hm : Membership.mem (γ := List (List α)) [] m), IsChain (fun (x y : α) ↦ r x y = true) m
Tactic: obtain hm | rfl := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ IsChain (fun (x y : α) ↦ r x y = true) m
have nil₁ : IsChain (fun (x y : α) ↦ r x y = true) (a :: g).reverse
Tactic: obtain hm | rfl := h
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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 (x y : α) ↦ r x y = true) (a :: g).reverse
have nil : IsChain (fun (b a : α) ↦ r a b = true) (a :: g).reverse.reverse
Tactic: apply List.isChain_reverse.1
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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).reverse.reverse
have nil : IsChain (fun (b a : α) ↦ r a b = true) (a :: g)
Tactic: rw [reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (hypothesis)
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 []
⊢ IsChain (fun (x y : α) ↦ r x y = true) m
have 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
Tactic: simp only [splitBy.loop, reverse_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ IsChain (fun (x y : α) ↦ r x y = true) m
have 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
Tactic: split at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ IsChain (fun (x y : α) ↦ r x y = true) m
have 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
Tactic: split at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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) []
⊢ IsChain (fun (x y : α) ↦ r x y = true) m
have apply : ∀ (b_1 : α), b_1 ∈ (a :: g).head? → r b_1 b = true
Tactic: apply IH _ (isChain_cons.2 ⟨hga, hg⟩) h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (hypothesis)
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]]
⊢ IsChain (fun (x y : α) ↦ r x y = true) m
have h₁ : m = g.reverse ++ [a] ∨ m ∈ splitBy.loop r l b [] []
Tactic: rw [splitByLoop_eq_append, mem_append, reverse_singleton, mem_singleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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 [] []
⊢ IsChain (fun (x y : α) ↦ r x y = true) m
have 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])
Tactic: obtain rfl | hm := h
Cleared hypotheses: m, IH, h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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])
⊢ IsChain (fun (x y : α) ↦ r x y = true) m
have h_2₁ : ∀ (hm : m ∈ splitBy.loop r l b [] []), IsChain (fun (x y : α) ↦ r x y = true) m
Tactic: obtain rfl | hm := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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 (x y : α) ↦ r x y = true) (g.reverse ++ [a])
have h_2 : IsChain (fun (b a : α) ↦ r a b = true) (g.reverse ++ [a]).reverse
Tactic: apply List.isChain_reverse.1
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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) (g.reverse ++ [a]).reverse
have h_2 : IsChain (fun (b a : α) ↦ r a b = true) ([a] ++ g)
Tactic: rw [reverse_append, reverse_cons, reverse_nil, nil_append, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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 []
⊢ IsChain (fun (x y : α) ↦ r x y = true) m
have 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
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
Cleared hypotheses: l, a, g, hga, hg, h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ IsChain (fun (x y : α) ↦ r x y = true) m
have 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
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
Cleared hypotheses: l, a, g, hga, hg, h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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 (x y : α) ↦ r x y = true) m
have apply : ∀ (b : α), Membership.mem (γ := Option α) (head? []) b → r b a = true
Tactic: apply isChain_of_mem_splitByLoop _ _ h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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
⊢ IsChain (fun (x y : α) ↦ r x y = true) m
have apply₁ : IsChain (fun (y x : α) ↦ r x y = true) []
Tactic: apply isChain_of_mem_splitByLoop _ _ h
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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 (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (splitBy.loop r [] a g gs)
have nil : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
  (gs.reverse ++ [(a :: g).reverse])
Tactic: rw [splitBy.loop, reverse_cons]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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 (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (gs.reverse ++ [(a :: g).reverse])
have nil : IsChain (fun (b a : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
  (gs.reverse ++ [(a :: g).reverse]).reverse
Tactic: apply List.isChain_reverse.1
-- 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
⊢ 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)
have 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))
Tactic: rw [splitBy.loop]
-- 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
⊢ 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))
have 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)
Tactic: split
-- 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
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)
⊢ 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))
have 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))
Tactic: split
-- 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
⊢ 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)
have 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
Tactic: refine IH hgs' hgs fun m hm ↦ ?_