awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ ∃ (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₁ : ∀ (ix : Fin l.length),
  l.get ix =
    l'.get
      ((OrderEmbedding.ofMapLEIff (fun (ix : Fin l.length) ↦ ⟨(f : (a : ℕ) → ℕ) (↑ix : ℕ), sorry⟩) sorry :
          (a : Fin l.length) → Fin l'.length)
        ix)
Tactic: refine ⟨OrderEmbedding.ofMapLEIff (fun ix => ⟨f ix, h ix.is_lt⟩) ?_, ?_⟩
-- 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
i : Fin l.length
⊢ l.get i =
    l'.get
      ((OrderEmbedding.ofMapLEIff (fun (ix : Fin l.length) ↦ ⟨(f : (a : ℕ) → ℕ) (↑ix : ℕ), ⋯⟩) ⋯ :
          (a : Fin l.length) → Fin l'.length)
        i)
have mp : some (l.get i) =
  some
    (l'.get
      ((OrderEmbedding.ofMapLEIff (fun (ix : Fin l.length) ↦ ⟨(f : (a : ℕ) → ℕ) (↑ix : ℕ), sorry⟩) sorry :
          (a : Fin l.length) → Fin l'.length)
        i))
Tactic: apply Option.some_injective
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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 : ℕ)
have mpr : StrictMono (β := ℕ) fun (i : ℕ) ↦
  if hi : i < l.length then (↑((f : (a : Fin l.length) → Fin l'.length) ⟨i, hi⟩) : ℕ) else i + l'.length
Tactic: refine
      ⟨OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then f ⟨i, hi⟩ else i + l'.length)
          ?_,
        ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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
⊢ ∃ (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₁ : ∀ (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)
              sorry :
            (a : ℕ) → ℕ)
          ix :
        ℕ)
Tactic: refine
      ⟨OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then f ⟨i, hi⟩ else i + l'.length)
          ?_,
        ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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
⊢ 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)
have 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⟩) : ℕ)
Tactic: split_ifs with hi hj hj
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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⟩) : ℕ)
⊢ 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)
have 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
Tactic: split_ifs with hi hj hj
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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
⊢ 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)
have pos₁ : ∀ (hi : ¬i < l.length) (hj : j < l.length), i + l'.length < (↑((f : (a : Fin l.length) → Fin l'.length) ⟨j, hj⟩) : ℕ)
Tactic: split_ifs with hi hj hj
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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⟩) : ℕ)
⊢ 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)
have neg₁ : ∀ (hi : ¬i < l.length) (hj : ¬j < l.length), i + l'.length < j + l'.length
Tactic: split_ifs with hi hj hj
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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)) : ℕ) <
    (↑((f : (a : Fin l.length) → Fin l'.length) ⟨j, hj⟩) : ℕ)
have 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)
Tactic: rwa [Fin.val_fin_lt, f.lt_iff_lt]
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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)
⊢ (↑((f : (a : Fin l.length) → Fin l'.length) (⟨i, hi⟩ : Fin l.length)) : ℕ) <
    (↑((f : (a : Fin l.length) → Fin l'.length) ⟨j, hj⟩) : ℕ)
have pos₁ : (⟨i, hi⟩ : Fin l.length) < ⟨j, hj⟩
Tactic: rwa [Fin.val_fin_lt, f.lt_iff_lt]
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
Goal:
α : Type u_1
l : List α
x : α
⊢ Duplicate x l ↔ ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m
have 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
Tactic: rw [duplicate_iff_two_le_count, ← replicate_sublist_iff,
      sublist_iff_exists_fin_orderEmbedding_get_eq]
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
Goal:
α : Type u_1
l : List α
x : α
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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
⊢ (∃ (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
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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)
⊢ ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m
have mp : x = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ⟨0, sorry⟩) ∧
  x = l.get ((f : (a : Fin (replicate 2 x).length) → Fin l.length) ⟨1, sorry⟩)
Tactic: refine ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩, f.lt_iff_lt.2 (Nat.zero_lt_one), ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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 = 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, ⋯⟩)
have mp : x = (replicate 2 x).get ⟨0, sorry⟩ ∧ x = (replicate 2 x).get ⟨1, sorry⟩
Tactic: rw [← hf, ← hf]
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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)
have mpr : StrictMono (β := Fin l.length) fun (i : Fin (replicate 2 x).length) ↦ if (↑i : ℕ) = 0 then n else m
Tactic: refine ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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
⊢ ∃ (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)
have 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) sorry :
          (a : Fin (replicate 2 x).length) → Fin l.length)
        ix)
Tactic: refine ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (hypothesis)
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 + 1, hi⟩ : Fin (replicate 2 x).length) < ⟨n_2 + 1, 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) ⟨n_2 + 1, hj⟩)
have hi₁ : n_1 = 0
Tactic: simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (hypothesis)
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_1 + 1, hi⟩ : Fin (replicate 2 x).length) < ⟨n_2 + 1, 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) ⟨n_2 + 1, hj⟩)
have hj₁ : n_2 = 0
Tactic: simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
Goal:
α : Type u_1
l : List α
x : α
⊢ Duplicate x l ↔ ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m
have 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
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'
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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
⊢ Duplicate x l ↔ ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m
have 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
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'
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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
⊢ Duplicate x l ↔ ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m
have 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
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'
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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
⊢ Duplicate x l ↔ ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m
have 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
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'
-- Lean 4 proof step from Mathlib.Data.List.NodupEquivFin (goal)
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
⊢ Duplicate x l ↔ ∃ (n : Fin l.length), ∃ (m : Fin l.length), ∃ (x_1 : n < m), x = l.get n ∧ x = l.get m
have 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)
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'
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ (ofFn f).get i = f (Fin.cast ⋯ i)
have simp : f (⟨(↑i : ℕ), sorry⟩ : Fin n) = f (Fin.cast sorry i)
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m n : ℕ
h : m = n
f : Fin m → α
⊢ ofFn f = ofFn (n := n) fun (i : Fin n) ↦ f (Fin.cast ⋯ i)
have subst : ofFn f = ofFn (n := m) fun (i : Fin m) ↦ f (Fin.cast sorry i)
Tactic: subst h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
m : ℕ
f : Fin m → α
⊢ ofFn f = ofFn (n := m) fun (i : Fin m) ↦ f (Fin.cast ⋯ i)
have simp_rw : ofFn f = ofFn (n := m) fun (i : Fin m) ↦ f (id i)
Tactic: simp_rw [Fin.cast_refl, id]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
f : Fin (succ 0) → α
⊢ ofFn f = concat (ofFn (n := 0) fun (i : Fin 0) ↦ f i.castSucc) (f (Fin.last 0))
have zero : ofFn f = concat [] (f (Fin.last 0))
Tactic: rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero, Fin.last_zero]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
f : Fin (succ 0) → α
zero : ofFn f = concat [] (f (Fin.last 0))
⊢ ofFn f = concat (ofFn (n := 0) fun (i : Fin 0) ↦ f i.castSucc) (f (Fin.last 0))
have zero₁ : ofFn f = [f (Fin.last 0)]
Tactic: rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero, Fin.last_zero]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
Goal:
α : Type u
f : Fin (succ 0) → α
zero : ofFn f = concat [] (f (Fin.last 0))
zero₁ : ofFn f = [f (Fin.last 0)]
⊢ ofFn f = concat (ofFn (n := 0) fun (i : Fin 0) ↦ f i.castSucc) (f (Fin.last 0))
have zero₂ : (f 0 :: ofFn (n := 0) fun (i : Fin 0) ↦ f i.succ) = [f (Fin.last 0)]
Tactic: rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero, Fin.last_zero]
-- Lean 4 proof step from Mathlib.Data.List.OfFn (goal)
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)]
⊢ ofFn f = concat (ofFn (n := 0) fun (i : Fin 0) ↦ f i.castSucc) (f (Fin.last 0))
have zero₃ : [f 0] = [f (Fin.last 0)]
Tactic: rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero, Fin.last_zero]