awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ)
apply : [hd] <+ take (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l'
⊢ [hd] ++ tl <+
    take (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l' ++
      drop (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l'

Tactic:
apply List.Sublist.append _ (IH _ this)

Premises used: List.Sublist.append
-- 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 : ℕ)
rw :
  getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (Nat.succ ((f : (a : ℕ) → ℕ) 0)) l')
      ((f : (a : ℕ) → ℕ) 0 : ℕ) ⋯ ∈
    take (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l'
⊢ [hd] <+ take (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l'

Tactic:
rw [List.singleton_sublist, ← h, l'.getElem_take' _ (Nat.lt_succ_self _)]

Premises used: Nat.lt_succ_self, List.getElem_take', List.singleton_sublist
-- 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 : ℕ)
⊢ getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (Nat.succ ((f : (a : ℕ) → ℕ) 0)) l')
      ((f : (a : ℕ) → ℕ) 0 : ℕ) ⋯ ∈
    take (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l'

Tactic:
List.getElem_mem _

Premises used: List.getElem_mem
-- 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 : ℕ)
⊢ getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (Nat.succ ((f : (a : ℕ) → ℕ) 0)) l')
      ((f : (a : ℕ) → ℕ) 0 : ℕ) ⋯ ∈
    take (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l'

Tactic:
exact List.getElem_mem _

Premises used: List.getElem_mem
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
mp :
  l <+ l' →
    ∃ (f : ℕ ↪o ℕ),
      ∀ (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 : ℕ)
mpr :
  (∃ (f : ℕ ↪o ℕ),
      ∀ (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'
⊢ l <+ l' ↔
    ∃ (f : ℕ ↪o ℕ),
      ∀ (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 : ℕ)

Tactic:
constructor
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
⊢ ∃ (f : ℕ ↪o ℕ),
    ∀ (ix : ℕ),
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] ix =
        getElem? (coll := List α) (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) []
          ((f : (a : ℕ) → ℕ) ix : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' l₁ l₂ : List α
a : α
h : l₁ <+ l₂
IH :
  ∃ (f : ℕ ↪o ℕ),
    ∀ (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 : ℕ)
mp :
  ∀ (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 : ℕ)),
    ∃ (f : ℕ ↪o ℕ),
      ∀ (ix : ℕ),
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ ix =
          getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂) ((f : (a : ℕ) → ℕ) ix : ℕ)
⊢ ∃ (f : ℕ ↪o ℕ),
    ∀ (ix : ℕ),
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ ix =
        getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂) ((f : (a : ℕ) → ℕ) ix : ℕ)

Tactic:
obtain ⟨f, hf⟩ := IH
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' l₁ l₂ : List α
a : α
h : l₁ <+ l₂
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 : ℕ)
x : ℕ
⊢ ∀ ⦃b : ℕ⦄, x < b → LT.lt (α := ℕ) ((fun (x : ℕ) ↦ x + 1) x) ((fun (x : ℕ) ↦ x + 1) b)

Tactic:
simp
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' l₁ l₂ : List α
a : α
h : l₁ <+ l₂
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 : ℕ)
mp :
  ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂)
        ((RelEmbedding.trans (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (t := fun (x1 x2 : ℕ) ↦
                x1 ≤ x2) f (OrderEmbedding.ofStrictMono (fun (x : ℕ) ↦ x + 1) ⋯) :
              (a : ℕ) → ℕ)
            ix :
          ℕ)
⊢ ∃ (f : ℕ ↪o ℕ),
    ∀ (ix : ℕ),
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ ix =
        getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂) ((f : (a : ℕ) → ℕ) ix : ℕ)

Tactic:
refine ⟨f.trans (OrderEmbedding.ofStrictMono (· + 1) fun _ => by simp), ?_⟩
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' l₁ l₂ : List α
a : α
h : l₁ <+ l₂
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 : ℕ)
⊢ ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂)
        ((RelEmbedding.trans (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (t := fun (x1 x2 : ℕ) ↦
                x1 ≤ x2) f (OrderEmbedding.ofStrictMono (fun (x : ℕ) ↦ x + 1) ⋯) :
              (a : ℕ) → ℕ)
            ix :
          ℕ)

Tactic:
simpa using hf
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' l₁ l₂ : List α
a : α
h : l₁ <+ l₂
IH :
  ∃ (f : ℕ ↪o ℕ),
    ∀ (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 : ℕ)
mp :
  ∀ (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 : ℕ)),
    ∃ (f : ℕ ↪o ℕ),
      ∀ (ix : ℕ),
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₁) ix =
          getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂) ((f : (a : ℕ) → ℕ) ix : ℕ)
⊢ ∃ (f : ℕ ↪o ℕ),
    ∀ (ix : ℕ),
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₁) ix =
        getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂) ((f : (a : ℕ) → ℕ) ix : ℕ)

Tactic:
obtain ⟨f, hf⟩ := IH
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' l₁ l₂ : List α
a : α
h : l₁ <+ l₂
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 : ℕ)
⊢ ∃ (f : ℕ ↪o ℕ),
    ∀ (ix : ℕ),
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₁) ix =
        getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂) ((f : (a : ℕ) → ℕ) ix : ℕ)

Tactic:
⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) ?_, ?_⟩

Premises used: Exists.intro, OrderEmbedding.ofMapLEIff, OfNat.ofNat, Nat.succ, Eq, DFunLike.coe, Nat.pred, ite
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' l₁ l₂ : List α
a : α
h : l₁ <+ l₂
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 : ℕ)
mp :
  ∀ (a b : ℕ),
    LE.le (α := ℕ) ((fun (ix : ℕ) ↦ if ix = 0 then 0 else Nat.succ ((f : (a : ℕ) → ℕ) ix.pred)) a)
        ((fun (ix : ℕ) ↦ if ix = 0 then 0 else Nat.succ ((f : (a : ℕ) → ℕ) ix.pred)) b) ↔
      a ≤ b
mp₁ :
  ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₁) ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂)
        ((OrderEmbedding.ofMapLEIff (fun (ix : ℕ) ↦ if ix = 0 then 0 else Nat.succ ((f : (a : ℕ) → ℕ) ix.pred)) ⋯ :
              (a : ℕ) → ℕ)
            ix :
          ℕ)
⊢ ∃ (f : ℕ ↪o ℕ),
    ∀ (ix : ℕ),
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₁) ix =
        getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂) ((f : (a : ℕ) → ℕ) ix : ℕ)

Tactic:
refine
        ⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) ?_, ?_⟩
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' l₁ l₂ : List α
a : α
h : l₁ <+ l₂
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 : ℕ)
⊢ LE.le (α := ℕ) ((fun (ix : ℕ) ↦ if ix = 0 then 0 else Nat.succ ((f : (a : ℕ) → ℕ) ix.pred)) 0)
      ((fun (ix : ℕ) ↦ if ix = 0 then 0 else Nat.succ ((f : (a : ℕ) → ℕ) ix.pred)) 0) ↔
    LE.le (α := ℕ) 0 0

Tactic:
simp [Nat.succ_le_succ_iff]

Premises used: Nat.succ_le_succ_iff
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' l₁ l₂ : List α
a : α
h : l₁ <+ l₂
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 : ℕ)
n : ℕ
⊢ LE.le (α := ℕ) ((fun (ix : ℕ) ↦ if ix = 0 then 0 else Nat.succ ((f : (a : ℕ) → ℕ) ix.pred)) 0)
      ((fun (ix : ℕ) ↦ if ix = 0 then 0 else Nat.succ ((f : (a : ℕ) → ℕ) ix.pred)) (n + 1)) ↔
    0 ≤ n + 1

Tactic:
simp [Nat.succ_le_succ_iff]

Premises used: Nat.succ_le_succ_iff
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' l₁ l₂ : List α
a : α
h : l₁ <+ l₂
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 : ℕ)
n : ℕ
⊢ LE.le (α := ℕ) ((fun (ix : ℕ) ↦ if ix = 0 then 0 else Nat.succ ((f : (a : ℕ) → ℕ) ix.pred)) (n + 1))
      ((fun (ix : ℕ) ↦ if ix = 0 then 0 else Nat.succ ((f : (a : ℕ) → ℕ) ix.pred)) 0) ↔
    n + 1 ≤ 0

Tactic:
simp [Nat.succ_le_succ_iff]

Premises used: Nat.succ_le_succ_iff
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' l₁ l₂ : List α
a : α
h : l₁ <+ l₂
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 : ℕ)
n n_1 : ℕ
⊢ LE.le (α := ℕ) ((fun (ix : ℕ) ↦ if ix = 0 then 0 else Nat.succ ((f : (a : ℕ) → ℕ) ix.pred)) (n + 1))
      ((fun (ix : ℕ) ↦ if ix = 0 then 0 else Nat.succ ((f : (a : ℕ) → ℕ) ix.pred)) (n_1 + 1)) ↔
    n + 1 ≤ n_1 + 1

Tactic:
simp [Nat.succ_le_succ_iff]

Premises used: Nat.succ_le_succ_iff
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' l₁ l₂ : List α
a : α
h : l₁ <+ l₂
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 : ℕ)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₁) 0 =
    getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂)
      ((OrderEmbedding.ofMapLEIff (fun (ix : ℕ) ↦ if ix = 0 then 0 else Nat.succ ((f : (a : ℕ) → ℕ) ix.pred)) ⋯ :
            (a : ℕ) → ℕ)
          0 :
        ℕ)

Tactic:
simp
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' l₁ l₂ : List α
a : α
h : l₁ <+ l₂
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 : ℕ)
n : ℕ
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₁) (n + 1) =
    getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂)
      ((OrderEmbedding.ofMapLEIff (fun (ix : ℕ) ↦ if ix = 0 then 0 else Nat.succ ((f : (a : ℕ) → ℕ) ix.pred)) ⋯ :
            (a : ℕ) → ℕ)
          (n + 1) :
        ℕ)

Tactic:
simpa using hf _
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
H : l <+ l'
mp :
  ∃ (f : ℕ ↪o ℕ),
    ∀ (ix : ℕ),
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] ix =
        getElem? (coll := List α) (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) []
          ((f : (a : ℕ) → ℕ) ix : ℕ)
mp₁ :
  ∀ {l₁ l₂ : List α} (a : α),
    l₁ <+ l₂ →
      ∀
        (IH :
          ∃ (f : ℕ ↪o ℕ),
            ∀ (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 : ℕ)),
        ∃ (f : ℕ ↪o ℕ),
          ∀ (ix : ℕ),
            getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ ix =
              getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂)
                ((f : (a : ℕ) → ℕ) ix : ℕ)
mp₂ :
  ∀ {l₁ l₂ : List α} (a : α),
    l₁ <+ l₂ →
      ∀
        (IH :
          ∃ (f : ℕ ↪o ℕ),
            ∀ (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 : ℕ)),
        ∃ (f : ℕ ↪o ℕ),
          ∀ (ix : ℕ),
            getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₁) ix =
              getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂)
                ((f : (a : ℕ) → ℕ) ix : ℕ)
⊢ ∃ (f : ℕ ↪o ℕ),
    ∀ (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 : ℕ)

Tactic:
induction H with
    | slnil => simp
    | cons _ _ IH =>
      obtain ⟨f, hf⟩ := IH
      refine ⟨f.trans (OrderEmbedding.ofStrictMono (· + 1) fun _ => by simp), ?_⟩
      simpa using hf
    | cons_cons _ _ IH =>
      obtain ⟨f, hf⟩ := IH
      refine
        ⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) ?_, ?_⟩
      · rintro ⟨_ | a⟩ ⟨_ | b⟩ <;> simp [Nat.succ_le_succ_iff]
      · rintro ⟨_ | i⟩
        · simp
        · simpa using hf _

Premises used: List.cons, Nat.succ_le_succ_iff
-- 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 : ℕ)
⊢ l <+ l'

Tactic:
sublist_of_orderEmbedding_getElem?_eq f hf

Premises used: List.sublist_of_orderEmbedding_getElem?_eq
-- 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 : ℕ)
⊢ l <+ l'

Tactic:
exact sublist_of_orderEmbedding_getElem?_eq f hf

Premises used: List.sublist_of_orderEmbedding_getElem?_eq
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
rw :
  (∃ (f : ℕ ↪o ℕ),
      ∀ (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 : ℕ)) ↔
    ∃ (f : Fin l.length ↪o Fin l'.length),
      ∀ (ix : Fin l.length), l.get ix = l'.get ((f : (a : Fin l.length) → Fin l'.length) ix)
⊢ l <+ l' ↔
    ∃ (f : Fin l.length ↪o Fin l'.length),
      ∀ (ix : Fin l.length), l.get ix = l'.get ((f : (a : Fin l.length) → Fin l'.length) ix)

Tactic:
rw [sublist_iff_exists_orderEmbedding_getElem?_eq]

Premises used: List.sublist_iff_exists_orderEmbedding_getElem?_eq
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
mp :
  (∃ (f : ℕ ↪o ℕ),
      ∀ (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 : ℕ)) →
    ∃ (f : Fin l.length ↪o Fin l'.length),
      ∀ (ix : Fin l.length), l.get ix = l'.get ((f : (a : Fin l.length) → Fin l'.length) ix)
mpr :
  (∃ (f : Fin l.length ↪o Fin l'.length),
      ∀ (ix : Fin l.length), l.get ix = l'.get ((f : (a : Fin l.length) → Fin l'.length) ix)) →
    ∃ (f : ℕ ↪o ℕ),
      ∀ (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 : ℕ)
⊢ (∃ (f : ℕ ↪o ℕ),
      ∀ (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 : ℕ)) ↔
    ∃ (f : Fin l.length ↪o Fin l'.length),
      ∀ (ix : Fin l.length), l.get ix = l'.get ((f : (a : Fin l.length) → Fin l'.length) ix)

Tactic:
constructor
-- 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 : ℕ)
i : ℕ
hi : i < l.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i =
    getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) i : ℕ)

Tactic:
specialize hf i
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < l.length
hf :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i =
    getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) i : ℕ)
⊢ ∃ (h : (f : (a : ℕ) → ℕ) i < l'.length),
    getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) i : ℕ) h =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi

Tactic:
rw [getElem?_eq_getElem hi, eq_comm, getElem?_eq_some_iff] at hf

Premises used: List.getElem?_eq_some_iff, eq_comm, List.getElem?_eq_getElem
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < l.length
hf :
  ∃ (h : (f : (a : ℕ) → ℕ) i < l'.length),
    getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l' ((f : (a : ℕ) → ℕ) i : ℕ) h =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
⊢ (f : (a : ℕ) → ℕ) i < l'.length

Tactic:
obtain ⟨h, -⟩ := hf
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < l.length
h : (f : (a : ℕ) → ℕ) i < l'.length
⊢ (f : (a : ℕ) → ℕ) i < l'.length

Tactic:
h