awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ take 1 (drop n l) = [l.get (⟨n, h⟩ : Fin l.length)]
have rw : [getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n h] = [l.get (⟨n, h⟩ : Fin l.length)]
Tactic: rw [drop_eq_getElem_cons h, take, take]
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
x : List α
n : ℕ
⊢ x = take n x ↔ x.length ≤ n
have rw : take n x = x ↔ x.length ≤ n
Tactic: rw [Eq.comm, take_eq_self_iff]
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
x : List α
n : ℕ
rw : take n x = x ↔ x.length ≤ n
⊢ x = take n x ↔ x.length ≤ n
have rw₁ : x.length ≤ n ↔ x.length ≤ n
Tactic: rw [Eq.comm, take_eq_self_iff]
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
x y : List α
n : ℕ
⊢ take n x = take n (x ++ y) ↔ y = [] ∨ n ≤ x.length
have rw : take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length
Tactic: rw [Eq.comm]
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
x : List α
m n : ℕ
⊢ take n (drop m x) ++ drop (m + n) x = drop m x
have rw : take n (drop m x) ++ drop n (drop m x) = drop m x
Tactic: rw [← drop_drop, take_append_drop]
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
x : List α
m n : ℕ
rw : take n (drop m x) ++ drop n (drop m x) = drop m x
⊢ take n (drop m x) ++ drop (m + n) x = drop m x
have rw₁ : drop m x = drop m x
Tactic: rw [← drop_drop, take_append_drop]
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
x : List α
m n : ℕ
⊢ take n (drop m x) ++ drop (n + m) x = drop m x
have rw : take n (drop m x) ++ drop (m + n) x = drop m x
Tactic: rw [Nat.add_comm, drop_take_append_drop]
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
x : List α
m n : ℕ
rw : take n (drop m x) ++ drop (m + n) x = drop m x
⊢ take n (drop m x) ++ drop (n + m) x = drop m x
have rw₁ : drop m x = drop m x
Tactic: rw [Nat.add_comm, drop_take_append_drop]
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]
have pos : ∀ (hl : l = []), drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]
Tactic: by_cases hl : l = []
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
pos : ∀ (hl : l = []), drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]
have neg : ∀ (hl : ¬l = []), drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]
Tactic: by_cases hl : l = []
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : ¬l = []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]
have neg : [l.getLast hl] = [(a :: l).getLast h]
Tactic: rw [length_cons, Nat.add_one_sub_one, List.drop_length_cons hl a]
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
l : List α
h : l ≠ []
⊢ drop (l.length - 1) l = [l.getLast h]
have nil : ∀ (h : Ne.{u + 1} (α := List α) [] []), drop (length.{u} (α := α) [] - 1) [] = [getLast [] h]
Tactic: induction l with
  | nil => aesop
  | cons a l ih =>
    by_cases hl : l = []
    · simp_all
    rw [length_cons, Nat.add_one_sub_one, List.drop_length_cons hl a]
    simp [getLast_cons, hl]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
l : List α
h : l ≠ []
nil : ∀ (h : Ne.{u + 1} (α := List α) [] []), drop (length.{u} (α := α) [] - 1) [] = [getLast [] h]
⊢ drop (l.length - 1) l = [l.getLast h]
have cons : ∀ (a : α) (l : List α) (ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]) (h : a :: l ≠ []),
  drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]
Tactic: induction l with
  | nil => aesop
  | cons a l ih =>
    by_cases hl : l = []
    · simp_all
    rw [length_cons, Nat.add_one_sub_one, List.drop_length_cons hl a]
    simp [getLast_cons, hl]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
l : List α
⊢ tail^[n + 1] l = drop (n + 1) l
have succ : Eq.{u + 1} (α := List α) (tail^[n + 1] []) (drop (n + 1) [])
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
l : List α
succ : Eq.{u + 1} (α := List α) (tail^[n + 1] []) (drop (n + 1) [])
⊢ tail^[n + 1] l = drop (n + 1) l
have succ₁ : ∀ (head : α) (tail : List α), List.tail^[n + 1] (head :: tail) = drop (n + 1) (head :: tail)
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ tail^[n] l = drop n l
have zero : ∀ (l : List α), tail^[0] l = drop 0 l
Tactic: induction n generalizing l with
  | zero => rfl
  | succ n ih => cases l <;> simp [*]
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
l : List α
n : ℕ
zero : ∀ (l : List α), tail^[0] l = drop 0 l
⊢ tail^[n] l = drop n l
have succ : ∀ (n : ℕ) (ih : ∀ (l : List α), tail^[n] l = drop n l) (l : List α), tail^[n + 1] l = drop (n + 1) l
Tactic: induction n generalizing l with
  | zero => rfl
  | succ n ih => cases l <;> simp [*]
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ (take n l).tail = take (n - 1) l.tail
have h : ∀ (i : ℕ) (a : α),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n l).tail i = some a ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n - 1) l.tail) i = some a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ (take n l).dropLast = take (n - 1) l.dropLast
have h : ∀ (i : ℕ) (a : α),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n l).dropLast i = some a ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n - 1) l.dropLast) i = some a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ (drop n l).tail = drop n l.tail
have h : ∀ (i : ℕ) (a : α),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop n l).tail i = some a ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop n l.tail) i = some a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ (drop n l).dropLast = drop n l.dropLast
have h : ∀ (i : ℕ) (a : α),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop n l).dropLast i = some a ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop n l.dropLast) i = some a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
inst : Inhabited α
l₁ l₂ : List α
n : ℕ
h : l₁.length = n
⊢ takeI n (l₁ ++ l₂) = l₁
have rw : takeI l₁.length (l₁ ++ l₂) = l₁
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
l₁ l₂ : List α
n : ℕ
a : α
h : l₁.length = n
⊢ takeD n (l₁ ++ l₂) a = l₁
have rw : takeD l₁.length (l₁ ++ l₂) a = l₁
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
p : α → Bool
a : α
l l₂ : List α
⊢ loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))
have false : ∀ (hp : p a = false), loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))
Tactic: cases hp : p a
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
p : α → Bool
a : α
l l₂ : List α
false : ∀ (hp : p a = Bool.false), loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))
⊢ loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))
have true : ∀ (hp : p a = true), loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))
Tactic: cases hp : p a
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
m : ℕ
xs : List α
⊢ dropSlice 0 m xs = take 0 xs ++ drop (0 + m) xs
have zero : dropSlice 0 m [] = HAppend.hAppend (α := List α) (take 0 []) (drop (0 + m) [])
Tactic: cases xs with grind [dropSlice]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
m : ℕ
xs : List α
zero : dropSlice 0 m [] = HAppend.hAppend (α := List α) (take 0 []) (drop (0 + m) [])
⊢ dropSlice 0 m xs = take 0 xs ++ drop (0 + m) xs
have zero₁ : ∀ (head : α) (tail : List α), dropSlice 0 m (head :: tail) = take 0 (head :: tail) ++ drop (0 + m) (head :: tail)
Tactic: cases xs with grind [dropSlice]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
m n : ℕ
h : ∀ (xs : List α), dropSlice n m xs = take n xs ++ drop (n + m) xs
xs : List α
⊢ dropSlice (n + 1) m xs = take (n + 1) xs ++ drop (n + 1 + m) xs
have succ : dropSlice (n + 1) m [] = HAppend.hAppend (α := List α) (take (n + 1) []) (drop (n + 1 + m) [])
Tactic: cases xs with grind [dropSlice]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
m n : ℕ
h : ∀ (xs : List α), dropSlice n m xs = take n xs ++ drop (n + m) xs
xs : List α
succ : dropSlice (n + 1) m [] = HAppend.hAppend (α := List α) (take (n + 1) []) (drop (n + 1 + m) [])
⊢ dropSlice (n + 1) m xs = take (n + 1) xs ++ drop (n + 1 + m) xs
have succ₁ : ∀ (head : α) (tail : List α),
  dropSlice (n + 1) m (head :: tail) = take (n + 1) (head :: tail) ++ drop (n + 1 + m) (head :: tail)
Tactic: cases xs with grind [dropSlice]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
xs : List α
n m : ℕ
⊢ dropSlice n m xs = take n xs ++ drop (n + m) xs
have zero : ∀ (xs : List α), dropSlice 0 m xs = take 0 xs ++ drop (0 + m) xs
Tactic: induction n generalizing xs with cases xs with grind [dropSlice]
Cleared hypotheses: xs, n
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
xs : List α
n m : ℕ
zero : ∀ (xs : List α), dropSlice 0 m xs = take 0 xs ++ drop (0 + m) xs
⊢ dropSlice n m xs = take n xs ++ drop (n + m) xs
have succ : ∀ (n : ℕ),
  (∀ (xs : List α), dropSlice n m xs = take n xs ++ drop (n + m) xs) →
    ∀ (xs : List α), dropSlice (n + 1) m xs = take (n + 1) xs ++ drop (n + 1 + m) xs
Tactic: induction n generalizing xs with cases xs with grind [dropSlice]
Cleared hypotheses: xs, n
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
i j : ℕ
⊢ length.{u} (α := α) (dropSlice i j []) = length.{u} (α := α) [] - min j (length.{u} (α := α) [] - i)
have nil : length.{u} (α := α) (dropSlice 0 j []) = length.{u} (α := α) [] - min j (length.{u} (α := α) [] - 0)
Tactic: cases i with grind [dropSlice]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
i j : ℕ
nil : length.{u} (α := α) (dropSlice 0 j []) = length.{u} (α := α) [] - min j (length.{u} (α := α) [] - 0)
⊢ length.{u} (α := α) (dropSlice i j []) = length.{u} (α := α) [] - min j (length.{u} (α := α) [] - i)
have nil₁ : ∀ (n : ℕ),
  length.{u} (α := α) (dropSlice (n + 1) j []) = length.{u} (α := α) [] - min j (length.{u} (α := α) [] - (n + 1))
Tactic: cases i with grind [dropSlice]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
head : α
tail : List α
tail_ih : ∀ (i j : ℕ), (dropSlice i j tail).length = tail.length - min j (tail.length - i)
i j : ℕ
⊢ (dropSlice i j (head :: tail)).length = (head :: tail).length - min j ((head :: tail).length - i)
have cons : (dropSlice 0 j (head :: tail)).length = (head :: tail).length - min j ((head :: tail).length - 0)
Tactic: cases i with grind [dropSlice]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
head : α
tail : List α
tail_ih : ∀ (i j : ℕ), (dropSlice i j tail).length = tail.length - min j (tail.length - i)
i j : ℕ
cons : (dropSlice 0 j (head :: tail)).length = (head :: tail).length - min j ((head :: tail).length - 0)
⊢ (dropSlice i j (head :: tail)).length = (head :: tail).length - min j ((head :: tail).length - i)
have cons₁ : ∀ (n : ℕ), (dropSlice (n + 1) j (head :: tail)).length = (head :: tail).length - min j ((head :: tail).length - (n + 1))
Tactic: cases i with grind [dropSlice]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
i j : ℕ
xs : List α
⊢ (dropSlice i j xs).length = xs.length - min j (xs.length - i)
have nil : ∀ (i j : ℕ), length.{u} (α := α) (dropSlice i j []) = length.{u} (α := α) [] - min j (length.{u} (α := α) [] - i)
Tactic: induction xs generalizing i j with cases i with grind [dropSlice]
Cleared hypotheses: i, j, xs
-- Lean 4 proof step from Mathlib.Data.List.TakeDrop (goal)
Goal:
α : Type u
i j : ℕ
xs : List α
nil : ∀ (i j : ℕ), length.{u} (α := α) (dropSlice i j []) = length.{u} (α := α) [] - min j (length.{u} (α := α) [] - i)
⊢ (dropSlice i j xs).length = xs.length - min j (xs.length - i)
have cons : ∀ (head : α) (tail : List α),
  (∀ (i j : ℕ), (dropSlice i j tail).length = tail.length - min j (tail.length - i)) →
    ∀ (i j : ℕ), (dropSlice i j (head :: tail)).length = (head :: tail).length - min j ((head :: tail).length - i)
Tactic: induction xs generalizing i j with cases i with grind [dropSlice]
Cleared hypotheses: i, j, xs
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get (⟨0, hl⟩ : Fin (dropWhile p tl).length)) = true
hl : 0 < (dropWhile p (hd :: tl)).length
⊢ ¬p ((dropWhile p (hd :: tl)).get (⟨0, hl⟩ : Fin (dropWhile p (hd :: tl)).length)) = true
have cons : ¬p
      (get
        (match (motive := Bool → List α) p hd with
        | true => dropWhile p tl
        | false => hd :: tl)
        (⟨0, hl⟩ :
          Fin
            (length.{u_1} (α := α)
              (match (motive := Bool → List α) p hd with
              | true => dropWhile p tl
              | false => hd :: tl)))) =
    true
Tactic: simp only [dropWhile]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get (⟨0, hl⟩ : Fin (dropWhile p tl).length)) = true
hl : 0 < (dropWhile p (hd :: tl)).length
⊢ ¬p
        (get
          (match (motive := Bool → List α) p hd with
          | true => dropWhile p tl
          | false => hd :: tl)
          (⟨0, hl⟩ :
            Fin
              (length.{u_1} (α := α)
                (match (motive := Bool → List α) p hd with
                | true => dropWhile p tl
                | false => hd :: tl)))) =
      true
have pos : ∀ (hp : p hd = true),
  ¬p
        (get
          (match (motive := Bool → List α) p hd with
          | true => dropWhile p tl
          | false => hd :: tl)
          (⟨0, hl⟩ :
            Fin
              (length.{u_1} (α := α)
                (match (motive := Bool → List α) p hd with
                | true => dropWhile p tl
                | false => hd :: tl)))) =
      true
Tactic: by_cases hp : p hd
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get (⟨0, hl⟩ : Fin (dropWhile p tl).length)) = true
hl : 0 < (dropWhile p (hd :: tl)).length
pos :
  ∀ (hp : p hd = true),
    ¬p
          (get
            (match (motive := Bool → List α) p hd with
            | true => dropWhile p tl
            | false => hd :: tl)
            (⟨0, hl⟩ :
              Fin
                (length.{u_1} (α := α)
                  (match (motive := Bool → List α) p hd with
                  | true => dropWhile p tl
                  | false => hd :: tl)))) =
        true
⊢ ¬p
        (get
          (match (motive := Bool → List α) p hd with
          | true => dropWhile p tl
          | false => hd :: tl)
          (⟨0, hl⟩ :
            Fin
              (length.{u_1} (α := α)
                (match (motive := Bool → List α) p hd with
                | true => dropWhile p tl
                | false => hd :: tl)))) =
      true
have neg : ∀ (hp : ¬p hd = true),
  ¬p
        (get
          (match (motive := Bool → List α) p hd with
          | true => dropWhile p tl
          | false => hd :: tl)
          (⟨0, hl⟩ :
            Fin
              (length.{u_1} (α := α)
                (match (motive := Bool → List α) p hd with
                | true => dropWhile p tl
                | false => hd :: tl)))) =
      true
Tactic: by_cases hp : p hd
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get (⟨0, hl⟩ : Fin (dropWhile p tl).length)) = true
hl : 0 < (dropWhile p (hd :: tl)).length
hp : p hd = true
⊢ ¬p
        (get
          (match (motive := Bool → List α) p hd with
          | true => dropWhile p tl
          | false => hd :: tl)
          (⟨0, hl⟩ :
            Fin
              (length.{u_1} (α := α)
                (match (motive := Bool → List α) p hd with
                | true => dropWhile p tl
                | false => hd :: tl)))) =
      true
have pos : ∀
  (IH :
    ∀ (hl : 0 < (dropWhile p tl).length),
      ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (dropWhile p tl) 0 sorry) = true)
  (hp_1 : p hd = true), ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (dropWhile p tl) 0 sorry) = true
Tactic: simp_all only [get_eq_getElem]
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
hl : 0 < (dropWhile p (hd :: tl)).length
hp_1 : p hd = true
IH :
  ∀ (hl : 0 < (dropWhile p tl).length),
    ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (dropWhile p tl) 0 ⋯) = true
hp : p hd = true
⊢ ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (dropWhile p tl) 0 ⋯) = true
have pos : 0 < (dropWhile p tl).length
Tactic: apply IH
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
hl : 0 < (dropWhile p l).length
⊢ ¬p ((dropWhile p l).get (⟨0, hl⟩ : Fin (dropWhile p l).length)) = true
have nil : ∀ (hl : 0 < (dropWhile p []).length), ¬p ((dropWhile p []).get (⟨0, hl⟩ : Fin (dropWhile p []).length)) = true
Tactic: induction l with
  | nil => cases hl
  | cons hd tl IH =>
    simp only [dropWhile]
    by_cases hp : p hd
    · simp_all only [get_eq_getElem]
      apply IH
      simp_all only [dropWhile_cons_of_pos]
    · simp [hp]
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
hl : 0 < (dropWhile p l).length
nil : ∀ (hl : 0 < (dropWhile p []).length), ¬p ((dropWhile p []).get (⟨0, hl⟩ : Fin (dropWhile p []).length)) = true
⊢ ¬p ((dropWhile p l).get (⟨0, hl⟩ : Fin (dropWhile p l).length)) = true
have cons : ∀ (hd : α) (tl : List α)
  (IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get (⟨0, hl⟩ : Fin (dropWhile p tl).length)) = true)
  (hl : 0 < (dropWhile p (hd :: tl)).length),
  ¬p ((dropWhile p (hd :: tl)).get (⟨0, hl⟩ : Fin (dropWhile p (hd :: tl)).length)) = true
Tactic: induction l with
  | nil => cases hl
  | cons hd tl IH =>
    simp only [dropWhile]
    by_cases hp : p hd
    · simp_all only [get_eq_getElem]
      apply IH
      simp_all only [dropWhile_cons_of_pos]
    · simp [hp]
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : (dropWhile p tail).length ≤ tail.length
⊢ (dropWhile p (head :: tail)).length ≤ (head :: tail).length
have cons : length.{u_1} (α := α)
    (match (motive := Bool → List α) p head with
    | true => dropWhile p tail
    | false => head :: tail) ≤
  tail.length + 1
Tactic: simp only [dropWhile, length_cons]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : (dropWhile p tail).length ≤ tail.length
⊢ length.{u_1} (α := α)
      (match (motive := Bool → List α) p head with
      | true => dropWhile p tail
      | false => head :: tail) ≤
    tail.length + 1
have h_1 : ∀ (x : Bool), p head = true → (dropWhile p tail).length ≤ tail.length + 1
Tactic: split
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : (dropWhile p tail).length ≤ tail.length
h_1 : ∀ (x : Bool), p head = true → (dropWhile p tail).length ≤ tail.length + 1
⊢ length.{u_1} (α := α)
      (match (motive := Bool → List α) p head with
      | true => dropWhile p tail
      | false => head :: tail) ≤
    tail.length + 1
have h_2 : ∀ (x : Bool), p head = false → (head :: tail).length ≤ tail.length + 1
Tactic: split
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ (dropWhile p l).length ≤ l.length
have nil : (dropWhile p []).length ≤ length.{u_1} (α := α) []
Tactic: induction l with
  | nil => simp
  | cons head tail ih =>
    simp only [dropWhile, length_cons]
    split
    · lia
    · simp
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
nil : (dropWhile p []).length ≤ length.{u_1} (α := α) []
⊢ (dropWhile p l).length ≤ l.length
have cons : ∀ (head : α) (tail : List α) (ih : (dropWhile p tail).length ≤ tail.length),
  (dropWhile p (head :: tail)).length ≤ (head :: tail).length
Tactic: induction l with
  | nil => simp
  | cons head tail ih =>
    simp only [dropWhile, length_cons]
    split
    · lia
    · simp
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true
⊢ dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
have pos : ∀ (hp : p x = true), dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
Tactic: by_cases hp : p x
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true
pos : ∀ (hp : p x = true), dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
⊢ dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
have neg : ∀ (hp : ¬p x = true), dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
Tactic: by_cases hp : p x
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true
have nil : dropWhile p [] = [] ↔ ∀ (x : α), Membership.mem (γ := List α) [] x → p x = true
Tactic: induction l with
  | nil => simp [dropWhile]
  | cons x xs IH => by_cases hp : p x <;> simp [hp, IH]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
nil : dropWhile p [] = [] ↔ ∀ (x : α), Membership.mem (γ := List α) [] x → p x = true
⊢ dropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true
have cons : ∀ (x : α) (xs : List α) (IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true),
  dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
Tactic: induction l with
  | nil => simp [dropWhile]
  | cons x xs IH => by_cases hp : p x <;> simp [hp, IH]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p l = l ↔
    ∀ (hl : 0 < l.length), ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 hl) = true
have nil : dropWhile p [] = [] ↔
  ∀ (hl : 0 < length.{u_1} (α := α) []),
    ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 hl) = true
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l