awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
m : List α
r : α → α → Bool
⊢ m = (splitBy r m).flatten ∧
    ¬[] ∈ splitBy r m ∧
      (∀ (m_1 : List α), m_1 ∈ 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 m)

Tactic:
exact ⟨(flatten_splitBy r m).symm, nil_notMem_splitBy r m, fun _ ↦ isChain_of_mem_splitBy,
      isChain_getLast_head_splitBy r m⟩
-- Module: Mathlib.Data.List.SplitBy
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

Tactic:
splitBy_flatten hn hc hc'

Premises used: List.splitBy_flatten
-- Module: Mathlib.Data.List.SplitBy
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

Tactic:
exact splitBy_flatten hn hc hc'

Premises used: List.splitBy_flatten
-- Module: Mathlib.Data.List.SplitBy
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
inr : ∀ (hl : l ≠ []), splitBy r (l ++ m) = splitBy r l ++ splitBy r m
⊢ splitBy r (l ++ m) = splitBy r l ++ splitBy r m

Tactic:
obtain rfl | hl := eq_or_ne l []

Premises used: eq_or_ne, rfl, List.nil
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
m : List α
ha : ∀ (x : α), Membership.mem (γ := Option α) (getLast? []) x → ∀ (y : α), y ∈ m.head? → r x y = false
⊢ splitBy r ([] ++ m) = splitBy r [] ++ splitBy r m

Tactic:
simp
-- Module: Mathlib.Data.List.SplitBy
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 []
inr₁ : ∀ (hm : m ≠ []), splitBy r (l ++ m) = splitBy r l ++ splitBy r m
⊢ splitBy r (l ++ m) = splitBy r l ++ splitBy r m

Tactic:
obtain rfl | hm := eq_or_ne m []

Premises used: eq_or_ne, rfl, List.nil
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
hl : l ≠ []
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), Membership.mem (γ := Option α) (head? []) y → r x y = false
⊢ splitBy r (l ++ []) = splitBy r l ++ splitBy r []

Tactic:
simp
-- Module: Mathlib.Data.List.SplitBy
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 :
  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)
⊢ splitBy r (l ++ m) = splitBy r l ++ splitBy r m

Tactic:
rw [splitBy_eq_iff]

Premises used: List.splitBy_eq_iff
-- Module: Mathlib.Data.List.SplitBy
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

Tactic:
simp
-- Module: Mathlib.Data.List.SplitBy
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 ++ splitBy r m

Tactic:
simp
-- Module: Mathlib.Data.List.SplitBy
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
inr₁ :
  IsChain (fun (a b : List α) ↦ ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
    (splitBy r l ++ splitBy r 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)

Tactic:
refine ⟨by simp, by simp, ?_, ?_⟩
-- Module: Mathlib.Data.List.SplitBy
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 ≠ []
⊢ ∀ (m_1 : List α), m_1 ∈ splitBy r l ++ splitBy r m → IsChain (fun (x y : α) ↦ r x y = true) m_1

Tactic:
aesop (add apply unsafe isChain_of_mem_splitBy)

Premises used: List.isChain_of_mem_splitBy
-- Module: Mathlib.Data.List.SplitBy
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 :
  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
⊢ 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 [isChain_append]

Premises used: List.isChain_append
-- Module: Mathlib.Data.List.SplitBy
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

Tactic:
⟨isChain_getLast_head_splitBy _ _, isChain_getLast_head_splitBy _ _, fun x hx y hy ↦ ?_⟩

Premises used: List.isChain_getLast_head_splitBy, And.intro
-- Module: Mathlib.Data.List.SplitBy
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 :
  ∀ (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
⊢ 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:
refine ⟨isChain_getLast_head_splitBy _ _, isChain_getLast_head_splitBy _ _, fun x hx y hy ↦ ?_⟩
-- Module: Mathlib.Data.List.SplitBy
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 : r (x.getLast ⋯) (y.head ⋯) = false
⊢ ∃ (ha : x ≠ []), ∃ (hb : y ≠ []), r (x.getLast ha) (y.head hb) = false

Tactic:
use ne_nil_of_mem_splitBy (mem_of_mem_getLast? hx), ne_nil_of_mem_splitBy (mem_of_mem_head? hy)

Premises used: List.mem_of_mem_head?, List.ne_nil_of_mem_splitBy, List.mem_of_mem_getLast?
-- Module: Mathlib.Data.List.SplitBy
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?
h₁ : y.head ⋯ ∈ m.head?
⊢ r (x.getLast ⋯) (y.head ⋯) = false

Tactic:
apply ha
-- Module: Mathlib.Data.List.SplitBy
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 : l.getLast hl ∈ l.getLast?
⊢ x.getLast ⋯ ∈ l.getLast?

Tactic:
simp_rw [← getLast_of_mem_getLast? hx, getLast_getLast_splitBy _ hl]

Premises used: List.getLast_getLast_splitBy, List.getLast_of_mem_getLast?
-- Module: Mathlib.Data.List.SplitBy
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?
⊢ l.getLast hl ∈ l.getLast?

Tactic:
getLast_mem_getLast? _

Premises used: List.getLast_mem_getLast?
-- Module: Mathlib.Data.List.SplitBy
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?
⊢ l.getLast hl ∈ l.getLast?

Tactic:
exact getLast_mem_getLast? _

Premises used: List.getLast_mem_getLast?
-- Module: Mathlib.Data.List.SplitBy
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 : m.head hm ∈ m.head?
⊢ y.head ⋯ ∈ m.head?

Tactic:
simp_rw [← head_of_mem_head? hy, head_head_splitBy _ hm]

Premises used: List.head_of_mem_head?, List.head_head_splitBy
-- Module: Mathlib.Data.List.SplitBy
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?
⊢ m.head hm ∈ m.head?

Tactic:
head_mem_head? _

Premises used: List.head_mem_head?
-- Module: Mathlib.Data.List.SplitBy
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?
⊢ m.head hm ∈ m.head?

Tactic:
exact head_mem_head? _

Premises used: List.head_mem_head?
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
a : α
m : List α
ha : ∀ (x : α), x ∈ l.getLast? → r x a = false
ha₁ : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ (a :: m).head? → r x y = false
⊢ splitBy r (l ++ a :: m) = splitBy r l ++ splitBy r (a :: m)

Tactic:
apply splitBy_append

Premises used: List.splitBy_append
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
l : List α
a : α
m : List α
ha : ∀ (x : α), x ∈ l.getLast? → r x a = false
⊢ ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ (a :: m).head? → r x y = false

Tactic:
simpa
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
nil : ∀ (l : List α), (splitLengths [] l).length = length (α := ℕ) []
cons :
  ∀ (head : ℕ) (tail : List ℕ),
    (∀ (l : List α), (tail.splitLengths l).length = tail.length) →
      ∀ (l : List α), ((head :: tail).splitLengths l).length = (head :: tail).length
⊢ (sz.splitLengths l).length = sz.length

Tactic:
induction sz generalizing l
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
⊢ (splitLengths [] l).length = length (α := ℕ) []

Tactic:
simp [splitLengths, *]

Premises used: List.splitLengths
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α), (tail.splitLengths l).length = tail.length
l : List α
⊢ ((head :: tail).splitLengths l).length = (head :: tail).length

Tactic:
simp [splitLengths, *]

Premises used: List.splitLengths
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
⊢ splitLengths [] l = []

Tactic:
rfl

Premises used: rfl, List.splitLengths
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
n : ℕ
⊢ (n :: sz).splitLengths l = take n l :: sz.splitLengths (drop n l)

Tactic:
simp [splitLengths]

Premises used: List.splitLengths
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
induction : ∀ (l : List α) (sz : List ℕ), take 0 (sz.splitLengths l) = (take 0 sz).splitLengths l
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
⊢ take i (sz.splitLengths l) = (take i sz).splitLengths l

Tactic:
induction i generalizing sz l
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
⊢ take 0 (sz.splitLengths l) = (take 0 sz).splitLengths l

Tactic:
simp
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
⊢ take 0 (sz.splitLengths l) = (take 0 sz).splitLengths l

Tactic:
case zero => simp
-- Module: Mathlib.Data.List.SplitLengths
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
cons :
  ∀ (head : ℕ) (tail : List ℕ),
    take (i + 1) ((head :: tail).splitLengths l) = (take (i + 1) (head :: tail)).splitLengths l
⊢ take (i + 1) (sz.splitLengths l) = (take (i + 1) sz).splitLengths l

Tactic:
cases sz
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
⊢ take (i + 1) (splitLengths [] l) = splitLengths (take (i + 1) []) l

Tactic:
simp
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
head : ℕ
tail : List ℕ
⊢ take (i + 1) ((head :: tail).splitLengths l) = (take (i + 1) (head :: tail)).splitLengths l

Tactic:
simp only [splitLengths_cons, take_succ_cons, hi]

Premises used: List.take_succ_cons, List.splitLengths_cons
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ i < sz.length

Tactic:
simpa using hi
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < (sz.splitLengths l).length
nil :
  ∀ (l : List α) {i : ℕ} {hi : i < (splitLengths [] l).length},
    (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (splitLengths [] l) i hi).length ≤
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] i ⋯
cons :
  ∀ (head : ℕ) (tail : List ℕ),
    (∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length},
        (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (tail.splitLengths l) i hi).length ≤
          getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) tail i ⋯) →
      ∀ (l : List α) {i : ℕ} {hi : i < ((head :: tail).splitLengths l).length},
        (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) ((head :: tail).splitLengths l) i
              hi).length ≤
          getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) i ⋯
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (sz.splitLengths l) i hi).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i ⋯

Tactic:
induction sz generalizing l i
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
i : ℕ
hi : i < (splitLengths [] l).length
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (splitLengths [] l) i hi).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] i ⋯

Tactic:
simp at hi
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih :
  ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length},
    (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (tail.splitLengths l) i hi).length ≤
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) tail i ⋯
l : List α
i : ℕ
hi : i < ((head :: tail).splitLengths l).length
simp :
  (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take head l :: tail.splitLengths (drop head l))
        i ⋯).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) i ⋯
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) ((head :: tail).splitLengths l) i hi).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) i ⋯

Tactic:
simp only [splitLengths_cons]

Premises used: List.splitLengths_cons
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih :
  ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length},
    (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (tail.splitLengths l) i hi).length ≤
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) tail i ⋯
l : List α
i : ℕ
hi : i < ((head :: tail).splitLengths l).length
zero :
  ∀ {hi : 0 < ((head :: tail).splitLengths l).length},
    (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length)
          (take head l :: tail.splitLengths (drop head l)) 0 ⋯).length ≤
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) 0 ⋯
succ :
  ∀ (n : ℕ) {hi : n + 1 < ((head :: tail).splitLengths l).length},
    (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length)
          (take head l :: tail.splitLengths (drop head l)) (n + 1) ⋯).length ≤
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) (n + 1) ⋯
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take head l :: tail.splitLengths (drop head l))
        i ⋯).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) i ⋯

Tactic:
cases i
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih :
  ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length},
    (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (tail.splitLengths l) i hi).length ≤
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) tail i ⋯
l : List α
hi : 0 < ((head :: tail).splitLengths l).length
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take head l :: tail.splitLengths (drop head l))
        0 ⋯).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) 0 ⋯

Tactic:
simp
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih :
  ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length},
    (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (tail.splitLengths l) i hi).length ≤
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) tail i ⋯
l : List α
n : ℕ
hi : n + 1 < ((head :: tail).splitLengths l).length
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take head l :: tail.splitLengths (drop head l))
        (n + 1) ⋯).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) (n + 1) ⋯

Tactic:
simp only [getElem_cons_succ, tail_ih]

Premises used: List.getElem_cons_succ
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
h : l.length ≤ sz.sum
nil : ∀ (l : List α) (h : l.length ≤ sum []), (splitLengths [] l).flatten = l
cons :
  ∀ (head : ℕ) (tail : List ℕ),
    (∀ (l : List α) (h : l.length ≤ tail.sum), (tail.splitLengths l).flatten = l) →
      ∀ (l : List α) (h : l.length ≤ (head :: tail).sum), ((head :: tail).splitLengths l).flatten = l
⊢ (sz.splitLengths l).flatten = l

Tactic:
induction sz generalizing l
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
h : l.length ≤ sum []
⊢ (splitLengths [] l).flatten = l

Tactic:
simp_all
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α) (h : l.length ≤ tail.sum), (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
simp : take head l ++ (tail.splitLengths (drop head l)).flatten = l
⊢ ((head :: tail).splitLengths l).flatten = l

Tactic:
simp only [splitLengths_cons, flatten_cons]

Premises used: List.splitLengths_cons, List.flatten_cons
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α) (h : l.length ≤ tail.sum), (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
h₁ : (drop head l).length ≤ tail.sum
⊢ take head l ++ (tail.splitLengths (drop head l)).flatten = l

Tactic:
rw [ih, take_append_drop]

Premises used: List.take_append_drop
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α) (h : l.length ≤ tail.sum), (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ (drop head l).length ≤ tail.sum

Tactic:
simpa [add_comm] using h

Premises used: add_comm
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
nil : ∀ (l : List α) (h : sum [] ≤ l.length), map length (splitLengths [] l) = []
cons :
  ∀ (head : ℕ) (tail : List ℕ),
    (∀ (l : List α) (h : tail.sum ≤ l.length), map length (tail.splitLengths l) = tail) →
      ∀ (l : List α) (h : (head :: tail).sum ≤ l.length), map length ((head :: tail).splitLengths l) = head :: tail
⊢ map length (sz.splitLengths l) = sz

Tactic:
induction sz generalizing l
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
h : sum [] ≤ l.length
⊢ map length (splitLengths [] l) = []

Tactic:
simp
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α) (h : tail.sum ≤ l.length), map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
simp : head ≤ l.length ∧ map length (tail.splitLengths (drop head l)) = tail
⊢ map length ((head :: tail).splitLengths l) = head :: tail

Tactic:
simp only [splitLengths_cons, map_cons, length_take, cons.injEq, min_eq_left_iff]

Premises used: List.map_cons, List.length_take, List.cons.injEq, List.splitLengths_cons, min_eq_left_iff
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α) (h : tail.sum ≤ l.length), map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
rw : head ≤ l.length ∧ tail = tail
h₁ : tail.sum ≤ (drop head l).length
⊢ head ≤ l.length ∧ map length (tail.splitLengths (drop head l)) = tail

Tactic:
rw [ih]
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α) (h : tail.sum ≤ l.length), map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ head ≤ l.length ∧ tail = tail

Tactic:
simp [Nat.le_of_add_right_le h]

Premises used: Nat.le_of_add_right_le
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α) (h : tail.sum ≤ l.length), map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ tail.sum ≤ (drop head l).length

Tactic:
simp [Nat.le_sub_of_add_le' h]

Premises used: Nat.le_sub_of_add_le'
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ i < (sz.splitLengths l).length

Tactic:
simpa