exact Option.eq_none_iff_forall_not_mem.mpr h |>.symm
case h.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
hn : rtr[Component.val cpt][i] = none
h : ∀ (x : Value), ¬vs i = some x
⊢ none = vs i
no goals