F : PFunctor
X : Type ?u.27518
f✝ : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
a : F.A
f : B F a → M F
i : B F a
⊢ isubtree ps (f (cast (_ : B F a = B F a) i)) = isubtree ps (f i)
F : PFunctor
X : Type ?u.27518
f✝ : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
a : F.A
f : B F a → M F
i : B F a
⊢ isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) = isubtree ps (f i)
simp only [isubtree, ichildren_mk, PFunctor.Obj.iget, dif_pos, isubtree, M.casesOn_mk']
no goals
F : PFunctor
X : Type ?u.27518
f✝ : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
a : F.A
f : B F a → M F
i : B F a
⊢ isubtree ps (f (cast (_ : B F a = B F a) i)) = isubtree ps (f i)
rfl