-- 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:
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
this : coprod.inl ≫ e'.inv = c.ι.app { as := i }
⊢ HasPullback g (c.ι.app { as := i })

Tactic:
rw [← this]

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
this : coprod.inl ≫ e'.inv = c.ι.app { as := i }
⊢ HasPullback g (coprod.inl ≫ e'.inv)

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 }
⊢ (Sigma.desc fun j => if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j => f ↑j) ⟨j, h⟩ ≫ coprod.inr) ≫
      coprod.desc (Sigma.ι f i) (Sigma.desc fun j => Sigma.ι f ↑j) =
    𝟙 (∐ f)

Tactic:
aesop_cat

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 := ⋯ }
e' : c.pt ≅ f i ⨿ ∐ fun j => f ↑j
this✝ : coprod.inl ≫ e'.inv = c.ι.app { as := i }
this : IsPullback (𝟙 X) (g ≫ e'.hom) g e'.inv
⊢ HasPullback g (coprod.inl ≫ e'.inv)

Tactic:
exact ⟨⟨⟨_, ((IsPullback.of_hasPullback (g ≫ e'.hom) coprod.inl).paste_horiz this).isLimit⟩⟩⟩

Result:
no goals

Proof state:
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)

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]

Result:
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}ᶜ
⊢ (if h : ↑j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j => f ↑j) ⟨↑j, ⋯⟩ ≫ coprod.inr) =
    Sigma.ι (fun j => f ↑j) j ≫ coprod.inr

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 := F.obj ∘ Discrete.mk
⊢ HasPullback g (c.ι.app i)

Tactic:
have : F = Discrete.functor f :=
  Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])

Result:
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
this : F = Discrete.functor f
⊢ HasPullback g (c.ι.app i)

Proof state:
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)

Tactic:
simp

Result:
no goals

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
⊢ HasPullback g (c.ι.app i)

Tactic:
let f : ι → C := F.obj ∘ Discrete.mk

Result:
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
⊢ 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
⊢ coprod.inl ≫ e'.inv = 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]

Result:
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 }

Proof state:
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}ᶜ
⊢ (if h : ↑j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j => f ↑j) ⟨↑j, ⋯⟩ ≫ coprod.inr) =
    Sigma.ι (fun j => f ↑j) j ≫ coprod.inr

Tactic:
exact dif_neg j.prop

Result:
no goals