awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected (goal)
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
have 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)
Tactic: refine (hc.pullbackOfHasExactColimitsOfShape f).hom_ext (fun j => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected (goal)
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.ι (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)
have 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)
Tactic: rw [← cancel_epi (pullbackObjIso _ _ _).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected (goal)
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 = 0
have suffices : f ≫ g = f ≫ 0
Tactic: suffices f ≫ g = f ≫ 0 by simpa
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected (goal)
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
⊢ IsLimit (F := pushout c.π (Functor.map (Functor.const J) f))
    { pt := X, π := pushout.inr c.π (Functor.map (Functor.const J) f) }
have 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)))
Tactic: suffices IsIso (limMap (pushout.inr c.π ((Functor.const J).map f))) from
    Cone.isLimitOfIsIsoLimMapπ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected (hypothesis)
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
⊢ 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)))
have hpush : 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))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected (hypothesis)
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) X)) (Y :=
    limit (pushout c.π (Functor.map (Functor.const J) f))) (limMap (pushout.inr c.π (Functor.map (Functor.const J) f)))
have this : IsIso (X := limit.{w', w, v, u} (Functor.obj (Functor.const J) c.pt)) (Y := limit F) (limMap c.π)
Tactic: have := hc.isIso_limMap_π
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected (goal)
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
have 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)
Tactic: refine (hc.pushoutOfHasExactLimitsOfShape f).hom_ext (fun j => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected (goal)
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.π (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)
have 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))
Tactic: rw [← cancel_mono (pushoutObjIso _ _ _).hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected (goal)
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
have suffices : g ≫ f = 0 ≫ f
Tactic: suffices g ≫ f = 0 ≫ f by simpa
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
⊢ IsGrothendieckAbelian.{w, v₂, u₂} D
have hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
Tactic: have hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D :=
    ⟨fun _ _ _ => Adjunction.hasColimitsOfShape_of_equivalence α.inverse⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ IsGrothendieckAbelian.{w, v₂, u₂} D
have refine_1 : LocallySmall.{w, v₂, u₂} D
Tactic: refine ⟨?_, hasFilteredColimits, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
refine_1 : LocallySmall.{w, v₂, u₂} D
⊢ IsGrothendieckAbelian.{w, v₂, u₂} D
have refine_2 : AB5OfSize.{w, w, v₂, u₂} D
Tactic: refine ⟨?_, hasFilteredColimits, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
refine_1 : LocallySmall.{w, v₂, u₂} D
refine_2 : AB5OfSize.{w, w, v₂, u₂} D
⊢ IsGrothendieckAbelian.{w, v₂, u₂} D
have refine_3 : HasSeparator.{v₂, u₂} D
Tactic: refine ⟨?_, hasFilteredColimits, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ AB5OfSize.{w, w, v₂, u₂} D
have refine_2 : ∀ (x : Type w) (x_1 : Category.{w, w} x) (x_2 : IsFiltered x), HasExactColimitsOfShape.{v₂, w, u₂, w} x D
Tactic: refine ⟨fun _ _ _ => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{w, v, u} C
⊢ AB4OfSize.{w, v, u} C
have this : HasFiniteBiproducts.{v, u} C
Tactic: have : HasFiniteBiproducts C := HasFiniteBiproducts.of_hasFiniteProducts
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
t₁ t₂ : Under j₀
f : t₁ ⟶ t₂
⊢ Functor.map (Functor.obj (Functor.const (Under j₀)) X) f ≫ y ≫ Y.map t₂.hom =
    (y ≫ Y.map t₁.hom) ≫ (Under.forget j₀ ⋙ Y).map f
have dsimp : 𝟙 X ≫ y ≫ Y.map t₂.hom = (y ≫ Y.map t₁.hom) ≫ Y.map (Under.Hom.right f)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
⊢ ∃ (j : J) (φ : j₀ ⟶ j), y ≫ Y.map φ = 0
have this : IsFiltered J
Tactic: have := isFiltered_of_isCardinalFiltered J κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
⊢ ∃ (j : J) (φ : j₀ ⟶ j), y ≫ Y.map φ = 0
have obtain : ∀ (j : Under j₀) (h : IsIso ((F y).obj j).obj (P := Over.isMono X).hom), ∃ (j : J) (φ : j₀ ⟶ j), y ≫ Y.map φ = 0
Tactic: obtain ⟨j, h⟩ := exists_isIso_of_functor_from_monoOver (F y) hXκ _
      (colimit.isColimit (kernel (g y))) (f y) (fun j ↦ by simpa using hf y j)
      (epi_f hc hy)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
j : Under j₀
h : IsIso (X := (kernel (g y)).obj j) (NatTrans.app (kernel.ι (g y)) j)
⊢ ∃ (j : J) (φ : j₀ ⟶ j), y ≫ Y.map φ = 0
have refine : y ≫ Y.map j.hom = 0
Tactic: refine ⟨j.right, j.hom, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
⊢ (y₁ - y₂) ≫ c.ι.app j₀ = 0
have rw : y₁ ≫ c.ι.app j₀ - y₂ ≫ c.ι.app j₀ = 0
Tactic: rw [Preadditive.sub_comp, sub_eq_zero, hy]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
rw : y₁ ≫ c.ι.app j₀ - y₂ ≫ c.ι.app j₀ = 0
rw₁ : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
⊢ (y₁ - y₂) ≫ c.ι.app j₀ = 0
have rw₂ : y₂ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
Tactic: rw [Preadditive.sub_comp, sub_eq_zero, hy]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
⊢ ∃ (j : J) (φ : j₀ ⟶ j), y₁ ≫ Y.map φ = y₂ ≫ Y.map φ
have obtain : ∀ (j : J) (φ : j₀ ⟶ j) (hφ : (y₁ - y₂) ≫ Y.map φ = 0), ∃ (j : J) (φ : j₀ ⟶ j), y₁ ≫ Y.map φ = y₂ ≫ Y.map φ
Tactic: obtain ⟨j, φ, hφ⟩ := injectivity₀ hc hXκ (y₁ - y₂)
    (by rw [Preadditive.sub_comp, sub_eq_zero, hy])
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst_4 : IsFiltered J
⊢ IsIso (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
    (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)
have refine_1 : Arrow.mk (X := Functor.obj colim (pullback c.ι (Functor.map (Functor.const J) z)))
    (Functor.map colim (pullback.snd c.ι (Functor.map (Functor.const J) z))) ≅
  Arrow.mk (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
    (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)
Tactic: refine ((MorphismProperty.isomorphisms C).arrow_mk_iso_iff ?_).1
    (MorphismProperty.of_isPullback
      ((IsPullback.of_hasPullback c.ι ((Functor.const _).map z)).map colim) ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst_4 : IsFiltered J
refine_1 :
  Arrow.mk (X := Functor.obj colim (pullback c.ι (Functor.map (Functor.const J) z)))
      (Functor.map colim (pullback.snd c.ι (Functor.map (Functor.const J) z))) ≅
    Arrow.mk (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
      (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)
⊢ IsIso (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
    (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)
have refine_2 : MorphismProperty.isomorphisms C (X := Functor.obj colim Y) (Functor.map colim c.ι)
Tactic: refine ((MorphismProperty.isomorphisms C).arrow_mk_iso_iff ?_).1
    (MorphismProperty.of_isPullback
      ((IsPullback.of_hasPullback c.ι ((Functor.const _).map z)).map colim) ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst_4 : IsFiltered J
⊢ Arrow.mk (X := Functor.obj colim (pullback c.ι (Functor.map (Functor.const J) z)))
      (Functor.map colim (pullback.snd c.ι (Functor.map (Functor.const J) z))) ≅
    Arrow.mk (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
      (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)
have refine_1 : Iso.hom
      (Iso.refl
        (Arrow.mk (X := Functor.obj colim (pullback c.ι (Functor.map (Functor.const J) z)))
            (Functor.map colim (pullback.snd c.ι (Functor.map (Functor.const J) z)))).left) ≫
    (Arrow.mk (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
        (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)).hom =
  (Arrow.mk (X := Functor.obj colim (pullback c.ι (Functor.map (Functor.const J) z)))
        (Functor.map colim (pullback.snd c.ι (Functor.map (Functor.const J) z)))).hom ≫
    Iso.hom
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Functor.obj (Functor.const J) X))
        (isColimitConstCocone J X))
Tactic: refine Arrow.isoMk (Iso.refl _)
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (isColimitConstCocone J X)) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst_4 : IsFiltered J
⊢ Iso.hom
        (Iso.refl
          (Arrow.mk (X := Functor.obj colim (pullback c.ι (Functor.map (Functor.const J) z)))
              (Functor.map colim (pullback.snd c.ι (Functor.map (Functor.const J) z)))).left) ≫
      (Arrow.mk (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
          (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)).hom =
    (Arrow.mk (X := Functor.obj colim (pullback c.ι (Functor.map (Functor.const J) z)))
          (Functor.map colim (pullback.snd c.ι (Functor.map (Functor.const J) z)))).hom ≫
      Iso.hom
        (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Functor.obj (Functor.const J) X))
          (isColimitConstCocone J X))
have refine_1 : 𝟙 (colimit (pullback c.ι (Functor.map (Functor.const J) z))) ≫ f z =
  CategoryStruct.comp (Y := colimit.{w, w, v, u} (Functor.obj (Functor.const J) X))
    (colimMap (pullback.snd c.ι (Functor.map (Functor.const J) z)))
    (Iso.hom
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Functor.obj (Functor.const J) X))
        (isColimitConstCocone J X)))
Tactic: dsimp