awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ Eq (α := List (ℕ × ℕ)) (map (Prod.swap ∘ fun (i : ℕ) ↦ (i, n - i)) (range (n + 1)))
    (map ((fun (i : ℕ) ↦ (i, n - i)) ∘ fun (x : ℕ) ↦ 0 + (n + 1) - 1 - x) (range (n + 1)))
have h : ∀ (a : ℕ),
  a ∈ range (n + 1) →
    Eq (α := ℕ × ℕ) ((Prod.swap ∘ fun (i : ℕ) ↦ (i, n - i)) a)
      (((fun (i : ℕ) ↦ (i, n - i)) ∘ fun (x : ℕ) ↦ 0 + (n + 1) - 1 - x) a)
Tactic: apply map_congr_left
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
⊢ (∀ (a : α), ¬[a, a] <+ l) → l.Nodup
have nil : (∀ (a : α), ¬[a, a] <+ []) → Nodup.{u} (α := α) []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
nil : (∀ (a : α), ¬[a, a] <+ []) → Nodup.{u} (α := α) []
⊢ (∀ (a : α), ¬[a, a] <+ l) → l.Nodup
have cons : ∀ (head : α) (tail : List α),
  ((∀ (a : α), ¬[a, a] <+ tail) → tail.Nodup) → (∀ (a : α), ¬[a, a] <+ head :: tail) → (head :: tail).Nodup
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
h :
  ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i _hi ≠
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j _hj
i j : Fin l.length
hg :
  Eq.{u + 1} (α := α)
    ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) i)
    ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) j)
⊢ i = j
have obtain : ∀ (i : ℕ) (hi : i < l.length)
  (hg :
    Eq.{u + 1} (α := α)
      ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) sorry) ⟨i, hi⟩)
      ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) sorry) j)),
  (⟨i, hi⟩ : Fin l.length) = j
Tactic: obtain ⟨i, hi⟩ := i
Cleared hypotheses: i, hg
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
h :
  ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i _hi ≠
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j _hj
j : Fin l.length
i : ℕ
hi : i < l.length
hg :
  Eq.{u + 1} (α := α)
    ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) ⟨i, hi⟩)
    ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) j)
⊢ (⟨i, hi⟩ : Fin l.length) = j
have obtain : ∀ (j : ℕ) (hj : j < l.length)
  (hg :
    Eq.{u + 1} (α := α)
      ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) sorry) ⟨i, hi⟩)
      ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) sorry) ⟨j, hj⟩)),
  (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩
Tactic: obtain ⟨j, hj⟩ := j
Cleared hypotheses: j, hg
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
h :
  ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i _hi ≠
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j _hj
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg :
  Eq.{u + 1} (α := α)
    ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) ⟨i, hi⟩)
    ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) ⟨j, hj⟩)
⊢ (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩
have inl : ∀ (hij : i < j), (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩
Tactic: rcases Nat.lt_trichotomy i j with (hij | rfl | hji)
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
h :
  ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i _hi ≠
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j _hj
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg :
  Eq.{u + 1} (α := α)
    ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) ⟨i, hi⟩)
    ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) ⟨j, hj⟩)
inl : ∀ (hij : i < j), (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩
⊢ (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩
have inr : ∀ (hj : i < l.length)
  (hg :
    Eq.{u + 1} (α := α)
      ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) sorry) ⟨i, hi⟩)
      ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) sorry) ⟨i, hj⟩)),
  (⟨i, hi⟩ : Fin l.length) = ⟨i, hj⟩
Tactic: rcases Nat.lt_trichotomy i j with (hij | rfl | hji)
Cleared hypotheses: j, hj, hg
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
h :
  ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i _hi ≠
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j _hj
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg :
  Eq.{u + 1} (α := α)
    ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) ⟨i, hi⟩)
    ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) ⟨j, hj⟩)
inl : ∀ (hij : i < j), (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩
inr :
  ∀ (hj : i < l.length)
    (hg :
      Eq.{u + 1} (α := α)
        ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) ⟨i, hi⟩)
        ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) ⟨i, hj⟩)),
    (⟨i, hi⟩ : Fin l.length) = ⟨i, hj⟩
⊢ (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩
have inr₁ : ∀ (hji : j < i), (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩
Tactic: rcases Nat.lt_trichotomy i j with (hij | rfl | hji)
-- Lean 4 proof step from Mathlib.Data.List.Nodup (hypothesis)
Goal:
α : Type u
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj ↔
    i = j
have this : l.get (⟨i, hi⟩ : Fin l.length) = l.get (⟨j, hj⟩ : Fin l.length) ↔ (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩
Tactic: have := @Nodup.get_inj_iff _ _ h ⟨i, hi⟩ ⟨j, hj⟩
-- Lean 4 proof step from Mathlib.Data.List.Nodup (hypothesis)
Goal:
α : Type u
x hd : α
tl : List α
hl : ∀ (h : tl.Nodup), tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
have hl₁ : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
Tactic: specialize hl h.of_cons
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
have pos : ∀ (hx : tl = [x]), hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
Tactic: by_cases hx : tl = [x]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
pos : ∀ (hx : tl = [x]), hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
have neg : ∀ (hx : ¬tl = [x]), hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
Tactic: by_cases hx : tl = [x]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (hypothesis)
Goal:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
have hx₁ : tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
Tactic: rw [← Ne, hl] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
hx : tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
have neg : ∀ (h : [hd].Nodup)
  (hl : [] ≠ [x] ↔ Eq.{u + 1} (α := List α) [] [] ∨ ∃ (y : α), Membership.mem (γ := List α) [] y ∧ y ≠ x),
  [hd] ≠ [x] ↔ [hd] = [] ∨ ∃ (y : α), y ∈ [hd] ∧ y ≠ x
Tactic: rcases hx with (rfl | ⟨y, hy, hx⟩)
Cleared hypotheses: tl, h, hl, hx
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
hx : tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
neg :
  ∀ (h : [hd].Nodup)
    (hl : [] ≠ [x] ↔ Eq.{u + 1} (α := List α) [] [] ∨ ∃ (y : α), Membership.mem (γ := List α) [] y ∧ y ≠ x),
    [hd] ≠ [x] ↔ [hd] = [] ∨ ∃ (y : α), y ∈ [hd] ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
have neg₁ : ∀ (y : α) (hy : y ∈ tl) (hx : y ≠ x), hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
Tactic: rcases hx with (rfl | ⟨y, hy, hx⟩)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
have neg : ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
Tactic: suffices ∃ y ∈ hd :: tl, y ≠ x by simpa [ne_nil_of_mem hy]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
h : l.Nodup
x : α
⊢ l ≠ [x] ↔ l = [] ∨ ∃ (y : α), y ∈ l ∧ y ≠ x
have nil : ∀ (h : Nodup.{u} (α := α) []),
  [] ≠ [x] ↔ Eq.{u + 1} (α := List α) [] [] ∨ ∃ (y : α), Membership.mem (γ := List α) [] y ∧ y ≠ x
Tactic: induction l with
  | nil => simp
  | cons hd tl hl =>
    specialize hl h.of_cons
    by_cases hx : tl = [x]
    · simpa [hx, and_comm, and_or_left] using h
    · rw [← Ne, hl] at hx
      rcases hx with (rfl | ⟨y, hy, hx⟩)
      · simp
      · suffices ∃ y ∈ hd :: tl, y ≠ x by simpa [ne_nil_of_mem hy]
        exact ⟨y, mem_cons_of_mem _ hy, hx⟩
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
h : l.Nodup
x : α
nil :
  ∀ (h : Nodup.{u} (α := α) []),
    [] ≠ [x] ↔ Eq.{u + 1} (α := List α) [] [] ∨ ∃ (y : α), Membership.mem (γ := List α) [] y ∧ y ≠ x
⊢ l ≠ [x] ↔ l = [] ∨ ∃ (y : α), y ∈ l ∧ y ≠ x
have cons : ∀ (hd : α) (tl : List α) (hl : ∀ (h : tl.Nodup), tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x) (h : (hd :: tl).Nodup),
  hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
Tactic: induction l with
  | nil => simp
  | cons hd tl hl =>
    specialize hl h.of_cons
    by_cases hx : tl = [x]
    · simpa [hx, and_comm, and_or_left] using h
    · rw [← Ne, hl] at hx
      rcases hx with (rfl | ⟨y, hy, hx⟩)
      · simp
      · suffices ∃ y ∈ hd :: tl, y ≠ x by simpa [ne_nil_of_mem hy]
        exact ⟨y, mem_cons_of_mem _ hy, hx⟩
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
xs : List α
n m : Fin xs.length
h : xs.get n = xs.get m
hne : n ≠ m
⊢ ¬xs.Nodup
have rw : ¬Injective xs.get
Tactic: rw [nodup_iff_injective_get]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
inst : BEq α
inst_1 : LawfulBEq α
x : α
⊢ count x l ≤ 1 ↔ x ∈ l → count x l = 1
have rw : count x l ≤ 1 ↔ 0 < count x l → count x l = 1
Tactic: rw [← count_pos_iff]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (hypothesis)
Goal:
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : ∀ (d : (map f tl).Nodup) ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (map f (hd :: tl)).Nodup
⊢ ∀ ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y
have d₁ : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
Tactic: simp only [map, nodup_cons, mem_map, not_exists, not_and, ← Ne.eq_def] at d
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : ∀ (d : (map f tl).Nodup) ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
⊢ ∀ ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y
have cons : ∀ ⦃x : α⦄, x = hd ∨ x ∈ tl → ∀ ⦃y : α⦄, y = hd ∨ y ∈ tl → f x = f y → x = y
Tactic: simp only [mem_cons]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
β : Type v
f : α → β
l : List α
d : (map f l).Nodup
⊢ ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → f x = f y → x = y
have nil : ∀ (d : (map f []).Nodup) ⦃x : α⦄,
  Membership.mem (γ := List α) [] x → ∀ ⦃y : α⦄, Membership.mem (γ := List α) [] y → f x = f y → x = y
Tactic: induction l with
  | nil => simp
  | cons hd tl ih =>
    simp only [map, nodup_cons, mem_map, not_exists, not_and, ← Ne.eq_def] at d
    simp only [mem_cons]
    rintro _ (rfl | h₁) _ (rfl | h₂) h₃
    · rfl
    · apply (d.1 _ h₂ h₃.symm).elim
    · apply (d.1 _ h₁ h₃).elim
    · apply ih d.2 h₁ h₂ h₃
Cleared hypotheses: l, d
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
β : Type v
f : α → β
l : List α
d : (map f l).Nodup
nil :
  ∀ (d : (map f []).Nodup) ⦃x : α⦄,
    Membership.mem (γ := List α) [] x → ∀ ⦃y : α⦄, Membership.mem (γ := List α) [] y → f x = f y → x = y
⊢ ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → f x = f y → x = y
have cons : ∀ (hd : α) (tl : List α) (ih : ∀ (d : (map f tl).Nodup) ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y)
  (d : (map f (hd :: tl)).Nodup) ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y
Tactic: induction l with
  | nil => simp
  | cons hd tl ih =>
    simp only [map, nodup_cons, mem_map, not_exists, not_and, ← Ne.eq_def] at d
    simp only [mem_cons]
    rintro _ (rfl | h₁) _ (rfl | h₂) h₃
    · rfl
    · apply (d.1 _ h₂ h₃.symm).elim
    · apply (d.1 _ h₁ h₃).elim
    · apply ih d.2 h₁ h₂ h₃
Cleared hypotheses: l, d
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
u : α
⊢ (l.concat u).Nodup ↔ ¬u ∈ l ∧ l.Nodup
have rw : (l.concat u).reverse.Nodup ↔ ¬u ∈ l ∧ l.Nodup
Tactic: rw [← nodup_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
a : α
l : List α
ih :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
    l.reverse.tail.Nodup ↔ l.tail.Nodup
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 = (a :: l).getLast?
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup
have pos : ∀ (hl : l = []), (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup
Tactic: by_cases hl : l = []
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
a : α
l : List α
ih :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
    l.reverse.tail.Nodup ↔ l.tail.Nodup
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 = (a :: l).getLast?
pos : ∀ (hl : l = []), (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup
have neg : ∀ (hl : ¬l = []), (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup
Tactic: by_cases hl : l = []
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
a : α
l : List α
ih :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
    l.reverse.tail.Nodup ↔ l.tail.Nodup
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 = (a :: l).getLast?
hl : ¬l = []
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup
have neg : ∀
  (ih :
    ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
      l.dropLast.Nodup ↔ l.tail.Nodup)
  (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 = (a :: l).getLast?) (hl : ¬l = []),
  (a :: l.dropLast).Nodup ↔ l.Nodup
Tactic: simp_all only [List.tail_reverse, List.nodup_reverse,
        List.dropLast_cons_of_ne_nil hl, List.tail_cons]
Cleared hypotheses: ih, h, hl
-- Lean 4 proof step from Mathlib.Data.List.Nodup (hypothesis)
Goal:
α : Type u
a : α
l : List α
ih :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
    l.dropLast.Nodup ↔ l.tail.Nodup
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 = (a :: l).getLast?
hl : ¬l = []
⊢ (a :: l.dropLast).Nodup ↔ l.Nodup
have h₁ : a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (l.length - 1) sorry
Tactic: simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem,
        Nat.add_one_sub_one, Nat.lt_add_one, Option.some.injEq, List.getElem_cons,
        show l.length ≠ 0 by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
a : α
l : List α
ih :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
    l.dropLast.Nodup ↔ l.tail.Nodup
hl : ¬l = []
h : a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (l.length - 1) ⋯
⊢ (a :: l.dropLast).Nodup ↔ l.Nodup
have neg : (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (l.length - 1) sorry :: l.dropLast).Nodup ↔
  ([l.getLast hl] ++ l.dropLast).Nodup
Tactic: rw [h,
        show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup by
          simp [List.dropLast_eq_take],
        List.nodup_append_comm]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?
⊢ l.reverse.tail.Nodup ↔ l.tail.Nodup
have nil : ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 = getLast? []),
  Nodup.{u} (α := α) (tail (reverse [])) ↔ Nodup.{u} (α := α) (tail [])
Tactic: induction l with
  | nil => simp
  | cons a l ih =>
    by_cases hl : l = []
    · simp_all
    · simp_all only [List.tail_reverse, List.nodup_reverse,
        List.dropLast_cons_of_ne_nil hl, List.tail_cons]
      simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem,
        Nat.add_one_sub_one, Nat.lt_add_one, Option.some.injEq, List.getElem_cons,
        show l.length ≠ 0 by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h
      rw [h,
        show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup by
          simp [List.dropLast_eq_take],
        List.nodup_append_comm]
      simp [List.getLast_eq_getElem]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?
nil :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 = getLast? []),
    Nodup.{u} (α := α) (tail (reverse [])) ↔ Nodup.{u} (α := α) (tail [])
⊢ l.reverse.tail.Nodup ↔ l.tail.Nodup
have cons : ∀ (a : α) (l : List α)
  (ih :
    ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
      l.reverse.tail.Nodup ↔ l.tail.Nodup)
  (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 = (a :: l).getLast?),
  (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup
Tactic: induction l with
  | nil => simp
  | cons a l ih =>
    by_cases hl : l = []
    · simp_all
    · simp_all only [List.tail_reverse, List.nodup_reverse,
        List.dropLast_cons_of_ne_nil hl, List.tail_cons]
      simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem,
        Nat.add_one_sub_one, Nat.lt_add_one, Option.some.injEq, List.getElem_cons,
        show l.length ≠ 0 by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h
      rw [h,
        show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup by
          simp [List.dropLast_eq_take],
        List.nodup_append_comm]
      simp [List.getLast_eq_getElem]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
l : List α
IH :
  ∀ (hl : l.Nodup) (i : ℕ) (h : i < l.length),
    l.erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h) = l.eraseIdx i
hl : (a :: l).Nodup
i : ℕ
h : i < (a :: l).length
⊢ (a :: l).erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) i h) = (a :: l).eraseIdx i
have cons : ∀ (h : 0 < (a :: l).length),
  (a :: l).erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 h) = (a :: l).eraseIdx 0
Tactic: cases i with
    | zero => simp
    | succ i => grind
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
l : List α
IH :
  ∀ (hl : l.Nodup) (i : ℕ) (h : i < l.length),
    l.erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h) = l.eraseIdx i
hl : (a :: l).Nodup
i : ℕ
h : i < (a :: l).length
cons :
  ∀ (h : 0 < (a :: l).length),
    (a :: l).erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 h) = (a :: l).eraseIdx 0
⊢ (a :: l).erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) i h) = (a :: l).eraseIdx i
have cons₁ : ∀ (i : ℕ) (h : i + 1 < (a :: l).length),
  (a :: l).erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) (i + 1) h) =
    (a :: l).eraseIdx (i + 1)
Tactic: cases i with
    | zero => simp
    | succ i => grind
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
hl : l.Nodup
i : ℕ
h : i < l.length
⊢ l.erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h) = l.eraseIdx i
have nil : ∀ (hl : Nodup.{u} (α := α) []) (i : ℕ) (h : i < length.{u} (α := α) []),
  List.erase [] (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] i h) = List.eraseIdx [] i
Tactic: induction l generalizing i with
  | nil => simp
  | cons a l IH =>
    cases i with
    | zero => simp
    | succ i => grind
Cleared hypotheses: l, hl, i, h
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
hl : l.Nodup
i : ℕ
h : i < l.length
nil :
  ∀ (hl : Nodup.{u} (α := α) []) (i : ℕ) (h : i < length.{u} (α := α) []),
    List.erase [] (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] i h) = List.eraseIdx [] i
⊢ l.erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h) = l.eraseIdx i
have cons : ∀ (a : α) (l : List α)
  (IH :
    ∀ (hl : l.Nodup) (i : ℕ) (h : i < l.length),
      l.erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h) = l.eraseIdx i)
  (hl : (a :: l).Nodup) (i : ℕ) (h : i < (a :: l).length),
  (a :: l).erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) i h) = (a :: l).eraseIdx i
Tactic: induction l generalizing i with
  | nil => simp
  | cons a l IH =>
    cases i with
    | zero => simp
    | succ i => grind
Cleared hypotheses: l, hl, i, h
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
β : Type v
l₁ : List α
f : α → List β
⊢ (flatMap f l₁).Nodup ↔ (∀ (x : α), x ∈ l₁ → (f x).Nodup) ∧ Pairwise (Disjoint on f) l₁
have simp : (Pairwise (fun (a b : α) ↦ (f a).Disjoint (f b)) l₁ ∧ ∀ (l : List β) (x : α), f x = l → x ∈ l₁ → l.Nodup) ↔
  Pairwise (Disjoint on f) l₁ ∧ ∀ (x : α), x ∈ l₁ → (f x).Nodup
Tactic: simp only [List.flatMap, nodup_flatten, pairwise_map, and_comm, mem_map,
    exists_imp, and_imp]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
β : Type v
l₁ : List α
f : α → List β
⊢ (Pairwise (fun (a b : α) ↦ (f a).Disjoint (f b)) l₁ ∧ ∀ (l : List β) (x : α), f x = l → x ∈ l₁ → l.Nodup) ↔
    Pairwise (Disjoint on f) l₁ ∧ ∀ (x : α), x ∈ l₁ → (f x).Nodup
have rw : (Pairwise (fun (a b : α) ↦ (f a).Disjoint (f b)) l₁ ∧ ∀ (x : α), x ∈ l₁ → (f x).Nodup) ↔
  Pairwise (Disjoint on f) l₁ ∧ ∀ (x : α), x ∈ l₁ → (f x).Nodup
Tactic: rw [show (∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔ ∀ x : α, x ∈ l₁ → Nodup (f x)
      from forall_comm.trans <| forall_congr' fun _ => forall_eq']