simp [hn] at h
case h.h_2
α : 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))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : (∃ b, vs i = some b) ↔ ∃ b, rtr[Component.val cpt][i] = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
case h.h_2
α : 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))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : ∃ b, vs i = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i