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₃
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
⊢ s.ι ≫ biprod.desc f (-g) = s.ι ≫ 0

Tactic:
s.condition

Premises used: CategoryTheory.Limits.Fork.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₃
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
h₁ : HSub.hSub (α := biprod.{v_1, u_1} X₂ X₃ ⟶ X₄) (biprod.fst ≫ f) (biprod.snd ≫ g) = biprod.desc f (-g)
h₂ : Eq (α := s.pt ⟶ X₄) 0 (s.ι ≫ 0)
⊢ s.ι ≫ HSub.hSub (α := biprod.{v_1, u_1} X₂ X₃ ⟶ X₄) (biprod.fst ≫ f) (biprod.snd ≫ g) = 0

Tactic:
convert! s.condition

Premises used: CategoryTheory.Limits.Fork.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₃
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
dsimp : PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ biprod.lift fst snd = s.ι
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork)
      ((fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
          PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯)
        s)
      (Fork.ι sq.kernelFork) =
    s.ι

Tactic:
dsimp
-- 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
h₀ :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃)
      (PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ biprod.lift fst snd) biprod.fst =
    s.ι ≫ biprod.fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃)
      (PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ biprod.lift fst snd) biprod.snd =
    s.ι ≫ biprod.snd
⊢ PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ biprod.lift fst snd = 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₃
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
h₀ : PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ fst = s.ι ≫ biprod.fst
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃)
      (PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ biprod.lift fst snd) biprod.fst =
    s.ι ≫ biprod.fst

Tactic:
simp only [assoc, biprod.lift_fst]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.lift_fst
-- 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
⊢ PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ fst = s.ι ≫ biprod.fst

Tactic:
apply PullbackCone.IsLimit.lift_fst h

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst
-- 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
h₁ : PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ snd = s.ι ≫ biprod.snd
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃)
      (PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ biprod.lift fst snd) biprod.snd =
    s.ι ≫ biprod.snd

Tactic:
simp only [assoc, biprod.lift_snd]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.lift_snd
-- 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
⊢ PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ snd = s.ι ≫ biprod.snd

Tactic:
apply PullbackCone.IsLimit.lift_snd h

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd
-- 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
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ Fork.ι sq.kernelFork = s.ι
h₀ :
  m ≫ (PullbackCone.mk fst snd ⋯).fst =
    (fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
          PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯)
        s ≫
      (PullbackCone.mk fst snd ⋯).fst
h₁ :
  m ≫ (PullbackCone.mk fst snd ⋯).snd =
    (fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
          PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯)
        s ≫
      (PullbackCone.mk fst snd ⋯).snd
⊢ m =
    (fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
        PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯)
      s

Tactic:
apply PullbackCone.IsLimit.hom_ext h

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.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₃
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
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ Fork.ι sq.kernelFork = s.ι
⊢ (m ≫ Fork.ι sq.kernelFork) ≫ biprod.fst = s.ι ≫ biprod.fst

Tactic:
replace hm := hm =≫ biprod.fst
-- 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
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : (m ≫ Fork.ι sq.kernelFork) ≫ biprod.fst = s.ι ≫ biprod.fst
h₀ : m ≫ fst = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ fst
⊢ m ≫ (PullbackCone.mk fst snd ⋯).fst =
    (fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
          PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯)
        s ≫
      (PullbackCone.mk fst snd ⋯).fst

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₃
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
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) (m ≫ biprod.lift fst snd) biprod.fst = s.ι ≫ biprod.fst
⊢ m ≫ fst = s.ι ≫ biprod.fst

Tactic:
simp only [assoc, biprod.lift_fst] at hm

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.lift_fst
-- 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
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ fst = s.ι ≫ biprod.fst
h₀ : s.ι ≫ biprod.fst = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ fst
⊢ m ≫ fst = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ fst

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₃
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
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ fst = s.ι ≫ biprod.fst
h₀ : PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ fst = s.ι ≫ biprod.fst
⊢ s.ι ≫ biprod.fst = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ fst

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₃
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
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ fst = s.ι ≫ biprod.fst
⊢ PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ fst = s.ι ≫ biprod.fst

Tactic:
apply PullbackCone.IsLimit.lift_fst h

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst
-- 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
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ Fork.ι sq.kernelFork = s.ι
⊢ (m ≫ Fork.ι sq.kernelFork) ≫ biprod.snd = s.ι ≫ biprod.snd

Tactic:
replace hm := hm =≫ biprod.snd
-- 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
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : (m ≫ Fork.ι sq.kernelFork) ≫ biprod.snd = s.ι ≫ biprod.snd
h₁ : m ≫ snd = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ snd
⊢ m ≫ (PullbackCone.mk fst snd ⋯).snd =
    (fun (s : Fork (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ↦
          PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯)
        s ≫
      (PullbackCone.mk fst snd ⋯).snd

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₃
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
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) (m ≫ biprod.lift fst snd) biprod.snd = s.ι ≫ biprod.snd
⊢ m ≫ snd = s.ι ≫ biprod.snd

Tactic:
simp only [assoc, biprod.lift_snd] at hm

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.lift_snd
-- 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
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ snd = s.ι ≫ biprod.snd
h₁ : s.ι ≫ biprod.snd = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ snd
⊢ m ≫ snd = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ snd

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₃
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
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ snd = s.ι ≫ biprod.snd
h₁ : PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ snd = s.ι ≫ biprod.snd
⊢ s.ι ≫ biprod.snd = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ snd

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₃
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
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
hm : m ≫ snd = s.ι ≫ biprod.snd
⊢ PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ snd = s.ι ≫ biprod.snd

Tactic:
apply PullbackCone.IsLimit.lift_snd h

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd
-- 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 (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
s : PullbackCone f g
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift s.fst s.snd) (biprod.desc f (-g)) = 0

Tactic:
simp [s.condition]

Premises used: CategoryTheory.Limits.PullbackCone.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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
s : PullbackCone f g
⊢ (fun (s : PullbackCone f g) ↦
          (h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) :
            Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0)
                (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) ⟶
              Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork))
        s ≫
      fst =
    s.fst

Tactic:
simpa using h.fac (KernelFork.ofι (biprod.lift s.fst s.snd)
        (by simp [s.condition])) .zero =≫ biprod.fst

Premises used: CategoryTheory.Limits.KernelFork.ofι, CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.biprod.lift, CategoryTheory.Limits.biprod.fst, CategoryTheory.Limits.PullbackCone.snd, CategoryTheory.Limits.WalkingParallelPair.zero, CategoryTheory.Limits.IsLimit.fac
-- 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 (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
s : PullbackCone f g
⊢ (fun (s : PullbackCone f g) ↦
          (h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) :
            Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0)
                (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) ⟶
              Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork))
        s ≫
      snd =
    s.snd

Tactic:
simpa using h.fac (KernelFork.ofι (biprod.lift s.fst s.snd)
        (by simp [s.condition])) .zero =≫ biprod.snd

Premises used: CategoryTheory.Limits.KernelFork.ofι, CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.biprod.snd, CategoryTheory.Limits.biprod.lift, CategoryTheory.Limits.PullbackCone.snd, CategoryTheory.Limits.WalkingParallelPair.zero, CategoryTheory.Limits.IsLimit.fac
-- 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 (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
s : PullbackCone f g
m : s.pt ⟶ X₁
hm₁ : m ≫ fst = s.fst
hm₂ : m ≫ snd = s.snd
apply :
  Eq (α := s.pt ⟶ biprod.{v_1, u_1} X₂ X₃) (m ≫ Fork.ι sq.kernelFork)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork)
      ((fun (s : PullbackCone f g) ↦
          (h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) :
            Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0)
                (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) ⟶
              Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork))
        s)
      (Fork.ι sq.kernelFork))
⊢ m =
    (fun (s : PullbackCone f g) ↦
        (h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) :
          Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0)
              (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) ⟶
            Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork))
      s

Tactic:
apply Fork.IsLimit.hom_ext h

Premises used: CategoryTheory.Limits.Fork.IsLimit.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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
s : PullbackCone f g
m : s.pt ⟶ X₁
hm₁ : m ≫ fst = s.fst
hm₂ : m ≫ snd = s.snd
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift s.fst s.snd) (biprod.desc f (-g)) = 0

Tactic:
simp [s.condition]

Premises used: CategoryTheory.Limits.PullbackCone.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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork
s : PullbackCone f g
m : s.pt ⟶ X₁
hm₁ : m ≫ fst = s.fst
hm₂ : m ≫ snd = s.snd
h₁ :
  (s.pt ⟶ biprod.{v_1, u_1} X₂ X₃) =
      (Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0)
          (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) ⟶
        (parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0).obj WalkingParallelPair.zero) →
    Eq (α := s.pt ⟶ biprod.{v_1, u_1} X₂ X₃) (m ≫ Fork.ι sq.kernelFork)
      (NatTrans.app (Cone.π (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯)) WalkingParallelPair.zero)
⊢ Eq (α := s.pt ⟶ biprod.{v_1, u_1} X₂ X₃) (m ≫ Fork.ι sq.kernelFork)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork)
      ((fun (s : PullbackCone f g) ↦
          (h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) :
            Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0)
                (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) ⟶
              Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) sq.kernelFork))
        s)
      (Fork.ι sq.kernelFork))

Tactic:
convert!
          (h.fac (KernelFork.ofι (biprod.lift s.fst s.snd) (by simp [s.condition])) .zero).symm

Premises used: CategoryTheory.Limits.KernelFork.ofι, CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.biprod.lift, CategoryTheory.Limits.PullbackCone.snd, Eq.symm, CategoryTheory.Limits.WalkingParallelPair.zero, CategoryTheory.Limits.IsLimit.fac
-- 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₄
h : IsPullback fst snd f g
rw : ∀ (P : C) (g_1 : P ⟶ ShortComplex.X₁ ⋯.shortComplex'), g_1 ≫ ShortComplex.f ⋯.shortComplex' = 0 → g_1 = 0
⊢ Mono (X := ShortComplex.X₁ ⋯.shortComplex') (ShortComplex.f ⋯.shortComplex')

Tactic:
rw [Preadditive.mono_iff_cancel_zero]

Premises used: CategoryTheory.Preadditive.mono_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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
P : C
b : P ⟶ ShortComplex.X₁ ⋯.shortComplex'
hb : b ≫ ShortComplex.f ⋯.shortComplex' = 0
⊢ Eq (α := P ⟶ biprod.{v_1, u_1} X₂ X₃) (b ≫ Fork.ι ⋯.kernelFork)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := biprod.{v_1, u_1} X₂ X₃) (biprod.desc f (-g)) 0) ⋯.kernelFork) 0
      (Fork.ι ⋯.kernelFork))

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₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
P : C
b : P ⟶ ShortComplex.X₁ ⋯.shortComplex'
hb : b ≫ ShortComplex.f ⋯.shortComplex' = 0
⊢ b = 0

Tactic:
exact Fork.IsLimit.hom_ext h.isLimitKernelFork (by simpa using hb)

Premises used: CategoryTheory.IsPullback.isLimitKernelFork, CategoryTheory.Limits.Fork.IsLimit.hom_ext