awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact h
-- 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 : ℕ}, 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
-- 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 : ℕ)
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)

Tactic:
⟨OrderEmbedding.ofMapLEIff (fun ix => ⟨f ix, h ix.is_lt⟩) ?_, ?_⟩

Premises used: Fin.mk, Fin.is_lt, Fin.val, Exists.intro, OrderEmbedding.ofMapLEIff, DFunLike.coe
-- 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 : ℕ)
h : ∀ {i : ℕ}, i < l.length → (f : (a : ℕ) → ℕ) i < l'.length
mp :
  ∀ (a b : Fin l.length),
    LE.le (α := Fin l'.length) ((fun (ix : Fin l.length) ↦ (⟨(f : (a : ℕ) → ℕ) (↑ix : ℕ), ⋯⟩ : Fin l'.length)) a)
        ((fun (ix : Fin l.length) ↦ (⟨(f : (a : ℕ) → ℕ) (↑ix : ℕ), ⋯⟩ : Fin l'.length)) b) ↔
      a ≤ b
mp₁ :
  ∀ (ix : Fin l.length),
    l.get ix =
      l'.get
        ((OrderEmbedding.ofMapLEIff (fun (ix : Fin l.length) ↦ ⟨(f : (a : ℕ) → ℕ) (↑ix : ℕ), ⋯⟩) ⋯ :
            (a : Fin l.length) → Fin l'.length)
          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:
refine ⟨OrderEmbedding.ofMapLEIff (fun ix => ⟨f ix, h ix.is_lt⟩) ?_, ?_⟩
-- 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 : ℕ)
h : ∀ {i : ℕ}, i < l.length → (f : (a : ℕ) → ℕ) i < l'.length
⊢ ∀ (a b : Fin l.length),
    LE.le (α := Fin l'.length) ((fun (ix : Fin l.length) ↦ (⟨(f : (a : ℕ) → ℕ) (↑ix : ℕ), ⋯⟩ : Fin l'.length)) a)
        ((fun (ix : Fin l.length) ↦ (⟨(f : (a : ℕ) → ℕ) (↑ix : ℕ), ⋯⟩ : Fin l'.length)) b) ↔
      a ≤ b

Tactic:
simp
-- 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 : ℕ)
h : ∀ {i : ℕ}, i < l.length → (f : (a : ℕ) → ℕ) i < l'.length
i : Fin l.length
mp :
  some (l.get i) =
    some
      (l'.get
        ((OrderEmbedding.ofMapLEIff (fun (ix : Fin l.length) ↦ ⟨(f : (a : ℕ) → ℕ) (↑ix : ℕ), ⋯⟩) ⋯ :
            (a : Fin l.length) → Fin l'.length)
          i))
⊢ l.get i =
    l'.get
      ((OrderEmbedding.ofMapLEIff (fun (ix : Fin l.length) ↦ ⟨(f : (a : ℕ) → ℕ) (↑ix : ℕ), ⋯⟩) ⋯ :
          (a : Fin l.length) → Fin l'.length)
        i)

Tactic:
apply Option.some_injective

Premises used: Option.some_injective
-- 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 : ℕ)
h : ∀ {i : ℕ}, i < l.length → (f : (a : ℕ) → ℕ) i < l'.length
i : Fin l.length
⊢ some (l.get i) =
    some
      (l'.get
        ((OrderEmbedding.ofMapLEIff (fun (ix : Fin l.length) ↦ ⟨(f : (a : ℕ) → ℕ) (↑ix : ℕ), ⋯⟩) ⋯ :
            (a : Fin l.length) → Fin l'.length)
          i))

Tactic:
simpa [getElem?_eq_getElem i.2, getElem?_eq_getElem (h i.2)] using hf i

Premises used: Fin.isLt, Fin.val, List.getElem?_eq_getElem
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (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:
⟨OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then f ⟨i, hi⟩ else i + l'.length)
          ?_,
        ?_⟩

Premises used: Fin.mk, Fin.val, dite, OrderEmbedding.ofStrictMono, HAdd.hAdd, LT.lt, Exists.intro, List.length, DFunLike.coe
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get ((f : (a : Fin l.length) → Fin l'.length) ix)
mpr :
  StrictMono (β := ℕ) fun (i : ℕ) ↦
    if hi : i < l.length then (↑((f : (a : Fin l.length) → Fin l'.length) ⟨i, hi⟩) : ℕ) else i + l'.length
mpr₁ :
  ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l'
        ((OrderEmbedding.ofStrictMono
                (fun (i : ℕ) ↦
                  if hi : i < l.length then (↑((f : (a : Fin l.length) → Fin l'.length) ⟨i, hi⟩) : ℕ)
                  else i + l'.length)
                ⋯ :
              (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:
refine
      ⟨OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then f ⟨i, hi⟩ else i + l'.length)
          ?_,
        ?_⟩
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get ((f : (a : Fin l.length) → Fin l'.length) ix)
i j : ℕ
h : i < j
pos :
  ∀ (hi : i < l.length) (hj : j < l.length),
    (↑((f : (a : Fin l.length) → Fin l'.length) (⟨i, hi⟩ : Fin l.length)) : ℕ) <
      (↑((f : (a : Fin l.length) → Fin l'.length) ⟨j, hj⟩) : ℕ)
neg :
  ∀ (hi : i < l.length) (hj : ¬j < l.length),
    (↑((f : (a : Fin l.length) → Fin l'.length) (⟨i, hi⟩ : Fin l.length)) : ℕ) < j + l'.length
pos₁ :
  ∀ (hi : ¬i < l.length) (hj : j < l.length), i + l'.length < (↑((f : (a : Fin l.length) → Fin l'.length) ⟨j, hj⟩) : ℕ)
neg₁ : ∀ (hi : ¬i < l.length) (hj : ¬j < l.length), i + l'.length < j + l'.length
⊢ LT.lt (α := ℕ)
    (if hi : i < l.length then (↑((f : (a : Fin l.length) → Fin l'.length) ⟨i, hi⟩) : ℕ) else i + l'.length)
    (if hi : j < l.length then (↑((f : (a : Fin l.length) → Fin l'.length) ⟨j, hi⟩) : ℕ) else j + l'.length)

Tactic:
split_ifs with hi hj hj
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get ((f : (a : Fin l.length) → Fin l'.length) ix)
i j : ℕ
h : i < j
hi : i < l.length
hj : j < l.length
pos :
  LT.lt (α := Fin l'.length) ((f : (a : Fin l.length) → Fin l'.length) ⟨i, hi⟩ : Fin l'.length)
    ((f : (a : Fin l.length) → Fin l'.length) ⟨j, hj⟩ : Fin l'.length)
pos₁ pos₂ pos₃ pos₄ : (⟨i, hi⟩ : Fin l.length) < ⟨j, hj⟩
⊢ (↑((f : (a : Fin l.length) → Fin l'.length) (⟨i, hi⟩ : Fin l.length)) : ℕ) <
    (↑((f : (a : Fin l.length) → Fin l'.length) ⟨j, hj⟩) : ℕ)

Tactic:
rwa [Fin.val_fin_lt, f.lt_iff_lt]

Premises used: Fin.val_fin_lt, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get ((f : (a : Fin l.length) → Fin l'.length) ix)
i j : ℕ
h : i < j
hi : i < l.length
hj : ¬j < l.length
⊢ (↑((f : (a : Fin l.length) → Fin l'.length) (⟨i, hi⟩ : Fin l.length)) : ℕ) < j + l'.length

Tactic:
lia
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get ((f : (a : Fin l.length) → Fin l'.length) ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : j < l.length
⊢ i + l'.length < (↑((f : (a : Fin l.length) → Fin l'.length) ⟨j, hj⟩) : ℕ)

Tactic:
absurd (h.trans hj) hi

Premises used: absurd, LT.lt.trans
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get ((f : (a : Fin l.length) → Fin l'.length) ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : j < l.length
⊢ i + l'.length < (↑((f : (a : Fin l.length) → Fin l'.length) ⟨j, hj⟩) : ℕ)

Tactic:
exact absurd (h.trans hj) hi

Premises used: absurd, LT.lt.trans
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get ((f : (a : Fin l.length) → Fin l'.length) ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : ¬j < l.length
⊢ i + l'.length < j + l'.length

Tactic:
simpa using h
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get ((f : (a : Fin l.length) → Fin l'.length) ix)
⊢ ∀ (ix : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ix =
      getElem? (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l'
        ((OrderEmbedding.ofStrictMono
                (fun (i : ℕ) ↦
                  if hi : i < l.length then (↑((f : (a : Fin l.length) → Fin l'.length) ⟨i, hi⟩) : ℕ)
                  else i + l'.length)
                ⋯ :
              (a : ℕ) → ℕ)
            ix :
          ℕ)

Tactic:
grind
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
rw :
  (∃ (f : Fin (replicate 2 x).length ↪o Fin l.length),
      ∀ (ix : Fin (replicate 2 x).length),
        (replicate 2 x).get ix = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ix)) ↔
    ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m
⊢ Duplicate x l ↔ ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m

Tactic:
rw [duplicate_iff_two_le_count, ← replicate_sublist_iff,
      sublist_iff_exists_fin_orderEmbedding_get_eq]

Premises used: List.replicate_sublist_iff, List.sublist_iff_exists_fin_orderEmbedding_get_eq, List.duplicate_iff_two_le_count
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
mp :
  (∃ (f : Fin (replicate 2 x).length ↪o Fin l.length),
      ∀ (ix : Fin (replicate 2 x).length),
        (replicate 2 x).get ix = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ix)) →
    ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m
mpr :
  (∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m) →
    ∃ (f : Fin (replicate 2 x).length ↪o Fin l.length),
      ∀ (ix : Fin (replicate 2 x).length),
        (replicate 2 x).get ix = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ix)
⊢ (∃ (f : Fin (replicate 2 x).length ↪o Fin l.length),
      ∀ (ix : Fin (replicate 2 x).length),
        (replicate 2 x).get ix = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ix)) ↔
    ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m

Tactic:
constructor
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf :
  ∀ (ix : Fin (replicate 2 x).length),
    (replicate 2 x).get ix = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ix)
⊢ 0 < (replicate 2 x).length

Tactic:
simp
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf :
  ∀ (ix : Fin (replicate 2 x).length),
    (replicate 2 x).get ix = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ix)
⊢ 1 < (replicate 2 x).length

Tactic:
simp
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf :
  ∀ (ix : Fin (replicate 2 x).length),
    (replicate 2 x).get ix = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ix)
mp :
  x = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ⟨0, ⋯⟩) ∧
    x = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ⟨1, ⋯⟩)
⊢ ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m

Tactic:
refine ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩, f.lt_iff_lt.2 (Nat.zero_lt_one), ?_⟩
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf :
  ∀ (ix : Fin (replicate 2 x).length),
    (replicate 2 x).get ix = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ix)
mp : x = (replicate 2 x).get ⟨0, ⋯⟩ ∧ x = (replicate 2 x).get ⟨1, ⋯⟩
⊢ x = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ⟨0, ⋯⟩) ∧
    x = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ⟨1, ⋯⟩)

Tactic:
rw [← hf, ← hf]
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf :
  ∀ (ix : Fin (replicate 2 x).length),
    (replicate 2 x).get ix = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ix)
⊢ x = (replicate 2 x).get ⟨0, ⋯⟩ ∧ x = (replicate 2 x).get ⟨1, ⋯⟩

Tactic:
simp
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ ∃ (f : Fin (replicate 2 x).length ↪o Fin l.length),
    ∀ (ix : Fin (replicate 2 x).length),
      (replicate 2 x).get ix = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ix)

Tactic:
⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) ?_, ?_⟩

Premises used: Fin.val, OrderEmbedding.ofStrictMono, Exists.intro, OfNat.ofNat, Eq, ite
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
mpr : StrictMono (β := Fin l.length) fun (i : Fin (replicate 2 x).length) ↦ if (↑i : ℕ) = 0 then n else m
mpr₁ :
  ∀ (ix : Fin (replicate 2 x).length),
    (replicate 2 x).get ix =
      l.get
        ((OrderEmbedding.ofStrictMono (fun (i : Fin (replicate 2 x).length) ↦ if (↑i : ℕ) = 0 then n else m) ⋯ :
            (a : Fin (replicate 2 x).length) → Fin l.length)
          ix)
⊢ ∃ (f : Fin (replicate 2 x).length ↪o Fin l.length),
    ∀ (ix : Fin (replicate 2 x).length),
      (replicate 2 x).get ix = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ix)

Tactic:
refine ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) ?_, ?_⟩
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi hj : 0 < (replicate 2 x).length
⊢ (⟨0, hi⟩ : Fin (replicate 2 x).length) < ⟨0, hj⟩ →
    LT.lt (α := Fin l.length) ((fun (i : Fin (replicate 2 x).length) ↦ if (↑i : ℕ) = 0 then n else m) ⟨0, hi⟩)
      ((fun (i : Fin (replicate 2 x).length) ↦ if (↑i : ℕ) = 0 then n else m) ⟨0, hj⟩)

Tactic:
simp
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi : 0 < (replicate 2 x).length
n_1 : ℕ
hj : n_1 + 1 < (replicate 2 x).length
⊢ (⟨0, hi⟩ : Fin (replicate 2 x).length) < ⟨n_1 + 1, hj⟩ →
    LT.lt (α := Fin l.length) ((fun (i : Fin (replicate 2 x).length) ↦ if (↑i : ℕ) = 0 then n else m) ⟨0, hi⟩)
      ((fun (i : Fin (replicate 2 x).length) ↦ if (↑i : ℕ) = 0 then n else m) ⟨n_1 + 1, hj⟩)

Tactic:
simp [hnm]
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n_1 : ℕ
hi : n_1 + 1 < (replicate 2 x).length
hj : 0 < (replicate 2 x).length
⊢ (⟨n_1 + 1, hi⟩ : Fin (replicate 2 x).length) < ⟨0, hj⟩ →
    LT.lt (α := Fin l.length) ((fun (i : Fin (replicate 2 x).length) ↦ if (↑i : ℕ) = 0 then n else m) ⟨n_1 + 1, hi⟩)
      ((fun (i : Fin (replicate 2 x).length) ↦ if (↑i : ℕ) = 0 then n else m) ⟨0, hj⟩)

Tactic:
simp
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n_1 : ℕ
hi : n_1 + 1 < (replicate 2 x).length
n_2 : ℕ
hj : n_2 + 1 < (replicate 2 x).length
⊢ n_1 = 0

Tactic:
simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj

Premises used: List.replicate, Nat.le_zero, Nat.lt_succ_iff, Nat.succ_le_succ_iff, List.length
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n_1 : ℕ
hi : n_1 + 1 < (replicate 2 x).length
n_2 : ℕ
hj : n_2 + 1 < (replicate 2 x).length
hi₁ : n_1 = 0
⊢ n_2 = 0

Tactic:
simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj

Premises used: List.replicate, Nat.le_zero, Nat.lt_succ_iff, Nat.succ_le_succ_iff, List.length
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n_1 : ℕ
hi_1 : n_1 + 1 < (replicate 2 x).length
n_2 : ℕ
hj_1 : n_2 + 1 < (replicate 2 x).length
hi : n_1 = 0
hj : n_2 = 0
⊢ (⟨n_1 + 1, hi_1⟩ : Fin (replicate 2 x).length) < ⟨n_2 + 1, hj_1⟩ →
    LT.lt (α := Fin l.length) ((fun (i : Fin (replicate 2 x).length) ↦ if (↑i : ℕ) = 0 then n else m) ⟨n_1 + 1, hi_1⟩)
      ((fun (i : Fin (replicate 2 x).length) ↦ if (↑i : ℕ) = 0 then n else m) ⟨n_2 + 1, hj_1⟩)

Tactic:
simp [hi, hj]
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi : 0 < (replicate 2 x).length
⊢ (replicate 2 x).get (⟨0, hi⟩ : Fin (replicate 2 x).length) =
    l.get
      ((OrderEmbedding.ofStrictMono (fun (i : Fin (replicate 2 x).length) ↦ if (↑i : ℕ) = 0 then n else m) ⋯ :
          (a : Fin (replicate 2 x).length) → Fin l.length)
        ⟨0, hi⟩)

Tactic:
simpa using h
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n_1 : ℕ
hi : n_1 + 1 < (replicate 2 x).length
⊢ (replicate 2 x).get (⟨n_1 + 1, hi⟩ : Fin (replicate 2 x).length) =
    l.get
      ((OrderEmbedding.ofStrictMono (fun (i : Fin (replicate 2 x).length) ↦ if (↑i : ℕ) = 0 then n else m) ⋯ :
          (a : Fin (replicate 2 x).length) → Fin l.length)
        ⟨n_1 + 1, hi⟩)

Tactic:
simpa using h'
-- Module: Mathlib.Data.List.NodupEquivFin
Goal:
α : Type u_1
l : List α
x : α
rw : 2 ≤ count x l ↔ ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m
rw₁ : replicate 2 x <+ l ↔ ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m
rw₂ rw₃ rw₄ :
  (∃ (f : Fin (replicate 2 x).length ↪o Fin l.length),
      ∀ (ix : Fin (replicate 2 x).length),
        (replicate 2 x).get ix = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ix)) ↔
    ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m
mp :
  (∃ (f : Fin (replicate 2 x).length ↪o Fin l.length),
      ∀ (ix : Fin (replicate 2 x).length),
        (replicate 2 x).get ix = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ix)) →
    ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m
mpr mpr₁ :
  (∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m) →
    ∃ (f : Fin (replicate 2 x).length ↪o Fin l.length),
      ∀ (ix : Fin (replicate 2 x).length),
        (replicate 2 x).get ix = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ix)
⊢ Duplicate x l ↔ ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m

Tactic:
classical
    rw [duplicate_iff_two_le_count, ← replicate_sublist_iff,
      sublist_iff_exists_fin_orderEmbedding_get_eq]
    constructor
    · rintro ⟨f, hf⟩
      refine ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩, f.lt_iff_lt.2 (Nat.zero_lt_one), ?_⟩
      rw [← hf, ← hf]; simp
    · rintro ⟨n, m, hnm, h, h'⟩
      refine ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) ?_, ?_⟩
      · rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩
        · simp
        · simp [hnm]
        · simp
        · simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj
          simp [hi, hj]
      · rintro ⟨⟨_ | i⟩, hi⟩
        · simpa using h
        · simpa using h'

Premises used: List.replicate, Nat.le_zero, List.replicate_sublist_iff, Nat.lt_succ_iff, Nat.succ_le_succ_iff, List.sublist_iff_exists_fin_orderEmbedding_get_eq, List.length, List.duplicate_iff_two_le_count
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ (ofFn f).length = n

Tactic:
simp
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
simp : f (⟨(↑i : ℕ), ⋯⟩ : Fin n) = f (Fin.cast ⋯ i)
⊢ (ofFn f).get i = f (Fin.cast ⋯ i)

Tactic:
simp
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ f (⟨(↑i : ℕ), ⋯⟩ : Fin n) = f (Fin.cast ⋯ i)

Tactic:
congr
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
β : Type u_1
n : ℕ
f : Fin n → α
g : α → β
⊢ (ofFn (n := n) fun (i : Fin n) ↦ g (f i)) = map g (ofFn f)

Tactic:
map_ofFn.symm

Premises used: List.map_ofFn, Eq.symm
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
m n : ℕ
h : m = n
f : Fin m → α
subst : ofFn f = ofFn (n := m) fun (i : Fin m) ↦ f (Fin.cast ⋯ i)
⊢ ofFn f = ofFn (n := n) fun (i : Fin n) ↦ f (Fin.cast ⋯ i)

Tactic:
subst h
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
m : ℕ
f : Fin m → α
simp_rw : ofFn f = ofFn (n := m) fun (i : Fin m) ↦ f (id i)
⊢ ofFn f = ofFn (n := m) fun (i : Fin m) ↦ f (Fin.cast ⋯ i)

Tactic:
simp_rw [Fin.cast_refl, id]

Premises used: id, Fin.cast_refl
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
f : Fin (succ 0) → α
zero : ofFn f = concat [] (f (Fin.last 0))
zero₁ : ofFn f = [f (Fin.last 0)]
zero₂ : (f 0 :: ofFn (n := 0) fun (i : Fin 0) ↦ f i.succ) = [f (Fin.last 0)]
zero₃ : [f 0] = [f (Fin.last 0)]
zero₄ zero₅ : [f 0] = [f 0]
⊢ ofFn f = concat (ofFn (n := 0) fun (i : Fin 0) ↦ f i.castSucc) (f (Fin.last 0))

Tactic:
rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero, Fin.last_zero]

Premises used: Fin.last_zero, List.concat_nil, List.ofFn_zero, List.ofFn_succ
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = concat (ofFn (n := n) fun (i : Fin n) ↦ f i.castSucc) (f (Fin.last n))
f : Fin (n + 1).succ → α
succ :
  f 0 :: concat (ofFn (n := n) fun (i : Fin n) ↦ f i.castSucc.succ) (f (Fin.last n.succ)) =
    f 0 :: concat (ofFn (n := n) fun (i : Fin n) ↦ f i.succ.castSucc) (f (Fin.last (n + 1)))
⊢ ofFn f = concat (ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ f i.castSucc) (f (Fin.last (n + 1)))

Tactic:
rw [ofFn_succ, IH, ofFn_succ, concat_cons, Fin.castSucc_zero, Fin.succ_last]

Premises used: List.concat_cons, Fin.castSucc_zero, Fin.succ_last, List.ofFn_succ
-- Module: Mathlib.Data.List.OfFn
Goal:
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = concat (ofFn (n := n) fun (i : Fin n) ↦ f i.castSucc) (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ f 0 :: concat (ofFn (n := n) fun (i : Fin n) ↦ f i.castSucc.succ) (f (Fin.last n.succ)) =
    f 0 :: concat (ofFn (n := n) fun (i : Fin n) ↦ f i.succ.castSucc) (f (Fin.last (n + 1)))

Tactic:
simp only [succ_eq_add_one, Fin.castSucc_succ]

Premises used: Nat.succ_eq_add_one, Fin.castSucc_succ