awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
m : List α
r : α → α → Bool
l : List α
hn : l ≠ []
h : IsChain (fun (x y : α) ↦ r x y = true) l
ha : ∀ (x : α), x ∈ m.head? → r (l.getLast hn) x = false
⊢ splitBy r (l ++ m) = l :: splitBy r m
have nil : ∀ (hn : Ne.{u_1 + 1} (α := List α) [] []) (h : IsChain (fun (x y : α) ↦ r x y = true) [])
  (ha : ∀ (x : α), x ∈ m.head? → r (getLast [] hn) x = false), splitBy r ([] ++ m) = [] :: splitBy r m
Tactic: cases l with
  | nil => contradiction
  | cons a l => rw [cons_append, splitBy, splitByLoop_append h ha]; simp
Cleared hypotheses: l, hn, h, ha
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
m : List α
r : α → α → Bool
l : List α
hn : l ≠ []
h : IsChain (fun (x y : α) ↦ r x y = true) l
ha : ∀ (x : α), x ∈ m.head? → r (l.getLast hn) x = false
nil :
  ∀ (hn : Ne.{u_1 + 1} (α := List α) [] []) (h : IsChain (fun (x y : α) ↦ r x y = true) [])
    (ha : ∀ (x : α), x ∈ m.head? → r (getLast [] hn) x = false), splitBy r ([] ++ m) = [] :: splitBy r m
⊢ splitBy r (l ++ m) = l :: splitBy r m
have cons : ∀ (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
Tactic: cases l with
  | nil => contradiction
  | cons a l => rw [cons_append, splitBy, splitByLoop_append h ha]; simp
Cleared hypotheses: l, hn, h, ha
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (hypothesis)
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬[] ∈ a :: l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (a :: l)
⊢ splitBy r (a :: l).flatten = a :: l
have hn₁ : ¬a = [] ∧ ¬[] ∈ l
Tactic: rw [mem_cons, not_or, eq_comm] at hn
Cleared hypotheses: hn, hc, hc'
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (a :: l)
⊢ splitBy r (a :: l).flatten = a :: l
have cons : ∀ (x : α), x ∈ l.flatten.head? → r (a.getLast sorry) x = false
Tactic: rw [flatten_cons, splitBy_append_of_isChain hn.1 (hc _ mem_cons_self),
      IH hn.2 (fun m hm ↦ hc _ (mem_cons_of_mem a hm)) hc'.tail]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (a :: l)
y : α
hy : y ∈ l.flatten.head?
⊢ r (a.getLast ⋯) y = false
have cons : r (a.getLast sorry) (l.flatten.head sorry) = false
Tactic: rw [← head_of_mem_head? hy]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (a :: l)
y : α
hy : y ∈ l.flatten.head?
⊢ r (a.getLast ⋯) (l.flatten.head ⋯) = false
have cons : ∀
  (hc' :
    (∀ (y : List α), y ∈ l.head? → ∃ (ha : a ≠ []), ∃ (hb : y ≠ []), r (a.getLast ha) (y.head hb) = false) ∧
      IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l)
  (y : α) (hy : y ∈ l.flatten.head?), r (a.getLast sorry) (l.flatten.head sorry) = false
Tactic: rw [isChain_cons] at hc'
Cleared hypotheses: hc', y, hy
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' :
  (∀ (y : List α), y ∈ l.head? → ∃ (ha : a ≠ []), ∃ (hb : y ≠ []), r (a.getLast ha) (y.head hb) = false) ∧
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
y : α
hy : y ∈ l.flatten.head?
⊢ r (a.getLast ⋯) (l.flatten.head ⋯) = false
have cons : ∀ (x : List α) (hx : x ∈ l), x ≠ [] → r (a.getLast sorry) (l.flatten.head sorry) = false
Tactic: obtain ⟨x, hx, _⟩ := flatten_ne_nil_iff.1 (ne_nil_of_mem (mem_of_mem_head? hy))
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (hypothesis)
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' :
  (∀ (y : List α), y ∈ l.head? → ∃ (ha : a ≠ []), ∃ (hb : y ≠ []), r (a.getLast ha) (y.head hb) = false) ∧
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
y : α
hy : y ∈ l.flatten.head?
x : List α
hx : x ∈ l
right : x ≠ []
⊢ r (a.getLast ⋯) (l.flatten.head ⋯) = false
have w : a ≠ []
Tactic: obtain ⟨_, _, H⟩ := hc'.1 (l.head (ne_nil_of_mem hx)) (head_mem_head? _)
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (hypothesis)
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' :
  (∀ (y : List α), y ∈ l.head? → ∃ (ha : a ≠ []), ∃ (hb : y ≠ []), r (a.getLast ha) (y.head hb) = false) ∧
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
y : α
hy : y ∈ l.flatten.head?
x : List α
hx : x ∈ l
right : x ≠ []
w : a ≠ []
⊢ r (a.getLast ⋯) (l.flatten.head ⋯) = false
have w₁ : l.head sorry ≠ []
Tactic: obtain ⟨_, _, H⟩ := hc'.1 (l.head (ne_nil_of_mem hx)) (head_mem_head? _)
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (hypothesis)
Goal:
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
    splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' :
  (∀ (y : List α), y ∈ l.head? → ∃ (ha : a ≠ []), ∃ (hb : y ≠ []), r (a.getLast ha) (y.head hb) = false) ∧
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
y : α
hy : y ∈ l.flatten.head?
x : List α
hx : x ∈ l
right : x ≠ []
w : a ≠ []
w₁ : l.head ⋯ ≠ []
⊢ r (a.getLast ⋯) (l.flatten.head ⋯) = false
have H : r (a.getLast w) ((l.head sorry).head w₁) = false
Tactic: obtain ⟨_, _, H⟩ := hc'.1 (l.head (ne_nil_of_mem hx)) (head_mem_head? _)
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l : List (List α)
hn : ¬[] ∈ l
hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
⊢ splitBy r l.flatten = l
have nil : ∀ (hn : ¬Membership.mem (γ := List (List α)) [] [])
  (hc : ∀ (m : List α), Membership.mem (γ := List (List α)) [] m → IsChain (fun (x y : α) ↦ r x y = true) m)
  (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) []),
  splitBy r (flatten []) = []
Tactic: induction l with
  | nil => rfl
  | cons a l IH =>
    rw [mem_cons, not_or, eq_comm] at hn
    rw [flatten_cons, splitBy_append_of_isChain hn.1 (hc _ mem_cons_self),
      IH hn.2 (fun m hm ↦ hc _ (mem_cons_of_mem a hm)) hc'.tail]
    intro y hy
    rw [← head_of_mem_head? hy]
    rw [isChain_cons] at hc'
    obtain ⟨x, hx, _⟩ := flatten_ne_nil_iff.1 (ne_nil_of_mem (mem_of_mem_head? hy))
    obtain ⟨_, _, H⟩ := hc'.1 (l.head (ne_nil_of_mem hx)) (head_mem_head? _)
    rwa [head_flatten_eq_head_head]
Cleared hypotheses: l, hn, hc, hc'
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l : List (List α)
hn : ¬[] ∈ l
hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m
hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
nil :
  ∀ (hn : ¬Membership.mem (γ := List (List α)) [] [])
    (hc : ∀ (m : List α), Membership.mem (γ := List (List α)) [] m → IsChain (fun (x y : α) ↦ r x y = true) m)
    (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) []),
    splitBy r (flatten []) = []
⊢ splitBy r l.flatten = l
have cons : ∀ (a : List α) (l : List (List α))
  (IH :
    ∀ (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m)
      (hc' : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l),
      splitBy r l.flatten = l)
  (hn : ¬[] ∈ a :: l) (hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun (x y : α) ↦ r x y = true) m)
  (hc' :
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (a :: l)),
  splitBy r (a :: l).flatten = a :: l
Tactic: induction l with
  | nil => rfl
  | cons a l IH =>
    rw [mem_cons, not_or, eq_comm] at hn
    rw [flatten_cons, splitBy_append_of_isChain hn.1 (hc _ mem_cons_self),
      IH hn.2 (fun m hm ↦ hc _ (mem_cons_of_mem a hm)) hc'.tail]
    intro y hy
    rw [← head_of_mem_head? hy]
    rw [isChain_cons] at hc'
    obtain ⟨x, hx, _⟩ := flatten_ne_nil_iff.1 (ne_nil_of_mem (mem_of_mem_head? hy))
    obtain ⟨_, _, H⟩ := hc'.1 (l.head (ne_nil_of_mem hx)) (head_mem_head? _)
    rwa [head_flatten_eq_head_head]
Cleared hypotheses: l, hn, hc, hc'
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
m : List α
r : α → α → Bool
l : List (List α)
⊢ splitBy r m = l ↔
    m = l.flatten ∧
      ¬[] ∈ l ∧
        (∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m) ∧
          IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
have mp : splitBy r m = l →
  m = l.flatten ∧
    ¬[] ∈ l ∧
      (∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m) ∧
        IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
m : List α
r : α → α → Bool
l : List (List α)
mp :
  splitBy r m = l →
    m = l.flatten ∧
      ¬[] ∈ l ∧
        (∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m) ∧
          IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
⊢ splitBy r m = l ↔
    m = l.flatten ∧
      ¬[] ∈ l ∧
        (∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m) ∧
          IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
have mpr : m = l.flatten ∧
    ¬[] ∈ l ∧
      (∀ (m : List α), m ∈ l → IsChain (fun (x y : α) ↦ r x y = true) m) ∧
        IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l →
  splitBy r m = l
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
⊢ splitBy r (l ++ m) = splitBy r l ++ splitBy r m
have inl : ∀ (ha : ∀ (x : α), Membership.mem (γ := Option α) (getLast? []) x → ∀ (y : α), y ∈ m.head? → r x y = false),
  splitBy r ([] ++ m) = splitBy r [] ++ splitBy r m
Tactic: obtain rfl | hl := eq_or_ne l []
Cleared hypotheses: l, ha
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
inl :
  ∀ (ha : ∀ (x : α), Membership.mem (γ := Option α) (getLast? []) x → ∀ (y : α), y ∈ m.head? → r x y = false),
    splitBy r ([] ++ m) = splitBy r [] ++ splitBy r m
⊢ splitBy r (l ++ m) = splitBy r l ++ splitBy r m
have inr : ∀ (hl : l ≠ []), splitBy r (l ++ m) = splitBy r l ++ splitBy r m
Tactic: obtain rfl | hl := eq_or_ne l []
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
⊢ splitBy r (l ++ m) = splitBy r l ++ splitBy r m
have inr : ∀ (ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), Membership.mem (γ := Option α) (head? []) y → r x y = false),
  splitBy r (l ++ []) = splitBy r l ++ splitBy r []
Tactic: obtain rfl | hm := eq_or_ne m []
Cleared hypotheses: m, ha
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
inr :
  ∀ (ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), Membership.mem (γ := Option α) (head? []) y → r x y = false),
    splitBy r (l ++ []) = splitBy r l ++ splitBy r []
⊢ splitBy r (l ++ m) = splitBy r l ++ splitBy r m
have inr₁ : ∀ (hm : m ≠ []), splitBy r (l ++ m) = splitBy r l ++ splitBy r m
Tactic: obtain rfl | hm := eq_or_ne m []
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ splitBy r (l ++ m) = splitBy r l ++ splitBy r m
have inr : l ++ m = (splitBy r l ++ splitBy r m).flatten ∧
  ¬[] ∈ splitBy r l ++ splitBy r m ∧
    (∀ (m_1 : List α), m_1 ∈ splitBy r l ++ splitBy r m → IsChain (fun (x y : α) ↦ r x y = true) m_1) ∧
      IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
        (splitBy r l ++ splitBy r m)
Tactic: rw [splitBy_eq_iff]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ l ++ m = (splitBy r l ++ splitBy r m).flatten ∧
    ¬[] ∈ splitBy r l ++ splitBy r m ∧
      (∀ (m_1 : List α), m_1 ∈ splitBy r l ++ splitBy r m → IsChain (fun (x y : α) ↦ r x y = true) m_1) ∧
        IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
          (splitBy r l ++ splitBy r m)
have inr : ∀ (m_1 : List α), m_1 ∈ splitBy r l ++ splitBy r m → IsChain (fun (x y : α) ↦ r x y = true) m_1
Tactic: refine ⟨by simp, by simp, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
inr : ∀ (m_1 : List α), m_1 ∈ splitBy r l ++ splitBy r m → IsChain (fun (x y : α) ↦ r x y = true) m_1
⊢ l ++ m = (splitBy r l ++ splitBy r m).flatten ∧
    ¬[] ∈ splitBy r l ++ splitBy r m ∧
      (∀ (m_1 : List α), m_1 ∈ splitBy r l ++ splitBy r m → IsChain (fun (x y : α) ↦ r x y = true) m_1) ∧
        IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
          (splitBy r l ++ splitBy r m)
have inr₁ : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
  (splitBy r l ++ splitBy r m)
Tactic: refine ⟨by simp, by simp, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (splitBy r l ++ splitBy r m)
have inr : IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (splitBy r l) ∧
  IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (splitBy r m) ∧
    ∀ (x : List α),
      x ∈ (splitBy r l).getLast? →
        ∀ (y : List α), y ∈ (splitBy r m).head? → ∃ (ha : x ≠ []), ∃ (hb : y ≠ []), r (x.getLast ha) (y.head hb) = false
Tactic: rw [isChain_append]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (splitBy r l) ∧
    IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
        (splitBy r m) ∧
      ∀ (x : List α),
        x ∈ (splitBy r l).getLast? →
          ∀ (y : List α),
            y ∈ (splitBy r m).head? → ∃ (ha : x ≠ []), ∃ (hb : y ≠ []), r (x.getLast ha) (y.head hb) = false
have inr : ∀ (x : List α) (hx : x ∈ (splitBy r l).getLast?) (y : List α) (hy : y ∈ (splitBy r m).head?),
  ∃ (ha : x ≠ []), ∃ (hb : y ≠ []), r (x.getLast ha) (y.head hb) = false
Tactic: refine ⟨isChain_getLast_head_splitBy _ _, isChain_getLast_head_splitBy _ _, fun x hx y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ ∃ (ha : x ≠ []), ∃ (hb : y ≠ []), r (x.getLast ha) (y.head hb) = false
have h : r (x.getLast sorry) (y.head sorry) = false
Tactic: use ne_nil_of_mem_splitBy (mem_of_mem_getLast? hx), ne_nil_of_mem_splitBy (mem_of_mem_head? hy)
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ r (x.getLast ⋯) (y.head ⋯) = false
have h : x.getLast sorry ∈ l.getLast?
Tactic: apply ha
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
h : x.getLast ⋯ ∈ l.getLast?
⊢ r (x.getLast ⋯) (y.head ⋯) = false
have h₁ : y.head sorry ∈ m.head?
Tactic: apply ha
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ x.getLast ⋯ ∈ l.getLast?
have h : l.getLast hl ∈ l.getLast?
Tactic: simp_rw [← getLast_of_mem_getLast? hx, getLast_getLast_splitBy _ hl]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ y.head ⋯ ∈ m.head?
have h : m.head hm ∈ m.head?
Tactic: simp_rw [← head_of_mem_head? hy, head_head_splitBy _ hm]
-- Lean 4 proof step from Mathlib.Data.List.SplitBy (goal)
Goal:
α : Type u_1
r : α → α → Bool
l : List α
a : α
m : List α
ha : ∀ (x : α), x ∈ l.getLast? → r x a = false
⊢ splitBy r (l ++ a :: m) = splitBy r l ++ splitBy r (a :: m)
have ha₁ : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ (a :: m).head? → r x y = false
Tactic: apply splitBy_append
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
⊢ (sz.splitLengths l).length = sz.length
have nil : ∀ (l : List α), (splitLengths [] l).length = length (α := ℕ) []
Tactic: induction sz generalizing l
Cleared hypotheses: l, sz
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
nil : ∀ (l : List α), (splitLengths [] l).length = length (α := ℕ) []
⊢ (sz.splitLengths l).length = sz.length
have cons : ∀ (head : ℕ) (tail : List ℕ),
  (∀ (l : List α), (tail.splitLengths l).length = tail.length) →
    ∀ (l : List α), ((head :: tail).splitLengths l).length = (head :: tail).length
Tactic: induction sz generalizing l
Cleared hypotheses: l, sz
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
⊢ take i (sz.splitLengths l) = (take i sz).splitLengths l
have induction : ∀ (l : List α) (sz : List ℕ), take 0 (sz.splitLengths l) = (take 0 sz).splitLengths l
Tactic: induction i generalizing sz l
Cleared hypotheses: l, sz, i
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
induction : ∀ (l : List α) (sz : List ℕ), take 0 (sz.splitLengths l) = (take 0 sz).splitLengths l
⊢ take i (sz.splitLengths l) = (take i sz).splitLengths l
have succ : ∀ (n : ℕ),
  (∀ (l : List α) (sz : List ℕ), take n (sz.splitLengths l) = (take n sz).splitLengths l) →
    ∀ (l : List α) (sz : List ℕ), take (n + 1) (sz.splitLengths l) = (take (n + 1) sz).splitLengths l
Tactic: induction i generalizing sz l
Cleared hypotheses: l, sz, i
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
sz : List ℕ
⊢ take (i + 1) (sz.splitLengths l) = (take (i + 1) sz).splitLengths l
have nil : take (i + 1) (splitLengths [] l) = splitLengths (take (i + 1) []) l
Tactic: cases sz
Cleared hypotheses: sz
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
sz : List ℕ
nil : take (i + 1) (splitLengths [] l) = splitLengths (take (i + 1) []) l
⊢ take (i + 1) (sz.splitLengths l) = (take (i + 1) sz).splitLengths l
have cons : ∀ (head : ℕ) (tail : List ℕ),
  take (i + 1) ((head :: tail).splitLengths l) = (take (i + 1) (head :: tail)).splitLengths l
Tactic: cases sz
Cleared hypotheses: sz