awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial.{v, u} W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
right :
  ∀ {m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt},
    PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl →
      PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr
⊢ PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inr ∧
    ∀ {m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt},
      PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl →
        PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr

Tactic:
use BinaryCofan.IsColimit.inr_desc H₂ _ _

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.inr_desc
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial.{v, u} W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt
h₁ : PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl
h₂ : PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr
right :
  ∀ (j : Discrete WalkingPair),
    (BinaryCofan.mk f g).ι.app j ≫ m = (BinaryCofan.mk f g).ι.app j ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr
⊢ m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr

Tactic:
apply H₂.hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial.{v, u} W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt
h₁ : PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl
h₂ : PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt)
    ((BinaryCofan.mk f g).ι.app { as := WalkingPair.left } ≫ m)
    ((BinaryCofan.mk f g).ι.app { as := WalkingPair.left } ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr)

Tactic:
h₁.trans (H₂.fac (BinaryCofan.mk s.inl s.inr) ⟨WalkingPair.left⟩).symm

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.PushoutCocone.inr, CategoryTheory.Limits.PushoutCocone.inl, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryCofan.mk, CategoryTheory.Limits.WalkingPair.left, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial.{v, u} W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt
h₁ : PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl
h₂ : PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt)
    ((BinaryCofan.mk f g).ι.app { as := WalkingPair.left } ≫ m)
    ((BinaryCofan.mk f g).ι.app { as := WalkingPair.left } ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr)

Tactic:
exact h₁.trans (H₂.fac (BinaryCofan.mk s.inl s.inr) ⟨WalkingPair.left⟩).symm

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.PushoutCocone.inr, CategoryTheory.Limits.PushoutCocone.inl, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryCofan.mk, CategoryTheory.Limits.WalkingPair.left, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial.{v, u} W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt
h₁ : PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl
h₂ : PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶ s.pt)
    ((BinaryCofan.mk f g).ι.app { as := WalkingPair.right } ≫ m)
    ((BinaryCofan.mk f g).ι.app { as := WalkingPair.right } ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr)

Tactic:
h₂.trans (H₂.fac (BinaryCofan.mk s.inl s.inr) ⟨WalkingPair.right⟩).symm

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.PushoutCocone.inr, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.PushoutCocone.inl, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryCofan.mk, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial.{v, u} W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt
h₁ : PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl
h₂ : PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶ s.pt)
    ((BinaryCofan.mk f g).ι.app { as := WalkingPair.right } ≫ m)
    ((BinaryCofan.mk f g).ι.app { as := WalkingPair.right } ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr)

Tactic:
exact h₂.trans (H₂.fac (BinaryCofan.mk s.inl s.inr) ⟨WalkingPair.right⟩).symm

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.PushoutCocone.inr, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.PushoutCocone.inl, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryCofan.mk, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasPushouts.{v, u} C
⊢ HasBinaryCoproducts.{v, u} C

Tactic:
{ has_colimit := fun F => HasColimit.mk (colimitCoconeOfInitialAndPushouts F) }

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.Limits.HasColimit.mk, colimitCoconeOfInitialAndPushouts
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
inst_2 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst_5 : PreservesColimitsOfShape WalkingSpan F
K : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
hc :
  IsColimit (F :=
    span (X := F.obj (initial.{v, u} C)) (F.map (initial.to (K.obj { as := WalkingPair.left })))
      (F.map (initial.to (K.obj { as := WalkingPair.right }))))
    (PushoutCocone.mk
        ((F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone).ι.app
          { as := WalkingPair.left : Discrete WalkingPair })
        ((F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone).ι.app { as := WalkingPair.right }) ⋯ :
      PushoutCocone (X := F.obj (initial.{v, u} C)) (F.map (initial.to (K.obj { as := WalkingPair.left })))
        (F.map (initial.to (K.obj { as := WalkingPair.right }))))
f : F.obj (initial.{v, u} C) ⟶ (K ⋙ F).obj { as := WalkingPair.left }
g : F.obj (initial.{v, u} C) ⟶ (K ⋙ F).obj { as := WalkingPair.right }
⊢ IsColimit (F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone)

Tactic:
apply
        isBinaryCoproductOfIsInitialIsPushout _ _
          (isColimitOfHasInitialOfPreservesColimit F)

Premises used: isBinaryCoproductOfIsInitialIsPushout, CategoryTheory.Limits.isColimitOfHasInitialOfPreservesColimit
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasPushouts.{v, u} C
X Y : C
inst_3 : HasBinaryCoproduct.{v, u} X Y
⊢ Eq.{v + 1} (α := X ⟶ pushout.{v, u} (X := initial.{v, u} C) (initial.to X) (initial.to Y))
    (CategoryStruct.comp (Y := coprod.{v, u} X Y) coprod.inl (Iso.hom (coprodIsoPushout X Y)) :
      X ⟶ pushout.{v, u} (X := initial.{v, u} C) (initial.to X) (initial.to Y))
    (pushout.inl (initial.to X) (initial.to Y) :
      X ⟶ pushout.{v, u} (X := initial.{v, u} C) (initial.to X) (initial.to Y))

Tactic:
colimit.isoColimitCocone_ι_hom (colimitCoconeOfInitialAndPushouts _) _

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.colimit, colimitCoconeOfInitialAndPushouts, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape, CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasPushouts.{v, u} C
X Y : C
inst_3 : HasBinaryCoproduct.{v, u} X Y
⊢ Eq.{v + 1} (α := Y ⟶ pushout.{v, u} (X := initial.{v, u} C) (initial.to X) (initial.to Y))
    (CategoryStruct.comp (Y := coprod.{v, u} X Y) coprod.inr (Iso.hom (coprodIsoPushout X Y)) :
      Y ⟶ pushout.{v, u} (X := initial.{v, u} C) (initial.to X) (initial.to Y))
    (pushout.inr (initial.to X) (initial.to Y) :
      Y ⟶ pushout.{v, u} (X := initial.{v, u} C) (initial.to X) (initial.to Y))

Tactic:
colimit.isoColimitCocone_ι_hom (colimitCoconeOfInitialAndPushouts _) _

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.colimit, colimitCoconeOfInitialAndPushouts, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape, CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasPushouts.{v, u} C
X Y : C
inst_3 : HasBinaryCoproduct.{v, u} X Y
⊢ Eq.{v + 1} (α := X ⟶ coprod.{v, u} X Y)
    (CategoryStruct.comp (Y := pushout.{v, u} (X := initial.{v, u} C) (initial.to X) (initial.to Y))
      (pushout.inl (initial.to X) (initial.to Y) :
        X ⟶ pushout.{v, u} (X := initial.{v, u} C) (initial.to X) (initial.to Y))
      (Iso.inv (coprodIsoPushout X Y) :
        pushout.{v, u} (X := initial.{v, u} C) (initial.to X) (initial.to Y) ⟶ coprod.{v, u} X Y))
    coprod.inl

Tactic:
colimit.isoColimitCocone_ι_inv (colimitCoconeOfInitialAndPushouts (pair X Y)) ⟨.left⟩

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv, CategoryTheory.Discrete.functor, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.mk, CategoryTheory.Limits.pair, colimitCoconeOfInitialAndPushouts, CategoryTheory.Limits.WalkingPair.left, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasPushouts.{v, u} C
X Y : C
inst_3 : HasBinaryCoproduct.{v, u} X Y
⊢ Eq.{v + 1} (α := Y ⟶ coprod.{v, u} X Y)
    (CategoryStruct.comp (Y := pushout.{v, u} (X := initial.{v, u} C) (initial.to X) (initial.to Y))
      (pushout.inr (initial.to X) (initial.to Y) :
        Y ⟶ pushout.{v, u} (X := initial.{v, u} C) (initial.to X) (initial.to Y))
      (Iso.inv (coprodIsoPushout X Y) :
        pushout.{v, u} (X := initial.{v, u} C) (initial.to X) (initial.to Y) ⟶ coprod.{v, u} X Y))
    coprod.inr

Tactic:
colimit.isoColimitCocone_ι_inv (colimitCoconeOfInitialAndPushouts (pair X Y)) ⟨.right⟩

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv, CategoryTheory.Discrete.functor, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.mk, CategoryTheory.Limits.pair, colimitCoconeOfInitialAndPushouts, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : PreservesLimit (cospan f f) F
inst_3 : Mono f
have :
  ∀
    (this :
      have this : F.map (𝟙 X) ≫ F.map f = F.map (𝟙 X) ≫ F.map f := ⋯;
      IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) this)),
    Mono (F.map f)
⊢ Mono (F.map f)

Tactic:
have := isLimitPullbackConeMapOfIsLimit F _ (PullbackCone.isLimitMkIdId f)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : PreservesLimit (cospan f f) F
inst_3 : Mono f
this :
  have this : F.map (𝟙 X) ≫ F.map f = F.map (𝟙 X) ≫ F.map f := ⋯;
  IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) this)
simp_rw :
  ∀ (this : IsLimit (F := cospan (F.map f) (F.map f)) (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)), Mono (F.map f)
⊢ Mono (F.map f)

Tactic:
simp_rw [F.map_id] at this

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : PreservesLimit (cospan f f) F
inst_3 : Mono f
this : IsLimit (F := cospan (F.map f) (F.map f)) (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)
⊢ Mono (F.map f)

Tactic:
apply PullbackCone.mono_of_isLimitMkIdId _ this

Premises used: CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : ReflectsLimit (cospan f f) F
inst_3 : Mono (F.map f)
have :
  ∀ (this : IsLimit.{0, v₂, 0, u₂} (F := cospan (F.map f) (F.map f)) (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)),
    Mono f
⊢ Mono f

Tactic:
have := PullbackCone.isLimitMkIdId (F.map f)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : ReflectsLimit (cospan f f) F
inst_3 : Mono (F.map f)
this : IsLimit.{0, v₂, 0, u₂} (F := cospan (F.map f) (F.map f)) (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)
simp_rw : ∀ (this : IsLimit (F := cospan (F.map f) (F.map f)) (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) ⋯)), Mono f
⊢ Mono f

Tactic:
simp_rw [← F.map_id] at this

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : ReflectsLimit (cospan f f) F
inst_3 : Mono (F.map f)
this : IsLimit (F := cospan (F.map f) (F.map f)) (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) ⋯)
⊢ Mono f

Tactic:
apply PullbackCone.mono_of_isLimitMkIdId _ (isLimitOfIsLimitPullbackConeMap F _ this)

Premises used: CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId, CategoryTheory.Limits.isLimitOfIsLimitPullbackConeMap
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : PreservesColimit (span f f) F
inst_3 : Epi f
have :
  ∀ (this : IsColimit (F := span (F.map f) (F.map f)) (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)), Epi (F.map f)
⊢ Epi (F.map f)

Tactic:
have := isColimitPushoutCoconeMapOfIsColimit F _ (PushoutCocone.isColimitMkIdId f)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : PreservesColimit (span f f) F
inst_3 : Epi f
this : IsColimit (F := span (F.map f) (F.map f)) (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)
simp_rw :
  ∀ (this : IsColimit.{0, v₂, 0, u₂} (F := span (F.map f) (F.map f)) (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)),
    Epi (F.map f)
⊢ Epi (F.map f)

Tactic:
simp_rw [F.map_id] at this

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : PreservesColimit (span f f) F
inst_3 : Epi f
this : IsColimit.{0, v₂, 0, u₂} (F := span (F.map f) (F.map f)) (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)
⊢ Epi (F.map f)

Tactic:
apply PushoutCocone.epi_of_isColimitMkIdId _ this

Premises used: CategoryTheory.Limits.PushoutCocone.epi_of_isColimitMkIdId
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : ReflectsColimit (span f f) F
inst_3 : Epi (F.map f)
have :
  ∀ (this : IsColimit.{0, v₂, 0, u₂} (F := span (F.map f) (F.map f)) (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)),
    Epi f
⊢ Epi f

Tactic:
have := PushoutCocone.isColimitMkIdId (F.map f)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : ReflectsColimit (span f f) F
inst_3 : Epi (F.map f)
this : IsColimit.{0, v₂, 0, u₂} (F := span (F.map f) (F.map f)) (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)
simp_rw : ∀ (this : IsColimit (F := span (F.map f) (F.map f)) (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)), Epi f
⊢ Epi f

Tactic:
simp_rw [← F.map_id] at this

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : ReflectsColimit (span f f) F
inst_3 : Epi (F.map f)
this : IsColimit (F := span (F.map f) (F.map f)) (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)
⊢ Epi f

Tactic:
apply
    PushoutCocone.epi_of_isColimitMkIdId _
      (isColimitOfIsColimitPushoutCoconeMap F _ this)

Premises used: CategoryTheory.Limits.PushoutCocone.epi_of_isColimitMkIdId, CategoryTheory.Limits.isColimitOfIsColimitPushoutCoconeMap
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ Eq (α :=
    pullback (Z := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ⟶
      F.obj WalkingParallelPair.zero)
    (CategoryStruct.comp (Y := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
      (pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      prod.fst)
    (CategoryStruct.comp (Y := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
      (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))
      prod.fst)

Tactic:
(eq_whisker pullback.condition Limits.prod.fst :
      (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) = _)

Premises used: CategoryTheory.eq_whisker, CategoryTheory.Limits.prod.fst, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
h :
  Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) (pullbackFst F)
    (CategoryStruct.comp (Y := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
      (pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      prod.fst)
h₁ :
  Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.zero)
    (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)))
    (CategoryStruct.comp (Y := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
      (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))
      prod.fst)
⊢ Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) (pullbackFst F)
    (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)))

Tactic:
convert!
    (eq_whisker pullback.condition Limits.prod.fst :
      (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) = _)

Premises used: CategoryTheory.eq_whisker, CategoryTheory.Limits.prod.fst, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) (pullbackFst F)
    (CategoryStruct.comp (Y := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
      (pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      prod.fst)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.zero)
    (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)))
    (CategoryStruct.comp (Y := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
      (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))
      prod.fst)

Tactic:
simp