awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : HasFiniteProducts.{u_2, u_1} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X Y : C
f : X ⟶ Y
h_1 : Mono f
obtain : ∀ (hf : AbelianStruct f), Nonempty (NormalMono f)
⊢ Nonempty (NormalMono f)

Tactic:
obtain ⟨hf⟩ := h f
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : HasFiniteProducts.{u_2, u_1} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X Y : C
f : X ⟶ Y
h_1 : Mono f
hf : AbelianStruct f
⊢ f ≫ Cofork.π hf.cokernelCofork = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : HasFiniteProducts.{u_2, u_1} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X Y : C
f : X ⟶ Y
h_1 : Mono f
hf : AbelianStruct f
⊢ Fork.ι hf.kernelFork = 0

Tactic:
simp [← cancel_mono f]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : HasFiniteProducts.{u_2, u_1} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X Y : C
f : X ⟶ Y
h_1 : Mono f
hf : AbelianStruct f
⊢ Nonempty (NormalMono f)

Tactic:
exact ⟨{
      Z := hf.cokernelCofork.pt
      g := hf.cokernelCofork.π
      w := by simp
      isLimit :=
        have : IsIso hf.imageπ :=
          CokernelCofork.IsColimit.isIso_π _ hf.imageIsCokernel (by simp [← cancel_mono f])
        IsLimit.ofIsoLimit hf.imageIsKernel (Fork.ext (asIso hf.imageπ)).symm }⟩
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : HasFiniteProducts.{u_2, u_1} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X Y : C
f : X ⟶ Y
h_1 : Epi f
obtain : ∀ (hf : AbelianStruct f), Nonempty (NormalEpi f)
⊢ Nonempty (NormalEpi f)

Tactic:
obtain ⟨hf⟩ := h f
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : HasFiniteProducts.{u_2, u_1} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X Y : C
f : X ⟶ Y
h_1 : Epi f
hf : AbelianStruct f
⊢ Fork.ι hf.kernelFork ≫ f = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : HasFiniteProducts.{u_2, u_1} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X Y : C
f : X ⟶ Y
h_1 : Epi f
hf : AbelianStruct f
⊢ Cofork.π hf.cokernelCofork = 0

Tactic:
simp [← cancel_epi f]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : HasFiniteProducts.{u_2, u_1} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X Y : C
f : X ⟶ Y
h_1 : Epi f
hf : AbelianStruct f
⊢ Nonempty (NormalEpi f)

Tactic:
exact ⟨{
      W := hf.kernelFork.pt
      g := hf.kernelFork.ι
      w := by simp
      isColimit :=
        have : IsIso hf.imageι :=
          KernelFork.IsLimit.isIso_ι _ hf.imageIsKernel (by simp [← cancel_epi f])
        IsColimit.ofIsoColimit hf.imageIsCokernel (Cofork.ext (asIso hf.imageι)) }⟩
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ MorphismProperty.IsStableUnderCobaseChange.{v, u} (MorphismProperty.monomorphisms C)

Tactic:
.mk' (fun _ _ _ _ _ _ (_ : Mono _) ↦ inferInstanceAs (Mono _))

Premises used: CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.mk', _private.0.CategoryTheory.Abelian.instIsStableUnderCobaseChangeMonomorphisms._proof_1
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ MorphismProperty.IsStableUnderBaseChange.{v, u} (MorphismProperty.epimorphisms C)

Tactic:
.mk' (fun _ _ _ _ _ _ (_ : Epi _) ↦ inferInstanceAs (Epi _))

Premises used: CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk', _private.0.CategoryTheory.Abelian.instIsStableUnderBaseChangeEpimorphisms._proof_1
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
⊢ ShortComplex.Exact ⋯.shortComplex

Tactic:
h.shortComplex.exact_of_g_is_cokernel
    h.isColimitCokernelCofork

Premises used: CategoryTheory.CommSq.shortComplex, CategoryTheory.ShortComplex.exact_of_g_is_cokernel, CategoryTheory.IsPushout.isColimitCokernelCofork, CategoryTheory.IsPushout.toCommSq
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
⊢ Epi (X := ShortComplex.X₂ ⋯.shortComplex) (ShortComplex.g ⋯.shortComplex)

Tactic:
have := h.epi_shortComplex_g
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi (X := ShortComplex.X₂ ⋯.shortComplex) (ShortComplex.g ⋯.shortComplex)
obtain :
  ∀ (T' : C) (π : T' ⟶ T),
    Epi π →
      ∀ (u : T' ⟶ ShortComplex.X₂ ⋯.shortComplex) (hu : π ≫ x₄ = u ≫ ShortComplex.g ⋯.shortComplex),
        ∃ (T' : C) (π : T' ⟶ T) (_ : Epi π) (x₂ : T' ⟶ X₂) (x₃ : T' ⟶ X₃), π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ ∃ (T' : C) (π : T' ⟶ T) (_ : Epi π) (x₂ : T' ⟶ X₂) (x₃ : T' ⟶ X₃), π ≫ x₄ = x₂ ≫ r + x₃ ≫ b

Tactic:
obtain ⟨T', π, _, u, hu⟩ := surjective_up_to_refinements_of_epi h.shortComplex.g x₄

Premises used: CategoryTheory.CommSq.shortComplex, CategoryTheory.surjective_up_to_refinements_of_epi, CategoryTheory.IsPushout.toCommSq, CategoryTheory.ShortComplex.g
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi (X := ShortComplex.X₂ ⋯.shortComplex) (ShortComplex.g ⋯.shortComplex)
T' : C
π : T' ⟶ T
w : Epi π
u : T' ⟶ ShortComplex.X₂ ⋯.shortComplex
hu : π ≫ x₄ = u ≫ ShortComplex.g ⋯.shortComplex
⊢ ∃ (T' : C) (π : T' ⟶ T) (_ : Epi π) (x₂ : T' ⟶ X₂) (x₃ : T' ⟶ X₃), π ≫ x₄ = x₂ ≫ r + x₃ ≫ b

Tactic:
⟨T', π, inferInstance, u ≫ biprod.fst, u ≫ biprod.snd, ?_⟩

Premises used: inferInstance, CategoryTheory.Limits.biprod.snd, CategoryTheory.Limits.biprod.fst, Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi (X := ShortComplex.X₂ ⋯.shortComplex) (ShortComplex.g ⋯.shortComplex)
T' : C
π : T' ⟶ T
w : Epi π
u : T' ⟶ ShortComplex.X₂ ⋯.shortComplex
hu : π ≫ x₄ = u ≫ ShortComplex.g ⋯.shortComplex
refine : π ≫ x₄ = (u ≫ biprod.fst) ≫ r + (u ≫ biprod.snd) ≫ b
⊢ ∃ (T' : C) (π : T' ⟶ T) (_ : Epi π) (x₂ : T' ⟶ X₂) (x₃ : T' ⟶ X₃), π ≫ x₄ = x₂ ≫ r + x₃ ≫ b

Tactic:
refine ⟨T', π, inferInstance, u ≫ biprod.fst, u ≫ biprod.snd, ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi (X := ShortComplex.X₂ ⋯.shortComplex) (ShortComplex.g ⋯.shortComplex)
T' : C
π : T' ⟶ T
w : Epi π
u : T' ⟶ ShortComplex.X₂ ⋯.shortComplex
hu : π ≫ x₄ = u ≫ ShortComplex.g ⋯.shortComplex
simp :
  u ≫ ShortComplex.g ⋯.shortComplex =
    u ≫ HAdd.hAdd (α := ShortComplex.X₂ ⋯.shortComplex ⟶ X₄) (biprod.fst ≫ r) (biprod.snd ≫ b)
⊢ π ≫ x₄ = (u ≫ biprod.fst) ≫ r + (u ≫ biprod.snd) ≫ b

Tactic:
simp only [hu, assoc, ← Preadditive.comp_add]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi (X := ShortComplex.X₂ ⋯.shortComplex) (ShortComplex.g ⋯.shortComplex)
T' : C
π : T' ⟶ T
w : Epi π
u : T' ⟶ ShortComplex.X₂ ⋯.shortComplex
hu : π ≫ x₄ = u ≫ ShortComplex.g ⋯.shortComplex
e_a :
  ShortComplex.g ⋯.shortComplex = HAdd.hAdd (α := ShortComplex.X₂ ⋯.shortComplex ⟶ X₄) (biprod.fst ≫ r) (biprod.snd ≫ b)
⊢ u ≫ ShortComplex.g ⋯.shortComplex =
    u ≫ HAdd.hAdd (α := ShortComplex.X₂ ⋯.shortComplex ⟶ X₄) (biprod.fst ≫ r) (biprod.snd ≫ b)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
obtain : ∀ (T₁ : C) (π : T₁ ⟶ T₀), Epi π → ∀ (x₂ : T₁ ⟶ X₂) (x₃ : T₁ ⟶ X₃) (eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b), x₄ = 0
⊢ x₄ = 0

Tactic:
obtain ⟨T₁, π, _, x₂, x₃, eq⟩ := hom_eq_add_up_to_refinements h₁ x₄

Premises used: CategoryTheory.IsPushout.hom_eq_add_up_to_refinements
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
rw : -x₂ ≫ r' = x₃ ≫ b'
rw₁ : x₂ ≫ r' + x₃ ≫ b' = 0
rw₂ : x₂ ≫ r' + x₃ ≫ b ≫ k = 0
rw₃ : x₂ ≫ r ≫ k + x₃ ≫ b ≫ k = 0
rw₄ : (x₂ ≫ r) ≫ k + x₃ ≫ b ≫ k = 0
rw₅ : (x₂ ≫ r) ≫ k + (x₃ ≫ b) ≫ k = 0
rw₆ : (x₂ ≫ r + x₃ ≫ b) ≫ k = 0
rw₇ : (π ≫ x₄) ≫ k = 0
rw₈ : π ≫ x₄ ≫ k = 0
rw₉ : Eq (α := T₁ ⟶ X₅) (π ≫ 0) 0
rw₁₀ rw₁₁ : Eq.{v + 1} (α := T₁ ⟶ X₅) 0 0
⊢ (-x₂) ≫ r' = x₃ ≫ b'

Tactic:
rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]

Premises used: CategoryTheory.Category.assoc, neg_eq_iff_add_eq_zero, CategoryTheory.Limits.comp_zero, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.neg_comp
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ (-x₂) ≫ r' = x₃ ≫ b'

Tactic:
have fac₃ : (-x₂) ≫ r' = x₃ ≫ b' := by
      rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ ∃ (x₂' : T₁ ⟶ X₂), π ≫ x₄ = x₂' ≫ r

Tactic:
⟨x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t, ?_⟩

Premises used: HAdd.hAdd, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsPullback.lift, Neg.neg
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
refine : π ≫ x₄ = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
⊢ ∃ (x₂' : T₁ ⟶ X₂), π ≫ x₄ = x₂' ≫ r

Tactic:
refine ⟨x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t, ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
rw : x₂ ≫ r + x₃ ≫ b = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
rw₁ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + (h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
rw₂ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + h₂.lift (-x₂) x₃ fac₃ ≫ t ≫ r
rw₃ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + h₂.lift (-x₂) x₃ fac₃ ≫ l ≫ b
rw₄ : x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + x₃ ≫ b
rw₅ rw₆ : x₃ ≫ b + x₂ ≫ r = x₃ ≫ b + x₂ ≫ r
⊢ π ≫ x₄ = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r

Tactic:
rw [eq, Preadditive.add_comp, assoc, h₁.w, IsPullback.lift_snd_assoc, add_comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsPullback.lift_snd_assoc, add_comm, CategoryTheory.Preadditive.add_comp, CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
obtain : ∀ (x₂' : T₁ ⟶ X₂) (hx₂' : π ≫ x₄ = x₂' ≫ r), x₄ = 0
⊢ x₄ = 0

Tactic:
obtain ⟨x₂', hx₂'⟩ : ∃ x₂', π ≫ x₄ = x₂' ≫ r := by
      refine ⟨x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t, ?_⟩
      rw [eq, Preadditive.add_comp, assoc, h₁.w, IsPullback.lift_snd_assoc, add_comm]
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
x₂' : T₁ ⟶ X₂
hx₂' : π ≫ x₄ = x₂' ≫ r
rw :
  Epi π →
    ∀ (x₂ : T₁ ⟶ X₂) (x₃ : T₁ ⟶ X₃) (eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b) (fac₃ : (-x₂) ≫ r' = x₃ ≫ b') (x₂' : T₁ ⟶ X₂)
      (hx₄ : x₂' ≫ r' = 0) (hx₂' : π ≫ x₄ = x₂' ≫ r), x₄ = 0
⊢ x₄ = 0

Tactic:
rw [← cancel_epi π, comp_zero, reassoc_of% hx₂', fac₁] at hx₄

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
x₂' : T₁ ⟶ X₂
hx₄ : x₂' ≫ r' = 0
hx₂' : π ≫ x₄ = x₂' ≫ r
⊢ Eq (α := T₁ ⟶ X₅) (0 ≫ r') 0

Tactic:
obtain rfl := zero_of_comp_mono _ hx₄

Premises used: CategoryTheory.Limits.zero_of_comp_mono, rfl
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
x₂' : T₁ ⟶ X₂
hx₄ : x₂' ≫ r' = 0
hx₂' : π ≫ x₄ = x₂' ≫ r
hx₅ : Eq (α := T₁ ⟶ X₅) (0 ≫ r') 0
⊢ π ≫ x₄ = 0 ≫ r

Tactic:
obtain rfl := zero_of_comp_mono _ hx₄

Premises used: CategoryTheory.Limits.zero_of_comp_mono, rfl
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
hx₄ : Eq (α := T₁ ⟶ X₅) (0 ≫ r') 0
hx₂' : π ≫ x₄ = 0 ≫ r
⊢ π ≫ x₄ = 0

Tactic:
rw [zero_comp] at hx₂'

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
hx₄ : Eq (α := T₁ ⟶ X₅) (0 ≫ r') 0
hx₂' : π ≫ x₄ = 0
rw : π ≫ x₄ = π ≫ 0
rw₁ : Eq (α := T₁ ⟶ X₄) 0 (π ≫ 0)
rw₂ rw₃ : Eq.{v + 1} (α := T₁ ⟶ X₄) 0 0
⊢ x₄ = 0

Tactic:
rw [← cancel_epi π, hx₂', comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPullback t l r b
⊢ ShortComplex.Exact ⋯.shortComplex'

Tactic:
h.shortComplex'.exact_of_f_is_kernel
    h.isLimitKernelFork

Premises used: CategoryTheory.CommSq.shortComplex', CategoryTheory.IsPullback.isLimitKernelFork, CategoryTheory.ShortComplex.exact_of_f_is_kernel, CategoryTheory.IsPullback.toCommSq
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
rw : ∀ (P : C) (g : P ⟶ cokernel t), Eq (α := P ⟶ cokernel b) (g ≫ cokernel.map t b l r ⋯) 0 → g = 0
⊢ Mono (X := cokernel t) (Y := cokernel b) (cokernel.map t b l r ⋯)

Tactic:
rw [Preadditive.mono_iff_cancel_zero]

Premises used: CategoryTheory.Preadditive.mono_iff_cancel_zero
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : Eq (α := A₀ ⟶ cokernel b) (z ≫ cokernel.map t b l r ⋯) 0
obtain : ∀ (A₁ : C) (π₁ : A₁ ⟶ A₀), Epi π₁ → ∀ (x₂ : A₁ ⟶ X₂) (hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t), z = 0
⊢ z = 0

Tactic:
obtain ⟨A₁, π₁, _, x₂, hx₂⟩ :=
    surjective_up_to_refinements_of_epi (cokernel.π t) z

Premises used: CategoryTheory.surjective_up_to_refinements_of_epi, CategoryTheory.Limits.cokernel.π
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : Eq (α := A₀ ⟶ cokernel b) (z ≫ cokernel.map t b l r ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A₀
w : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
⊢ ShortComplex.Exact (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)

Tactic:
have : (ShortComplex.mk _ _ (cokernel.condition b)).Exact :=
    ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel b)
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : Eq (α := A₀ ⟶ cokernel b) (z ≫ cokernel.map t b l r ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A₀
w : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
this : ShortComplex.Exact (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)
⊢ Eq (α := A₁ ⟶ ShortComplex.X₃ (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯))
    ((x₂ ≫ r) ≫ ShortComplex.g (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)) 0

Tactic:
simpa [hz] using hx₂.symm =≫ cokernel.map _ _ _ _ sq.w

Premises used: CategoryTheory.Limits.cokernel.map, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : Eq (α := A₀ ⟶ cokernel b) (z ≫ cokernel.map t b l r ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A₀
w : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
this : ShortComplex.Exact (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)
obtain :
  ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁),
    Epi π₂ →
      ∀ (x₃ : A₂ ⟶ ShortComplex.X₁ (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯))
        (hx₃ : π₂ ≫ x₂ ≫ r = x₃ ≫ ShortComplex.f (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)), z = 0
⊢ z = 0

Tactic:
obtain ⟨A₂, π₂, _, x₃, hx₃⟩ := this.exact_up_to_refinements (x₂ ≫ r) (by
    simpa [hz] using hx₂.symm =≫ cokernel.map _ _ _ _ sq.w)

Premises used: CategoryTheory.ShortComplex.Exact.exact_up_to_refinements, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : Eq (α := A₀ ⟶ cokernel b) (z ≫ cokernel.map t b l r ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A₀
w : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
this : ShortComplex.Exact (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
x₃ : A₂ ⟶ ShortComplex.X₁ (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)
hx₃ : π₂ ≫ x₂ ≫ r = x₃ ≫ ShortComplex.f (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)
⊢ (π₂ ≫ x₂) ≫ r = x₃ ≫ b

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : Eq (α := A₀ ⟶ cokernel b) (z ≫ cokernel.map t b l r ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A₀
w : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
this : ShortComplex.Exact (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
x₃ : A₂ ⟶ ShortComplex.X₁ (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)
hx₃ : π₂ ≫ x₂ ≫ r = x₃ ≫ ShortComplex.f (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)
obtain :
  ∀ (x₁ : A₂ ⟶ X₁) (hx₁ : x₁ ≫ t = π₂ ≫ x₂)
    (hx₃ : π₂ ≫ x₂ ≫ r = (x₁ ≫ l) ≫ ShortComplex.f (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)), z = 0
⊢ z = 0

Tactic:
obtain ⟨x₁, hx₁, rfl⟩ := sq.exists_lift (π₂ ≫ x₂) x₃ (by simpa)

Premises used: CategoryTheory.IsPullback.exists_lift, CategoryTheory.CategoryStruct.comp, rfl
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : Eq (α := A₀ ⟶ cokernel b) (z ≫ cokernel.map t b l r ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A₀
w : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
this : ShortComplex.Exact (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
x₁ : A₂ ⟶ X₁
hx₁ : x₁ ≫ t = π₂ ≫ x₂
hx₃ : π₂ ≫ x₂ ≫ r = (x₁ ≫ l) ≫ ShortComplex.f (ShortComplex.mk (X₃ := cokernel b) b (cokernel.π b) ⋯)
⊢ z = 0

Tactic:
simp [← cancel_epi π₁, ← cancel_epi π₂, hx₂, ← reassoc_of% hx₁]

Premises used: CategoryTheory.cancel_epi