-- Mathlib/CategoryTheory/Extensive.lean
lemma FinitaryPreExtensive.hasPullbacks_of_is_coproduct [FinitaryPreExtensive C] {ι : Type*}
    [Finite ι] {F : Discrete ι ⥤ C} {c : Cocone F} (hc : IsColimit c) (i : Discrete ι) {X : C}
    (g : X ⟶ _) : HasPullback g (c.ι.app i)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
i : Discrete ι
X : C
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj i
f : ι → C
this : F = Discrete.functor f
⊢ HasPullback g (c.ι.app i)

Tactic:
subst this

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
i : Discrete ι
X : C
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj i
⊢ HasPullback g (c.ι.app i)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
e : ∐ f ≅ f i ⨿ ∐ fun j => f ↑j :=
  {
    hom :=
      Sigma.desc fun j => if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j => f ↑j) ⟨j, h⟩ ≫ coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun j => Sigma.ι f ↑j), hom_inv_id := ⋯, inv_hom_id := ⋯ }
e' : c.pt ≅ f i ⨿ ∐ fun j => f ↑j := hc.coconePointUniqueUpToIso (getColimitCocone (Discrete.functor f)).isColimit ≪≫ e
⊢ Sigma.ι f i ≫ (hc.coconePointUniqueUpToIso (getColimitCocone (Discrete.functor f)).isColimit).inv =
    c.ι.app { as := i }

Tactic:
exact colimit.comp_coconePointUniqueUpToIso_inv _ _

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
⊢ (coprod.desc (Sigma.ι f i) (Sigma.desc fun j => Sigma.ι f ↑j) ≫
      Sigma.desc fun j => if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j => f ↑j) ⟨j, h⟩ ≫ coprod.inr) =
    𝟙 (f i ⨿ ∐ fun j => f ↑j)

Tactic:
ext j

Result:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
⊢ (coprod.inl ≫
      coprod.desc (Sigma.ι f i) (Sigma.desc fun j => Sigma.ι f ↑j) ≫
        Sigma.desc fun j => if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j => f ↑j) ⟨j, h⟩ ≫ coprod.inr) =
    coprod.inl ≫ 𝟙 (f i ⨿ ∐ fun j => f ↑j)

case h₂.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
j : ↑{i}ᶜ
⊢ (Sigma.ι (fun j => f ↑j) j ≫
      coprod.inr ≫
        coprod.desc (Sigma.ι f i) (Sigma.desc fun j => Sigma.ι f ↑j) ≫
          Sigma.desc fun j =>
            if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j => f ↑j) ⟨j, h⟩ ≫ coprod.inr) =
    Sigma.ι (fun j => f ↑j) j ≫ coprod.inr ≫ 𝟙 (f i ⨿ ∐ fun j => f ↑j)

Proof state:
case mk.mk.up.up
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
i✝ : Discrete ι
X : C
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj i✝
f : ι → C := F.obj ∘ Discrete.mk
i : ι
⊢ HEq (F.map { down := { down := ⋯ } }) ((Discrete.functor f).map { down := { down := ⋯ } })

Tactic:
simp [f]

Result:
no goals

Proof state:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
e : ∐ f ≅ f i ⨿ ∐ fun j => f ↑j :=
  {
    hom :=
      Sigma.desc fun j => if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j => f ↑j) ⟨j, h⟩ ≫ coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun j => Sigma.ι f ↑j), hom_inv_id := ⋯, inv_hom_id := ⋯ }
⊢ HasPullback g (c.ι.app { as := i })

Tactic:
let e' : c.pt ≅ f i ⨿ (∐ fun j : ({i}ᶜ : Set ι) ↦ f j) :=
  hc.coconePointUniqueUpToIso (getColimitCocone _).2 ≪≫ e

Result:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
e : ∐ f ≅ f i ⨿ ∐ fun j => f ↑j :=
  {
    hom :=
      Sigma.desc fun j => if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j => f ↑j) ⟨j, h⟩ ≫ coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun j => Sigma.ι f ↑j), hom_inv_id := ⋯, inv_hom_id := ⋯ }
e' : c.pt ≅ f i ⨿ ∐ fun j => f ↑j := hc.coconePointUniqueUpToIso (getColimitCocone (Discrete.functor f)).isColimit ≪≫ e
⊢ HasPullback g (c.ι.app { as := i })