split
case h.mp.right
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
⊢ (match h : Fin.find? fun b => decide (Setoid.r i b) with
    | some j =>
      let_fun this := ⋯;
      encodeSubtype (repr s) ⟨j, this⟩
    | none => absurd ⋯ ⋯) =
    k
case h.mp.right.h_1
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
j✝ : Fin n
heq✝ : (Fin.find? fun b => decide (Setoid.r i b)) = some j✝
⊢ (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨j✝, this⟩) =
    k

case h.mp.right.h_2
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
heq✝ : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ absurd ⋯ ⋯ = k