awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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
⊢ dropWhile p l = l ↔
    ∀ (hl : 0 < l.length), ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 hl) = true
have 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
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
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
have 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
Tactic: rw [dropWhile]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
⊢ (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
have 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
Tactic: by_cases h_p_hd : p hd
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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
⊢ (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
have 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
Tactic: by_cases h_p_hd : p hd
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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
have pos : ¬dropWhile p tl = hd :: tl
Tactic: simp only [h_p_hd, length_cons, Nat.zero_lt_succ, getElem_cons_zero, not_true_eq_false,
        imp_false, iff_false]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (hypothesis)
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
h : dropWhile p tl = hd :: tl
⊢ False
have h₁ : (dropWhile p tl).length = (hd :: tl).length
Tactic: replace h := congrArg length h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (hypothesis)
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
h : (dropWhile p tl).length = (hd :: tl).length
⊢ False
have this : (dropWhile p tl).length ≤ tl.length
Tactic: have := length_dropWhile_le p tl
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
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
have pos : ∀ (hp : p x = true), takeWhile p (x :: xs) = 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 : 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
⊢ takeWhile p (x :: xs) = x :: xs ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
have neg : ∀ (hp : ¬p x = true), takeWhile p (x :: xs) = 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 α
⊢ takeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true
have nil : takeWhile p [] = [] ↔ ∀ (x : α), Membership.mem (γ := List α) [] x → p x = true
Tactic: induction l with
  | nil => simp
  | 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 : takeWhile p [] = [] ↔ ∀ (x : α), Membership.mem (γ := List α) [] x → p x = true
⊢ takeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true
have 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
Tactic: induction l with
  | nil => simp
  | 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 α
⊢ takeWhile p [] = [] ↔
    ∀ (hl : 0 < length.{u_1} (α := α) []), ¬p (get [] (⟨0, hl⟩ : Fin (length.{u_1} (α := α) []))) = true
have nil : ∀ (hl : 0 < length.{u_1} (α := α) []), p (get [] (⟨0, hl⟩ : Fin (length.{u_1} (α := α) []))) = false
Tactic: simp only [takeWhile_nil, Bool.not_eq_true, true_iff]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get (⟨0, hl⟩ : Fin (x :: xs).length)) = true
have 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
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 : 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
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get (⟨0, hl⟩ : Fin (x :: xs).length)) = true
have 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
Tactic: by_cases hp : p x
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = [] ↔ ∀ (hl : 0 < l.length), ¬p (l.get (⟨0, hl⟩ : Fin l.length)) = true
have nil : takeWhile p [] = [] ↔
  ∀ (hl : 0 < length.{u_1} (α := α) []), ¬p (get [] (⟨0, hl⟩ : Fin (length.{u_1} (α := α) []))) = 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]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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
⊢ takeWhile p l = [] ↔ ∀ (hl : 0 < l.length), ¬p (l.get (⟨0, hl⟩ : Fin l.length)) = true
have 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
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]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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
⊢ p x = true
have cons : ∀ (hp : p hd = false), p x = true
Tactic: cases hp : p hd
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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
⊢ p x = true
have cons₁ : ∀ (hp : p hd = true), p x = true
Tactic: cases hp : p hd
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (hypothesis)
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
⊢ p x = true
have hx₁ : x = hd ∨ x ∈ takeWhile p tl
Tactic: rw [hp, mem_cons] at hx
Cleared hypotheses: hx, hp
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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
⊢ p x = true
have cons : ∀ (hp : p x = true), p x = true
Tactic: rcases hx with (rfl | hx)
Cleared hypotheses: hd, hx, hp
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ takeWhile p l
⊢ p x = true
have cons : ∀ (hd : α) (tl : List α) (IH : ∀ (hx : x ∈ takeWhile p tl), p x = true) (hx : x ∈ takeWhile p (hd :: tl)), 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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
⊢ p x = true
have 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
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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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
⊢ p x = true
have nil : ∀ (hx : x ∈ takeWhile p []), 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
have pos : ∀ (hp : p hd = true),
  takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
Tactic: by_cases hp : p hd
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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)
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
have neg : ∀ (hp : ¬p hd = true),
  takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
Tactic: by_cases hp : p hd
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
have pos : ∀ (hq : q hd = true),
  takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
Tactic: by_cases hq : q hd
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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)
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
have neg : ∀ (hq : ¬q hd = true),
  takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
Tactic: by_cases hq : q hd
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
have pos : ∀ (hq : q hd = true),
  takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
Tactic: by_cases hq : q hd
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
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)
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
have neg : ∀ (hq : ¬q hd = true),
  takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
Tactic: by_cases hq : q hd
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p q : α → Bool
l : List α
⊢ takeWhile p (takeWhile q l) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) l
have nil : takeWhile p (takeWhile q []) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) []
Tactic: induction l with
  | nil => simp
  | cons hd tl IH => by_cases hp : p hd <;> by_cases hq : q hd <;> simp [takeWhile, hp, hq, IH]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p q : α → Bool
l : List α
nil : takeWhile p (takeWhile q []) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) []
⊢ takeWhile p (takeWhile q l) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) l
have cons : ∀ (hd : α) (tl : List α)
  (IH : takeWhile p (takeWhile q tl) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) tl),
  takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
Tactic: induction l with
  | nil => simp
  | cons hd tl IH => by_cases hp : p hd <;> by_cases hq : q hd <;> simp [takeWhile, hp, hq, IH]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p (takeWhile p l) = takeWhile p l
have simp_rw : takeWhile (fun (a : α) ↦ decide (p a = true ∧ p a = true)) l = takeWhile p l
Tactic: simp_rw [takeWhile_takeWhile, and_self_iff, Bool.decide_coe]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
simp_rw : takeWhile (fun (a : α) ↦ decide (p a = true ∧ p a = true)) l = takeWhile p l
⊢ takeWhile p (takeWhile p l) = takeWhile p l
have simp_rw₁ : takeWhile (fun (a : α) ↦ decide (p a = true)) l = takeWhile p l
Tactic: simp_rw [takeWhile_takeWhile, and_self_iff, Bool.decide_coe]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ find? p l = (dropWhile (fun (x : α) ↦ !p x) l).head?
have induction : find? p [] = head? (dropWhile (fun (x : α) ↦ !p x) [])
Tactic: induction l
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
induction : find? p [] = head? (dropWhile (fun (x : α) ↦ !p x) [])
⊢ find? p l = (dropWhile (fun (x : α) ↦ !p x) l).head?
have cons : ∀ (head : α) (tail : List α),
  find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head? →
    find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?
Tactic: induction l
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (hypothesis)
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
⊢ find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?
have phh : let ph := p head;
ph = p head
Tactic: set ph := p head with phh
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
ph : Bool := p head
phh : ph = p head
⊢ find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?
have false : ∀ (phh : false = p head), find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?
Tactic: rcases ph with rfl | rfl
Cleared hypotheses: ph, phh
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
ph : Bool := p head
phh : ph = p head
false : ∀ (phh : Bool.false = p head), find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?
⊢ find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?
have true : ∀ (phh : true = p head), find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?
Tactic: rcases ph with rfl | rfl
Cleared hypotheses: ph, phh
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (hypothesis)
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
phh : false = p head
⊢ find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?
have phh' : ¬p head = true
Tactic: have phh' : ¬(p head = true) := by simp [phh.symm]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
phh : Bool.false = p head
phh' : ¬p head = true
false : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
⊢ find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?
have false₁ : (!p head) = true
Tactic: rw [find?_cons_of_neg phh', dropWhile_cons_of_pos]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
phh : true = p head
⊢ find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?
have true : some head = (head :: tail).head?
Tactic: rw [find?_cons_of_pos phh.symm, dropWhile_cons_of_neg]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
phh : Bool.true = p head
true : some head = (head :: tail).head?
⊢ find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?
have true₁ : ¬(!p head) = Bool.true
Tactic: rw [find?_cons_of_pos phh.symm, dropWhile_cons_of_neg]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ find? (fun (x : α) ↦ !p x) l = (dropWhile p l).head?
have h : ∀ (x : α), p x = !!p x
Tactic: convert! l.find?_eq_head?_dropWhile_not ?_
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
h : ∃ (x : α), x ∈ l ∧ p x = true
⊢ find? p l = some ((dropWhile (fun (x : α) ↦ !p x) l).head ⋯)
have rw : (dropWhile (fun (x : α) ↦ !p x) l).head? = some ((dropWhile (fun (x : α) ↦ !p x) l).head sorry)
Tactic: rw [l.find?_eq_head?_dropWhile_not p, ← head_eq_iff_head?_eq_some]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
h : ∃ (x : α), x ∈ l ∧ p x = true
rw : (dropWhile (fun (x : α) ↦ !p x) l).head? = some ((dropWhile (fun (x : α) ↦ !p x) l).head ⋯)
⊢ find? p l = some ((dropWhile (fun (x : α) ↦ !p x) l).head ⋯)
have rw₁ : (dropWhile (fun (x : α) ↦ !p x) l).head sorry = (dropWhile (fun (x : α) ↦ !p x) l).head sorry
Tactic: rw [l.find?_eq_head?_dropWhile_not p, ← head_eq_iff_head?_eq_some]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
h : ∃ (x : α), x ∈ l ∧ p x = true
rw : (dropWhile (fun (x : α) ↦ !p x) l).head? = some ((dropWhile (fun (x : α) ↦ !p x) l).head ⋯)
rw₁ : (dropWhile (fun (x : α) ↦ !p x) l).head ⋯ = (dropWhile (fun (x : α) ↦ !p x) l).head ⋯
⊢ find? p l = some ((dropWhile (fun (x : α) ↦ !p x) l).head ⋯)
have rw₂ : dropWhile (fun (x : α) ↦ !p x) l ≠ []
Tactic: rw [l.find?_eq_head?_dropWhile_not p, ← head_eq_iff_head?_eq_some]
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
h : ∃ (x : α), x ∈ l ∧ ¬p x = true
⊢ find? (fun (x : α) ↦ !p x) l = some ((dropWhile p l).head ⋯)
have h₁ : ∀ (x : α), p x = !!p x
Tactic: convert! l.find?_eq_head_dropWhile_not ?_
-- Lean 4 proof step from Mathlib.Data.List.TakeWhile (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
h : ∃ (x : α), x ∈ l ∧ ¬p x = true
h₁ : ∀ (x : α), p x = !!p x
⊢ find? (fun (x : α) ↦ !p x) l = some ((dropWhile p l).head ⋯)
have convert_2 : ∃ (x : α), x ∈ l ∧ (!p x) = true
Tactic: convert! l.find?_eq_head_dropWhile_not ?_
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
M : Type u_1
inst : Zero M
l : List M
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
n_1 n : ℕ
⊢ n ∈ {i ∈ Finset.range l.length | l.getD i 0 ≠ 0} ↔ l.getD n 0 ≠ 0
have simp : ¬l.getD n 0 = 0 → n < l.length
Tactic: simp only [Ne, Finset.mem_filter, Finset.mem_range, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
M : Type u_1
inst : Zero M
l : List M
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
n_1 n : ℕ
⊢ ¬l.getD n 0 = 0 → n < l.length
have contrapose! : l.length ≤ n → l.getD n 0 = 0
Tactic: contrapose!