awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Sort (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
head : α
tail : List α
ih : ∀ {c : List α} (hr : Pairwise r c) (hc : c <+ tail), c <+ insertionSort r tail
l₁ : List α
hr : Pairwise r (head :: l₁)
h : l₁ <+ tail
hr₁ : ∀ (a' : α), a' ∈ l₁ → r head a'
⊢ head :: l₁ <+ insertionSort r (head :: tail)
have hp : Pairwise r l₁
Tactic: obtain ⟨hr, hp⟩ := pairwise_cons.mp hr
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
head : α
tail : List α
ih : ∀ {c : List α} (hr : Pairwise r c) (hc : c <+ tail), c <+ insertionSort r tail
c : List α
hr : Pairwise r c
hc : c <+ head :: tail
⊢ c <+ insertionSort r (head :: tail)
have cons : ∀ (h : c <+ tail), c <+ insertionSort r (head :: tail)
Tactic: cases hc with
    | cons  _ h => exact ih hr h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      obtain ⟨hr, hp⟩ := pairwise_cons.mp hr
      exact cons_sublist_orderedInsert (ih hp h) hr
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
head : α
tail : List α
ih : ∀ {c : List α} (hr : Pairwise r c) (hc : c <+ tail), c <+ insertionSort r tail
c : List α
hr : Pairwise r c
hc : c <+ head :: tail
cons : ∀ (h : c <+ tail), c <+ insertionSort r (head :: tail)
⊢ c <+ insertionSort r (head :: tail)
have cons₁ : ∀ {l₁ : List α} (hr : Pairwise r (head :: l₁)) (h : l₁ <+ tail), head :: l₁ <+ insertionSort r (head :: tail)
Tactic: cases hc with
    | cons  _ h => exact ih hr h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      obtain ⟨hr, hp⟩ := pairwise_cons.mp hr
      exact cons_sublist_orderedInsert (ih hp h) hr
Cleared hypotheses: c, hr, hc
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l c : List α
hr : Pairwise r c
hc : c <+ l
⊢ c <+ insertionSort r l
have nil : ∀ {c : List α} (hr : Pairwise r c) (hc : c <+ []), c <+ insertionSort r []
Tactic: induction l generalizing c with
  | nil         => grind
  | cons _ _ ih =>
    cases hc with
    | cons  _ h => exact ih hr h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      obtain ⟨hr, hp⟩ := pairwise_cons.mp hr
      exact cons_sublist_orderedInsert (ih hp h) hr
Cleared hypotheses: l, c, hr, hc
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l c : List α
hr : Pairwise r c
hc : c <+ l
nil : ∀ {c : List α} (hr : Pairwise r c) (hc : c <+ []), c <+ insertionSort r []
⊢ c <+ insertionSort r l
have cons : ∀ (head : α) (tail : List α) (ih : ∀ {c : List α} (hr : Pairwise r c) (hc : c <+ tail), c <+ insertionSort r tail)
  {c : List α} (hr : Pairwise r c) (hc : c <+ head :: tail), c <+ insertionSort r (head :: tail)
Tactic: induction l generalizing c with
  | nil         => grind
  | cons _ _ ih =>
    cases hc with
    | cons  _ h => exact ih hr h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      obtain ⟨hr, hp⟩ := pairwise_cons.mp hr
      exact cons_sublist_orderedInsert (ih hp h) hr
Cleared hypotheses: l, c, hr, hc
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
l c : List α
hs : Pairwise r c
hc : c <+~ l
⊢ c <+ insertionSort r l
have obtain : ∀ (d : List α) (hc : d ~ c) (hd : d <+ l), c <+ insertionSort r l
Tactic: obtain ⟨d, hc, hd⟩ := hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.List.Sort (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
a : α
tail : List α
ih : ∀ {c : List α} (hs : Pairwise r c) (d : List α) (hc : d ~ c) (hd : d <+ tail), c <+ insertionSort r tail
c : List α
hs : Pairwise r c
l₁ : List α
hc : a :: l₁ ~ c
h : l₁ <+ tail
⊢ c <+ insertionSort r (a :: tail)
have ih₁ : c.erase a <+ insertionSort r tail
Tactic: specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.List.Sort (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
a : α
tail c : List α
hs : Pairwise r c
l₁ : List α
hc : a :: l₁ ~ c
h : l₁ <+ tail
ih : c.erase a <+ insertionSort r tail
⊢ c <+ insertionSort r (a :: tail)
have hm : a ∈ c
Tactic: have hm := hc.mem_iff.mp <| mem_cons_self ..
-- Lean 4 proof step from Mathlib.Data.List.Sort (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
a : α
tail c : List α
hs : Pairwise r c
l₁ : List α
hc : a :: l₁ ~ c
h : l₁ <+ tail
ih : c.erase a <+ insertionSort r tail
hm : a ∈ c
⊢ c <+ insertionSort r (a :: tail)
have he : orderedInsert r a (c.erase a) = c
Tactic: have he := orderedInsert_erase _ _ hm hs
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
a : α
tail : List α
ih : ∀ {c : List α} (hs : Pairwise r c) (d : List α) (hc : d ~ c) (hd : d <+ tail), c <+ insertionSort r tail
c : List α
hs : Pairwise r c
d : List α
hc : d ~ c
hd : d <+ a :: tail
⊢ c <+ insertionSort r (a :: tail)
have cons : ∀ (h : d <+ tail), c <+ insertionSort r (a :: tail)
Tactic: cases hd with
    | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h
      have hm := hc.mem_iff.mp <| mem_cons_self ..
      have he := orderedInsert_erase _ _ hm hs
      exact he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
a : α
tail : List α
ih : ∀ {c : List α} (hs : Pairwise r c) (d : List α) (hc : d ~ c) (hd : d <+ tail), c <+ insertionSort r tail
c : List α
hs : Pairwise r c
d : List α
hc : d ~ c
hd : d <+ a :: tail
cons : ∀ (h : d <+ tail), c <+ insertionSort r (a :: tail)
⊢ c <+ insertionSort r (a :: tail)
have cons₁ : ∀ {l₁ : List α} (hc : a :: l₁ ~ c) (h : l₁ <+ tail), c <+ insertionSort r (a :: tail)
Tactic: cases hd with
    | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h
      have hm := hc.mem_iff.mp <| mem_cons_self ..
      have he := orderedInsert_erase _ _ hm hs
      exact he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)
Cleared hypotheses: d, hc, hd
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
l c : List α
hs : Pairwise r c
d : List α
hc : d ~ c
hd : d <+ l
⊢ c <+ insertionSort r l
have nil : ∀ {c : List α} (hs : Pairwise r c) (d : List α) (hc : d ~ c) (hd : d <+ []), c <+ insertionSort r []
Tactic: induction l generalizing c d with
  | nil         => grind [nil_perm]
  | cons a _ ih =>
    cases hd with
    | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h
      have hm := hc.mem_iff.mp <| mem_cons_self ..
      have he := orderedInsert_erase _ _ hm hs
      exact he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)
Cleared hypotheses: l, c, hs, d, hc, hd
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
l c : List α
hs : Pairwise r c
d : List α
hc : d ~ c
hd : d <+ l
nil : ∀ {c : List α} (hs : Pairwise r c) (d : List α) (hc : d ~ c) (hd : d <+ []), c <+ insertionSort r []
⊢ c <+ insertionSort r l
have cons : ∀ (a : α) (tail : List α)
  (ih : ∀ {c : List α} (hs : Pairwise r c) (d : List α) (hc : d ~ c) (hd : d <+ tail), c <+ insertionSort r tail)
  {c : List α} (hs : Pairwise r c) (d : List α) (hc : d ~ c) (hd : d <+ a :: tail), c <+ insertionSort r (a :: tail)
Tactic: induction l generalizing c d with
  | nil         => grind [nil_perm]
  | cons a _ ih =>
    cases hd with
    | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h
      have hm := hc.mem_iff.mp <| mem_cons_self ..
      have he := orderedInsert_erase _ _ hm hs
      exact he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)
Cleared hypotheses: l, c, hs, d, hc, hd
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
l c : List α
hs : Pairwise r c
hc : c <+~ l
⊢ c <+ insertionSort r l
have obtain : ∀ (d : List α) (hc : d ~ c) (hd : d <+ l), c <+ insertionSort r l
Tactic: classical
  obtain ⟨d, hc, hd⟩ := hc
  induction l generalizing c d with
  | nil         => grind [nil_perm]
  | cons a _ ih =>
    cases hd with
    | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h
      have hm := hc.mem_iff.mp <| mem_cons_self ..
      have he := orderedInsert_erase _ _ hm hs
      exact he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Antisymm r
l₁ l₂ : List α
hp : l₁ <+~ l₂
hs₁ : Pairwise r l₁
hs₂ : Pairwise r l₂
⊢ l₁ <+ l₂
have let : ∀ (w : List α) (h : w ~ l₁) (h' : w <+ l₂), l₁ <+ l₂
Tactic: let ⟨_, h, h'⟩ := hp
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedLE ↔ Pairwise (fun (x1 x2 : α) ↦ x1 ≤ x2) l
have simp : (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
    (⟨i, h⟩ : Fin l.length) < ⟨i_1, h_1⟩ → l.get (⟨i, h⟩ : Fin l.length) ≤ l.get (⟨i_1, h_1⟩ : Fin l.length)) ↔
  Pairwise (fun (x1 x2 : α) ↦ x1 ≤ x2) l
Tactic: simp only [sortedLE_iff_monotone_get, monotone_iff_forall_lt, Fin.forall_iff]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedGE ↔ Pairwise (fun (x1 x2 : α) ↦ x1 ≥ x2) l
have simp : (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
    (⟨i, h⟩ : Fin l.length) < ⟨i_1, h_1⟩ → l.get (⟨i_1, h_1⟩ : Fin l.length) ≤ l.get (⟨i, h⟩ : Fin l.length)) ↔
  Pairwise (fun (x1 x2 : α) ↦ x1 ≥ x2) l
Tactic: simp only [sortedGE_iff_antitone_get, antitone_iff_forall_lt, Fin.forall_iff]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedLT ↔ Pairwise (fun (x1 x2 : α) ↦ x1 < x2) l
have simp : (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
    (⟨i, h⟩ : Fin l.length) < ⟨i_1, h_1⟩ → l.get (⟨i, h⟩ : Fin l.length) < l.get (⟨i_1, h_1⟩ : Fin l.length)) ↔
  Pairwise (fun (x1 x2 : α) ↦ x1 < x2) l
Tactic: simp only [sortedLT_iff_strictMono_get, StrictMono, Fin.forall_iff]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedGT ↔ Pairwise (fun (x1 x2 : α) ↦ x1 > x2) l
have simp : (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
    (⟨i, h⟩ : Fin l.length) < ⟨i_1, h_1⟩ → l.get (⟨i_1, h_1⟩ : Fin l.length) < l.get (⟨i, h⟩ : Fin l.length)) ↔
  Pairwise (fun (x1 x2 : α) ↦ x1 > x2) l
Tactic: simp only [sortedGT_iff_strictAnti_get, StrictAnti, Fin.forall_iff]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
l : List α
⊢ SortedLE.{u_2} (α := β) (map (⇑e : (a : α) → β) l) ↔ l.SortedLE
have simp_rw : List.Pairwise (fun (x1 x2 : β) ↦ x1 ≤ x2) (map (⇑e : (a : α) → β) l) ↔ List.Pairwise (fun (x1 x2 : α) ↦ x1 ≤ x2) l
Tactic: simp_rw [sortedLE_iff_pairwise, e.pairwise_listMap]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
l : List α
⊢ SortedLT.{u_2} (α := β) (map (⇑e : (a : α) → β) l) ↔ l.SortedLT
have simp_rw : List.Pairwise (fun (x1 x2 : β) ↦ x1 < x2) (map (⇑e : (a : α) → β) l) ↔ List.Pairwise (fun (x1 x2 : α) ↦ x1 < x2) l
Tactic: simp_rw [sortedLT_iff_pairwise]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
l : List α
⊢ SortedGE.{u_2} (α := β) (map (⇑e : (a : α) → β) l) ↔ l.SortedGE
have simp_rw : SortedLE.{u_2} (α := β) (reverse (map (⇑e : (a : α) → β) l)) ↔ l.reverse.SortedLE
Tactic: simp_rw [← sortedLE_reverse, ← map_reverse, sortedLE_listMap]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
l : List α
simp_rw : SortedLE.{u_2} (α := β) (reverse (map (⇑e : (a : α) → β) l)) ↔ l.reverse.SortedLE
⊢ SortedGE.{u_2} (α := β) (map (⇑e : (a : α) → β) l) ↔ l.SortedGE
have simp_rw₁ : SortedLE.{u_2} (α := β) (map (⇑e : (a : α) → β) l.reverse) ↔ l.reverse.SortedLE
Tactic: simp_rw [← sortedLE_reverse, ← map_reverse, sortedLE_listMap]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
l : List α
⊢ SortedGT.{u_2} (α := β) (map (⇑e : (a : α) → β) l) ↔ l.SortedGT
have simp_rw : SortedLT.{u_2} (α := β) (reverse (map (⇑e : (a : α) → β) l)) ↔ l.reverse.SortedLT
Tactic: simp_rw [← sortedLT_reverse, ← map_reverse, sortedLT_listMap]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
l : List α
simp_rw : SortedLT.{u_2} (α := β) (reverse (map (⇑e : (a : α) → β) l)) ↔ l.reverse.SortedLT
⊢ SortedGT.{u_2} (α := β) (map (⇑e : (a : α) → β) l) ↔ l.SortedGT
have simp_rw₁ : SortedLT.{u_2} (α := β) (map (⇑e : (a : α) → β) l.reverse) ↔ l.reverse.SortedLT
Tactic: simp_rw [← sortedLT_reverse, ← map_reverse, sortedLT_listMap]
-- 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 α)), 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 []
have cons : (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)) =
  HAppend.hAppend (β := List (List α)) gs.reverse
    (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: simp_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 α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
⊢ (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)) =
    HAppend.hAppend (β := List (List α)) gs.reverse
      (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) gs = gs.reverse ++ 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 α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
h_1 : ∀ (x : Bool), r a b = true → splitBy.loop r l b (a :: g) gs = gs.reverse ++ splitBy.loop r l b (a :: g) []
⊢ (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)) =
    HAppend.hAppend (β := List (List α)) gs.reverse
      (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 :: gs) = gs.reverse ++ 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 α} (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 = true
⊢ splitBy.loop r l b (a :: g) gs = gs.reverse ++ splitBy.loop r l b (a :: g) []
have h_1 : gs.reverse ++ splitBy.loop r l b (a :: g) [] = gs.reverse ++ splitBy.loop r l b (a :: g) []
Tactic: rw [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 α)), 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
⊢ splitBy.loop r l b [] ((a :: g).reverse :: gs) = gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]
have h_2 : ((a :: g).reverse :: gs).reverse ++ splitBy.loop r l b [] [] = gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]
Tactic: rw [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 α)), 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
| gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]
have rw : gs.reverse ++ ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] [])
Tactic: rw [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 α)), 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 ++ splitBy.loop r l b [] [(a :: g).reverse]
have h_2 : ((a :: g).reverse :: gs).reverse ++ splitBy.loop r l b [] [] =
  gs.reverse ++ ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] [])
Tactic: conv_rhs => rw [IH]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
gs : List (List α)
⊢ splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
have nil : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r [] a g gs = gs.reverse ++ splitBy.loop r [] 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
Cleared hypotheses: l, a, g, gs
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
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 []
⊢ splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
have 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 []
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
Cleared hypotheses: l, a, g, gs
-- 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 []).flatten = g.reverse ++ a :: l
a : α
g : List α
⊢ (splitBy.loop r (b :: l) a g []).flatten = g.reverse ++ a :: b :: l
have 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
Tactic: rw [splitBy.loop, splitByLoop_eq_append [_]]
-- 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 []).flatten = g.reverse ++ a :: l
a : α
g : List α
⊢ 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
have h_1 : ∀ (x : Bool), r a b = true → (splitBy.loop r l b (a :: g) []).flatten = g.reverse ++ a :: b :: l
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 []).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
⊢ 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
have h_2 : ∀ (x : Bool),
  r a b = false → ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] []).flatten = g.reverse ++ a :: b :: l
Tactic: split
-- 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 []).flatten = g.reverse ++ a :: l
have nil : ∀ {a : α} {g : List α}, (splitBy.loop r [] a g []).flatten = g.reverse ++ [a]
Tactic: induction l generalizing a g with
  | nil => simp [splitBy.loop]
  | cons b l IH =>
    rw [splitBy.loop, splitByLoop_eq_append [_]]
    split <;> simp [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 []).flatten = g.reverse ++ [a]
⊢ (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
have 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
Tactic: induction l generalizing a g with
  | nil => simp [splitBy.loop]
  | cons b l IH =>
    rw [splitBy.loop, splitByLoop_eq_append [_]]
    split <;> simp [IH]
Cleared hypotheses: l, a, g
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (hypothesis)
Goal:
α : Type u_1
r : α → α → Bool
l : List α
⊢ splitBy r l = [] ↔ l = []
have this : (splitBy r l).flatten = l
Tactic: have := flatten_splitBy r l
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l : List α
this : (splitBy r l).flatten = l
⊢ splitBy r l = [] ↔ l = []
have refine_1 : splitBy r l = [] → l = []
Tactic: refine ⟨fun _ ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l : List α
this : (splitBy r l).flatten = l
refine_1 : splitBy r l = [] → l = []
⊢ splitBy r l = [] ↔ l = []
have refine_2 : l = [] → splitBy r l = []
Tactic: refine ⟨fun _ ↦ ?_, ?_⟩