F : PFunctor
X : Type ?u.26833
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
x : Obj F (M F)
i : IdxCat F
⊢ (if H' : i.fst = head (M.mk x) then children (M.mk x) (cast (_ : B F i.fst = B F (head (M.mk x))) i.snd)
    else default) =
    if h : i.fst = x.fst then Sigma.snd x (cast (_ : B F i.fst = B F x.fst) i.snd) else default
F : PFunctor
X : Type ?u.26833
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
x : Obj F (M F)
i : IdxCat F
⊢ ichildren i (M.mk x) = Obj.iget x i
dsimp only [ichildren, PFunctor.Obj.iget]
no goals
F : PFunctor
X : Type ?u.26833
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
x : Obj F (M F)
i : IdxCat F
⊢ (if H' : i.fst = head (M.mk x) then children (M.mk x) (cast (_ : B F i.fst = B F (head (M.mk x))) i.snd)
    else default) =
    if h : i.fst = x.fst then Sigma.snd x (cast (_ : B F i.fst = B F x.fst) i.snd) else default
congr with h