split
case h
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
⊢ (match rtr[Component.val cpt][i], fun x => some (Option.getD (vs i) x) with
    | none, x => none
    | some a, b => b a) =
    vs i
case h.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
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))
heq✝ : rtr[Component.val cpt][i] = none
⊢ none = vs i

case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
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)
heq✝ : rtr[Component.val cpt][i] = some a✝
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i