Theorem: CategoryTheory.piCompInvdesc (Sieves/ExtensiveRegular.lean)

State before:
C : Type u
inst✝³ : Category C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasPullbackOfIsIsodesc C
α : Type
inst✝ : Fintype α
Z : α → C
X : C
π : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc π)
a : α
⊢ π a ≫ inv (Sigma.desc π) = Sigma.ι Z a
Tactic:
simp
State after:
no goals