awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₁, u₂} D
inst_3 : HasZeroMorphisms.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
inst_4 : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ Iso.hom
        (Iso.refl
          (Cone.pt (F :=
            parallelPair (X := F.obj Y) (Y := F.obj (F.objPreimage (@NormalMono.Z _ _ _ _ inst_3 (F.map f) _)))
              (F.map
                (F.preimage (NormalMono.g ≫ Iso.inv (F.objObjPreimageIso (@NormalMono.Z _ _ _ _ inst_3 (F.map f) _)))))
              0)
            (KernelFork.ofι (Z :=
              Cone.pt (F := parallelPair (X := F.obj Y) (Y := @NormalMono.Z _ _ _ _ inst_3 (F.map f) _) NormalMono.g 0)
                (KernelFork.ofι (F.map f) ⋯))
              (Fork.ι (KernelFork.ofι (F.map f) ⋯)) ⋯))) ≫
      Fork.ι
        (Functor.obj (C :=
          Cone
            (parallelPair (X := Y) (Y := F.objPreimage (@NormalMono.Z _ _ _ _ inst_3 (F.map f) _))
                (F.preimage (NormalMono.g ≫ Iso.inv (F.objObjPreimageIso (@NormalMono.Z _ _ _ _ inst_3 (F.map f) _))))
                0 ⋙
              F))
          (Equivalence.functor (Cone.postcomposeEquivalence (compNatIso F))) (F.mapCone (KernelFork.ofι f ⋯))) =
    Fork.ι
      (KernelFork.ofι (Z :=
        Cone.pt (F := parallelPair (X := F.obj Y) (Y := @NormalMono.Z _ _ _ _ inst_3 (F.map f) _) NormalMono.g 0)
          (KernelFork.ofι (F.map f) ⋯))
        (Fork.ι (KernelFork.ofι (F.map f) ⋯)) ⋯)

Tactic:
simp [compNatIso, Fork.ι]

Premises used: CategoryTheory.Limits.compNatIso, CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
f : X ⟶ Y
I : NormalMono f
⊢ Eq (α := X ⟶ @Z _ _ _ _ inst_1 f _) (f ≫ g) (f ≫ 0)

Tactic:
simpa using I.w

Premises used: CategoryTheory.NormalMono.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
f : X ⟶ Y
I : NormalMono f
⊢ IsRegularMono f

Tactic:
⟨⟨I.regularMono⟩⟩

Premises used: CategoryTheory.NormalMono.regularMono, Nonempty.intro, CategoryTheory.IsRegularMono.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
W : C
h' : S ⟶ W
⊢ f ≫ h ≫ h' = g ≫ k ≫ h'

Tactic:
simp only [← Category.assoc, eq_whisker comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ ∀ {W : C} (h' : S ⟶ W), f ≫ h ≫ h' = g ≫ k ≫ h'

Tactic:
have reassoc' {W : C} (h' : S ⟶ W) : f ≫ h ≫ h' = g ≫ k ≫ h' := by
      simp only [← Category.assoc, eq_whisker comm]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
reassoc' : ∀ {W : C} (h' : S ⟶ W), f ≫ h ≫ h' = g ≫ k ≫ h'
rw : Eq (α := P ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) (f ≫ h ≫ NormalMono.g) 0
rw₁ : Eq (α := P ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) (f ≫ 0) 0
rw₂ rw₃ : Eq.{v₁ + 1} (α := P ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) 0 0
⊢ Eq (α := P ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) (g ≫ k ≫ NormalMono.g) 0

Tactic:
rw [← reassoc', hn.w, HasZeroMorphisms.comp_zero]

Premises used: CategoryTheory.NormalMono.w, CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
gr : RegularMono g := regularOfIsPullbackSndOfRegular (NormalMono.regularMono h) comm t
⊢ Eq (α := R ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) 0 (k ≫ 0)

Tactic:
have q := (HasZeroMorphisms.comp_zero k hn.Z).symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
gr : RegularMono g := regularOfIsPullbackSndOfRegular (NormalMono.regularMono h) comm t
q : Eq (α := R ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) 0 (k ≫ 0)
⊢ IsLimit (F := parallelPair (Y := @NormalMono.Z _ _ _ _ inst_1 h _) (k ≫ NormalMono.g) 0) (KernelFork.ofι g ⋯)

Tactic:
convert! gr.isLimit

Premises used: CategoryTheory.RegularMono.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ Arrow.Hom.left e.inv ≫ (Arrow.mk f).hom = (Arrow.mk f').hom ≫ Arrow.Hom.right e.inv

Tactic:
have := Arrow.w e.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
this : Arrow.Hom.left e.inv ≫ f = f' ≫ Arrow.Hom.right e.inv
rw : Eq (α := X' ⟶ @Z _ _ _ _ inst_1 f _) (Arrow.Hom.left e.inv ≫ f ≫ g) 0
rw₁ : Eq (α := X' ⟶ @Z _ _ _ _ inst_1 f _) (Arrow.Hom.left e.inv ≫ 0) 0
rw₂ rw₃ : Eq.{v₁ + 1} (α := X' ⟶ @Z _ _ _ _ inst_1 f _) 0 0
⊢ Eq (α := X' ⟶ @Z _ _ _ _ inst_1 f _) (f' ≫ Arrow.Hom.right e.inv ≫ g) 0

Tactic:
rw [← reassoc_of% this, hf.w, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.NormalMono.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
refine_1 :
  parallelPair (X := Y) (Y := @Z _ _ _ _ inst_1 f _) g 0 ≅
    parallelPair (Y := @Z _ _ _ _ inst_1 f _) (Arrow.Hom.right e.inv ≫ g) 0
refine_2 :
  Functor.obj
      (Cone.postcompose
        (Iso.hom
          (parallelPair.ext (Functor.mapIso Arrow.rightFunc e)
            (Iso.refl
              (Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := Y) (Y := @Z _ _ _ _ inst_1 f _) g 0)
                WalkingParallelPair.one))
            ⋯ ⋯)))
      (KernelFork.ofι f ⋯) ≅
    KernelFork.ofι f' ⋯
⊢ IsLimit (KernelFork.ofι f' ⋯)

Tactic:
refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).1 hf.isLimit

Premises used: CategoryTheory.NormalMono.isLimit, Equiv.toFun, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ parallelPair (X := Y) (Y := @Z _ _ _ _ inst_1 f _) g 0 ≅
    parallelPair (Y := @Z _ _ _ _ inst_1 f _) (Arrow.Hom.right e.inv ≫ g) 0

Tactic:
exact parallelPair.ext (Arrow.rightFunc.mapIso e) (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.parallelPair.ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ Functor.obj
      (Cone.postcompose
        (Iso.hom
          (parallelPair.ext (Functor.mapIso Arrow.rightFunc e)
            (Iso.refl
              (Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := Y) (Y := @Z _ _ _ _ inst_1 f _) g 0)
                WalkingParallelPair.one))
            ⋯ ⋯)))
      (KernelFork.ofι f ⋯) ≅
    KernelFork.ofι f' ⋯

Tactic:
exact Fork.ext (Arrow.leftFunc.mapIso e)

Premises used: CategoryTheory.Limits.Fork.ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : IsNormalMonoCategory.{v₁, u₁} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Mono f
haveI : ∀ (this : NormalMono f), IsRegularMono f
⊢ IsRegularMono f

Tactic:
haveI := normalMonoOfMono f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : IsNormalMonoCategory.{v₁, u₁} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Mono f
this : NormalMono f
⊢ IsRegularMono f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₁, u₂} D
inst_3 : HasZeroMorphisms.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
inst_4 : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ Eq (α := F.obj (F.objPreimage (@NormalEpi.W _ _ _ _ inst_3 (F.map f) _)) ⟶ F.obj Y)
    (F.map (F.preimage (Iso.hom (F.objObjPreimageIso (@NormalEpi.W _ _ _ _ inst_3 (F.map f) _)) ≫ NormalEpi.g) ≫ f))
    (F.map 0)

Tactic:
simp [hf.w]

Premises used: CategoryTheory.NormalEpi.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₁, u₂} D
inst_3 : HasZeroMorphisms.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
inst_4 : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ Eq (α := @NormalEpi.W _ _ _ _ inst_3 (F.map f) _ ⟶ F.obj X)
    (CategoryStruct.comp (Y := F.obj (F.objPreimage (@NormalEpi.W _ _ _ _ inst_3 (F.map f) _)))
      (Iso.hom (Iso.symm (F.objObjPreimageIso (@NormalEpi.W _ _ _ _ inst_3 (F.map f) _))))
      (F.map (F.preimage (Iso.hom (F.objObjPreimageIso (@NormalEpi.W _ _ _ _ inst_3 (F.map f) _)) ≫ NormalEpi.g))))
    NormalEpi.g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₁, u₂} D
inst_3 : HasZeroMorphisms.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
inst_4 : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ Cofork.π
        (CokernelCofork.ofπ (Z :=
          Cocone.pt (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_3 (F.map f) _) NormalEpi.g 0)
            (CokernelCofork.ofπ (F.map f) ⋯))
          (Cofork.π (CokernelCofork.ofπ (F.map f) ⋯)) ⋯) ≫
      Iso.hom
        (Iso.refl
          (Cocone.pt (F :=
            parallelPair (X := F.obj (F.objPreimage (@NormalEpi.W _ _ _ _ inst_3 (F.map f) _)))
              (F.map
                (F.preimage (Iso.hom (F.objObjPreimageIso (@NormalEpi.W _ _ _ _ inst_3 (F.map f) _)) ≫ NormalEpi.g)))
              0)
            (CokernelCofork.ofπ (Z :=
              Cocone.pt (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_3 (F.map f) _) NormalEpi.g 0)
                (CokernelCofork.ofπ (F.map f) ⋯))
              (Cofork.π (CokernelCofork.ofπ (F.map f) ⋯)) ⋯))) =
    Cofork.π
      (Functor.obj (C :=
        Cocone
          (parallelPair (X := F.objPreimage (@NormalEpi.W _ _ _ _ inst_3 (F.map f) _))
              (F.preimage (Iso.hom (F.objObjPreimageIso (@NormalEpi.W _ _ _ _ inst_3 (F.map f) _)) ≫ NormalEpi.g)) 0 ⋙
            F))
        (Equivalence.functor (Cocone.precomposeEquivalence (compNatIso F))) (F.mapCocone (CokernelCofork.ofπ f ⋯)))

Tactic:
simp [compNatIso, Cofork.π]

Premises used: CategoryTheory.Limits.compNatIso, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
f : X ⟶ Y
I : NormalEpi f
⊢ Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y) (g ≫ f) (0 ≫ f)

Tactic:
simpa using I.w

Premises used: CategoryTheory.NormalEpi.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
f : X ⟶ Y
I : NormalEpi f
⊢ IsRegularEpi f

Tactic:
⟨⟨I.regularEpi⟩⟩

Premises used: CategoryTheory.NormalEpi.regularEpi, Nonempty.intro, CategoryTheory.IsRegularEpi.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
W : C
h' : R ⟶ W
rw : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) ((NormalEpi.g ≫ g) ≫ h') (0 ≫ h')
rw₁ rw₂ : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) (0 ≫ h') (0 ≫ h')
⊢ Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) (NormalEpi.g ≫ g ≫ h') (0 ≫ h')

Tactic:
rw [← Category.assoc, eq_whisker gn.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker, CategoryTheory.NormalEpi.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ ∀ {W : C} (h' : R ⟶ W), Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) (NormalEpi.g ≫ g ≫ h') (0 ≫ h')

Tactic:
have reassoc' {W : C} (h' : R ⟶ W) : gn.g ≫ g ≫ h' = 0 ≫ h' := by
      rw [← Category.assoc, eq_whisker gn.w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
reassoc' : ∀ {W : C} (h' : R ⟶ W), Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) (NormalEpi.g ≫ g ≫ h') (0 ≫ h')
rw : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) (NormalEpi.g ≫ f ≫ h) 0
rw₁ : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) (NormalEpi.g ≫ g ≫ k) 0
rw₂ : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) (0 ≫ k) 0
rw₃ rw₄ : Eq.{v₁ + 1} (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) 0 0
⊢ Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) ((NormalEpi.g ≫ f) ≫ h) 0

Tactic:
rw [Category.assoc, comm, reassoc', zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
hn : RegularEpi h := regularOfIsPushoutSndOfRegular (NormalEpi.regularEpi g) comm t
⊢ Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ Q) 0 (0 ≫ f)

Tactic:
have q := (@zero_comp _ _ _ gn.W _ _ f).symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
hn : RegularEpi h := regularOfIsPushoutSndOfRegular (NormalEpi.regularEpi g) comm t
q : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ Q) 0 (0 ≫ f)
⊢ IsColimit (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 g _) (NormalEpi.g ≫ f) 0) (CokernelCofork.ofπ h ⋯)

Tactic:
convert! hn.isColimit

Premises used: CategoryTheory.RegularEpi.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ Arrow.Hom.left e.hom ≫ (Arrow.mk f').hom = (Arrow.mk f).hom ≫ Arrow.Hom.right e.hom

Tactic:
have := Arrow.w e.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
this : Arrow.Hom.left e.hom ≫ f' = f ≫ Arrow.Hom.right e.hom
rw : Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') (g ≫ Arrow.Hom.left e.hom ≫ f') 0
rw₁ : Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') (g ≫ f ≫ Arrow.Hom.right e.hom) 0
rw₂ : Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') (0 ≫ Arrow.Hom.right e.hom) 0
rw₃ rw₄ : Eq.{v₁ + 1} (α := @W _ _ _ _ inst_1 f _ ⟶ Y') 0 0
⊢ Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') ((g ≫ Arrow.Hom.left e.hom) ≫ f') 0

Tactic:
rw [Category.assoc, this, reassoc_of% hf.w, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NormalEpi.w, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
refine_1 :
  parallelPair (X := @W _ _ _ _ inst_1 f _) g 0 ≅ parallelPair (X := @W _ _ _ _ inst_1 f _) (g ≫ Arrow.Hom.left e.hom) 0
refine_2 :
  Functor.obj
      (Cocone.precompose
        (Iso.inv
          (parallelPair.ext
            (Iso.refl
              (Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := @W _ _ _ _ inst_1 f _) g 0) WalkingParallelPair.zero))
            (Functor.mapIso Arrow.leftFunc e) ⋯ ⋯)))
      (CokernelCofork.ofπ f ⋯) ≅
    CokernelCofork.ofπ f' ⋯
⊢ IsColimit (CokernelCofork.ofπ f' ⋯)

Tactic:
refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1 hf.isColimit

Premises used: CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, CategoryTheory.NormalEpi.isColimit, Equiv.toFun
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ parallelPair (X := @W _ _ _ _ inst_1 f _) g 0 ≅ parallelPair (X := @W _ _ _ _ inst_1 f _) (g ≫ Arrow.Hom.left e.hom) 0

Tactic:
exact parallelPair.ext (Iso.refl _) (Arrow.leftFunc.mapIso e)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.parallelPair.ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (F := parallelPair (X := @W _ _ _ _ inst_1 f _) (g ≫ Arrow.Hom.left e.hom) 0)
        (Functor.obj
            (Cocone.precompose
              (Iso.inv
                (parallelPair.ext
                  (Iso.refl
                    (Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := @W _ _ _ _ inst_1 f _) g 0)
                      WalkingParallelPair.zero))
                  (Functor.mapIso Arrow.leftFunc e) ⋯ ⋯)))
            (CokernelCofork.ofπ f ⋯) :
          Cocone (parallelPair (X := @W _ _ _ _ inst_1 f _) (g ≫ Arrow.Hom.left e.hom) 0)))
      (Cofork.π
        (Functor.obj
          (Cocone.precompose
            (Iso.inv
              (parallelPair.ext
                (Iso.refl
                  (Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := @W _ _ _ _ inst_1 f _) g 0) WalkingParallelPair.zero))
                (Functor.mapIso Arrow.leftFunc e) ⋯ ⋯)))
          (CokernelCofork.ofπ f ⋯)))
      (Iso.hom (Functor.mapIso Arrow.rightFunc e)) =
    Cofork.π (CokernelCofork.ofπ f' ⋯)

Tactic:
simp [Cofork.π]

Premises used: CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ Functor.obj
      (Cocone.precompose
        (Iso.inv
          (parallelPair.ext
            (Iso.refl
              (Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := @W _ _ _ _ inst_1 f _) g 0) WalkingParallelPair.zero))
            (Functor.mapIso Arrow.leftFunc e) ⋯ ⋯)))
      (CokernelCofork.ofπ f ⋯) ≅
    CokernelCofork.ofπ f' ⋯

Tactic:
exact Cofork.ext (Arrow.rightFunc.mapIso e) (by simp [Cofork.π])

Premises used: CategoryTheory.Limits.Cofork.ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : Eq (α := op (@NormalMono.Z _ _ _ _ inst_1 f.unop _) ⟶ Z') (Quiver.Hom.op NormalMono.g ≫ f ≫ m') 0
a :
  m'.unop =
    Quiver.Hom.unop
      ((fun {Z' : Cᵒᵖ} (g' : X ⟶ Z')
            (w' : Eq (α := op (@NormalMono.Z _ _ _ _ inst_1 f.unop _) ⟶ Z') (Quiver.Hom.op NormalMono.g ≫ g') 0) ↦
          (Quiver.Hom.op
              (↑(KernelFork.IsLimit.lift' NormalMono.isLimit g'.unop ⋯) : unop Z' ⟶ (KernelFork.ofι f.unop ⋯).pt) :
            op
                (Cone.pt (F := parallelPair (X := unop X) (Y := @NormalMono.Z _ _ _ _ inst_1 f.unop _) NormalMono.g 0)
                  (KernelFork.ofι f.unop ⋯)) ⟶
              op (unop Z')))
        (f ≫ m') w')
⊢ m' =
    (fun {Z' : Cᵒᵖ} (g' : X ⟶ Z')
          (w' : Eq (α := op (@NormalMono.Z _ _ _ _ inst_1 f.unop _) ⟶ Z') (Quiver.Hom.op NormalMono.g ≫ g') 0) ↦
        (Quiver.Hom.op
            (↑(KernelFork.IsLimit.lift' NormalMono.isLimit g'.unop ⋯) : unop Z' ⟶ (KernelFork.ofι f.unop ⋯).pt) :
          op
              (Cone.pt (F := parallelPair (X := unop X) (Y := @NormalMono.Z _ _ _ _ inst_1 f.unop _) NormalMono.g 0)
                (KernelFork.ofι f.unop ⋯)) ⟶
            op (unop Z')))
      (f ≫ m') w'

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : Eq (α := op (@NormalMono.Z _ _ _ _ inst_1 f.unop _) ⟶ Z') (Quiver.Hom.op NormalMono.g ≫ f ≫ m') 0
a :
  ∀ (j : WalkingParallelPair),
    Eq (α :=
      Cone.pt (F := parallelPair (X := unop X) (Y := @NormalMono.Z _ _ _ _ inst_1 f.unop _) NormalMono.g 0)
          (KernelFork.ofι (m'.unop ≫ f.unop) ⋯) ⟶
        Functor.obj.{0, v₁, 0, u₁}
          (parallelPair (X := unop X) (Y := @NormalMono.Z _ _ _ _ inst_1 f.unop _) NormalMono.g 0) j)
      (m'.unop ≫ NatTrans.app (Cone.π (KernelFork.ofι f.unop ⋯)) j)
      (NatTrans.app (Cone.π (KernelFork.ofι (m'.unop ≫ f.unop) ⋯)) j)
⊢ m'.unop =
    Quiver.Hom.unop
      ((fun {Z' : Cᵒᵖ} (g' : X ⟶ Z')
            (w' : Eq (α := op (@NormalMono.Z _ _ _ _ inst_1 f.unop _) ⟶ Z') (Quiver.Hom.op NormalMono.g ≫ g') 0) ↦
          (Quiver.Hom.op
              (↑(KernelFork.IsLimit.lift' NormalMono.isLimit g'.unop ⋯) : unop Z' ⟶ (KernelFork.ofι f.unop ⋯).pt) :
            op
                (Cone.pt (F := parallelPair (X := unop X) (Y := @NormalMono.Z _ _ _ _ inst_1 f.unop _) NormalMono.g 0)
                  (KernelFork.ofι f.unop ⋯)) ⟶
              op (unop Z')))
        (f ≫ m') w')

Tactic:
apply m.isLimit.uniq (KernelFork.ofι (m'.unop ≫ f.unop) _) m'.unop

Premises used: CategoryTheory.Limits.KernelFork.ofι, CategoryTheory.NormalMono.isLimit, Quiver.Hom.unop, CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.CategoryStruct.comp