P : PFunctor
α✝ β✝ : Type u
inst✝² : DecidableEq P.A
α β : Type u
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x : Obj P α
f : α → β
i : IdxCat P
h : i.fst = x.fst
⊢ Sigma.snd (f <$> x) (cast (_ : B P i.fst = B P (f <$> x).fst) i.snd) =
    f (Sigma.snd x (cast (_ : B P i.fst = B P x.fst) i.snd))
P : PFunctor
α✝ β✝ : Type u
inst✝² : DecidableEq P.A
α β : Type u
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x : Obj P α
f : α → β
i : IdxCat P
h : i.fst = x.fst
⊢ Obj.iget (f <$> x) i = f (Obj.iget x i)
simp only [Obj.iget, fst_map, *, dif_pos, eq_self_iff_true]
case mk
P : PFunctor
α✝ β✝ : Type u
inst✝² : DecidableEq P.A
α β : Type u
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
i : IdxCat P
fst✝ : P.A
snd✝ : B P fst✝ → α
h : i.fst = { fst := fst✝, snd := snd✝ }.fst
⊢ Sigma.snd (f <$> { fst := fst✝, snd := snd✝ })
      (cast (_ : B P i.fst = B P (f <$> { fst := fst✝, snd := snd✝ }).fst) i.snd) =
    f (Sigma.snd { fst := fst✝, snd := snd✝ } (cast (_ : B P i.fst = B P { fst := fst✝, snd := snd✝ }.fst) i.snd))
P : PFunctor
α✝ β✝ : Type u
inst✝² : DecidableEq P.A
α β : Type u
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x : Obj P α
f : α → β
i : IdxCat P
h : i.fst = x.fst
⊢ Sigma.snd (f <$> x) (cast (_ : B P i.fst = B P (f <$> x).fst) i.snd) =
    f (Sigma.snd x (cast (_ : B P i.fst = B P x.fst) i.snd))
cases x
no goals
case mk
P : PFunctor
α✝ β✝ : Type u
inst✝² : DecidableEq P.A
α β : Type u
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
i : IdxCat P
fst✝ : P.A
snd✝ : B P fst✝ → α
h : i.fst = { fst := fst✝, snd := snd✝ }.fst
⊢ Sigma.snd (f <$> { fst := fst✝, snd := snd✝ })
      (cast (_ : B P i.fst = B P (f <$> { fst := fst✝, snd := snd✝ }).fst) i.snd) =
    f (Sigma.snd { fst := fst✝, snd := snd✝ } (cast (_ : B P i.fst = B P { fst := fst✝, snd := snd✝ }.fst) i.snd))
rfl