awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.TakeWhile
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
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
⊢ ¬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
-- Module: Mathlib.Data.List.TakeWhile
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
pos :
  ∀
    (IH :
      ∀ (hl : 0 < (dropWhile p tl).length),
        ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (dropWhile p tl) 0 ⋯) = true)
    (hp_1 : p hd = true), ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (dropWhile p tl) 0 ⋯) = 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:
simp_all only [get_eq_getElem]

Premises used: List.get_eq_getElem
-- Module: Mathlib.Data.List.TakeWhile
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
pos : 0 < (dropWhile p tl).length
⊢ ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (dropWhile p tl) 0 ⋯) = true

Tactic:
apply IH
-- Module: Mathlib.Data.List.TakeWhile
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
⊢ 0 < (dropWhile p tl).length

Tactic:
simp_all only [dropWhile_cons_of_pos]

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

Tactic:
simp [hp]
-- Module: Mathlib.Data.List.TakeWhile
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
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
⊢ ¬p ((dropWhile p l).get (⟨0, hl⟩ : Fin (dropWhile p l).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]

Premises used: List.dropWhile_cons_of_pos, List.get_eq_getElem, List.cons, List.dropWhile, List.nil
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
⊢ (dropWhile p []).length ≤ length.{u_1} (α := α) []

Tactic:
simp
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : (dropWhile p tail).length ≤ tail.length
cons :
  length.{u_1} (α := α)
      (match (motive := Bool → List α) p head with
      | true => dropWhile p tail
      | false => head :: tail) ≤
    tail.length + 1
⊢ (dropWhile p (head :: tail)).length ≤ (head :: tail).length

Tactic:
simp only [dropWhile, length_cons]

Premises used: List.length_cons, List.dropWhile
-- Module: Mathlib.Data.List.TakeWhile
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
h_2 : ∀ (x : Bool), p head = false → (head :: 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

Tactic:
split
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : (dropWhile p tail).length ≤ tail.length
x : Bool
heq : p head = true
⊢ (dropWhile p tail).length ≤ tail.length + 1

Tactic:
lia
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : (dropWhile p tail).length ≤ tail.length
x : Bool
heq : p head = false
⊢ (head :: tail).length ≤ tail.length + 1

Tactic:
simp
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
nil : (dropWhile p []).length ≤ length.{u_1} (α := α) []
cons :
  ∀ (head : α) (tail : List α) (ih : (dropWhile p tail).length ≤ tail.length),
    (dropWhile p (head :: tail)).length ≤ (head :: tail).length
⊢ (dropWhile p l).length ≤ l.length

Tactic:
induction l with
  | nil => simp
  | cons head tail ih =>
    simp only [dropWhile, length_cons]
    split
    · lia
    · simp

Premises used: List.head, List.length_cons, List.tail, List.cons, List.dropWhile, List.nil
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p [] = [] ↔ ∀ (x : α), Membership.mem (γ := List α) [] x → p x = true

Tactic:
simp [dropWhile]

Premises used: List.dropWhile
-- Module: Mathlib.Data.List.TakeWhile
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
neg : ∀ (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

Tactic:
by_cases hp : p x
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true
hp : p x = true
⊢ dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

Tactic:
simp [hp, IH]
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true
hp : ¬p x = true
⊢ dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

Tactic:
simp [hp, IH]
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
nil : dropWhile p [] = [] ↔ ∀ (x : α), Membership.mem (γ := List α) [] x → p x = true
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
⊢ dropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
induction l with
  | nil => simp [dropWhile]
  | cons x xs IH => by_cases hp : p x <;> simp [hp, IH]

Premises used: List.cons, List.dropWhile, List.nil
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
nil :
  dropWhile p [] = [] ↔
    ∀ (hl : 0 < length.{u_1} (α := α) []),
      ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 hl) = true
cons :
  ∀ (hd : α) (tl : List α),
    dropWhile p (hd :: tl) = hd :: tl ↔
      ∀ (hl : 0 < (hd :: tl).length),
        ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) 0 hl) = true
⊢ dropWhile p l = l ↔
    ∀ (hl : 0 < l.length), ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 hl) = true

Tactic:
rcases l with - | ⟨hd, tl⟩
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
⊢ dropWhile p [] = [] ↔
    ∀ (hl : 0 < length.{u_1} (α := α) []),
      ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 hl) = true

Tactic:
simp
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
cons :
  (match (motive := Bool → List α) p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < (hd :: tl).length),
      ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) 0 hl) = true
⊢ dropWhile p (hd :: tl) = hd :: tl ↔
    ∀ (hl : 0 < (hd :: tl).length),
      ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) 0 hl) = true

Tactic:
rw [dropWhile]

Premises used: List.dropWhile
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
pos :
  ∀ (h_p_hd : p hd = true),
    (match (motive := Bool → List α) p hd with
        | true => dropWhile p tl
        | false => hd :: tl) =
        hd :: tl ↔
      ∀ (hl : 0 < (hd :: tl).length),
        ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) 0 hl) = true
neg :
  ∀ (h_p_hd : ¬p hd = true),
    (match (motive := Bool → List α) p hd with
        | true => dropWhile p tl
        | false => hd :: tl) =
        hd :: tl ↔
      ∀ (hl : 0 < (hd :: tl).length),
        ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) 0 hl) = true
⊢ (match (motive := Bool → List α) p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < (hd :: tl).length),
      ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) 0 hl) = true

Tactic:
by_cases h_p_hd : p hd
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
pos : ¬dropWhile p tl = hd :: tl
⊢ (match (motive := Bool → List α) p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < (hd :: tl).length),
      ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) 0 hl) = true

Tactic:
simp only [h_p_hd, length_cons, Nat.zero_lt_succ, getElem_cons_zero, not_true_eq_false,
        imp_false, iff_false]

Premises used: iff_false, List.length_cons, imp_false, Nat.zero_lt_succ, not_true_eq_false, List.getElem_cons_zero
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
h : dropWhile p tl = hd :: tl
⊢ (dropWhile p tl).length = (hd :: tl).length

Tactic:
replace h := congrArg length h
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
h : (dropWhile p tl).length = (hd :: tl).length
⊢ (dropWhile p tl).length ≤ tl.length

Tactic:
have := length_dropWhile_le p tl
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
h : (dropWhile p tl).length = tl.length + 1
this : (dropWhile p tl).length ≤ tl.length
⊢ False

Tactic:
lia
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : ¬p hd = true
⊢ (match (motive := Bool → List α) p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < (hd :: tl).length),
      ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) 0 hl) = true

Tactic:
simp [h_p_hd]
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p [] = [] ↔ ∀ (x : α), Membership.mem (γ := List α) [] x → p x = true

Tactic:
simp
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = xs ↔ ∀ (x : α), x ∈ xs → p x = true
pos : ∀ (hp : p x = true), takeWhile p (x :: xs) = x :: xs ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
neg : ∀ (hp : ¬p x = true), takeWhile p (x :: xs) = x :: xs ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
⊢ takeWhile p (x :: xs) = x :: xs ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

Tactic:
by_cases hp : p x
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = xs ↔ ∀ (x : α), x ∈ xs → p x = true
hp : p x = true
⊢ takeWhile p (x :: xs) = x :: xs ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

Tactic:
simp [hp, IH]
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = xs ↔ ∀ (x : α), x ∈ xs → p x = true
hp : ¬p x = true
⊢ takeWhile p (x :: xs) = x :: xs ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

Tactic:
simp [hp, IH]
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
nil : takeWhile p [] = [] ↔ ∀ (x : α), Membership.mem (γ := List α) [] x → p x = true
cons :
  ∀ (x : α) (xs : List α) (IH : takeWhile p xs = xs ↔ ∀ (x : α), x ∈ xs → p x = true),
    takeWhile p (x :: xs) = x :: xs ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
⊢ takeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
induction l with
  | nil => simp
  | cons x xs IH => by_cases hp : p x <;> simp [hp, IH]

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
nil : ∀ (hl : 0 < length.{u_1} (α := α) []), p (get [] (⟨0, hl⟩ : Fin (length.{u_1} (α := α) []))) = false
⊢ takeWhile p [] = [] ↔
    ∀ (hl : 0 < length.{u_1} (α := α) []), ¬p (get [] (⟨0, hl⟩ : Fin (length.{u_1} (α := α) []))) = true

Tactic:
simp only [takeWhile_nil, Bool.not_eq_true, true_iff]

Premises used: true_iff, Bool.not_eq_true, List.takeWhile_nil
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
h : 0 < length.{u_1} (α := α) []
⊢ p (get [] (⟨0, h⟩ : Fin (length.{u_1} (α := α) []))) = false

Tactic:
simp at h
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < xs.length), ¬p (xs.get (⟨0, hl⟩ : Fin xs.length)) = true
pos :
  ∀ (hp : p x = true),
    takeWhile p (x :: xs) = [] ↔
      ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get (⟨0, hl⟩ : Fin (x :: xs).length)) = true
neg :
  ∀ (hp : ¬p x = true),
    takeWhile p (x :: xs) = [] ↔
      ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get (⟨0, hl⟩ : Fin (x :: xs).length)) = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get (⟨0, hl⟩ : Fin (x :: xs).length)) = true

Tactic:
by_cases hp : p x
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < xs.length), ¬p (xs.get (⟨0, hl⟩ : Fin xs.length)) = true
hp : p x = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get (⟨0, hl⟩ : Fin (x :: xs).length)) = true

Tactic:
simp [hp]
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < xs.length), ¬p (xs.get (⟨0, hl⟩ : Fin xs.length)) = true
hp : ¬p x = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get (⟨0, hl⟩ : Fin (x :: xs).length)) = true

Tactic:
simp [hp]
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
nil :
  takeWhile p [] = [] ↔
    ∀ (hl : 0 < length.{u_1} (α := α) []), ¬p (get [] (⟨0, hl⟩ : Fin (length.{u_1} (α := α) []))) = true
cons :
  ∀ (x : α) (xs : List α)
    (IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < xs.length), ¬p (xs.get (⟨0, hl⟩ : Fin xs.length)) = true),
    takeWhile p (x :: xs) = [] ↔
      ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get (⟨0, hl⟩ : Fin (x :: xs).length)) = true
⊢ takeWhile p l = [] ↔ ∀ (hl : 0 < l.length), ¬p (l.get (⟨0, hl⟩ : Fin l.length)) = true

Tactic:
induction l with
  | nil =>
    simp only [takeWhile_nil, Bool.not_eq_true, true_iff]
    intro h
    simp at h
  | cons x xs IH => by_cases hp : p x <;> simp [hp]

Premises used: true_iff, List.cons, Bool.not_eq_true, List.nil, List.takeWhile_nil
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : ∀ (hx : x ∈ takeWhile p tl), p x = true
hx :
  Membership.mem (γ := List α)
    (match (motive := Bool → List α) p hd with
      | true => hd :: takeWhile p tl
      | false => [] :
      List α)
    x
cons : ∀ (hp : p hd = false), p x = true
cons₁ : ∀ (hp : p hd = true), p x = true
⊢ p x = true

Tactic:
cases hp : p hd
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : ∀ (hx : x ∈ takeWhile p tl), p x = true
hx :
  Membership.mem (γ := List α)
    (match (motive := Bool → List α) p hd with
      | true => hd :: takeWhile p tl
      | false => [] :
      List α)
    x
hp : p hd = false
⊢ p x = true

Tactic:
simp [hp] at hx
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : ∀ (hx : x ∈ takeWhile p tl), p x = true
hx :
  Membership.mem (γ := List α)
    (match (motive := Bool → List α) p hd with
      | true => hd :: takeWhile p tl
      | false => [] :
      List α)
    x
hp : p hd = true
⊢ x = hd ∨ x ∈ takeWhile p tl

Tactic:
rw [hp, mem_cons] at hx

Premises used: List.mem_cons
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : ∀ (hx : x ∈ takeWhile p tl), p x = true
hx :
  Membership.mem (γ := List α)
    (match (motive := Bool → List α) p hd with
      | true => hd :: takeWhile p tl
      | false => [] :
      List α)
    x
hp : p hd = true
hx₁ : x = hd ∨ x ∈ takeWhile p tl
⊢ p hd = true

Tactic:
rw [hp, mem_cons] at hx

Premises used: List.mem_cons
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : ∀ (hx : x ∈ takeWhile p tl), p x = true
hx : x = hd ∨ x ∈ takeWhile p tl
hp : p hd = true
cons : ∀ (hp : p x = true), p x = true
cons₁ : ∀ (hx : x ∈ takeWhile p tl), p x = true
⊢ p x = true

Tactic:
rcases hx with (rfl | hx)

Premises used: rfl
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
tl : List α
IH : ∀ (hx : x ∈ takeWhile p tl), p x = true
hp : p x = true
⊢ p x = true

Tactic:
hp
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
tl : List α
IH : ∀ (hx : x ∈ takeWhile p tl), p x = true
hp : p x = true
⊢ p x = true

Tactic:
exact hp
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : ∀ (hx : x ∈ takeWhile p tl), p x = true
hp : p hd = true
hx : x ∈ takeWhile p tl
⊢ p x = true

Tactic:
IH hx
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : ∀ (hx : x ∈ takeWhile p tl), p x = true
hp : p hd = true
hx : x ∈ takeWhile p tl
⊢ p x = true

Tactic:
exact IH hx
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ takeWhile p []
⊢ p x = true

Tactic:
simp [takeWhile] at hx

Premises used: List.takeWhile
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ takeWhile p l
cons :
  ∀ (hd : α) (tl : List α) (IH : ∀ (hx : x ∈ takeWhile p tl), p x = true) (hx : x ∈ takeWhile p (hd :: tl)), p x = true
cons₁ :
  ∀ (hd : α) (tl : List α) (IH : ∀ (hx : x ∈ takeWhile p tl), p x = true)
    (hx :
      Membership.mem (γ := List α)
        (match (motive := Bool → List α) p hd with
          | true => hd :: takeWhile p tl
          | false => [] :
          List α)
        x),
    p x = true
nil : ∀ (hx : x ∈ takeWhile p []), p x = true
⊢ p x = true

Tactic:
induction l with simp [takeWhile] at hx
  | cons hd tl IH =>
    cases hp : p hd
    · simp [hp] at hx
    · rw [hp, mem_cons] at hx
      rcases hx with (rfl | hx)
      · exact hp
      · exact IH hx

Premises used: List.cons, List.mem_cons, List.takeWhile, rfl
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p q : α → Bool
⊢ takeWhile p (takeWhile q []) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) []

Tactic:
simp
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) tl
pos :
  ∀ (hp : p hd = true),
    takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
neg :
  ∀ (hp : ¬p hd = true),
    takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
by_cases hp : p hd
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) tl
hp : p hd = true
pos :
  ∀ (hq : q hd = true),
    takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
neg :
  ∀ (hq : ¬q hd = true),
    takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
by_cases hq : q hd
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) tl
hp : ¬p hd = true
pos :
  ∀ (hq : q hd = true),
    takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
neg :
  ∀ (hq : ¬q hd = true),
    takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
by_cases hq : q hd
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) tl
hp : p hd = true
hq : q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
simp [takeWhile, hp, hq, IH]

Premises used: List.takeWhile
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) tl
hp : p hd = true
hq : ¬q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
simp [takeWhile, hp, hq, IH]

Premises used: List.takeWhile