awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
x : α × β
h₁ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₁) x
h₂ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₂) x
⊢ False
have rcases : ∀ (b₁ : β),
  b₁ ∈ l₂ →
    ∀ (h₁ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₁) (a₁, b₁))
      (h₂ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₂) (a₁, b₁)), False
Tactic: rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩
Cleared hypotheses: x, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.List.Nodup (hypothesis)
Goal:
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : β
left : b₁ ∈ l₂
h₁ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₁) (a₁, b₁)
h₂ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₂) (a₁, b₁)
⊢ False
have n₁ : a₁ ≠ a₁
Tactic: rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩
Cleared hypotheses: a₂, n, h₂
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
x : (a : α) × σ a
h₁ : Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₁) x
h₂ : Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₂) x
⊢ False
have rcases : ∀ (b₁ : σ a₁),
  b₁ ∈ l₂ a₁ →
    ∀
      (h₁ :
        Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₁)
          (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁))
      (h₂ :
        Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₂)
          (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)),
      False
Tactic: rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩
Cleared hypotheses: x, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.List.Nodup (hypothesis)
Goal:
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : σ a₁
left : b₁ ∈ l₂ a₁
h₁ :
  Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₁)
    (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)
h₂ :
  Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₂)
    (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)
⊢ False
have n₁ : a₁ ≠ a₁
Tactic: rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩
Cleared hypotheses: a₂, n, h₂
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b' ∈ f a
have rw : b ∈ f a
Tactic: rw [← e]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
a : α
h : ¬a ∈ l
h' : l.Nodup
⊢ (l.concat a).Nodup
have rw : (l ++ [a]).Nodup
Tactic: rw [concat_eq_append]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l : List α
a : α
inst : BEq α
inst_1 : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ (List.insert a l).Nodup
have rw : ¬a ∈ l ∧ l.Nodup
Tactic: rw [insert_of_not_mem h', nodup_cons]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
l₁ : List α
h : l₂.Nodup
⊢ (l₁ ∪ l₂).Nodup
have nil : ∀ {l₂ : List α} (h : l₂.Nodup), ([] ∪ l₂).Nodup
Tactic: induction l₁ generalizing l₂ with
  | nil => exact h
  | cons a l₁ ih => exact (ih h).insert
Cleared hypotheses: l₂, l₁, h
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
l₁ : List α
h : l₂.Nodup
nil : ∀ {l₂ : List α} (h : l₂.Nodup), ([] ∪ l₂).Nodup
⊢ (l₁ ∪ l₂).Nodup
have cons : ∀ (a : α) (l₁ : List α) (ih : ∀ {l₂ : List α} (h : l₂.Nodup), (l₁ ∪ l₂).Nodup) {l₂ : List α} (h : l₂.Nodup),
  (a :: l₁ ∪ l₂).Nodup
Tactic: induction l₁ generalizing l₂ with
  | nil => exact h
  | cons a l₁ ih => exact (ih h).insert
Cleared hypotheses: l₂, l₁, h
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : l₁.Nodup
⊢ l₁.diff (a :: l₂) = List.filter (fun (x : α) ↦ decide ¬x ∈ a :: l₂) l₁
have rw : List.filter (fun (a_1 : α) ↦ decide ¬a_1 ∈ l₂ && a_1 != a) l₁ = List.filter (fun (x : α) ↦ decide ¬x ∈ a :: l₂) l₁
Tactic: rw [diff_cons, (hl₁.erase _).diff_eq_filter, hl₁.erase_eq_filter, filter_filter]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l₁ l₂ : List α
a : α
inst : BEq α
inst_1 : LawfulBEq α
hl₁ : l₁.Nodup
⊢ a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂
have rw : a ∈ List.filter (fun (x : α) ↦ decide ¬x ∈ l₂) l₁ ↔ a ∈ l₁ ∧ ¬a ∈ l₂
Tactic: rw [hl₁.diff_eq_filter, mem_filter, decide_eq_true_iff]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l₁ l₂ : List α
a : α
inst : BEq α
inst_1 : LawfulBEq α
hl₁ : l₁.Nodup
rw : a ∈ List.filter (fun (x : α) ↦ decide ¬x ∈ l₂) l₁ ↔ a ∈ l₁ ∧ ¬a ∈ l₂
⊢ a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂
have rw₁ : a ∈ l₁ ∧ (decide ¬a ∈ l₂) = true ↔ a ∈ l₁ ∧ ¬a ∈ l₂
Tactic: rw [hl₁.diff_eq_filter, mem_filter, decide_eq_true_iff]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
l₁ l₂ : List α
a : α
inst : BEq α
inst_1 : LawfulBEq α
hl₁ : l₁.Nodup
rw : a ∈ List.filter (fun (x : α) ↦ decide ¬x ∈ l₂) l₁ ↔ a ∈ l₁ ∧ ¬a ∈ l₂
rw₁ : a ∈ l₁ ∧ (decide ¬a ∈ l₂) = true ↔ a ∈ l₁ ∧ ¬a ∈ l₂
⊢ a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂
have rw₂ : a ∈ l₁ ∧ ¬a ∈ l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂
Tactic: rw [hl₁.diff_eq_filter, mem_filter, decide_eq_true_iff]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
l : List α
hl : l.Nodup
f : α → β
x : α
y : β
⊢ map (update (β := fun (a : α) ↦ β) f x y) l = if x ∈ l then (map f l).set (idxOf x l) y else map f l
have cons : ∀ (hd : α) (tl : List α)
  (ihl :
    ∀ (hl : tl.Nodup),
      map (update (β := fun (a : α) ↦ β) f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl)
  (hl : (hd :: tl).Nodup),
  map (update (β := fun (a : α) ↦ β) f x y) (hd :: tl) =
    if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)
Tactic: induction l with | nil => simp | cons hd tl ihl => ?_
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.Nodup (hypothesis)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl :
  ∀ (hl : tl.Nodup),
    map (update (β := fun (a : α) ↦ β) f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : (hd :: tl).Nodup
⊢ map (update (β := fun (a : α) ↦ β) f x y) (hd :: tl) =
    if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)
have hl₁ : ¬hd ∈ tl ∧ tl.Nodup
Tactic: rw [nodup_cons] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl :
  ∀ (hl : tl.Nodup),
    map (update (β := fun (a : α) ↦ β) f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ tl.Nodup
⊢ map (update (β := fun (a : α) ↦ β) f x y) (hd :: tl) =
    if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)
have cons : (update (β := fun (a : α) ↦ β) f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
  if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl
Tactic: simp only [mem_cons, map, ihl hl.2]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl :
  ∀ (hl : tl.Nodup),
    map (update (β := fun (a : α) ↦ β) f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ tl.Nodup
⊢ (update (β := fun (a : α) ↦ β) f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl
have pos : ∀ (H : hd = x),
  (update (β := fun (a : α) ↦ β) f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl
Tactic: by_cases H : hd = x
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl :
  ∀ (hl : tl.Nodup),
    map (update (β := fun (a : α) ↦ β) f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ tl.Nodup
pos :
  ∀ (H : hd = x),
    (update (β := fun (a : α) ↦ β) f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
      if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl
⊢ (update (β := fun (a : α) ↦ β) f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl
have neg : ∀ (H : ¬hd = x),
  (update (β := fun (a : α) ↦ β) f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl
Tactic: by_cases H : hd = x
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl :
  ∀ (hl : tl.Nodup),
    map (update (β := fun (a : α) ↦ β) f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ tl.Nodup
H : hd = x
⊢ (update (β := fun (a : α) ↦ β) f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl
have pos : ∀ (hl : ¬x ∈ tl ∧ tl.Nodup),
  (update (β := fun (a : α) ↦ β) f x y x :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = x ∨ x ∈ tl then (f x :: map f tl).set (idxOf x (x :: tl)) y else f x :: map f tl
Tactic: subst hd
Cleared hypotheses: hd, hl, H
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ take (n + 1) (b :: l) = List.filter (fun (a : α) ↦ elem a (take (n + 1) (b :: l))) (b :: l)
have rw : b :: List.filter (fun (a : α) ↦ elem a (take n l)) l =
  b :: List.filter (fun (a : α) ↦ elem a (b :: List.filter (fun (a : α) ↦ elem a (take n l)) l)) l
Tactic: rw [take_succ_cons, Nodup.take_eq_filter_mem (Nodup.of_cons hl), filter_cons_of_pos (by simp)]
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ b :: List.filter (fun (a : α) ↦ elem a (take n l)) l =
    b :: List.filter (fun (a : α) ↦ elem a (b :: List.filter (fun (a : α) ↦ elem a (take n l)) l)) l
have e_tail : List.filter (fun (a : α) ↦ elem a (take n l)) l =
  List.filter (fun (a : α) ↦ elem a (b :: List.filter (fun (a : α) ↦ elem a (take n l)) l)) l
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.List.Nodup (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ List.filter (fun (a : α) ↦ elem a (take n l)) l =
    List.filter (fun (a : α) ↦ elem a (b :: List.filter (fun (a : α) ↦ elem a (take n l)) l)) l
have e_tail : ∀ (x : α), x ∈ l → elem x (take n l) = elem x (b :: List.filter (fun (a : α) ↦ elem a (take n l)) l)
Tactic: refine List.filter_congr ?_
-- Lean 4 proof step from Mathlib.Data.List.Nodup (hypothesis)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
x : α
hx : x ∈ l
⊢ elem x (take n l) = elem x (b :: List.filter (fun (a : α) ↦ elem a (take n l)) l)
have this : x ≠ b
Tactic: have : x ≠ b := fun h => (nodup_cons.1 hl).1 (h ▸ hx)
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
Goal:
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf :
  ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)
⊢ l <+ l'
have cons : ∀ (hd : α) (tl : List α)
  (IH :
    ∀ {l' : List α} (f : ℕ ↪o ℕ)
      (hf :
        ∀ (ix : ℕ),
          getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tl ix =
            getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)),
      tl <+ l')
  {l' : List α} (f : ℕ ↪o ℕ)
  (hf :
    ∀ (ix : ℕ),
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) ix =
        getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)),
  hd :: tl <+ l'
Tactic: induction l generalizing l' f with
  | nil => simp
  | cons hd tl IH => ?_
Cleared hypotheses: l, l', f, hf
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (hypothesis)
Goal:
α : Type u_1
hd : α
tl : List α
IH :
  ∀ {l' : List α} (f : ℕ ↪o ℕ)
    (hf :
      ∀ (ix : ℕ),
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tl ix =
          getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)),
    tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf :
  ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)
⊢ hd :: tl <+ l'
have this : some hd = getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) 0 : ℕ)
Tactic: have : some hd = l'[f 0]? := by simpa using hf 0
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (hypothesis)
Goal:
α : Type u_1
hd : α
tl : List α
IH :
  ∀ {l' : List α} (f : ℕ ↪o ℕ)
    (hf :
      ∀ (ix : ℕ),
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tl ix =
          getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)),
    tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf :
  ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)
this : some hd = getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) 0 : ℕ)
⊢ hd :: tl <+ l'
have this₁ : ∃ (h : (f : (a : ℕ) → ℕ) 0 < l'.length),
  getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) 0 : ℕ) h = hd
Tactic: rw [eq_comm, List.getElem?_eq_some_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (hypothesis)
Goal:
α : Type u_1
hd : α
tl : List α
IH :
  ∀ {l' : List α} (f : ℕ ↪o ℕ)
    (hf :
      ∀ (ix : ℕ),
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tl ix =
          getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)),
    tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf :
  ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)
this :
  ∃ (h : (f : (a : ℕ) → ℕ) 0 < l'.length),
    getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) 0 : ℕ) h = hd
⊢ hd :: tl <+ l'
have w : (f : (a : ℕ) → ℕ) 0 < l'.length
Tactic: obtain ⟨w, h⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (hypothesis)
Goal:
α : Type u_1
hd : α
tl : List α
IH :
  ∀ {l' : List α} (f : ℕ ↪o ℕ)
    (hf :
      ∀ (ix : ℕ),
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tl ix =
          getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)),
    tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf :
  ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)
this :
  ∃ (h : (f : (a : ℕ) → ℕ) 0 < l'.length),
    getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) 0 : ℕ) h = hd
w : (f : (a : ℕ) → ℕ) 0 < l'.length
⊢ hd :: tl <+ l'
have h : getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) 0 : ℕ) w = hd
Tactic: obtain ⟨w, h⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
Goal:
α : Type u_1
hd : α
tl : List α
IH :
  ∀ {l' : List α} (f : ℕ ↪o ℕ)
    (hf :
      ∀ (ix : ℕ),
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tl ix =
          getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)),
    tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf :
  ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)
w : (f : (a : ℕ) → ℕ) 0 < l'.length
h : getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) 0 : ℕ) w = hd
a b : ℕ
⊢ HSub.hSub (α := ℕ) ((f : (a : ℕ) → ℕ) (a + 1) : ℕ) (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) ≤
      HSub.hSub (α := ℕ) ((f : (a : ℕ) → ℕ) (b + 1) : ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) ↔
    a ≤ b
have rw : HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ) ≤ (f : (a : ℕ) → ℕ) (b + 1)
Tactic: rw [Nat.sub_le_sub_iff_right, OrderEmbedding.le_iff_le, Nat.succ_le_succ_iff]
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
Goal:
α : Type u_1
hd : α
tl : List α
IH :
  ∀ {l' : List α} (f : ℕ ↪o ℕ)
    (hf :
      ∀ (ix : ℕ),
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tl ix =
          getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)),
    tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf :
  ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)
w : (f : (a : ℕ) → ℕ) 0 < l'.length
h : getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) 0 : ℕ) w = hd
a b : ℕ
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ) ≤ (f : (a : ℕ) → ℕ) (b + 1)
have rw : 0 < b + 1
Tactic: rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
Goal:
α : Type u_1
hd : α
tl : List α
IH :
  ∀ {l' : List α} (f : ℕ ↪o ℕ)
    (hf :
      ∀ (ix : ℕ),
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tl ix =
          getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)),
    tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf :
  ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)
w : (f : (a : ℕ) → ℕ) 0 < l'.length
h : getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) 0 : ℕ) w = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff
    (fun (i : ℕ) ↦
      HSub.hSub (α := ℕ) ((f : (a : ℕ) → ℕ) (i + 1) : ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)))
    ⋯
ix : ℕ
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tl ix =
    getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (drop (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l') ((f' : (a : ℕ) → ℕ) ix : ℕ)
have rw : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tl ix =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) (ix + 1)
Tactic: rw [List.getElem?_drop, OrderEmbedding.coe_ofMapLEIff, Nat.add_sub_cancel', ← hf]
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
Goal:
α : Type u_1
hd : α
tl : List α
IH :
  ∀ {l' : List α} (f : ℕ ↪o ℕ)
    (hf :
      ∀ (ix : ℕ),
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tl ix =
          getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)),
    tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf :
  ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)
w : (f : (a : ℕ) → ℕ) 0 < l'.length
h : getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) 0 : ℕ) w = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff
    (fun (i : ℕ) ↦
      HSub.hSub (α := ℕ) ((f : (a : ℕ) → ℕ) (i + 1) : ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)))
    ⋯
ix : ℕ
rw :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tl ix =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) (ix + 1)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tl ix =
    getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (drop (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l') ((f' : (a : ℕ) → ℕ) ix : ℕ)
have rw₁ : HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ) ≤ (f : (a : ℕ) → ℕ) (ix + 1)
Tactic: rw [List.getElem?_drop, OrderEmbedding.coe_ofMapLEIff, Nat.add_sub_cancel', ← hf]
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
Goal:
α : Type u_1
hd : α
tl : List α
IH :
  ∀ {l' : List α} (f : ℕ ↪o ℕ)
    (hf :
      ∀ (ix : ℕ),
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tl ix =
          getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)),
    tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf :
  ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)
w : (f : (a : ℕ) → ℕ) 0 < l'.length
h : getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) 0 : ℕ) w = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff
    (fun (i : ℕ) ↦
      HSub.hSub (α := ℕ) ((f : (a : ℕ) → ℕ) (i + 1) : ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)))
    ⋯
ix : ℕ
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ) ≤ (f : (a : ℕ) → ℕ) (ix + 1)
have rw : 0 < ix + 1
Tactic: rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]