split
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
⊢ (if h : Logic.Any (List.map (Setoid.r x) xs) then
      let_fun this := ⋯;
      ⋯ ▸ dedup s (unmap (Setoid.r x) h.get)
    else
      let_fun this := ⋯;
      ⋯ ▸ head) =
    j
case isTrue
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ dedup s (unmap (Setoid.r x) h✝.get)) =
    j

case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ head) =
    j