Theorem: CategoryTheory.HasProductT (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
S : Presieve X
hS : S = Presieve.ofArrows Z π
⊢ Finite ((Y : C) × { f // S f })
Tactic:
exact Fintype.finite <| FintypeT hS
State after:
no goals

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
S : Presieve X
hS : S = Presieve.ofArrows Z π
this : Finite ((Y : C) × { f // S f })
⊢ HasProduct fun f => f.fst.op
Tactic:
infer_instance
State after:
no goals