α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)) ↔
    ∃ n m x_1, x = get l n ∧ x = get l m
α : Type u_1
l : List α
x : α
⊢ Duplicate x l ↔ ∃ n m x_1, x = get l n ∧ x = get l m
rw [duplicate_iff_two_le_count, le_count_iff_replicate_sublist,
  sublist_iff_exists_fin_orderEmbedding_get_eq]
case mp
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)) →
    ∃ n m x_1, x = get l n ∧ x = get l m

case mpr
α : Type u_1
l : List α
x : α
⊢ (∃ n m x_1, x = get l n ∧ x = get l m) →
    ∃ f, ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)) ↔
    ∃ n m x_1, x = get l n ∧ x = get l m
constructor
case mp.intro
α : Type u_1
l : List α
x : α
f : Fin (length (replicate 2 x)) ↪o Fin (length l)
hf : ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
⊢ ∃ n m x_1, x = get l n ∧ x = get l m
case mp
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)) →
    ∃ n m x_1, x = get l n ∧ x = get l m
rintro ⟨f, hf⟩
case mp.intro
α : Type u_1
l : List α
x : α
f : Fin (length (replicate 2 x)) ↪o Fin (length l)
hf : ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
⊢ x = get l (↑f { val := 0, isLt := (_ : 0 < Nat.succ 1) }) ∧ x = get l (↑f { val := 1, isLt := (_ : 1 < Nat.succ 1) })
case mp.intro
α : Type u_1
l : List α
x : α
f : Fin (length (replicate 2 x)) ↪o Fin (length l)
hf : ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
⊢ ∃ n m x_1, x = get l n ∧ x = get l m
refine' ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩,
  f.lt_iff_lt.2 (show (0 : ℕ) < 1 from zero_lt_one), _⟩
no goals
α : Type u_1
l : List α
x : α
f : Fin (length (replicate 2 x)) ↪o Fin (length l)
hf : ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
⊢ 0 < length (replicate 2 x)
simp
no goals
α : Type u_1
l : List α
x : α
f : Fin (length (replicate 2 x)) ↪o Fin (length l)
hf : ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
⊢ 1 < length (replicate 2 x)
simp
case mp.intro
α : Type u_1
l : List α
x : α
f : Fin (length (replicate 2 x)) ↪o Fin (length l)
hf : ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
⊢ x = get (replicate 2 x) { val := 0, isLt := (_ : 0 < Nat.succ 1) } ∧
    x = get (replicate 2 x) { val := 1, isLt := (_ : 1 < Nat.succ 1) }
case mp.intro
α : Type u_1
l : List α
x : α
f : Fin (length (replicate 2 x)) ↪o Fin (length l)
hf : ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
⊢ x = get l (↑f { val := 0, isLt := (_ : 0 < Nat.succ 1) }) ∧ x = get l (↑f { val := 1, isLt := (_ : 1 < Nat.succ 1) })
rw [← hf, ← hf]
no goals
case mp.intro
α : Type u_1
l : List α
x : α
f : Fin (length (replicate 2 x)) ↪o Fin (length l)
hf : ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
⊢ x = get (replicate 2 x) { val := 0, isLt := (_ : 0 < Nat.succ 1) } ∧
    x = get (replicate 2 x) { val := 1, isLt := (_ : 1 < Nat.succ 1) }
simp
case mpr.intro.intro.intro.intro
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
⊢ ∃ f, ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
case mpr
α : Type u_1
l : List α
x : α
⊢ (∃ n m x_1, x = get l n ∧ x = get l m) →
    ∃ f, ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
rintro ⟨n, m, hnm, h, h'⟩
case mpr.intro.intro.intro.intro.refine'_1
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
⊢ StrictMono fun i => if ↑i = 0 then n else m

case mpr.intro.intro.intro.intro.refine'_2
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
⊢ ∀ (ix : Fin (length (replicate 2 x))),
    get (replicate 2 x) ix =
      get l
        (↑(OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m) ?mpr.intro.intro.intro.intro.refine'_1) ix)
case mpr.intro.intro.intro.intro
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
⊢ ∃ f, ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
refine' ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) _, _⟩
case mpr.intro.intro.intro.intro.refine'_1.mk.zero.mk.zero
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
hi hj : Nat.zero < length (replicate 2 x)
⊢ { val := Nat.zero, isLt := hi } < { val := Nat.zero, isLt := hj } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.zero, isLt := hi } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.zero, isLt := hj }

case mpr.intro.intro.intro.intro.refine'_1.mk.zero.mk.succ
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
hi : Nat.zero < length (replicate 2 x)
n✝ : ℕ
hj : Nat.succ n✝ < length (replicate 2 x)
⊢ { val := Nat.zero, isLt := hi } < { val := Nat.succ n✝, isLt := hj } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.zero, isLt := hi } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝, isLt := hj }

case mpr.intro.intro.intro.intro.refine'_1.mk.succ.mk.zero
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
n✝ : ℕ
hi : Nat.succ n✝ < length (replicate 2 x)
hj : Nat.zero < length (replicate 2 x)
⊢ { val := Nat.succ n✝, isLt := hi } < { val := Nat.zero, isLt := hj } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝, isLt := hi } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.zero, isLt := hj }

case mpr.intro.intro.intro.intro.refine'_1.mk.succ.mk.succ
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
n✝¹ : ℕ
hi : Nat.succ n✝¹ < length (replicate 2 x)
n✝ : ℕ
hj : Nat.succ n✝ < length (replicate 2 x)
⊢ { val := Nat.succ n✝¹, isLt := hi } < { val := Nat.succ n✝, isLt := hj } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝¹, isLt := hi } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝, isLt := hj }
case mpr.intro.intro.intro.intro.refine'_1
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
⊢ StrictMono fun i => if ↑i = 0 then n else m
rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩
no goals
case mpr.intro.intro.intro.intro.refine'_1.mk.zero.mk.zero
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
hi hj : Nat.zero < length (replicate 2 x)
⊢ { val := Nat.zero, isLt := hi } < { val := Nat.zero, isLt := hj } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.zero, isLt := hi } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.zero, isLt := hj }
simp
no goals
case mpr.intro.intro.intro.intro.refine'_1.mk.zero.mk.succ
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
hi : Nat.zero < length (replicate 2 x)
n✝ : ℕ
hj : Nat.succ n✝ < length (replicate 2 x)
⊢ { val := Nat.zero, isLt := hi } < { val := Nat.succ n✝, isLt := hj } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.zero, isLt := hi } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝, isLt := hj }
simp [hnm]
no goals
case mpr.intro.intro.intro.intro.refine'_1.mk.succ.mk.zero
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
n✝ : ℕ
hi : Nat.succ n✝ < length (replicate 2 x)
hj : Nat.zero < length (replicate 2 x)
⊢ { val := Nat.succ n✝, isLt := hi } < { val := Nat.zero, isLt := hj } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝, isLt := hi } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.zero, isLt := hj }
simp
case mpr.intro.intro.intro.intro.refine'_1.mk.succ.mk.succ
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
n✝¹ : ℕ
hi✝ : Nat.succ n✝¹ < length (replicate 2 x)
n✝ : ℕ
hj✝ : Nat.succ n✝ < length (replicate 2 x)
hi : n✝¹ = 0
hj : n✝ = 0
⊢ { val := Nat.succ n✝¹, isLt := hi✝ } < { val := Nat.succ n✝, isLt := hj✝ } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝¹, isLt := hi✝ } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝, isLt := hj✝ }
case mpr.intro.intro.intro.intro.refine'_1.mk.succ.mk.succ
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
n✝¹ : ℕ
hi : Nat.succ n✝¹ < length (replicate 2 x)
n✝ : ℕ
hj : Nat.succ n✝ < length (replicate 2 x)
⊢ { val := Nat.succ n✝¹, isLt := hi } < { val := Nat.succ n✝, isLt := hj } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝¹, isLt := hi } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝, isLt := hj }
simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length,
  nonpos_iff_eq_zero] at hi hj
no goals
case mpr.intro.intro.intro.intro.refine'_1.mk.succ.mk.succ
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
n✝¹ : ℕ
hi✝ : Nat.succ n✝¹ < length (replicate 2 x)
n✝ : ℕ
hj✝ : Nat.succ n✝ < length (replicate 2 x)
hi : n✝¹ = 0
hj : n✝ = 0
⊢ { val := Nat.succ n✝¹, isLt := hi✝ } < { val := Nat.succ n✝, isLt := hj✝ } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝¹, isLt := hi✝ } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝, isLt := hj✝ }
simp [hi, hj]
case mpr.intro.intro.intro.intro.refine'_2.mk.zero
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
hi : Nat.zero < length (replicate 2 x)
⊢ get (replicate 2 x) { val := Nat.zero, isLt := hi } =
    get l
      (↑(OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m)
            (_ :
              ∀ ⦃a b : Fin (length (replicate 2 x))⦄,
                a < b → (fun i => if ↑i = 0 then n else m) a < (fun i => if ↑i = 0 then n else m) b))
        { val := Nat.zero, isLt := hi })

case mpr.intro.intro.intro.intro.refine'_2.mk.succ
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
n✝ : ℕ
hi : Nat.succ n✝ < length (replicate 2 x)
⊢ get (replicate 2 x) { val := Nat.succ n✝, isLt := hi } =
    get l
      (↑(OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m)
            (_ :
              ∀ ⦃a b : Fin (length (replicate 2 x))⦄,
                a < b → (fun i => if ↑i = 0 then n else m) a < (fun i => if ↑i = 0 then n else m) b))
        { val := Nat.succ n✝, isLt := hi })
case mpr.intro.intro.intro.intro.refine'_2
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
⊢ ∀ (ix : Fin (length (replicate 2 x))),
    get (replicate 2 x) ix =
      get l
        (↑(OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m)
              (_ :
                ∀ ⦃a b : Fin (length (replicate 2 x))⦄,
                  a < b → (fun i => if ↑i = 0 then n else m) a < (fun i => if ↑i = 0 then n else m) b))
          ix)
rintro ⟨⟨_ | i⟩, hi⟩
no goals
case mpr.intro.intro.intro.intro.refine'_2.mk.zero
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
hi : Nat.zero < length (replicate 2 x)
⊢ get (replicate 2 x) { val := Nat.zero, isLt := hi } =
    get l
      (↑(OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m)
            (_ :
              ∀ ⦃a b : Fin (length (replicate 2 x))⦄,
                a < b → (fun i => if ↑i = 0 then n else m) a < (fun i => if ↑i = 0 then n else m) b))
        { val := Nat.zero, isLt := hi })
simpa using h
no goals
case mpr.intro.intro.intro.intro.refine'_2.mk.succ
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
n✝ : ℕ
hi : Nat.succ n✝ < length (replicate 2 x)
⊢ get (replicate 2 x) { val := Nat.succ n✝, isLt := hi } =
    get l
      (↑(OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m)
            (_ :
              ∀ ⦃a b : Fin (length (replicate 2 x))⦄,
                a < b → (fun i => if ↑i = 0 then n else m) a < (fun i => if ↑i = 0 then n else m) b))
        { val := Nat.succ n✝, isLt := hi })
simpa using h'