-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
i : Discrete ι
X : C
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) i
let let₁ let₂ : HasPullback g (c.ι.app i)
let₃ :
  let f := F.obj ∘ Discrete.mk;
  ∀ (this : F = Discrete.functor f), HasPullback g (c.ι.app i)
let₄ : ∀ (f : ι → C) (this : F = Discrete.functor f), HasPullback g (c.ι.app i)
let₅ :
  ∀ (f : ι → C) {c : Cocone.{u_1, v, u_1, u} (Discrete.functor f)} (hc : IsColimit c)
    (g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) i), HasPullback g (c.ι.app i)
let₆ :
  ∀ (f : ι → C) {c : Cofan.{u_1, v, u} f} (hc : IsColimit c)
    (g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) i), HasPullback g (c.ι.app i)
let₇ let₈ let₉ :
  ∀ (f : ι → C) {c : Cofan.{u_1, v, u} f} (hc : IsColimit c) (i : ι)
    (g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }),
    HasPullback g (c.ι.app { as := i : Discrete ι })
⊢ HasPullback g (c.ι.app i)
have let₁₀ : ∀ (f : ι → C) {c : Cofan.{u_1, v, u} f} (hc : IsColimit c) (i : ι)
  (g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }),
  let e :=
    {
      hom :=
        Sigma.desc fun (j : ι) ↦
          if h : j = i then eqToHom sorry ≫ coprod.inl
          else
            Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
                (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
              coprod.inr,
      inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)), hom_inv_id := sorry,
      inv_hom_id := sorry :
      sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) };
  let e' := hc.coconePointUniqueUpToIso (ColimitCocone.isColimit (getColimitCocone (Discrete.functor f))) ≪≫ e;
  ∀ (this : coprod.inl ≫ e'.inv = c.ι.app { as := i }), HasPullback g (c.ι.app { as := i : Discrete ι })
Tactic: classical
  let f : ι → C := F.obj ∘ Discrete.mk
  have : F = Discrete.functor f :=
    Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
  clear_value f
  subst this
  change Cofan f at c
  obtain ⟨i⟩ := i
  let e : ∐ f ≅ f i ⨿ (∐ fun j : ({i}ᶜ : Set ι) ↦ f j) :=
  { hom := Sigma.desc (fun j ↦ if h : j = i then eqToHom (congr_arg f h) ≫ coprod.inl else
      Sigma.ι (fun j : ({i}ᶜ : Set ι) ↦ f j) ⟨j, h⟩ ≫ coprod.inr)
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun j ↦ Sigma.ι f j)
    hom_inv_id := by cat_disch
    inv_hom_id := by
      ext j
      · simp
      · simp only [coprod.desc_comp, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app,
          eqToHom_refl, Category.id_comp, dite_true, BinaryCofan.mk_pt, BinaryCofan.ι_app_right,
          BinaryCofan.mk_inr, colimit.ι_desc_assoc, Discrete.functor_obj, Category.comp_id]
        exact dif_neg j.prop }
  let e' : c.pt ≅ f i ⨿ (∐ fun j : ({i}ᶜ : Set ι) ↦ f j) :=
    hc.coconePointUniqueUpToIso (getColimitCocone _).2 ≪≫ e
  have : coprod.inl ≫ e'.inv = c.ι.app ⟨i⟩ := by
    simp only [e, e', Iso.trans_inv, coprod.desc_comp, colimit.ι_desc, BinaryCofan.mk_pt,
      BinaryCofan.ι_app_left, BinaryCofan.mk_inl]
    exact colimit.comp_coconePointUniqueUpToIso_inv _ _
  clear_value e'
  rw [← this]
  have : IsPullback (𝟙 _) (g ≫ e'.hom) g e'.inv := IsPullback.of_horiz_isIso ⟨by simp⟩
  exact ⟨⟨⟨_, ((IsPullback.of_hasPullback (g ≫ e'.hom) coprod.inl).paste_horiz this).isLimit⟩⟩⟩
Cleared hypotheses: F, c, hc, i, g