-- Mathlib/Data/List/NodupEquivFin.lean
theorem duplicate_iff_exists_distinct_get {l : List α} {x : α} :
    l.Duplicate x ↔
      ∃ (n m : Fin l.length) (_ : n < m),
        x = l.get n ∧ x = l.get m

Proof state:
case mpr
α : Type u_1
l : List α
x : α
⊢ (∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m) →
    ∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)

Tactic:
rintro ⟨n, m, hnm, h, h'⟩

Result:
case mpr.intro.intro.intro.intro
α : 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, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)

Proof state:
case mp.intro
α : 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 ix)
⊢ x = (replicate 2 x).get ⟨0, ⋯⟩ ∧ x = (replicate 2 x).get ⟨1, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
case mp
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)) →
    ∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m

Tactic:
rintro ⟨f, hf⟩

Result:
case mp.intro
α : 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 ix)
⊢ ∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m

Proof state:
case mpr.intro.intro.intro.intro.refine_2.mk.succ
α : 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✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
⊢ (replicate 2 x).get ⟨n✝ + 1, hi⟩ =
    l.get ((OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m) ⋯) ⟨n✝ + 1, hi⟩)

Tactic:
simpa using h'

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.refine_2
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ ∀ (ix : Fin (replicate 2 x).length),
    (replicate 2 x).get ix = l.get ((OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m) ⋯) ix)

Tactic:
rintro ⟨⟨_ | i⟩, hi⟩

Result:
case mpr.intro.intro.intro.intro.refine_2.mk.zero
α : 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⟩ = l.get ((OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m) ⋯) ⟨0, hi⟩)

case mpr.intro.intro.intro.intro.refine_2.mk.succ
α : 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✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
⊢ (replicate 2 x).get ⟨n✝ + 1, hi⟩ =
    l.get ((OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m) ⋯) ⟨n✝ + 1, hi⟩)

Proof state:
α : 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 ix)
⊢ 1 < (replicate 2 x).length

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.refine_1.mk.zero.mk.succ
α : 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✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨n✝ + 1, hj⟩ → (fun i => if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i => if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

Tactic:
simp [hnm]

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.refine_1.mk.succ.mk.succ
α : 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✝¹ : ℕ
hi✝ : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj✝ : n✝ + 1 < (replicate 2 x).length
hi : n✝¹ = 0
hj : n✝ = 0
⊢ ⟨n✝¹ + 1, hi✝⟩ < ⟨n✝ + 1, hj✝⟩ →
    (fun i => if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi✝⟩ < (fun i => if ↑i = 0 then n else m) ⟨n✝ + 1, hj✝⟩

Tactic:
simp [hi, hj]

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.refine_1.mk.succ.mk.zero
α : 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✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
hj : 0 < (replicate 2 x).length
⊢ ⟨n✝ + 1, hi⟩ < ⟨0, hj⟩ → (fun i => if ↑i = 0 then n else m) ⟨n✝ + 1, hi⟩ < (fun i => if ↑i = 0 then n else m) ⟨0, hj⟩

Tactic:
simp

Result:
no goals

Proof state:
case mp.intro
α : 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 ix)
⊢ ∃ n m, ∃ (_ : 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), ?_⟩

Result:
case mp.intro
α : 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 ix)
⊢ x = l.get (f ⟨0, ⋯⟩) ∧ x = l.get (f ⟨1, ⋯⟩)

Proof state:
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)) ↔
    ∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m

Tactic:
constructor

Result:
case mp
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)) →
    ∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m

case mpr
α : Type u_1
l : List α
x : α
⊢ (∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m) →
    ∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)

Proof state:
case mpr.intro.intro.intro.intro.refine_1
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ StrictMono fun i => if ↑i = 0 then n else m

Tactic:
rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩

Result:
case mpr.intro.intro.intro.intro.refine_1.mk.zero.mk.zero
α : 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⟩ < ⟨0, hj⟩ → (fun i => if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i => if ↑i = 0 then n else m) ⟨0, hj⟩

case mpr.intro.intro.intro.intro.refine_1.mk.zero.mk.succ
α : 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✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨n✝ + 1, hj⟩ → (fun i => if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i => if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

case mpr.intro.intro.intro.intro.refine_1.mk.succ.mk.zero
α : 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✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
hj : 0 < (replicate 2 x).length
⊢ ⟨n✝ + 1, hi⟩ < ⟨0, hj⟩ → (fun i => if ↑i = 0 then n else m) ⟨n✝ + 1, hi⟩ < (fun i => if ↑i = 0 then n else m) ⟨0, hj⟩

case mpr.intro.intro.intro.intro.refine_1.mk.succ.mk.succ
α : 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✝¹ : ℕ
hi : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i => if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i => if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

Proof state:
case mpr.intro.intro.intro.intro.refine_2.mk.zero
α : 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⟩ = l.get ((OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m) ⋯) ⟨0, hi⟩)

Tactic:
simpa using h

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.refine_1.mk.zero.mk.zero
α : 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⟩ < ⟨0, hj⟩ → (fun i => if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i => if ↑i = 0 then n else m) ⟨0, hj⟩

Tactic:
simp

Result:
no goals

Proof state:
α : 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 ix)
⊢ 0 < (replicate 2 x).length

Tactic:
simp

Result:
no goals