awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
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
⊢ take (n + 1) (b :: l) = List.filter (fun (a : α) ↦ elem a (take (n + 1) (b :: l))) (b :: l)

Tactic:
rw [take_succ_cons, Nodup.take_eq_filter_mem (Nodup.of_cons hl), filter_cons_of_pos (by simp)]

Premises used: List.take_succ_cons, List.filter_cons_of_pos, List.Nodup.of_cons
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
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
⊢ 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:
congr 1
-- Module: Mathlib.Data.List.Nodup
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

Tactic:
List.filter_congr ?_

Premises used: List.filter_congr
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
e_tail : ∀ (x : α), x ∈ l → elem x (take n l) = elem x (b :: List.filter (fun (a : α) ↦ elem a (take n l)) l)
⊢ 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:
refine List.filter_congr ?_

Premises used: List.filter_congr
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
x : α
hx : x ∈ l
⊢ x ≠ b

Tactic:
have : x ≠ b := fun h => (nodup_cons.1 hl).1 (h ▸ hx)
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
x : α
hx : x ∈ l
this : x ≠ b
⊢ elem x (take n l) = elem x (b :: List.filter (fun (a : α) ↦ elem a (take n l)) l)

Tactic:
simp +contextual [List.mem_filter, this, hx]

Premises used: List.mem_filter
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
H : l.Nodup
i : Fin l.length
⊢ (fun (x : { x : α // x ∈ l }) ↦ (⟨idxOf (↑x : α) l, ⋯⟩ : Fin l.length))
      ((fun (i : Fin l.length) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ l) (l.get i) ⋯) i) =
    i

Tactic:
simp only [List.get_idxOf, Fin.eta, H]

Premises used: Fin.eta, List.get_idxOf
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
H : l.Nodup
x : { x : α // x ∈ l }
⊢ (fun (i : Fin l.length) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ l) (l.get i) ⋯)
      ((fun (x : { x : α // x ∈ l }) ↦ (⟨idxOf (↑x : α) l, ⋯⟩ : Fin l.length)) x) =
    x

Tactic:
simp
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
nd : l.Nodup
h : ∀ (x : α), x ∈ l
i : Fin l.length
⊢ (fun (a : α) ↦ (⟨idxOf a l, ⋯⟩ : Fin l.length)) ((fun (i : Fin l.length) ↦ l.get i) i) = i

Tactic:
simp [nd]
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
nd : l.Nodup
h : ∀ (x : α), x ∈ l
a : α
⊢ (fun (i : Fin l.length) ↦ l.get i) ((fun (a : α) ↦ (⟨idxOf a l, ⋯⟩ : Fin l.length)) a) = a

Tactic:
simp
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
inst : Preorder α
l : List α
inst_1 : DecidableEq α
H : l.SortedLT
i : Fin l.length
⊢ (↑((getIso l H : (a : Fin l.length) → { x : α // x ∈ l }) i) : α) = l.get i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
inst : Preorder α
l : List α
inst_1 : DecidableEq α
H : l.SortedLT
x : { x : α // x ∈ l }
⊢ (↑(((getIso l H).symm : (a : { x : α // x ∈ l }) → Fin l.length) x) : ℕ) = idxOf (↑x : α) l

Tactic:
rfl

Premises used: List.idxOf, rfl
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l' : List α
f : ℕ ↪o ℕ
hf :
  ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) ix : ℕ)
⊢ [] <+ l'

Tactic:
simp
-- Module: Mathlib.Data.List.NodupEquivFin
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'

Tactic:
?_
-- Module: Mathlib.Data.List.NodupEquivFin
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 : ℕ)
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'
⊢ l <+ l'

Tactic:
induction l generalizing l' f with
  | nil => simp
  | cons hd tl IH => ?_

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.NodupEquivFin
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 : ℕ)
⊢ some hd = getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) 0 : ℕ)

Tactic:
simpa using hf 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Data.List.NodupEquivFin
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 : ℕ)
⊢ 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
-- Module: Mathlib.Data.List.NodupEquivFin
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 : ℕ)
⊢ ∃ (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

Premises used: List.getElem?_eq_some_iff, eq_comm
-- Module: Mathlib.Data.List.NodupEquivFin
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
⊢ (f : (a : ℕ) → ℕ) 0 < l'.length

Tactic:
obtain ⟨w, h⟩ := this
-- Module: Mathlib.Data.List.NodupEquivFin
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
⊢ getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) 0 : ℕ) w = hd

Tactic:
obtain ⟨w, h⟩ := this
-- Module: Mathlib.Data.List.NodupEquivFin
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 : ℕ
rw : HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ) ≤ (f : (a : ℕ) → ℕ) (b + 1)
⊢ 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

Tactic:
rw [Nat.sub_le_sub_iff_right, OrderEmbedding.le_iff_le, Nat.succ_le_succ_iff]

Premises used: Nat.succ_le_succ_iff, OrderEmbedding.le_iff_le, Nat.sub_le_sub_iff_right
-- Module: Mathlib.Data.List.NodupEquivFin
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 : ℕ
rw : 0 < b + 1
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ) ≤ (f : (a : ℕ) → ℕ) (b + 1)

Tactic:
rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]

Premises used: OrderEmbedding.lt_iff_lt, Nat.succ_le_iff
-- Module: Mathlib.Data.List.NodupEquivFin
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 : ℕ
⊢ 0 < b + 1

Tactic:
b.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.List.NodupEquivFin
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 : ℕ
⊢ 0 < b + 1

Tactic:
exact b.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.List.NodupEquivFin
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)
rw₁ : HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ) ≤ (f : (a : ℕ) → ℕ) (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 : ℕ)

Tactic:
rw [List.getElem?_drop, OrderEmbedding.coe_ofMapLEIff, Nat.add_sub_cancel', ← hf]

Premises used: List.getElem?_drop, Nat.add_sub_cancel', OrderEmbedding.coe_ofMapLEIff
-- Module: Mathlib.Data.List.NodupEquivFin
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? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) (ix + 1)

Tactic:
simp only [getElem?_cons_succ]

Premises used: List.getElem?_cons_succ
-- Module: Mathlib.Data.List.NodupEquivFin
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 : 0 < ix + 1
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ) ≤ (f : (a : ℕ) → ℕ) (ix + 1)

Tactic:
rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]

Premises used: OrderEmbedding.lt_iff_lt, Nat.succ_le_iff
-- Module: Mathlib.Data.List.NodupEquivFin
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 : ℕ
⊢ 0 < ix + 1

Tactic:
ix.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.List.NodupEquivFin
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 : ℕ
⊢ 0 < ix + 1

Tactic:
exact ix.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.List.NodupEquivFin
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 : ℕ)

Tactic:
have : ∀ ix, tl[ix]? = (l'.drop (f 0 + 1))[f' ix]? := by
    intro ix
    rw [List.getElem?_drop, OrderEmbedding.coe_ofMapLEIff, Nat.add_sub_cancel', ← hf]
    · simp only [getElem?_cons_succ]
    rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
    exact ix.succ_pos
-- Module: Mathlib.Data.List.NodupEquivFin
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 : ℕ)))
    ⋯
this :
  ∀ (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 : ℕ)
cons :
  [hd] ++ tl <+
    take (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l' ++
      drop (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l'
⊢ hd :: tl <+ l'

Tactic:
rw [← List.take_append_drop (f 0 + 1) l', ← List.singleton_append]

Premises used: List.take_append_drop, List.singleton_append, HAdd.hAdd, OfNat.ofNat, DFunLike.coe