awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
X : C
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 ι }
j : (↑{i}ᶜ : Type u_1)
⊢ CategoryStruct.comp (Y := sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
      (Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) j)
      (CategoryStruct.comp (Y := coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
        coprod.inr
        (CategoryStruct.comp (Y := sigmaObj.{u_1, v, u} f)
          (coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)))
          (Sigma.desc fun (j : ι) ↦
            if h : j = i then eqToHom ⋯ ≫ 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))) =
    Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) j ≫
      coprod.inr ≫ 𝟙 (coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
have h₂ : Eq.{v + 1} (α := f (↑j : ι) ⟶ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑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 : ι) sorry) ≫
        coprod.inr :
    f (↑j : ι) ⟶ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
  (Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) j ≫ coprod.inr :
    f (↑j : ι) ⟶ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
Tactic: 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]
-- 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 ι
X : C
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 ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ 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 := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  hc.coconePointUniqueUpToIso (ColimitCocone.isColimit (getColimitCocone (Discrete.functor f))) ≪≫ e
⊢ coprod.inl ≫ e'.inv = c.ι.app { as := i }
have simp : CategoryStruct.comp (Y :=
    Cocone.pt.{u_1, v, u_1, u} (F := Discrete.functor f) (ColimitCocone.cocone (getColimitCocone (Discrete.functor f))))
    (Sigma.ι f i)
    (Iso.inv (hc.coconePointUniqueUpToIso (ColimitCocone.isColimit (getColimitCocone (Discrete.functor f))))) =
  c.ι.app { as := i }
Tactic: simp only [e, e', Iso.trans_inv, coprod.desc_comp, colimit.ι_desc, BinaryCofan.mk_pt,
      BinaryCofan.ι_app_left, BinaryCofan.mk_inl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
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 ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ 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 := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  hc.coconePointUniqueUpToIso (ColimitCocone.isColimit (getColimitCocone (Discrete.functor f))) ≪≫ e
⊢ HasPullback g (c.ι.app { as := i : Discrete ι })
have this : coprod.inl ≫ e'.inv = c.ι.app { as := i }
Tactic: 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 _ _
-- 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 ι
X : C
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 ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ 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 := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  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 ι })
have clear_value : ∀ (e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
  (this : coprod.inl ≫ e'.inv = c.ι.app { as := i }), HasPullback g (c.ι.app { as := i : Discrete ι })
Tactic: clear_value e'
Cleared hypotheses: e', this
-- 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 ι
X : C
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 ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ 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 := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
this : coprod.inl ≫ e'.inv = c.ι.app { as := i }
⊢ HasPullback g (c.ι.app { as := i : Discrete ι })
have rw : HasPullback g (coprod.inl ≫ e'.inv)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
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 ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ 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 := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
this : coprod.inl ≫ e'.inv = c.ι.app { as := i }
⊢ HasPullback g (coprod.inl ≫ e'.inv)
have this₁ : IsPullback (𝟙 X) (g ≫ e'.hom) g e'.inv
Tactic: have : IsPullback (𝟙 _) (g ≫ e'.hom) g e'.inv := IsPullback.of_horiz_isIso ⟨by simp⟩
-- 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)
⊢ HasPullback g (c.ι.app i)
have let₃ : let f := F.obj ∘ Discrete.mk;
∀ (this : F = Discrete.functor f), HasPullback g (c.ι.app i)
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⟩⟩⟩
-- 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)
⊢ HasPullback g (c.ι.app i)
have let₄ : ∀ (f : ι → C) (this : F = Discrete.functor f), HasPullback g (c.ι.app i)
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⟩⟩⟩
-- 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)
⊢ HasPullback g (c.ι.app i)
have 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)
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, g
-- 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)
⊢ HasPullback g (c.ι.app i)
have 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)
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, g
-- 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)
⊢ 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 ι }),
  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
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y : C
inst_3 : FinitaryExtensive.{v, u} C
ι : Type u_1
inst_4 : Finite ι
X : ι → C
⊢ CoproductDisjoint.{v, u, u_1} X
have refine : ∀ {c : Cofan.{u_1, v, u} X} (hc : IsColimit c) (i j : ι) (e : i ≠ j) (s : PullbackCone (c.inj i) (c.inj j))
  (hs : IsLimit s), Nonempty (IsInitial.{v, u} s.pt)
Tactic: refine ⟨fun {c} hc i j e s hs ↦ ?_, fun hc i ↦ FinitaryExtensive.mono_ι hc ⟨i⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : FinitaryPreExtensive.{v, u} C
X Z : C
α : Type u_1
f : X ⟶ Z
Y : (a : α) → C
i : (a : α) → Y a ⟶ Z
inst_4 : Finite α
hi : IsIso (X := sigmaObj.{u_1, v, u} Y) (Sigma.desc i)
a : α
⊢ HasPullback f (i a)
have hc : IsColimit (Cofan.mk Z i)
Tactic: apply FinitaryPreExtensive.hasPullbacks_of_is_coproduct (c := Cofan.mk Z i)
-- 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
inst_2 : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (X := sigmaObj.{0, v, u} Z) (Sigma.desc π)
c : Cofan.{0, v, u} (C := C) fun (x : α) ↦ pullback f (π x) := Cofan.mk Y fun (x : α) ↦ pullback.fst f (π x)
⊢ IsIso.{v, u} (C := C) (X := sigmaObj.{0, v, u} fun (x : α) ↦ pullback f (π x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst f (π x))
have apply : Nonempty (IsColimit c)
Tactic: apply c.nonempty_isColimit_iff_isIso_sigmaDesc.mp
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
α : Type
inst_2 : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (X := sigmaObj.{0, v, u} Z) (Sigma.desc π)
c : Cofan.{0, v, u} (C := C) fun (x : α) ↦ pullback f (π x) := Cofan.mk Y fun (x : α) ↦ pullback.fst f (π x)
⊢ Nonempty (IsColimit c)
have hau : IsUniversalColimit (Cofan.mk X π)
Tactic: have hau : IsUniversalColimit (Cofan.mk X π) := FinitaryPreExtensive.isUniversal_finiteCoproducts
    ((Cofan.nonempty_isColimit_iff_isIso_sigmaDesc _).mpr hπ).some
-- 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
inst_2 : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (X := sigmaObj.{0, v, u} Z) (Sigma.desc π)
c : Cofan.{0, v, u} (C := C) fun (x : α) ↦ pullback f (π x) := Cofan.mk Y fun (x : α) ↦ pullback.fst f (π x)
hau : IsUniversalColimit (Cofan.mk X π)
⊢ Nonempty (IsColimit c)
have refine : (i : α) → IsLimit (limit.cone (cospan f (π i)))
Tactic: refine hau.nonempty_isColimit_of_pullbackCone_left _ (𝟙 _) _ _ (fun i ↦ ?_)
    (PullbackCone.mk (𝟙 _) f (by simp)) (IsPullback.id_horiz f).isLimit _ (Iso.refl _)
    (by simp) (by simp [c]) (by simp [pullback.condition, c])