awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : ¬R a c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
have simp : (destutter' R b l).length ≤ (destutter' R a l).length
Tactic: simp only [if_neg hac]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : ¬R a c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
have case : (destutter' R b l).length ≤ (destutter' R a l).length
Tactic: case neg =>
        simp only [if_neg hac]
        exact length_destutter'_cotrans_ge hba
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
have case : (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
Tactic: case neg =>
      simp only [destutter', if_neg hbc]
      by_cases hac : R a c
      case pos =>
        simp only [if_pos hac, length_cons]
        exact Nat.le_succ_of_le (length_destutter'_cotrans_ge hbc)
      case neg =>
        simp only [if_neg hac]
        exact length_destutter'_cotrans_ge hba
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
case : (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
have case₁ : ∀ (hac : R a c), (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
Tactic: case neg =>
      simp only [destutter', if_neg hbc]
      by_cases hac : R a c
      case pos =>
        simp only [if_pos hac, length_cons]
        exact Nat.le_succ_of_le (length_destutter'_cotrans_ge hbc)
      case neg =>
        simp only [if_neg hac]
        exact length_destutter'_cotrans_ge hba
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
case : (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
case₁ : ∀ (hac : R a c), (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
have case₂ : ∀ (hac : ¬R a c), (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
Tactic: case neg =>
      simp only [destutter', if_neg hbc]
      by_cases hac : R a c
      case pos =>
        simp only [if_pos hac, length_cons]
        exact Nat.le_succ_of_le (length_destutter'_cotrans_ge hbc)
      case neg =>
        simp only [if_neg hac]
        exact length_destutter'_cotrans_ge hba
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
⊢ (destutter' R b []).length ≤ (destutter' R a [b]).length
have pos : ∀ (hab : R a b), (destutter' R b []).length ≤ (destutter' R a [b]).length
Tactic: by_cases hab : (R a b)
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
pos : ∀ (hab : R a b), (destutter' R b []).length ≤ (destutter' R a [b]).length
⊢ (destutter' R b []).length ≤ (destutter' R a [b]).length
have neg : ∀ (hab : ¬R a b), (destutter' R b []).length ≤ (destutter' R a [b]).length
Tactic: by_cases hab : (R a b)
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
c : α
cs : List α
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
have by_cases : ∀ (hab : R a b), (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
Tactic: by_cases hab : R a b
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
c : α
cs : List α
by_cases : ∀ (hab : R a b), (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
have neg : ∀ (hab : ¬R a b), (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
Tactic: by_cases hab : R a b
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
have neg : ∀ (hac : R a c), (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
Tactic: obtain hac | hac : R a c ∨ Rᶜ a c := em _
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
neg : ∀ (hac : R a c), (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
have neg₁ : ∀ (hac : Rᶜ a c), (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
Tactic: obtain hac | hac : R a c ∨ Rᶜ a c := em _
-- Lean 4 proof step from Mathlib.Data.List.Destutter (hypothesis)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : R a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
have hbc : ¬Rᶜ b c
Tactic: have hbc : ¬Rᶜ b c := mt (_root_.trans hab) (not_not.2 hac)
-- Lean 4 proof step from Mathlib.Data.List.Destutter (hypothesis)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
have hbc : ¬R b c
Tactic: have hbc : ¬R b c := trans (symm hab) hac
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
hbc : ¬R b c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
have neg : (destutter' R b cs).length ≤ (destutter' R a cs).length
Tactic: simp only [destutter', if_neg hbc, if_neg hac, if_neg hab]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
inst_1 : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length
have pos : ∀ (hab : R a b), (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length
Tactic: by_cases hab : R a b
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
inst_1 : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
pos : ∀ (hab : R a b), (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length
have neg : ∀ (hab : ¬R a b), (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length
Tactic: by_cases hab : R a b
-- Lean 4 proof step from Mathlib.Data.List.Destutter (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
h : Pairwise r (x :: y :: xs)
⊢ destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: y :: xs) = (x :: y :: xs).dedup
have h₁ : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
Tactic: rw [pairwise_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
⊢ destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: y :: xs) = (x :: y :: xs).dedup
have rw : (if x ≠ y then x :: (y :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
Tactic: rw [destutter_cons_cons, ← destutter_cons', ← destutter_cons', h.2.destutter_eq_dedup]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
have inl : ∀ (h : (∀ (a' : α), a' ∈ x :: xs → r x a') ∧ Pairwise r (x :: xs)),
  (if x ≠ x then x :: (x :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: x :: xs).dedup
Tactic: obtain rfl | hxy := eq_or_ne x y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
inl :
  ∀ (h : (∀ (a' : α), a' ∈ x :: xs → r x a') ∧ Pairwise r (x :: xs)),
    (if x ≠ x then x :: (x :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: x :: xs).dedup
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
have inr : ∀ (hxy : x ≠ y),
  (if x ≠ y then x :: (y :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
Tactic: obtain rfl | hxy := eq_or_ne x y
-- Lean 4 proof step from Mathlib.Data.List.Destutter (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
hxy : x ≠ y
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
have h₁ : (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs
Tactic: simp only [mem_cons, forall_eq_or_imp, pairwise_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Destutter (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
hxy : x ≠ y
h : (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
have this : ¬x ∈ xs
Tactic: have : x ∉ xs := fun hx ↦ hxy (antisymm h.1.1 (h.2.1 x hx))
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
hxy : x ≠ y
h : (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs
this : ¬x ∈ xs
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
have inr : x :: (y :: xs).dedup = (x :: y :: xs).dedup
Tactic: rw [if_pos hxy, dedup_cons_of_notMem (a := x) (by simp [*])]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
hxy : x ≠ y
h : (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs
this : ¬x ∈ xs
inr : x :: (y :: xs).dedup = (x :: y :: xs).dedup
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
have inr₁ : x :: (y :: xs).dedup = x :: (y :: xs).dedup
Tactic: rw [if_pos hxy, dedup_cons_of_notMem (a := x) (by simp [*])]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
n : ℕ
⊢ take ((xs ++ [x]).length - n) (xs ++ [x]) = (drop n (xs ++ [x]).reverse).reverse
have append_singleton : take ((xs ++ [x]).length - 0) (xs ++ [x]) = (drop 0 (xs ++ [x]).reverse).reverse
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
n : ℕ
append_singleton : take ((xs ++ [x]).length - 0) (xs ++ [x]) = (drop 0 (xs ++ [x]).reverse).reverse
⊢ take ((xs ++ [x]).length - n) (xs ++ [x]) = (drop n (xs ++ [x]).reverse).reverse
have append_singleton₁ : ∀ (n : ℕ), take ((xs ++ [x]).length - (n + 1)) (xs ++ [x]) = (drop (n + 1) (xs ++ [x]).reverse).reverse
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l : List α
n : ℕ
⊢ take (l.length - n) l = (drop n l.reverse).reverse
have nil : ∀ (n : ℕ), Eq.{u_1 + 1} (α := List α) (take (length.{u_1} (α := α) [] - n) []) (reverse (drop n (reverse [])))
Tactic: induction l using List.reverseRecOn generalizing n with
  | nil => simp
  | append_singleton xs x IH =>
    cases n
    · simp [take_length_add_append]
    · simp [take_append, IH]
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l : List α
n : ℕ
nil : ∀ (n : ℕ), Eq.{u_1 + 1} (α := List α) (take (length.{u_1} (α := α) [] - n) []) (reverse (drop n (reverse [])))
⊢ take (l.length - n) l = (drop n l.reverse).reverse
have append_singleton : ∀ (xs : List α) (x : α) (IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse) (n : ℕ),
  take ((xs ++ [x]).length - n) (xs ++ [x]) = (drop n (xs ++ [x]).reverse).reverse
Tactic: induction l using List.reverseRecOn generalizing n with
  | nil => simp
  | append_singleton xs x IH =>
    cases n
    · simp [take_length_add_append]
    · simp [take_append, IH]
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
n : ℕ
⊢ drop ((xs ++ [x]).length - n) (xs ++ [x]) = (take n (xs ++ [x]).reverse).reverse
have append_singleton : drop ((xs ++ [x]).length - 0) (xs ++ [x]) = (take 0 (xs ++ [x]).reverse).reverse
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
n : ℕ
append_singleton : drop ((xs ++ [x]).length - 0) (xs ++ [x]) = (take 0 (xs ++ [x]).reverse).reverse
⊢ drop ((xs ++ [x]).length - n) (xs ++ [x]) = (take n (xs ++ [x]).reverse).reverse
have append_singleton₁ : ∀ (n : ℕ), drop ((xs ++ [x]).length - (n + 1)) (xs ++ [x]) = (take (n + 1) (xs ++ [x]).reverse).reverse
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l : List α
n : ℕ
⊢ drop (l.length - n) l = (take n l.reverse).reverse
have nil : ∀ (n : ℕ), Eq.{u_1 + 1} (α := List α) (drop (length.{u_1} (α := α) [] - n) []) (reverse (take n (reverse [])))
Tactic: induction l using List.reverseRecOn generalizing n with
  | nil => simp
  | append_singleton xs x IH =>
    cases n
    · exact drop_length
    · simp [drop_append, IH]
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l : List α
n : ℕ
nil : ∀ (n : ℕ), Eq.{u_1 + 1} (α := List α) (drop (length.{u_1} (α := α) [] - n) []) (reverse (take n (reverse [])))
⊢ drop (l.length - n) l = (take n l.reverse).reverse
have append_singleton : ∀ (xs : List α) (x : α) (IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse) (n : ℕ),
  drop ((xs ++ [x]).length - n) (xs ++ [x]) = (take n (xs ++ [x]).reverse).reverse
Tactic: induction l using List.reverseRecOn generalizing n with
  | nil => simp
  | append_singleton xs x IH =>
    cases n
    · exact drop_length
    · simp [drop_append, IH]
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
⊢ rdropWhile p (l ++ [x]) = if p x = true then rdropWhile p l else l ++ [x]
have simp : reverse
    (match (motive := Bool → List α) p x with
    | true => dropWhile p l.reverse
    | false => x :: l.reverse) =
  if p x = true then (dropWhile p l.reverse).reverse else l ++ [x]
Tactic: simp only [rdropWhile, dropWhile, reverse_append, reverse_singleton, singleton_append]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
⊢ reverse
      (match (motive := Bool → List α) p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse) =
    if p x = true then (dropWhile p l.reverse).reverse else l ++ [x]
have pos : ∀ (h : p x = true),
  reverse
      (match (motive := Bool → List α) p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse) =
    (dropWhile p l.reverse).reverse
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
pos :
  ∀ (h : p x = true),
    reverse
        (match (motive := Bool → List α) p x with
        | true => dropWhile p l.reverse
        | false => x :: l.reverse) =
      (dropWhile p l.reverse).reverse
⊢ reverse
      (match (motive := Bool → List α) p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse) =
    if p x = true then (dropWhile p l.reverse).reverse else l ++ [x]
have neg : ∀ (h : ¬p x = true),
  reverse
      (match (motive := Bool → List α) p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse) =
    l ++ [x]
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ rdropWhile p (l ++ [x]) = rdropWhile p l
have rw : (if p x = true then rdropWhile p l else l ++ [x]) = rdropWhile p l
Tactic: rw [rdropWhile_concat, if_pos h]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
rw : (if p x = true then rdropWhile p l else l ++ [x]) = rdropWhile p l
⊢ rdropWhile p (l ++ [x]) = rdropWhile p l
have rw₁ : rdropWhile p l = rdropWhile p l
Tactic: rw [rdropWhile_concat, if_pos h]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ rdropWhile p (l ++ [x]) = l ++ [x]
have rw : (if p x = true then rdropWhile p l else l ++ [x]) = l ++ [x]
Tactic: rw [rdropWhile_concat, if_neg h]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
rw : (if p x = true then rdropWhile p l else l ++ [x]) = l ++ [x]
⊢ rdropWhile p (l ++ [x]) = l ++ [x]
have rw₁ : l ++ [x] = l ++ [x]
Tactic: rw [rdropWhile_concat, if_neg h]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
x : α
⊢ rdropWhile p [x] = if p x = true then [] else [x]
have rw : rdropWhile p ([] ++ [x]) = if p x = true then [] else [] ++ [x]
Tactic: rw [← nil_append [x], rdropWhile_concat, rdropWhile_nil]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
x : α
rw : rdropWhile p ([] ++ [x]) = if p x = true then [] else [] ++ [x]
⊢ rdropWhile p [x] = if p x = true then [] else [x]
have rw₁ : (if p x = true then rdropWhile p [] else [] ++ [x]) = if p x = true then [] else [] ++ [x]
Tactic: rw [← nil_append [x], rdropWhile_concat, rdropWhile_nil]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
x : α
rw : rdropWhile p ([] ++ [x]) = if p x = true then [] else [] ++ [x]
rw₁ : (if p x = true then rdropWhile p [] else [] ++ [x]) = if p x = true then [] else [] ++ [x]
⊢ rdropWhile p [x] = if p x = true then [] else [x]
have rw₂ : (if p x = true then [] else [] ++ [x]) = if p x = true then [] else [] ++ [x]
Tactic: rw [← nil_append [x], rdropWhile_concat, rdropWhile_nil]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬p ((rdropWhile p l).getLast hl) = true
have simp_rw : ¬p ((dropWhile p l.reverse).reverse.getLast sorry) = true
Tactic: simp_rw [rdropWhile]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬p ((dropWhile p l.reverse).reverse.getLast ⋯) = true
have rw : ¬false = true
Tactic: rw [getLast_reverse, head_dropWhile_not p]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l <+: l
have rw : dropWhile p l.reverse <:+ l.reverse
Tactic: rw [← reverse_suffix, rdropWhile, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p (dropWhile p l) = dropWhile p l
have simp : ∀ (hl : 0 < (dropWhile p l).length),
  ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (dropWhile p l) 0 hl) = true
Tactic: simp only [dropWhile_eq_self_iff]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
⊢ rtakeWhile p (l ++ [x]) = if p x = true then rtakeWhile p l ++ [x] else []
have simp : reverse
    (match (motive := Bool → List α) p x with
    | true => x :: takeWhile p l.reverse
    | false => []) =
  if p x = true then (takeWhile p l.reverse).reverse ++ [x] else []
Tactic: simp only [rtakeWhile, takeWhile, reverse_append, reverse_singleton, singleton_append]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
⊢ reverse
      (match (motive := Bool → List α) p x with
      | true => x :: takeWhile p l.reverse
      | false => []) =
    if p x = true then (takeWhile p l.reverse).reverse ++ [x] else []
have pos : ∀ (h : p x = true),
  reverse
      (match (motive := Bool → List α) p x with
      | true => x :: takeWhile p l.reverse
      | false => []) =
    (takeWhile p l.reverse).reverse ++ [x]
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
pos :
  ∀ (h : p x = true),
    reverse
        (match (motive := Bool → List α) p x with
        | true => x :: takeWhile p l.reverse
        | false => []) =
      (takeWhile p l.reverse).reverse ++ [x]
⊢ reverse
      (match (motive := Bool → List α) p x with
      | true => x :: takeWhile p l.reverse
      | false => []) =
    if p x = true then (takeWhile p l.reverse).reverse ++ [x] else []
have neg : ∀ (h : ¬p x = true),
  Eq.{u_1 + 1} (α := List α)
    (reverse
      (match (motive := Bool → List α) p x with
      | true => x :: takeWhile p l.reverse
      | false => []))
    []
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ rtakeWhile p (l ++ [x]) = rtakeWhile p l ++ [x]
have rw : (if p x = true then rtakeWhile p l ++ [x] else []) = rtakeWhile p l ++ [x]
Tactic: rw [rtakeWhile_concat, if_pos h]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
rw : (if p x = true then rtakeWhile p l ++ [x] else []) = rtakeWhile p l ++ [x]
⊢ rtakeWhile p (l ++ [x]) = rtakeWhile p l ++ [x]
have rw₁ : rtakeWhile p l ++ [x] = rtakeWhile p l ++ [x]
Tactic: rw [rtakeWhile_concat, if_pos h]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ rtakeWhile p (l ++ [x]) = []
have rw : (if p x = true then rtakeWhile p l ++ [x] else []) = []
Tactic: rw [rtakeWhile_concat, if_neg h]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
rw : (if p x = true then rtakeWhile p l ++ [x] else []) = []
⊢ rtakeWhile p (l ++ [x]) = []
have rw₁ : Eq.{u_1 + 1} (α := List α) [] []
Tactic: rw [rtakeWhile_concat, if_neg h]