Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case e'_7.e
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
e_3✝ :
  (∐ fun p ↦ pullback (f p.1) (g p.2)) =
    (Cofan.mk (∐ fun p ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun p ↦ pullback (f p.1) (g p.2))).pt
e_4✝ : ∐ X = (Cofan.mk (∐ X) fun i ↦ Sigma.ι X i).pt
⊢ @Sigma.desc (ι × ι') C inst✝⁴ (fun p ↦ pullback (f p.1) (g p.2)) ⋯ =
    @Cofan.IsColimit.desc (ι × ι') C inst✝⁴ (fun b ↦ pullback (f b.1) (g b.2))
      (Cofan.mk (∐ fun p ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun p ↦ pullback (f p.1) (g p.2)))
      (coproductIsCoproduct fun p ↦ pullback (f p.1) (g p.2))

pp: case e'_8.e
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
e_3✝ :
  (∐ fun p ↦ pullback (f p.1) (g p.2)) =
    (Cofan.mk (∐ fun p ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun p ↦ pullback (f p.1) (g p.2))).pt
e_5✝ : ∐ Y = (Cofan.mk (∐ Y) fun i ↦ Sigma.ι Y i).pt
⊢ @Sigma.desc (ι × ι') C inst✝⁴ (fun p ↦ pullback (f p.1) (g p.2)) ⋯ =
    @Cofan.IsColimit.desc (ι × ι') C inst✝⁴ (fun b ↦ pullback (f b.1) (g b.2))
      (Cofan.mk (∐ fun p ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun p ↦ pullback (f p.1) (g p.2)))
      (coproductIsCoproduct fun p ↦ pullback (f p.1) (g p.2))

pp: case convert_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsUniversalColimit (Cofan.mk (∐ X) fun i ↦ Sigma.ι X i)

pp: case convert_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsUniversalColimit (Cofan.mk (∐ Y) fun i ↦ Sigma.ι Y i)

Tactic:
· ext
    simp [Cofan.IsColimit.desc, Sigma.ι, coproductIsCoproduct]

Goal state after:
case e'_8.e
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
e_3✝ :
  (∐ fun p ↦ pullback (f p.1) (g p.2)) =
    (Cofan.mk (∐ fun p ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun p ↦ pullback (f p.1) (g p.2))).pt
e_5✝ : ∐ Y = (Cofan.mk (∐ Y) fun i ↦ Sigma.ι Y i).pt
⊢ @Sigma.desc (ι × ι') C inst✝⁴ (fun p ↦ pullback (f p.1) (g p.2)) ⋯ =
    @Cofan.IsColimit.desc (ι × ι') C inst✝⁴ (fun b ↦ pullback (f b.1) (g b.2))
      (Cofan.mk (∐ fun p ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun p ↦ pullback (f p.1) (g p.2)))
      (coproductIsCoproduct fun p ↦ pullback (f p.1) (g p.2))

case convert_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsUniversalColimit (Cofan.mk (∐ X) fun i ↦ Sigma.ι X i)

case convert_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsUniversalColimit (Cofan.mk (∐ Y) fun i ↦ Sigma.ι Y i)