awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
h₀ :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) biprod.inl
      (biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯) =
    biprod.inl ≫ s.π
h₁ :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) biprod.inr
      (biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯) =
    biprod.inr ≫ s.π
⊢ biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = s.π

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
h₀ : inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = biprod.inl ≫ s.π
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) biprod.inl
      (biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯) =
    biprod.inl ≫ s.π

Tactic:
simp only [biprod.inl_desc_assoc]

Premises used: CategoryTheory.Limits.biprod.inl_desc_assoc
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
⊢ inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = biprod.inl ≫ s.π

Tactic:
apply PushoutCocone.IsColimit.inl_desc h

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
h₁ : inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = biprod.inr ≫ s.π
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) biprod.inr
      (biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯) =
    biprod.inr ≫ s.π

Tactic:
simp only [biprod.inr_desc_assoc]

Premises used: CategoryTheory.Limits.biprod.inr_desc_assoc
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
⊢ inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = biprod.inr ≫ s.π

Tactic:
apply PushoutCocone.IsColimit.inr_desc h

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : Cofork.π sq.cokernelCofork ≫ m = s.π
h₀ :
  (PushoutCocone.mk inl inr ⋯).inl ≫ m =
    (PushoutCocone.mk inl inr ⋯).inl ≫
      (fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
          PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯)
        s
h₁ :
  (PushoutCocone.mk inl inr ⋯).inr ≫ m =
    (PushoutCocone.mk inl inr ⋯).inr ≫
      (fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
          PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯)
        s
⊢ m =
    (fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
        PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯)
      s

Tactic:
apply PushoutCocone.IsColimit.hom_ext h

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : Cofork.π sq.cokernelCofork ≫ m = s.π
⊢ biprod.inl ≫ Cofork.π sq.cokernelCofork ≫ m = biprod.inl ≫ s.π

Tactic:
replace hm := biprod.inl ≫= hm
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : biprod.inl ≫ Cofork.π sq.cokernelCofork ≫ m = biprod.inl ≫ s.π
h₀ : inl ≫ m = inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯
⊢ (PushoutCocone.mk inl inr ⋯).inl ≫ m =
    (PushoutCocone.mk inl inr ⋯).inl ≫
      (fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
          PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯)
        s

Tactic:
dsimp at hm ⊢
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) biprod.inl (biprod.desc inl inr ≫ m) = biprod.inl ≫ s.π
⊢ inl ≫ m = biprod.inl ≫ s.π

Tactic:
simp only [biprod.inl_desc_assoc] at hm

Premises used: CategoryTheory.Limits.biprod.inl_desc_assoc
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : inl ≫ m = biprod.inl ≫ s.π
h₀ : biprod.inl ≫ s.π = inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯
⊢ inl ≫ m = inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

Tactic:
rw [hm]
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : inl ≫ m = biprod.inl ≫ s.π
h₀ : inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = biprod.inl ≫ s.π
⊢ biprod.inl ≫ s.π = inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

Tactic:
symm
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : inl ≫ m = biprod.inl ≫ s.π
⊢ inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = biprod.inl ≫ s.π

Tactic:
apply PushoutCocone.IsColimit.inl_desc h

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : Cofork.π sq.cokernelCofork ≫ m = s.π
⊢ biprod.inr ≫ Cofork.π sq.cokernelCofork ≫ m = biprod.inr ≫ s.π

Tactic:
replace hm := biprod.inr ≫= hm
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : biprod.inr ≫ Cofork.π sq.cokernelCofork ≫ m = biprod.inr ≫ s.π
h₁ : inr ≫ m = inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯
⊢ (PushoutCocone.mk inl inr ⋯).inr ≫ m =
    (PushoutCocone.mk inl inr ⋯).inr ≫
      (fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
          PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯)
        s

Tactic:
dsimp at hm ⊢
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) biprod.inr (biprod.desc inl inr ≫ m) = biprod.inr ≫ s.π
⊢ inr ≫ m = biprod.inr ≫ s.π

Tactic:
simp only [biprod.inr_desc_assoc] at hm

Premises used: CategoryTheory.Limits.biprod.inr_desc_assoc
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : inr ≫ m = biprod.inr ≫ s.π
h₁ : biprod.inr ≫ s.π = inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯
⊢ inr ≫ m = inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

Tactic:
rw [hm]
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : inr ≫ m = biprod.inr ≫ s.π
h₁ : inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = biprod.inr ≫ s.π
⊢ biprod.inr ≫ s.π = inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

Tactic:
symm
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶ s.pt
hm : inr ≫ m = biprod.inr ≫ s.π
⊢ inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = biprod.inr ≫ s.π

Tactic:
apply PushoutCocone.IsColimit.inr_desc h

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork
s : PushoutCocone f g
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) (biprod.desc s.inl s.inr) = 0

Tactic:
simp [s.condition]

Premises used: CategoryTheory.Limits.PushoutCocone.condition
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork
s : PushoutCocone f g
⊢ inl ≫
      (fun (s : PushoutCocone f g) ↦
          (h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯) :
            Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶
              Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0)
                (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯)))
        s =
    s.inl

Tactic:
simpa using biprod.inl ≫=
                h.fac (CokernelCofork.ofπ (biprod.desc s.inl s.inr)
                  (by simp [s.condition])) .one

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.biprod.desc, CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.PushoutCocone.inr, CategoryTheory.Limits.PushoutCocone.inl, CategoryTheory.Limits.biprod.inl, CategoryTheory.Limits.CokernelCofork.ofπ
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork
s : PushoutCocone f g
⊢ inr ≫
      (fun (s : PushoutCocone f g) ↦
          (h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯) :
            Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶
              Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0)
                (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯)))
        s =
    s.inr

Tactic:
simpa using biprod.inr ≫=
                h.fac (CokernelCofork.ofπ (biprod.desc s.inl s.inr)
                  (by simp [s.condition])) .one

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.biprod.desc, CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.PushoutCocone.inr, CategoryTheory.Limits.PushoutCocone.inl, CategoryTheory.Limits.biprod.inr, CategoryTheory.Limits.CokernelCofork.ofπ
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork
s : PushoutCocone f g
m : X₄ ⟶ s.pt
hm₁ : inl ≫ m = s.inl
hm₂ : inr ≫ m = s.inr
apply :
  Eq (α := biprod.{v_1, u_1} X₂ X₃ ⟶ s.pt) (Cofork.π sq.cokernelCofork ≫ m)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork)
      (Cofork.π sq.cokernelCofork)
      ((fun (s : PushoutCocone f g) ↦
          (h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯) :
            Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶
              Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0)
                (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯)))
        s))
⊢ m =
    (fun (s : PushoutCocone f g) ↦
        (h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯) :
          Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶
            Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0)
              (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯)))
      s

Tactic:
apply Cofork.IsColimit.hom_ext h

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork
s : PushoutCocone f g
m : X₄ ⟶ s.pt
hm₁ : inl ≫ m = s.inl
hm₂ : inr ≫ m = s.inr
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) (biprod.desc s.inl s.inr) = 0

Tactic:
simp [s.condition]

Premises used: CategoryTheory.Limits.PushoutCocone.condition
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork
s : PushoutCocone f g
m : X₄ ⟶ s.pt
hm₁ : inl ≫ m = s.inl
hm₂ : inr ≫ m = s.inr
h₁ :
  (biprod.{v_1, u_1} X₂ X₃ ⟶ s.pt) =
      ((parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0).obj WalkingParallelPair.one ⟶
        Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0)
          (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯)) →
    Eq (α := biprod.{v_1, u_1} X₂ X₃ ⟶ s.pt) (Cofork.π sq.cokernelCofork ≫ m : biprod.{v_1, u_1} X₂ X₃ ⟶ s.pt)
      (NatTrans.app (Cocone.ι (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯)) WalkingParallelPair.one :
        (parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0).obj WalkingParallelPair.one ⟶
          Functor.obj.{0, v_1, 0, u_1}
            (Functor.obj (Functor.const WalkingParallelPair)
              (Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0)
                (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯)))
            WalkingParallelPair.one)
⊢ Eq (α := biprod.{v_1, u_1} X₂ X₃ ⟶ s.pt) (Cofork.π sq.cokernelCofork ≫ m)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork)
      (Cofork.π sq.cokernelCofork)
      ((fun (s : PushoutCocone f g) ↦
          (h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯) :
            Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork ⟶
              Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0)
                (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯)))
        s))

Tactic:
convert!
          (h.fac (CokernelCofork.ofπ (biprod.desc s.inl s.inr) (by simp [s.condition])) .one).symm

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.biprod.desc, CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.PushoutCocone.inr, CategoryTheory.Limits.PushoutCocone.inl, Eq.symm, CategoryTheory.Limits.CokernelCofork.ofπ
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
h : IsPushout f g inl inr
rw : ∀ (R : C) (g_1 : ShortComplex.X₃ ⋯.shortComplex ⟶ R), ShortComplex.g ⋯.shortComplex ≫ g_1 = 0 → g_1 = 0
⊢ Epi (X := ShortComplex.X₂ ⋯.shortComplex) (ShortComplex.g ⋯.shortComplex)

Tactic:
rw [Preadditive.epi_iff_cancel_zero]

Premises used: CategoryTheory.Preadditive.epi_iff_cancel_zero
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
h : IsPushout f g inl inr
R : C
b : ShortComplex.X₃ ⋯.shortComplex ⟶ R
hb : ShortComplex.g ⋯.shortComplex ≫ b = 0
⊢ Eq (α := biprod.{v_1, u_1} X₂ X₃ ⟶ R) (Cofork.π ⋯.cokernelCofork ≫ b)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ⋯.cokernelCofork)
      (Cofork.π ⋯.cokernelCofork) 0)

Tactic:
simpa using hb
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
h : IsPushout f g inl inr
R : C
b : ShortComplex.X₃ ⋯.shortComplex ⟶ R
hb : ShortComplex.g ⋯.shortComplex ≫ b = 0
⊢ b = 0

Tactic:
exact Cofork.IsColimit.hom_ext h.isColimitCokernelCofork (by simpa using hb)

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext, CategoryTheory.IsPushout.isColimitCokernelCofork
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift fst snd) (biprod.desc f (-g)) = 0

Tactic:
simp [sq.w]

Premises used: CategoryTheory.CommSq.w
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0
rw : s.ι ≫ HSub.hSub (α := biprod.{v_1, u_1} X₂ X₃ ⟶ X₄) (biprod.fst ≫ f) (biprod.snd ≫ g) = 0
⊢ (s.ι ≫ biprod.fst) ≫ f = (s.ι ≫ biprod.snd) ≫ g

Tactic:
rw [← sub_eq_zero, assoc, assoc, ← Preadditive.comp_sub]

Premises used: CategoryTheory.Category.assoc, sub_eq_zero, CategoryTheory.Preadditive.comp_sub