awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasColimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactColimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cocone F
hc : IsColimit c
X : C
f : X ⟶ c.pt
hpull :
  IsPullback (P := colimit (pullback c.ι (Functor.map (Functor.const J) f))) (X := colimit F) (Y :=
    colimit.{w', w, v, u} (Functor.obj (Functor.const J) X)) (Z :=
    colimit.{w', w, v, u} (Functor.obj (Functor.const J) c.pt))
    (colimMap (pullback.fst c.ι (Functor.map (Functor.const J) f)))
    (colimMap (pullback.snd c.ι (Functor.map (Functor.const J) f))) (colimMap c.ι)
    (colimMap (Functor.map (Functor.const J) f))
this : IsIso (X := colimit F) (Y := colimit.{w', w, v, u} (Functor.obj (Functor.const J) c.pt)) (colimMap c.ι)
⊢ IsIso (X := colimit (pullback c.ι (Functor.map (Functor.const J) f))) (Y :=
    colimit.{w', w, v, u} (Functor.obj (Functor.const J) X))
    (colimMap (pullback.snd c.ι (Functor.map (Functor.const J) f)))

Tactic:
apply hpull.isIso_snd_of_isIso

Premises used: CategoryTheory.IsPullback.isIso_snd_of_isIso
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasColimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactColimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g h : c.pt ⟶ Y
hf :
  ∀ (j : J),
    Eq (α := pullback (c.ι.app j) f ⟶ Y) (pullback.snd (c.ι.app j) f ≫ f ≫ g) (pullback.snd (c.ι.app j) f ≫ f ≫ h)
⊢ f ≫ g = f ≫ h

Tactic:
(hc.pullbackOfHasExactColimitsOfShape f).hom_ext (fun j => ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.IsColimit.pullbackOfHasExactColimitsOfShape
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasColimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactColimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g h : c.pt ⟶ Y
hf :
  ∀ (j : J),
    Eq (α := pullback (c.ι.app j) f ⟶ Y) (pullback.snd (c.ι.app j) f ≫ f ≫ g) (pullback.snd (c.ι.app j) f ≫ f ≫ h)
refine :
  ∀ (j : J),
    Eq (α := (pullback c.ι (Functor.map (Functor.const J) f)).obj j ⟶ Y)
      (NatTrans.app (Cocone.ι { pt := X, ι := pullback.snd c.ι (Functor.map (Functor.const J) f) }) j ≫ f ≫ g)
      (NatTrans.app (Cocone.ι { pt := X, ι := pullback.snd c.ι (Functor.map (Functor.const J) f) }) j ≫ f ≫ h)
⊢ f ≫ g = f ≫ h

Tactic:
refine (hc.pullbackOfHasExactColimitsOfShape f).hom_ext (fun j => ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.IsColimit.pullbackOfHasExactColimitsOfShape
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasColimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactColimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g h : c.pt ⟶ Y
hf :
  ∀ (j : J),
    Eq (α := pullback (c.ι.app j) f ⟶ Y) (pullback.snd (c.ι.app j) f ≫ f ≫ g) (pullback.snd (c.ι.app j) f ≫ f ≫ h)
j : J
rw :
  Eq (α := pullback (c.ι.app j) (NatTrans.app (Functor.map (Functor.const J) f) j) ⟶ Y)
    (CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) f)).obj j)
        (Iso.inv (pullbackObjIso c.ι (Functor.map (Functor.const J) f) j) :
          pullback (c.ι.app j) (NatTrans.app (Functor.map (Functor.const J) f) j) ⟶
            (pullback c.ι (Functor.map (Functor.const J) f)).obj j)
        (NatTrans.app (Cocone.ι { pt := X, ι := pullback.snd c.ι (Functor.map (Functor.const J) f) }) j ≫ f ≫ g :
          (pullback c.ι (Functor.map (Functor.const J) f)).obj j ⟶ Y) :
      pullback (c.ι.app j) (NatTrans.app (Functor.map (Functor.const J) f) j) ⟶ Y)
    (CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) f)).obj j)
        (Iso.inv (pullbackObjIso c.ι (Functor.map (Functor.const J) f) j) :
          pullback (c.ι.app j) (NatTrans.app (Functor.map (Functor.const J) f) j) ⟶
            (pullback c.ι (Functor.map (Functor.const J) f)).obj j)
        (NatTrans.app (Cocone.ι { pt := X, ι := pullback.snd c.ι (Functor.map (Functor.const J) f) }) j ≫ f ≫ h :
          (pullback c.ι (Functor.map (Functor.const J) f)).obj j ⟶ Y) :
      pullback (c.ι.app j) (NatTrans.app (Functor.map (Functor.const J) f) j) ⟶ Y)
⊢ Eq (α := (pullback c.ι (Functor.map (Functor.const J) f)).obj j ⟶ Y)
    (NatTrans.app (Cocone.ι { pt := X, ι := pullback.snd c.ι (Functor.map (Functor.const J) f) }) j ≫ f ≫ g)
    (NatTrans.app (Cocone.ι { pt := X, ι := pullback.snd c.ι (Functor.map (Functor.const J) f) }) j ≫ f ≫ h)

Tactic:
rw [← cancel_epi (pullbackObjIso _ _ _).inv]

Premises used: CategoryTheory.Limits.pullbackObjIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasColimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactColimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g h : c.pt ⟶ Y
hf :
  ∀ (j : J),
    Eq (α := pullback (c.ι.app j) f ⟶ Y) (pullback.snd (c.ι.app j) f ≫ f ≫ g) (pullback.snd (c.ι.app j) f ≫ f ≫ h)
j : J
⊢ Eq (α := pullback (c.ι.app j) (NatTrans.app (Functor.map (Functor.const J) f) j) ⟶ Y)
    (CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) f)).obj j)
        (Iso.inv (pullbackObjIso c.ι (Functor.map (Functor.const J) f) j) :
          pullback (c.ι.app j) (NatTrans.app (Functor.map (Functor.const J) f) j) ⟶
            (pullback c.ι (Functor.map (Functor.const J) f)).obj j)
        (NatTrans.app (Cocone.ι { pt := X, ι := pullback.snd c.ι (Functor.map (Functor.const J) f) }) j ≫ f ≫ g :
          (pullback c.ι (Functor.map (Functor.const J) f)).obj j ⟶ Y) :
      pullback (c.ι.app j) (NatTrans.app (Functor.map (Functor.const J) f) j) ⟶ Y)
    (CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) f)).obj j)
        (Iso.inv (pullbackObjIso c.ι (Functor.map (Functor.const J) f) j) :
          pullback (c.ι.app j) (NatTrans.app (Functor.map (Functor.const J) f) j) ⟶
            (pullback c.ι (Functor.map (Functor.const J) f)).obj j)
        (NatTrans.app (Cocone.ι { pt := X, ι := pullback.snd c.ι (Functor.map (Functor.const J) f) }) j ≫ f ≫ h :
          (pullback c.ι (Functor.map (Functor.const J) f)).obj j ⟶ Y) :
      pullback (c.ι.app j) (NatTrans.app (Functor.map (Functor.const J) f) j) ⟶ Y)

Tactic:
simpa using hf j
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasColimitsOfShape.{w', w, v, u} J C
inst_6 : HasExactColimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g : c.pt ⟶ Y
hf : ∀ (j : J), Eq (α := pullback (c.ι.app j) f ⟶ Y) (pullback.snd (c.ι.app j) f ≫ f ≫ g) 0
this : f ≫ g = f ≫ 0
⊢ f ≫ g = 0

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasColimitsOfShape.{w', w, v, u} J C
inst_6 : HasExactColimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g : c.pt ⟶ Y
hf : ∀ (j : J), Eq (α := pullback (c.ι.app j) f ⟶ Y) (pullback.snd (c.ι.app j) f ≫ f ≫ g) 0
suffices : f ≫ g = f ≫ 0
⊢ f ≫ g = 0

Tactic:
suffices f ≫ g = f ≫ 0 by simpa
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasColimitsOfShape.{w', w, v, u} J C
inst_6 : HasExactColimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g : c.pt ⟶ Y
hf : ∀ (j : J), Eq (α := pullback (c.ι.app j) f ⟶ Y) (pullback.snd (c.ι.app j) f ≫ f ≫ g) 0
⊢ ∀ (j : J),
    Eq (α := pullback (c.ι.app j) f ⟶ Y) (pullback.snd (c.ι.app j) f ≫ f ≫ g) (pullback.snd (c.ι.app j) f ≫ f ≫ 0)

Tactic:
simpa using hf
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasColimitsOfShape.{w', w, v, u} J C
inst_6 : HasExactColimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g : c.pt ⟶ Y
hf : ∀ (j : J), Eq (α := pullback (c.ι.app j) f ⟶ Y) (pullback.snd (c.ι.app j) f ≫ f ≫ g) 0
⊢ f ≫ g = f ≫ 0

Tactic:
exact hc.pullback_hom_ext (by simpa using hf)

Premises used: CategoryTheory.Limits.IsColimit.pullback_hom_ext
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : HasLimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactLimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cone F
hc : IsLimit c
X : C
f : c.pt ⟶ X
suffices :
  IsIso (X := limit.{w', w, v, u} (Functor.obj (Functor.const J) X)) (Y :=
    limit (pushout c.π (Functor.map (Functor.const J) f))) (limMap (pushout.inr c.π (Functor.map (Functor.const J) f)))
⊢ IsLimit (F := pushout c.π (Functor.map (Functor.const J) f))
    { pt := X, π := pushout.inr c.π (Functor.map (Functor.const J) f) }

Tactic:
suffices IsIso (limMap (pushout.inr c.π ((Functor.const J).map f))) from
    Cone.isLimitOfIsIsoLimMapπ _
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : HasLimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactLimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cone F
hc : IsLimit c
X : C
f : c.pt ⟶ X
⊢ IsPushout (Z := Functor.obj (C := Functor.{w', v, w, u} J C) lim (Functor.obj (Functor.const J) c.pt)) (P :=
    Functor.obj lim (pushout c.π (Functor.map (Functor.const J) f))) (Functor.map lim c.π)
    (Functor.map lim (Functor.map (Functor.const J) f))
    (Functor.map lim (pushout.inl c.π (Functor.map (Functor.const J) f)))
    (Functor.map lim (pushout.inr c.π (Functor.map (Functor.const J) f)))

Tactic:
have hpush := lim.map_isPushout (IsPushout.of_hasPushout c.π ((Functor.const J).map f))
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : HasLimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactLimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cone F
hc : IsLimit c
X : C
f : c.pt ⟶ X
hpush :
  IsPushout (Z := limit.{w', w, v, u} (Functor.obj (Functor.const J) c.pt)) (X := limit F) (Y :=
    limit.{w', w, v, u} (Functor.obj (Functor.const J) X)) (P := limit (pushout c.π (Functor.map (Functor.const J) f)))
    (limMap c.π) (limMap (Functor.map (Functor.const J) f)) (limMap (pushout.inl c.π (Functor.map (Functor.const J) f)))
    (limMap (pushout.inr c.π (Functor.map (Functor.const J) f)))
⊢ IsIso (X := limit.{w', w, v, u} (Functor.obj (Functor.const J) c.pt)) (Y := limit F) (limMap c.π)

Tactic:
have := hc.isIso_limMap_π
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : HasLimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactLimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cone F
hc : IsLimit c
X : C
f : c.pt ⟶ X
hpush :
  IsPushout (Z := limit.{w', w, v, u} (Functor.obj (Functor.const J) c.pt)) (X := limit F) (Y :=
    limit.{w', w, v, u} (Functor.obj (Functor.const J) X)) (P := limit (pushout c.π (Functor.map (Functor.const J) f)))
    (limMap c.π) (limMap (Functor.map (Functor.const J) f)) (limMap (pushout.inl c.π (Functor.map (Functor.const J) f)))
    (limMap (pushout.inr c.π (Functor.map (Functor.const J) f)))
this : IsIso (X := limit.{w', w, v, u} (Functor.obj (Functor.const J) c.pt)) (Y := limit F) (limMap c.π)
⊢ IsIso (X := limit.{w', w, v, u} (Functor.obj (Functor.const J) X)) (Y :=
    limit (pushout c.π (Functor.map (Functor.const J) f))) (limMap (pushout.inr c.π (Functor.map (Functor.const J) f)))

Tactic:
apply hpush.isIso_inr_of_isIso

Premises used: CategoryTheory.IsPushout.isIso_inr_of_isIso
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : HasLimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactLimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cone F
hc : IsLimit c
X Y : C
g h : Y ⟶ c.pt
f : c.pt ⟶ X
hf :
  ∀ (j : J), Eq (α := Y ⟶ pushout (c.π.app j) f) (g ≫ f ≫ pushout.inr (c.π.app j) f) (h ≫ f ≫ pushout.inr (c.π.app j) f)
⊢ g ≫ f = h ≫ f

Tactic:
(hc.pushoutOfHasExactLimitsOfShape f).hom_ext (fun j => ?_)

Premises used: CategoryTheory.Limits.IsLimit.pushoutOfHasExactLimitsOfShape, CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : HasLimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactLimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cone F
hc : IsLimit c
X Y : C
g h : Y ⟶ c.pt
f : c.pt ⟶ X
hf :
  ∀ (j : J), Eq (α := Y ⟶ pushout (c.π.app j) f) (g ≫ f ≫ pushout.inr (c.π.app j) f) (h ≫ f ≫ pushout.inr (c.π.app j) f)
refine :
  ∀ (j : J),
    Eq (α := Y ⟶ (pushout c.π (Functor.map (Functor.const J) f)).obj j)
      ((g ≫ f) ≫ NatTrans.app (Cone.π { pt := X, π := pushout.inr c.π (Functor.map (Functor.const J) f) }) j)
      ((h ≫ f) ≫ NatTrans.app (Cone.π { pt := X, π := pushout.inr c.π (Functor.map (Functor.const J) f) }) j)
⊢ g ≫ f = h ≫ f

Tactic:
refine (hc.pushoutOfHasExactLimitsOfShape f).hom_ext (fun j => ?_)

Premises used: CategoryTheory.Limits.IsLimit.pushoutOfHasExactLimitsOfShape, CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : HasLimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactLimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cone F
hc : IsLimit c
X Y : C
g h : Y ⟶ c.pt
f : c.pt ⟶ X
hf :
  ∀ (j : J), Eq (α := Y ⟶ pushout (c.π.app j) f) (g ≫ f ≫ pushout.inr (c.π.app j) f) (h ≫ f ≫ pushout.inr (c.π.app j) f)
j : J
rw :
  Eq (α := Y ⟶ pushout (c.π.app j) (NatTrans.app (Functor.map (Functor.const J) f) j))
    (CategoryStruct.comp (Y := (pushout c.π (Functor.map (Functor.const J) f)).obj j)
        ((g ≫ f) ≫ NatTrans.app (Cone.π { pt := X, π := pushout.inr c.π (Functor.map (Functor.const J) f) }) j :
          Y ⟶ (pushout c.π (Functor.map (Functor.const J) f)).obj j)
        (Iso.hom (pushoutObjIso c.π (Functor.map (Functor.const J) f) j) :
          (pushout c.π (Functor.map (Functor.const J) f)).obj j ⟶
            pushout (c.π.app j) (NatTrans.app (Functor.map (Functor.const J) f) j)) :
      Y ⟶ pushout (c.π.app j) (NatTrans.app (Functor.map (Functor.const J) f) j))
    (CategoryStruct.comp (Y := (pushout c.π (Functor.map (Functor.const J) f)).obj j)
        ((h ≫ f) ≫ NatTrans.app (Cone.π { pt := X, π := pushout.inr c.π (Functor.map (Functor.const J) f) }) j :
          Y ⟶ (pushout c.π (Functor.map (Functor.const J) f)).obj j)
        (Iso.hom (pushoutObjIso c.π (Functor.map (Functor.const J) f) j) :
          (pushout c.π (Functor.map (Functor.const J) f)).obj j ⟶
            pushout (c.π.app j) (NatTrans.app (Functor.map (Functor.const J) f) j)) :
      Y ⟶ pushout (c.π.app j) (NatTrans.app (Functor.map (Functor.const J) f) j))
⊢ Eq (α := Y ⟶ (pushout c.π (Functor.map (Functor.const J) f)).obj j)
    ((g ≫ f) ≫ NatTrans.app (Cone.π { pt := X, π := pushout.inr c.π (Functor.map (Functor.const J) f) }) j)
    ((h ≫ f) ≫ NatTrans.app (Cone.π { pt := X, π := pushout.inr c.π (Functor.map (Functor.const J) f) }) j)

Tactic:
rw [← cancel_mono (pushoutObjIso _ _ _).hom]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.pushoutObjIso, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : HasLimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactLimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cone F
hc : IsLimit c
X Y : C
g h : Y ⟶ c.pt
f : c.pt ⟶ X
hf :
  ∀ (j : J), Eq (α := Y ⟶ pushout (c.π.app j) f) (g ≫ f ≫ pushout.inr (c.π.app j) f) (h ≫ f ≫ pushout.inr (c.π.app j) f)
j : J
⊢ Eq (α := Y ⟶ pushout (c.π.app j) (NatTrans.app (Functor.map (Functor.const J) f) j))
    (CategoryStruct.comp (Y := (pushout c.π (Functor.map (Functor.const J) f)).obj j)
        ((g ≫ f) ≫ NatTrans.app (Cone.π { pt := X, π := pushout.inr c.π (Functor.map (Functor.const J) f) }) j :
          Y ⟶ (pushout c.π (Functor.map (Functor.const J) f)).obj j)
        (Iso.hom (pushoutObjIso c.π (Functor.map (Functor.const J) f) j) :
          (pushout c.π (Functor.map (Functor.const J) f)).obj j ⟶
            pushout (c.π.app j) (NatTrans.app (Functor.map (Functor.const J) f) j)) :
      Y ⟶ pushout (c.π.app j) (NatTrans.app (Functor.map (Functor.const J) f) j))
    (CategoryStruct.comp (Y := (pushout c.π (Functor.map (Functor.const J) f)).obj j)
        ((h ≫ f) ≫ NatTrans.app (Cone.π { pt := X, π := pushout.inr c.π (Functor.map (Functor.const J) f) }) j :
          Y ⟶ (pushout c.π (Functor.map (Functor.const J) f)).obj j)
        (Iso.hom (pushoutObjIso c.π (Functor.map (Functor.const J) f) j) :
          (pushout c.π (Functor.map (Functor.const J) f)).obj j ⟶
            pushout (c.π.app j) (NatTrans.app (Functor.map (Functor.const J) f) j)) :
      Y ⟶ pushout (c.π.app j) (NatTrans.app (Functor.map (Functor.const J) f) j))

Tactic:
simpa using hf j
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasPushouts.{v, u} C
inst_5 : HasLimitsOfShape.{w', w, v, u} J C
inst_6 : HasExactLimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cone F
hc : IsLimit c
X Y : C
g : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), Eq (α := Y ⟶ pushout (c.π.app j) f) (g ≫ f ≫ pushout.inr (c.π.app j) f) 0
this : g ≫ f = 0 ≫ f
⊢ g ≫ f = 0

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasPushouts.{v, u} C
inst_5 : HasLimitsOfShape.{w', w, v, u} J C
inst_6 : HasExactLimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cone F
hc : IsLimit c
X Y : C
g : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), Eq (α := Y ⟶ pushout (c.π.app j) f) (g ≫ f ≫ pushout.inr (c.π.app j) f) 0
suffices : g ≫ f = 0 ≫ f
⊢ g ≫ f = 0

Tactic:
suffices g ≫ f = 0 ≫ f by simpa
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasPushouts.{v, u} C
inst_5 : HasLimitsOfShape.{w', w, v, u} J C
inst_6 : HasExactLimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cone F
hc : IsLimit c
X Y : C
g : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), Eq (α := Y ⟶ pushout (c.π.app j) f) (g ≫ f ≫ pushout.inr (c.π.app j) f) 0
⊢ ∀ (j : J), Eq (α := Y ⟶ pushout (c.π.app j) f) (g ≫ f ≫ pushout.inr (c.π.app j) f) (0 ≫ f ≫ pushout.inr (c.π.app j) f)

Tactic:
simpa using hf
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasPushouts.{v, u} C
inst_5 : HasLimitsOfShape.{w', w, v, u} J C
inst_6 : HasExactLimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cone F
hc : IsLimit c
X Y : C
g : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), Eq (α := Y ⟶ pushout (c.π.app j) f) (g ≫ f ≫ pushout.inr (c.π.app j) f) 0
⊢ g ≫ f = 0 ≫ f

Tactic:
exact hc.pushout_hom_ext (by simpa using hf)

Premises used: CategoryTheory.Limits.IsLimit.pushout_hom_ext
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
inst_3 : HasFiniteLimits.{v, u} C
⊢ HasExactColimitsOfShape J (Ind.{v, u} C)

Tactic:
HasExactColimitsOfShape.domain_of_functor J (Ind.inclusion C)

Premises used: CategoryTheory.HasExactColimitsOfShape.domain_of_functor, CategoryTheory.Ind.inclusion
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
Goal:
C : Type u
A : Type u₁
K : Type u₂
inst : Category.{v, u} C
inst_1 : Category.{v₁, u₁} A
inst_2 : Category.{v₂, u₂} K
J : GrothendieckTopology.{v, u} C
inst_3 : HasWeakSheafify.{v, v₁, u, u₁} J A
inst_4 : HasFiniteLimits.{v₁, u₁} A
inst_5 : HasColimitsOfShape.{v₂, u₂, v₁, u₁} K A
inst_6 : HasExactColimitsOfShape.{v₁, v₂, u₁, u₂} K A
inst_7 : PreservesColimitsOfShape (C := Sheaf.{v, v₁, u, u₁} J A) K (sheafToPresheaf J A)
⊢ HasExactColimitsOfShape K (Sheaf.{v, v₁, u, u₁} J A)

Tactic:
HasExactColimitsOfShape.domain_of_functor K (sheafToPresheaf J A)

Premises used: CategoryTheory.HasExactColimitsOfShape.domain_of_functor, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
Goal:
C : Type u
A : Type u₁
K : Type u₂
inst : Category.{v, u} C
inst_1 : Category.{v₁, u₁} A
inst_2 : Category.{v₂, u₂} K
J : GrothendieckTopology.{v, u} C
inst_3 : HasWeakSheafify.{v, v₁, u, u₁} J A
inst_4 : HasFiniteColimits.{v₁, u₁} A
inst_5 : HasLimitsOfShape.{v₂, u₂, v₁, u₁} K A
inst_6 : HasExactLimitsOfShape.{v₁, v₂, u₁, u₂} K A
inst_7 : PreservesFiniteColimits (C := Sheaf.{v, v₁, u, u₁} J A) (sheafToPresheaf J A)
⊢ HasExactLimitsOfShape K (Sheaf.{v, v₁, u, u₁} J A)

Tactic:
HasExactLimitsOfShape.domain_of_functor K (sheafToPresheaf J A)

Premises used: CategoryTheory.HasExactLimitsOfShape.domain_of_functor, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
Goal:
C : Type u
A : Type u₁
K_1 : Type u₂
inst : Category.{v, u} C
inst_1 : Category.{v₁, u₁} A
inst_2 : Category.{v₂, u₂} K_1
J : GrothendieckTopology.{v, u} C
inst_3 : HasSheafify.{v, v₁, u, u₁} J A
inst_4 : HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} A
K : Type u₂
⊢ ∀ [inst_5 : Category.{v₂, u₂} K] [IsFiltered.{v₂, u₂} K], HasColimitsOfShape K (Sheaf.{v, v₁, u, u₁} J A)

Tactic:
infer_instance