awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ)
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 : ℕ)))
    ⋯
⊢ hd :: tl <+ l'
have 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 : ℕ)
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
-- 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 : ℕ)))
    ⋯
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 : ℕ)
⊢ hd :: tl <+ l'
have cons : [hd] ++ tl <+
  take (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l' ++
    drop (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l'
Tactic: rw [← List.take_append_drop (f 0 + 1) l', ← List.singleton_append]
-- 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 : ℕ)))
    ⋯
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 : ℕ)
⊢ [hd] ++ tl <+
    take (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l' ++
      drop (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l'
have apply : [hd] <+ take (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l'
Tactic: apply List.Sublist.append _ (IH _ 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
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 : ℕ)
⊢ [hd] <+ take (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l'
have rw : getElem (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (Nat.succ ((f : (a : ℕ) → ℕ) 0)) l')
    ((f : (a : ℕ) → ℕ) 0 : ℕ) sorry ∈
  take (HAdd.hAdd (α := ℕ) (β := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)) l'
Tactic: rw [List.singleton_sublist, ← h, l'.getElem_take' _ (Nat.lt_succ_self _)]
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
Goal:
α : Type u_1
l l' : List α
⊢ 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 : ℕ)
have 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 : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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 : ℕ)
⊢ 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 : ℕ)
have 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'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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 : ℕ)
⊢ ∃ (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 : ℕ)
have 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 : ℕ)
Tactic: obtain ⟨f, hf⟩ := IH
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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) l₁ ix =
        getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l₂) ((f : (a : ℕ) → ℕ) ix : ℕ)
have 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) sorry) :
            (a : ℕ) → ℕ)
          ix :
        ℕ)
Tactic: refine ⟨f.trans (OrderEmbedding.ofStrictMono (· + 1) fun _ => by simp), ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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 : ℕ)
⊢ ∃ (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 : ℕ)
have 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 : ℕ)
Tactic: obtain ⟨f, hf⟩ := IH
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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 : ℕ)
have 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
Tactic: refine
        ⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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
⊢ ∃ (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 : ℕ)
have 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)) sorry :
            (a : ℕ) → ℕ)
          ix :
        ℕ)
Tactic: refine
        ⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
Goal:
α : Type u_1
l l' : List α
H : 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 : ℕ)
have 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 : ℕ)
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 _
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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 : ℕ)
⊢ ∃ (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 : ℕ)
have 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 : ℕ)
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 _
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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 : ℕ)
⊢ ∃ (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 : ℕ)
have 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 : ℕ)
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 _
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
Goal:
α : Type u_1
l l' : List α
⊢ 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)
have 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)
Tactic: rw [sublist_iff_exists_orderEmbedding_getElem?_eq]
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
Goal:
α : Type u_1
l l' : List α
⊢ (∃ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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)
⊢ (∃ (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)
have 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 : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (hypothesis)
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
⊢ (f : (a : ℕ) → ℕ) i < l'.length
have 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 : ℕ)
Tactic: specialize hf i
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (hypothesis)
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 : ℕ)
⊢ (f : (a : ℕ) → ℕ) i < l'.length
have 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
Tactic: rw [getElem?_eq_getElem hi, eq_comm, getElem?_eq_some_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (hypothesis)
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 : ℕ)
⊢ ∃ (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)
have h : ∀ {i : ℕ}, i < l.length → (f : (a : ℕ) → ℕ) i < l'.length
Tactic: have h : ∀ {i : ℕ}, i < l.length → f i < l'.length := by
      intro i hi
      specialize hf i
      rw [getElem?_eq_getElem hi, eq_comm, getElem?_eq_some_iff] at hf
      obtain ⟨h, -⟩ := hf
      exact h
-- 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 : ℕ)
h : ∀ {i : ℕ}, i < l.length → (f : (a : ℕ) → ℕ) i < l'.length
⊢ ∃ (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)
have mp : ∀ (a b : Fin l.length),
  LE.le (α := Fin l'.length) ((fun (ix : Fin l.length) ↦ (⟨(f : (a : ℕ) → ℕ) (↑ix : ℕ), sorry⟩ : Fin l'.length)) a)
      ((fun (ix : Fin l.length) ↦ (⟨(f : (a : ℕ) → ℕ) (↑ix : ℕ), sorry⟩ : Fin l'.length)) b) ↔
    a ≤ b
Tactic: refine ⟨OrderEmbedding.ofMapLEIff (fun ix => ⟨f ix, h ix.is_lt⟩) ?_, ?_⟩