awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p l <:+ l
have rw : takeWhile p l.reverse <+: l.reverse
Tactic: rw [← reverse_prefix, rtakeWhile, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true
have nil : rtakeWhile p [] = [] ↔ ∀ (hl : Ne.{u_1 + 1} (α := List α) [] []), ¬p (getLast [] hl) = true
Tactic: induction l using List.reverseRecOn
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
nil : rtakeWhile p [] = [] ↔ ∀ (hl : Ne.{u_1 + 1} (α := List α) [] []), ¬p (getLast [] hl) = true
⊢ rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true
have append_singleton : ∀ (l : List α) (a : α),
  (rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true) →
    (rtakeWhile p (l ++ [a]) = [] ↔ ∀ (hl : l ++ [a] ≠ []), ¬p ((l ++ [a]).getLast hl) = true)
Tactic: induction l using List.reverseRecOn
-- Lean 4 proof step from Mathlib.Data.List.DropRight (hypothesis)
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ rtakeWhile p l
⊢ p x = true
have hx₁ : x ∈ takeWhile p l.reverse
Tactic: rw [rtakeWhile, mem_reverse] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ (dropWhile p l.reverse).reverse ++ (takeWhile p l.reverse).reverse = l
have rw : (takeWhile p l.reverse ++ dropWhile p l.reverse).reverse = l
Tactic: rw [← List.reverse_append, takeWhile_append_dropWhile, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
rw : (takeWhile p l.reverse ++ dropWhile p l.reverse).reverse = l
⊢ (dropWhile p l.reverse).reverse ++ (takeWhile p l.reverse).reverse = l
have rw₁ : l.reverse.reverse = l
Tactic: rw [← List.reverse_append, takeWhile_append_dropWhile, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
p : α → Bool
l : List α
rw : (takeWhile p l.reverse ++ dropWhile p l.reverse).reverse = l
rw₁ : l.reverse.reverse = l
⊢ (dropWhile p l.reverse).reverse ++ (takeWhile p l.reverse).reverse = l
have rw₂ : l = l
Tactic: rw [← List.reverse_append, takeWhile_append_dropWhile, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l : List α
i j : ℕ
⊢ (l.rdrop i).rdrop j = l.rdrop (i + j)
have simp_rw : (drop j (drop i l.reverse).reverse.reverse).reverse = (drop (i + j) l.reverse).reverse
Tactic: simp_rw [rdrop_eq_reverse_drop_reverse, reverse_reverse, drop_drop]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l : List α
i j : ℕ
simp_rw : (drop j (drop i l.reverse).reverse.reverse).reverse = (drop (i + j) l.reverse).reverse
⊢ (l.rdrop i).rdrop j = l.rdrop (i + j)
have simp_rw₁ : (drop j (drop i l.reverse)).reverse = (drop (i + j) l.reverse).reverse
Tactic: simp_rw [rdrop_eq_reverse_drop_reverse, reverse_reverse, drop_drop]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
⊢ (l₁ ++ l₂).rdrop l₂.length = l₁
have rw : (drop l₂.length (l₁ ++ l₂).reverse).reverse = l₁
Tactic: rw [rdrop_eq_reverse_drop_reverse, ← length_reverse,
      reverse_append, drop_left, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
rw : (drop l₂.length (l₁ ++ l₂).reverse).reverse = l₁
⊢ (l₁ ++ l₂).rdrop l₂.length = l₁
have rw₁ : (drop l₂.reverse.length (l₁ ++ l₂).reverse).reverse = l₁
Tactic: rw [rdrop_eq_reverse_drop_reverse, ← length_reverse,
      reverse_append, drop_left, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
rw : (drop l₂.length (l₁ ++ l₂).reverse).reverse = l₁
rw₁ : (drop l₂.reverse.length (l₁ ++ l₂).reverse).reverse = l₁
⊢ (l₁ ++ l₂).rdrop l₂.length = l₁
have rw₂ : (drop l₂.reverse.length (l₂.reverse ++ l₁.reverse)).reverse = l₁
Tactic: rw [rdrop_eq_reverse_drop_reverse, ← length_reverse,
      reverse_append, drop_left, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
rw : (drop l₂.length (l₁ ++ l₂).reverse).reverse = l₁
rw₁ : (drop l₂.reverse.length (l₁ ++ l₂).reverse).reverse = l₁
rw₂ : (drop l₂.reverse.length (l₂.reverse ++ l₁.reverse)).reverse = l₁
⊢ (l₁ ++ l₂).rdrop l₂.length = l₁
have rw₃ : l₁.reverse.reverse = l₁
Tactic: rw [rdrop_eq_reverse_drop_reverse, ← length_reverse,
      reverse_append, drop_left, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
rw : (drop l₂.length (l₁ ++ l₂).reverse).reverse = l₁
rw₁ : (drop l₂.reverse.length (l₁ ++ l₂).reverse).reverse = l₁
rw₂ : (drop l₂.reverse.length (l₂.reverse ++ l₁.reverse)).reverse = l₁
rw₃ : l₁.reverse.reverse = l₁
⊢ (l₁ ++ l₂).rdrop l₂.length = l₁
have rw₄ : l₁ = l₁
Tactic: rw [rdrop_eq_reverse_drop_reverse, ← length_reverse,
      reverse_append, drop_left, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (hypothesis)
Goal:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.length
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k
have hk₁ : k ≤ l₂.reverse.length
Tactic: rw [← length_reverse] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k
have rw : (drop k (l₁ ++ l₂).reverse).reverse = l₁ ++ l₂.rdrop k
Tactic: rw [rdrop_eq_reverse_drop_reverse, reverse_append, drop_append_of_le_length hk,
    reverse_append, reverse_reverse, ← rdrop_eq_reverse_drop_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
rw : (drop k (l₁ ++ l₂).reverse).reverse = l₁ ++ l₂.rdrop k
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k
have rw₁ : (drop k (l₂.reverse ++ l₁.reverse)).reverse = l₁ ++ l₂.rdrop k
Tactic: rw [rdrop_eq_reverse_drop_reverse, reverse_append, drop_append_of_le_length hk,
    reverse_append, reverse_reverse, ← rdrop_eq_reverse_drop_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
rw : (drop k (l₁ ++ l₂).reverse).reverse = l₁ ++ l₂.rdrop k
rw₁ : (drop k (l₂.reverse ++ l₁.reverse)).reverse = l₁ ++ l₂.rdrop k
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k
have rw₂ : (drop k l₂.reverse ++ l₁.reverse).reverse = l₁ ++ l₂.rdrop k
Tactic: rw [rdrop_eq_reverse_drop_reverse, reverse_append, drop_append_of_le_length hk,
    reverse_append, reverse_reverse, ← rdrop_eq_reverse_drop_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
rw : (drop k (l₁ ++ l₂).reverse).reverse = l₁ ++ l₂.rdrop k
rw₁ : (drop k (l₂.reverse ++ l₁.reverse)).reverse = l₁ ++ l₂.rdrop k
rw₂ : (drop k l₂.reverse ++ l₁.reverse).reverse = l₁ ++ l₂.rdrop k
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k
have rw₃ : l₁.reverse.reverse ++ (drop k l₂.reverse).reverse = l₁ ++ l₂.rdrop k
Tactic: rw [rdrop_eq_reverse_drop_reverse, reverse_append, drop_append_of_le_length hk,
    reverse_append, reverse_reverse, ← rdrop_eq_reverse_drop_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
rw : (drop k (l₁ ++ l₂).reverse).reverse = l₁ ++ l₂.rdrop k
rw₁ : (drop k (l₂.reverse ++ l₁.reverse)).reverse = l₁ ++ l₂.rdrop k
rw₂ : (drop k l₂.reverse ++ l₁.reverse).reverse = l₁ ++ l₂.rdrop k
rw₃ : l₁.reverse.reverse ++ (drop k l₂.reverse).reverse = l₁ ++ l₂.rdrop k
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k
have rw₄ : l₁ ++ (drop k l₂.reverse).reverse = l₁ ++ l₂.rdrop k
Tactic: rw [rdrop_eq_reverse_drop_reverse, reverse_append, drop_append_of_le_length hk,
    reverse_append, reverse_reverse, ← rdrop_eq_reverse_drop_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
rw : (drop k (l₁ ++ l₂).reverse).reverse = l₁ ++ l₂.rdrop k
rw₁ : (drop k (l₂.reverse ++ l₁.reverse)).reverse = l₁ ++ l₂.rdrop k
rw₂ : (drop k l₂.reverse ++ l₁.reverse).reverse = l₁ ++ l₂.rdrop k
rw₃ : l₁.reverse.reverse ++ (drop k l₂.reverse).reverse = l₁ ++ l₂.rdrop k
rw₄ : l₁ ++ (drop k l₂.reverse).reverse = l₁ ++ l₂.rdrop k
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k
have rw₅ : l₁ ++ l₂.rdrop k = l₁ ++ l₂.rdrop k
Tactic: rw [rdrop_eq_reverse_drop_reverse, reverse_append, drop_append_of_le_length hk,
    reverse_append, reverse_reverse, ← rdrop_eq_reverse_drop_reverse]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
k : ℕ
⊢ (l₁ ++ l₂).rdrop (l₂.length + k) = l₁.rdrop k
have rw : ((l₁ ++ l₂).rdrop l₂.length).rdrop k = l₁.rdrop k
Tactic: rw [← rdrop_add, rdrop_append_length]
-- Lean 4 proof step from Mathlib.Data.List.DropRight (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
k : ℕ
rw : ((l₁ ++ l₂).rdrop l₂.length).rdrop k = l₁.rdrop k
⊢ (l₁ ++ l₂).rdrop (l₂.length + k) = l₁.rdrop k
have rw₁ : l₁.rdrop k = l₁.rdrop k
Tactic: rw [← rdrop_add, rdrop_append_length]
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l
have cons_mem : ∀ {l : List α}, x ∈ l → x ∈ x :: l
Tactic: induction h with
  | cons_mem => exact mem_cons_self
  | cons_duplicate _ hm => exact mem_cons_of_mem _ hm
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x : α
h : x ∈+ l
cons_mem : ∀ {l : List α}, x ∈ l → x ∈ x :: l
⊢ x ∈ l
have cons_duplicate : ∀ {y : α} {l : List α}, x ∈+ l → ∀ (hm : x ∈ l), x ∈ y :: l
Tactic: induction h with
  | cons_mem => exact mem_cons_self
  | cons_duplicate _ hm => exact mem_cons_of_mem _ hm
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x : α
h : x ∈+ x :: l
⊢ x ∈ l
have cons_mem : ∀ (h : x ∈ l), x ∈ l
Tactic: obtain h | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x : α
h : x ∈+ x :: l
cons_mem : ∀ (h : x ∈ l), x ∈ l
⊢ x ∈ l
have cons_duplicate : ∀ (h : x ∈+ l), x ∈ l
Tactic: obtain h | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x : α
h : x ∈+ l
y : α
⊢ l ≠ [y]
have cons_mem : ∀ {l : List α} (h : x ∈ l), x :: l ≠ [y]
Tactic: induction h with
  | cons_mem h => simp [ne_nil_of_mem h]
  | cons_duplicate h => simp [ne_nil_of_mem h.mem]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x : α
h : x ∈+ l
y : α
cons_mem : ∀ {l : List α} (h : x ∈ l), x :: l ≠ [y]
⊢ l ≠ [y]
have cons_duplicate : ∀ {y_1 : α} {l : List α} (h : x ∈+ l), l ≠ [y] → y_1 :: l ≠ [y]
Tactic: induction h with
  | cons_mem h => simp [ne_nil_of_mem h]
  | cons_duplicate h => simp [ne_nil_of_mem h.mem]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x y : α
⊢ x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l
have refine_1 : ∀ (h : x ∈+ y :: l), y = x ∧ x ∈ l ∨ x ∈+ l
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x y : α
refine_1 : ∀ (h : x ∈+ y :: l), y = x ∧ x ∈ l ∨ x ∈+ l
⊢ x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l
have refine_2 : ∀ (h : y = x ∧ x ∈ l ∨ x ∈+ l), x ∈+ y :: l
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l
have refine_1 : ∀ (hm : x ∈ l), x = x ∧ x ∈ l ∨ x ∈+ l
Tactic: obtain hm | hm := h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
refine_1 : ∀ (hm : x ∈ l), x = x ∧ x ∈ l ∨ x ∈+ l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l
have refine_1₁ : ∀ (hm : x ∈+ l), y = x ∧ x ∈ l ∨ x ∈+ l
Tactic: obtain hm | hm := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x y : α
h : y = x ∧ x ∈ l ∨ x ∈+ l
⊢ x ∈+ y :: l
have refine_2 : x ∈ l → x ∈+ x :: l
Tactic: rcases h with (⟨rfl | h⟩ | h)
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x y : α
h : y = x ∧ x ∈ l ∨ x ∈+ l
refine_2 : x ∈ l → x ∈+ x :: l
⊢ x ∈+ y :: l
have refine_2₁ : ∀ (h : x ∈+ l), x ∈+ y :: l
Tactic: rcases h with (⟨rfl | h⟩ | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : ∀ (hx : x ∈+ l₁), x ∈+ l₂
hx : x ∈+ y :: l₁
⊢ x ∈+ y :: l₂
have cons_cons : ∀ (hx : y = x ∧ x ∈ l₁ ∨ x ∈+ l₁), y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
Tactic: rw [duplicate_cons_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : ∀ (hx : x ∈+ l₁), x ∈+ l₂
hx : y = x ∧ x ∈ l₁ ∨ x ∈+ l₁
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
have cons_cons : ∀ (IH : ∀ (hx : y ∈+ l₁), y ∈+ l₂) (hx : y ∈ l₁), y = y ∧ y ∈ l₂ ∨ y ∈+ l₂
Tactic: rcases hx with (⟨rfl, hx⟩ | hx)
Cleared hypotheses: x, IH, hx
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : ∀ (hx : x ∈+ l₁), x ∈+ l₂
hx : y = x ∧ x ∈ l₁ ∨ x ∈+ l₁
cons_cons : ∀ (IH : ∀ (hx : y ∈+ l₁), y ∈+ l₂) (hx : y ∈ l₁), y = y ∧ y ∈ l₂ ∨ y ∈+ l₂
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
have cons_cons₁ : ∀ (hx : x ∈+ l₁), y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
Tactic: rcases hx with (⟨rfl, hx⟩ | hx)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ l
h : l <+ l'
⊢ x ∈+ l'
have slnil : ∀ (hx : x ∈+ []), x ∈+ []
Tactic: induction h with
  | slnil => exact hx
  | cons y _ IH => exact (IH hx).duplicate_cons _
  | cons_cons y h IH =>
    rw [duplicate_cons_iff] at hx ⊢
    rcases hx with (⟨rfl, hx⟩ | hx)
    · simp [h.subset hx]
    · simp [IH hx]
Cleared hypotheses: hx, h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ l
h : l <+ l'
slnil : ∀ (hx : x ∈+ []), x ∈+ []
⊢ x ∈+ l'
have cons : ∀ {l₁ l₂ : List α} (y : α), l₁ <+ l₂ → ∀ (IH : ∀ (hx : x ∈+ l₁), x ∈+ l₂) (hx : x ∈+ l₁), x ∈+ y :: l₂
Tactic: induction h with
  | slnil => exact hx
  | cons y _ IH => exact (IH hx).duplicate_cons _
  | cons_cons y h IH =>
    rw [duplicate_cons_iff] at hx ⊢
    rcases hx with (⟨rfl, hx⟩ | hx)
    · simp [h.subset hx]
    · simp [IH hx]
Cleared hypotheses: hx, h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ l
h : l <+ l'
slnil : ∀ (hx : x ∈+ []), x ∈+ []
cons : ∀ {l₁ l₂ : List α} (y : α), l₁ <+ l₂ → ∀ (IH : ∀ (hx : x ∈+ l₁), x ∈+ l₂) (hx : x ∈+ l₁), x ∈+ y :: l₂
⊢ x ∈+ l'
have cons_cons : ∀ {l₁ l₂ : List α} (y : α) (h : l₁ <+ l₂) (IH : ∀ (hx : x ∈+ l₁), x ∈+ l₂) (hx : x ∈+ y :: l₁), x ∈+ y :: l₂
Tactic: induction h with
  | slnil => exact hx
  | cons y _ IH => exact (IH hx).duplicate_cons _
  | cons_cons y h IH =>
    rw [duplicate_cons_iff] at hx ⊢
    rcases hx with (⟨rfl, hx⟩ | hx)
    · simp [h.subset hx]
    · simp [IH hx]
Cleared hypotheses: hx, h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l_1 : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l
have pos : ∀ (hx : x = y), x ∈+ y :: l ↔ [x, x] <+ y :: l
Tactic: by_cases hx : x = y
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l_1 : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
pos : ∀ (hx : x = y), x ∈+ y :: l ↔ [x, x] <+ y :: l
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l
have neg : ∀ (hx : ¬x = y), x ∈+ y :: l ↔ [x, x] <+ y :: l
Tactic: by_cases hx : x = y
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l_1 : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l
have neg : [x, x] <+ l ↔ [x, x] <+ y :: l
Tactic: rw [duplicate_cons_iff_of_ne hx, IH]
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l_1 : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ [x, x] <+ l ↔ [x, x] <+ y :: l
have neg : ∀ (h : [x, x] <+ y :: l), [x, x] <+ l
Tactic: refine ⟨sublist_cons_of_sublist y, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l_1 : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
h : [x, x] <+ y :: l
⊢ [x, x] <+ l
have neg : [x, x] <+ l → [x, x] <+ l
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l_1 : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
h : [x, x] <+ y :: l
neg : [x, x] <+ l → [x, x] <+ l
⊢ [x, x] <+ l
have neg₁ : ∀ (hx : ¬x = x), [x] <+ l → [x, x] <+ l
Tactic: cases h
Cleared hypotheses: y, hx, h
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x : α
⊢ x ∈+ l ↔ [x, x] <+ l
have nil : x ∈+ [] ↔ [x, x] <+ []
Tactic: induction l with
  | nil => simp
  | cons y l IH =>
    by_cases hx : x = y
    · simp [hx, cons_sublist_cons, singleton_sublist]
    · rw [duplicate_cons_iff_of_ne hx, IH]
      refine ⟨sublist_cons_of_sublist y, fun h => ?_⟩
      cases h
      · assumption
      · contradiction
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
x : α
nil : x ∈+ [] ↔ [x, x] <+ []
⊢ x ∈+ l ↔ [x, x] <+ l
have cons : ∀ (y : α) (l : List α) (IH : x ∈+ l ↔ [x, x] <+ l), x ∈+ y :: l ↔ [x, x] <+ y :: l
Tactic: induction l with
  | nil => simp
  | cons y l IH =>
    by_cases hx : x = y
    · simp [hx, cons_sublist_cons, singleton_sublist]
    · rw [duplicate_cons_iff_of_ne hx, IH]
      refine ⟨sublist_cons_of_sublist y, fun h => ?_⟩
      cases h
      · assumption
      · contradiction
-- Lean 4 proof step from Mathlib.Data.List.Duplicate (goal)
Goal:
α : Type u_1
l : List α
⊢ l.Nodup ↔ ∀ (x : α), ¬x ∈+ l
have simp_rw : (∀ (a : α), ¬[a, a] <+ l) ↔ ∀ (x : α), ¬x ∈+ l
Tactic: simp_rw [nodup_iff_sublist, duplicate_iff_sublist]
-- Lean 4 proof step from Mathlib.Data.List.FinRange (goal)
Goal:
α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = pmap (P := fun (i : ℕ) ↦ i < n) (fun (i : ℕ) (hi : i < n) ↦ f ⟨i, hi⟩) (range n) ⋯
have h : ∀ (i : ℕ) (a : α),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) i = some a ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
        (pmap (P := fun (i : ℕ) ↦ i < n) (fun (i : ℕ) (hi : i < n) ↦ f (⟨i, hi⟩ : Fin n)) (range n) sorry) i =
      some a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.List.FinRange (goal)
Goal:
α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = map f (finRange n)
have rw : ofFn f = map f (ofFn id)
Tactic: rw [← ofFn_id, map_ofFn, Function.comp_id]
-- Lean 4 proof step from Mathlib.Data.List.FinRange (goal)
Goal:
α : Type u
n : ℕ
f : Fin n → α
rw : ofFn f = map f (ofFn id)
⊢ ofFn f = map f (finRange n)
have rw₁ : ofFn f = ofFn (f ∘ id)
Tactic: rw [← ofFn_id, map_ofFn, Function.comp_id]
-- Lean 4 proof step from Mathlib.Data.List.FinRange (goal)
Goal:
α : Type u
n : ℕ
f : Fin n → α
rw : ofFn f = map f (ofFn id)
rw₁ : ofFn f = ofFn (f ∘ id)
⊢ ofFn f = map f (finRange n)
have rw₂ : ofFn f = ofFn f
Tactic: rw [← ofFn_id, map_ofFn, Function.comp_id]
-- Lean 4 proof step from Mathlib.Data.List.FinRange (goal)
Goal:
α : Type u
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ (ofFn f).Nodup
have rw : Nodup.{u} (α := α) (pmap (P := fun (i : ℕ) ↦ i < n) (fun (i : ℕ) (hi : i < n) ↦ f ⟨i, hi⟩) (range n) sorry)
Tactic: rw [ofFn_eq_pmap]
-- Lean 4 proof step from Mathlib.Data.List.FinRange (goal)
Goal:
α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn f).Nodup ↔ Function.Injective f
have refine : (ofFn f).Nodup → Function.Injective f
Tactic: refine ⟨?_, nodup_ofFn_ofInjective⟩
-- Lean 4 proof step from Mathlib.Data.List.FinRange (goal)
Goal:
α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn f).Nodup → Function.Injective f
have refine_1 : Nodup.{u} (α := α) (ofFn Fin.elim0) → Function.Injective.{1, u + 1} (β := α) Fin.elim0
Tactic: refine Fin.consInduction ?_ (fun x₀ xs ih => ?_) f
-- Lean 4 proof step from Mathlib.Data.List.FinRange (goal)
Goal:
α : Type u
n : ℕ
f : Fin n → α
refine_1 : Nodup.{u} (α := α) (ofFn Fin.elim0) → Function.Injective.{1, u + 1} (β := α) Fin.elim0
⊢ (ofFn f).Nodup → Function.Injective f
have refine_2 : ∀ {n : ℕ} (x₀ : α) (xs : Fin n → α) (ih : (ofFn xs).Nodup → Function.Injective xs),
  Nodup.{u} (α := α) (ofFn (n := n + 1) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ α) x₀ xs)) →
    Function.Injective.{1, u + 1} (α := Fin (n + 1)) (β := α) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ α) x₀ xs)
Tactic: refine Fin.consInduction ?_ (fun x₀ xs ih => ?_) f
-- Lean 4 proof step from Mathlib.Data.List.FinRange (goal)
Goal:
α : Type u
n : ℕ
f : Fin n → α
n_1 : ℕ
x₀ : α
xs : Fin n_1 → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : Nodup.{u} (α := α) (ofFn (n := n_1 + 1) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ α) x₀ xs))
⊢ Function.Injective.{1, u + 1} (α := Fin (n_1 + 1)) (β := α) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ α) x₀ xs)
have refine_2 : ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
Tactic: rw [Fin.cons_injective_iff]
-- Lean 4 proof step from Mathlib.Data.List.FinRange (hypothesis)
Goal:
α : Type u
n : ℕ
f : Fin n → α
n_1 : ℕ
x₀ : α
xs : Fin n_1 → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : Nodup.{u} (α := α) (ofFn (n := n_1 + 1) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ α) x₀ xs))
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
have h₁ : (¬∃ (i : Fin n_1), xs i = x₀) ∧ Nodup.{u} (α := α) (ofFn (n := n_1) fun (i : Fin n_1) ↦ xs i)
Tactic: simp_rw [ofFn_succ, Fin.cons_succ, nodup_cons, Fin.cons_zero, mem_ofFn] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.FinRange (goal)
Goal:
n : ℕ
σ : Perm (Fin n)
⊢ map (⇑σ : (a : Fin n) → Fin n) (finRange n) ~ finRange n
have rw : ∀ (a : Fin n), Membership.mem (γ := List (Fin n)) (map (⇑σ : (a : Fin n) → Fin n) (finRange n)) a ↔ a ∈ finRange n
Tactic: rw [perm_ext_iff_of_nodup ((nodup_finRange n).map σ.injective) <| nodup_finRange n]
-- Lean 4 proof step from Mathlib.Data.List.FinRange (goal)
Goal:
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ ofFn (n := n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ~ ofFn f
have rw : map f (map (⇑σ : (a : Fin n) → Fin n) (finRange n)) ~ map f (finRange n)
Tactic: rw [ofFn_eq_map, ofFn_eq_map, ← map_map]
-- Lean 4 proof step from Mathlib.Data.List.Flatten (goal)
Goal:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <+ l₂
⊢ l₁.flatten <+ l₂.flatten
have slnil : Sublist.{u_1} (α := α) (flatten []) (flatten [])
Tactic: induction h with grind
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Flatten (goal)
Goal:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <+ l₂
slnil : Sublist.{u_1} (α := α) (flatten []) (flatten [])
⊢ l₁.flatten <+ l₂.flatten
have cons : ∀ {l₁ l₂ : List (List α)} (a : List α), l₁ <+ l₂ → l₁.flatten <+ l₂.flatten → l₁.flatten <+ (a :: l₂).flatten
Tactic: induction h with grind
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Flatten (goal)
Goal:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <+ l₂
slnil : Sublist.{u_1} (α := α) (flatten []) (flatten [])
cons : ∀ {l₁ l₂ : List (List α)} (a : List α), l₁ <+ l₂ → l₁.flatten <+ l₂.flatten → l₁.flatten <+ (a :: l₂).flatten
⊢ l₁.flatten <+ l₂.flatten
have cons_cons : ∀ {l₁ l₂ : List (List α)} (a : List α), l₁ <+ l₂ → l₁.flatten <+ l₂.flatten → (a :: l₁).flatten <+ (a :: l₂).flatten
Tactic: induction h with grind
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Flatten (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
f g : α → List β
h : ∀ (a : α), a ∈ l → f a <+ g a
⊢ flatMap f l <+ flatMap g l
have nil : ∀ (h : ∀ (a : α), Membership.mem (γ := List α) [] a → f a <+ g a), flatMap f [] <+ flatMap g []
Tactic: induction l with grind
Cleared hypotheses: l, h