apply h
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
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : ¬Setoid.r i i
⊢ False
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
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : ¬Setoid.r i i
⊢ Setoid.r i i