next j hj =>
  rw [←specSubtype] at h
  rw [h]
  symmetry
  apply of_decide_eq_true
  exact Fin.find?_some j hj
case h.mpr.a.h_1
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
j✝ : Fin n
heq✝ : (Fin.find? fun b => decide (Setoid.r i b)) = some j✝
h :
  (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨j✝, this⟩) =
    k
⊢ (decodeSubtype (repr s) k).val ≈ i

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