-- Mathlib/CategoryTheory/Extensive.lean
lemma FinitaryPreExtensive.sigma_desc_iso [FinitaryPreExtensive C] {α : Type} [Finite α] {X : C}
    {Z : α → C} (π : (a : α) → Z a ⟶ X) {Y : C} (f : Y ⟶ X) (hπ : IsIso (Sigma.desc π)) :
    IsIso (Sigma.desc ((fun _ ↦ pullback.fst _ _) : (a : α) → pullback f (π a) ⟶ _))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
this : IsColimit (Cofan.mk X π) := (coproductIsCoproduct Z).ofPointIso
⊢ IsColimit (Cofan.mk Y fun x => pullback.fst f (π x))

Tactic:
refine (FinitaryPreExtensive.isUniversal_finiteCoproducts this
  (Cofan.mk _ ((fun _ ↦ pullback.fst _ _) : (a : α) → pullback f (π a) ⟶ _))
  (Discrete.natTrans fun i ↦ pullback.snd _ _) f ?_
  (NatTrans.equifibered_of_discrete _) ?_).some

Result:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
this : IsColimit (Cofan.mk X π) := (coproductIsCoproduct Z).ofPointIso
⊢ (Discrete.natTrans fun i => pullback.snd f (π i.as)) ≫ (Cofan.mk X π).ι =
    (Cofan.mk Y fun x => pullback.fst f (π x)).ι ≫ (Functor.const (Discrete α)).map f

case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
this : IsColimit (Cofan.mk X π) := (coproductIsCoproduct Z).ofPointIso
⊢ ∀ (j : Discrete α),
    IsPullback ((Cofan.mk Y fun x => pullback.fst f (π x)).ι.app j)
      ((Discrete.natTrans fun i => pullback.snd f (π i.as)).app j) f ((Cofan.mk X π).ι.app j)

Proof state:
case refine_1.w.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
this : IsColimit (Cofan.mk X π) := (coproductIsCoproduct Z).ofPointIso
x✝ : Discrete α
⊢ ((Discrete.natTrans fun i => pullback.snd f (π i.as)) ≫ (Cofan.mk X π).ι).app x✝ =
    ((Cofan.mk Y fun x => pullback.fst f (π x)).ι ≫ (Functor.const (Discrete α)).map f).app x✝

Tactic:
simp [pullback.condition]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
this : IsColimit (Cofan.mk Y fun x => pullback.fst f (π x))
⊢ IsIso (Sigma.desc fun x => pullback.fst f (π x))

Tactic:
change IsIso (this.coconePointUniqueUpToIso (getColimitCocone _).2).inv

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
this : IsColimit (Cofan.mk Y fun x => pullback.fst f (π x))
⊢ IsIso (this.coconePointUniqueUpToIso (getColimitCocone (Discrete.functor fun x => pullback f (π x))).isColimit).inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
⊢ IsColimit (Cofan.mk Y fun x => pullback.fst f (π x))

Tactic:
let this : IsColimit (Cofan.mk X π) := by
  refine @IsColimit.ofPointIso (t := Cofan.mk X π) (P := coproductIsCoproduct Z) (i := ?_)
  convert hπ
  simp [coproductIsCoproduct]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
this : IsColimit (Cofan.mk X π) := (coproductIsCoproduct Z).ofPointIso
⊢ IsColimit (Cofan.mk Y fun x => pullback.fst f (π x))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
⊢ IsIso (Sigma.desc fun x => pullback.fst f (π x))

Tactic:
suffices IsColimit (Cofan.mk _ ((fun _ ↦ pullback.fst _ _) : (a : α) → pullback f (π a) ⟶ _)) by
  change IsIso (this.coconePointUniqueUpToIso (getColimitCocone _).2).inv
  infer_instance

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
⊢ IsColimit (Cofan.mk Y fun x => pullback.fst f (π x))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
⊢ IsColimit (Cofan.mk X π)

Tactic:
refine @IsColimit.ofPointIso (t := Cofan.mk X π) (P := coproductIsCoproduct Z) (i := ?_)

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
⊢ IsIso ((coproductIsCoproduct Z).desc (Cofan.mk X π))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
⊢ IsIso ((coproductIsCoproduct Z).desc (Cofan.mk X π))

Tactic:
convert hπ

Result:
case h.e'_5.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
e_3✝ : (Cofan.mk (∐ Z) (Sigma.ι Z)).pt = ∐ Z
e_4✝ : (Cofan.mk X π).pt = X
⊢ (coproductIsCoproduct Z).desc (Cofan.mk X π) = Sigma.desc π

Proof state:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
this : IsColimit (Cofan.mk X π) := (coproductIsCoproduct Z).ofPointIso
⊢ (Discrete.natTrans fun i => pullback.snd f (π i.as)) ≫ (Cofan.mk X π).ι =
    (Cofan.mk Y fun x => pullback.fst f (π x)).ι ≫ (Functor.const (Discrete α)).map f

Tactic:
ext

Result:
case refine_1.w.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
this : IsColimit (Cofan.mk X π) := (coproductIsCoproduct Z).ofPointIso
x✝ : Discrete α
⊢ ((Discrete.natTrans fun i => pullback.snd f (π i.as)) ≫ (Cofan.mk X π).ι).app x✝ =
    ((Cofan.mk Y fun x => pullback.fst f (π x)).ι ≫ (Functor.const (Discrete α)).map f).app x✝

Proof state:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
this : IsColimit (Cofan.mk X π) := (coproductIsCoproduct Z).ofPointIso
⊢ ∀ (j : Discrete α),
    IsPullback ((Cofan.mk Y fun x => pullback.fst f (π x)).ι.app j)
      ((Discrete.natTrans fun i => pullback.snd f (π i.as)).app j) f ((Cofan.mk X π).ι.app j)

Tactic:
exact fun j ↦ IsPullback.of_hasPullback f (π j.as)

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
this : IsColimit (Cofan.mk Y fun x => pullback.fst f (π x))
⊢ IsIso (this.coconePointUniqueUpToIso (getColimitCocone (Discrete.functor fun x => pullback f (π x))).isColimit).inv

Tactic:
infer_instance

Result:
no goals

Proof state:
case h.e'_5.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
e_3✝ : (Cofan.mk (∐ Z) (Sigma.ι Z)).pt = ∐ Z
e_4✝ : (Cofan.mk X π).pt = X
⊢ (coproductIsCoproduct Z).desc (Cofan.mk X π) = Sigma.desc π

Tactic:
simp [coproductIsCoproduct]

Result:
no goals