awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ Eq (α :=
      A ⟶
        Cocone.pt (F := parallelPair (Y := S.cycles) S.toCycles 0)
          (CokernelCofork.ofπ (Z := S.homology) S.homologyπ ⋯ : CokernelCofork (Y := S.cycles) S.toCycles))
      (CategoryStruct.comp (Y := S.cycles) (S.liftCycles x₂ hx₂ : A ⟶ S.cycles)
          (Cofork.π (CokernelCofork.ofπ (Z := S.homology) S.homologyπ ⋯) :
            S.cycles ⟶
              Cocone.pt (F := parallelPair (Y := S.cycles) S.toCycles 0)
                (CokernelCofork.ofπ (Z := S.homology) S.homologyπ ⋯ : CokernelCofork (Y := S.cycles) S.toCycles)) :
        A ⟶
          Cocone.pt (F := parallelPair (Y := S.cycles) S.toCycles 0)
            (CokernelCofork.ofπ (Z := S.homology) S.homologyπ ⋯ : CokernelCofork (Y := S.cycles) S.toCycles))
      (0 :
        A ⟶
          Cocone.pt (F := parallelPair (Y := S.cycles) S.toCycles 0)
            (CokernelCofork.ofπ (Z := S.homology) S.homologyπ ⋯ : CokernelCofork (Y := S.cycles) S.toCycles)) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁),
      Eq (α := A' ⟶ S.cycles) (π ≫ S.liftCycles x₂ hx₂) (x ≫ S.toCycles)

Tactic:
have := CokernelCofork.IsColimit.comp_π_eq_zero_iff_up_to_refinements
        S.homologyIsCokernel (S.liftCycles x₂ hx₂)
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
this :
  Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁),
      Eq (α := A' ⟶ S.cycles) (π ≫ S.liftCycles x₂ hx₂) (x ≫ S.toCycles)
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f

Tactic:
simp [this, ← cancel_mono S.iCycles]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
x₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
⊢ (x₂ - x₂') ≫ S.g = 0

Tactic:
simp [hx₂, hx₂']
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
x₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
this :
  Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) ↔
    Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ) 0
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = π ≫ x₂' + x₁ ≫ S.f

Tactic:
simp [this, S.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements,
      sub_eq_iff_eq_add']

Premises used: CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements, sub_eq_iff_eq_add'
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
x₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
suffices :
  Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) ↔
    Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ) 0
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = π ≫ x₂' + x₁ ≫ S.f

Tactic:
suffices S.liftCycles x₂ hx₂ ≫ S.homologyπ = S.liftCycles x₂' hx₂' ≫ S.homologyπ ↔
      S.liftCycles (x₂ - x₂') (by simp [hx₂, hx₂']) ≫ S.homologyπ = 0 by
    simp [this, S.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements,
      sub_eq_iff_eq_add']
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
x₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
rw :
  HSub.hSub (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) = 0 ↔
    Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ) 0
rw₁ :
  Eq (α := A ⟶ S.homology) (HSub.hSub (α := A ⟶ S.cycles) (S.liftCycles x₂ hx₂) (S.liftCycles x₂' hx₂') ≫ S.homologyπ)
      0 ↔
    Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ) 0
rw₂ rw₃ :
  Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ) 0 ↔
    Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ) 0
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) ↔
    Eq (α := A ⟶ S.homology) (S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ) 0

Tactic:
rw [← sub_eq_zero, ← sub_comp, sub_liftCycles]

Premises used: sub_eq_zero, CategoryTheory.ShortComplex.sub_liftCycles, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
z₂ : A ⟶ S.cycles
⊢ (z₂ ≫ S.iCycles) ≫ S.g = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
z₂ : A ⟶ S.cycles
⊢ z₂ = S.liftCycles (z₂ ≫ S.iCycles) ⋯

Tactic:
simp [← cancel_mono S.iCycles, liftCycles_i]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.liftCycles_i, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
z₂ : A ⟶ S.cycles
obtain :
  ∀ (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0),
    Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) 0 ↔
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁),
        Eq (α := A' ⟶ S.cycles) (π ≫ S.liftCycles x₂ hx₂) (x₁ ≫ S.toCycles)
⊢ Eq (α := A ⟶ S.homology) (z₂ ≫ S.homologyπ) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ z₂ = x₁ ≫ S.toCycles

Tactic:
obtain ⟨x₂, hx₂, rfl⟩ : ∃ (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0), z₂ = S.liftCycles x₂ hx₂ :=
    ⟨z₂ ≫ S.iCycles, by simp, by simp [← cancel_mono S.iCycles, liftCycles_i]⟩

Premises used: CategoryTheory.ShortComplex.g, rfl, CategoryTheory.ShortComplex.X₂
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁),
      Eq (α := A' ⟶ S.cycles) (π ≫ S.liftCycles x₂ hx₂) (x₁ ≫ S.toCycles)

Tactic:
simp [liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements, ← cancel_mono S.iCycles]

Premises used: CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
z₂ z₂' : A ⟶ S.cycles
⊢ (z₂ ≫ S.iCycles) ≫ S.g = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
z₂ z₂' : A ⟶ S.cycles
⊢ z₂ = S.liftCycles (z₂ ≫ S.iCycles) ⋯

Tactic:
simp [← cancel_mono S.iCycles]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
z₂ z₂' : A ⟶ S.cycles
obtain :
  ∀ (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0),
    Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (z₂' ≫ S.homologyπ) ↔
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ S.liftCycles x₂ hx₂ = π ≫ z₂' + x₁ ≫ S.toCycles
⊢ Eq (α := A ⟶ S.homology) (z₂ ≫ S.homologyπ) (z₂' ≫ S.homologyπ) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ z₂ = π ≫ z₂' + x₁ ≫ S.toCycles

Tactic:
obtain ⟨x₂, hx₂, rfl⟩ : ∃ (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0), z₂ = S.liftCycles x₂ hx₂ :=
    ⟨z₂ ≫ S.iCycles, by simp, by simp [← cancel_mono S.iCycles]⟩

Premises used: CategoryTheory.ShortComplex.g, rfl, CategoryTheory.ShortComplex.X₂
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
z₂' : A ⟶ S.cycles
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ (z₂' ≫ S.iCycles) ≫ S.g = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
z₂' : A ⟶ S.cycles
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ z₂' = S.liftCycles (z₂' ≫ S.iCycles) ⋯

Tactic:
simp [← cancel_mono S.iCycles]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
z₂' : A ⟶ S.cycles
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
obtain :
  ∀ (x₂' : A ⟶ S.X₂) (hx₂' : x₂' ≫ S.g = 0),
    Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) ↔
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁),
        π ≫ S.liftCycles x₂ hx₂ = HAdd.hAdd (α := A' ⟶ S.cycles) (π ≫ S.liftCycles x₂' hx₂') (x₁ ≫ S.toCycles)
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (z₂' ≫ S.homologyπ) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ S.liftCycles x₂ hx₂ = π ≫ z₂' + x₁ ≫ S.toCycles

Tactic:
obtain ⟨x₂', hx₂', rfl⟩ : ∃ (x₂' : A ⟶ S.X₂) (hx₂' : x₂' ≫ S.g = 0), z₂' =
    S.liftCycles x₂' hx₂' := ⟨z₂' ≫ S.iCycles, by simp,
      by simp [← cancel_mono S.iCycles]⟩

Premises used: CategoryTheory.ShortComplex.g, rfl, CategoryTheory.ShortComplex.X₂
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
x₂' : A ⟶ S.X₂
hx₂' : x₂' ≫ S.g = 0
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles x₂ hx₂ ≫ S.homologyπ) (S.liftCycles x₂' hx₂' ≫ S.homologyπ) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁),
      π ≫ S.liftCycles x₂ hx₂ = HAdd.hAdd (α := A' ⟶ S.cycles) (π ≫ S.liftCycles x₂' hx₂') (x₁ ≫ S.toCycles)

Tactic:
simp [liftCycles_comp_homologyπ_eq_iff_up_to_refinements, ← cancel_mono S.iCycles]

Premises used: CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_iff_up_to_refinements, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
x₂ : A ⟶ S.X₂
⊢ Eq (α := A ⟶ S.opcycles) (x₂ ≫ S.pOpcycles) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f

Tactic:
CokernelCofork.IsColimit.comp_π_eq_zero_iff_up_to_refinements
    S.opcyclesIsCokernel x₂

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.Limits.CokernelCofork.IsColimit.comp_π_eq_zero_iff_up_to_refinements, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ShortComplex.opcyclesIsCokernel, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
⊢ Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
      x₂ ≫ S₁.g = 0 →
        ∀ (y₁ : A ⟶ S₂.X₁),
          x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f

Tactic:
⟨fun h A x₂ hx₂ y₁ fac ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
refine_1 :
  ∀ (h : Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)) (A : C) (x₂ : A ⟶ S₁.X₂) (hx₂ : x₂ ≫ S₁.g = 0)
    (y₁ : A ⟶ S₂.X₁) (fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
refine_2 :
  ∀
    (h :
      ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
        x₂ ≫ S₁.g = 0 →
          ∀ (y₁ : A ⟶ S₂.X₁),
            x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f),
    Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
⊢ Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
      x₂ ≫ S₁.g = 0 →
        ∀ (y₁ : A ⟶ S₂.X₁),
          x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f

Tactic:
refine ⟨fun h A x₂ hx₂ y₁ fac ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
this rwa : Eq (α := A ⟶ S₁.homology) (S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ) 0
hx₃ : x₂ ≫ S₁.g = 0
rwa₁ : Eq (α := A ⟶ S₁.homology) (S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ) 0
hx₄ : x₂ ≫ S₁.g = 0
rwa₂ : Eq (α := A ⟶ S₁.homology) (S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ) 0
hx₅ : x₂ ≫ S₁.g = 0
rwa₃ : Eq (α := A ⟶ S₁.homology) (S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ) 0
hx₆ : x₂ ≫ S₁.g = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f

Tactic:
rwa [← S₁.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements]

Premises used: CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
refine_1 : Eq (α := A ⟶ S₁.homology) (S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ) 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f

Tactic:
suffices S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ = 0 by
      rwa [← S₁.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements]
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
refine_1 : ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₂.X₁), π ≫ x₂ ≫ φ.τ₂ = x₁ ≫ S₂.f
⊢ Eq (α := A ⟶ S₁.homology) (S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ) 0

Tactic:
simp only [← cancel_mono (homologyMap φ), zero_comp, assoc,
      homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      S₂.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.liftCycles_comp_cyclesMap_assoc, CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements, CategoryTheory.ShortComplex.homologyπ_naturality, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
⊢ 𝟙 A ≫ x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f

Tactic:
simpa using fac
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₂.X₁), π ≫ x₂ ≫ φ.τ₂ = x₁ ≫ S₂.f

Tactic:
exact ⟨A, 𝟙 A, inferInstance, y₁, by simpa using fac⟩
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
refine_2 : ∀ (P : C) (g : P ⟶ S₁.homology), Eq (α := P ⟶ S₂.homology) (g ≫ homologyMap φ) 0 → g = 0
⊢ Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
rw [Preadditive.mono_iff_cancel_zero]

Premises used: CategoryTheory.Preadditive.mono_iff_cancel_zero
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
hγ : Eq (α := A ⟶ S₂.homology) (γ ≫ homologyMap φ) 0
refine_2 :
  ∀ (A₁ : C) (π₁ : A₁ ⟶ A) (hπ₁ : Epi π₁) (z : A₁ ⟶ S₁.X₂) (hz : z ≫ S₁.g = 0)
    (fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ), γ = 0
⊢ γ = 0

Tactic:
obtain ⟨A₁, π₁, hπ₁, z, hz, fac⟩ := S₁.eq_liftCycles_homologyπ_up_to_refinements γ

Premises used: CategoryTheory.ShortComplex.π₁, CategoryTheory.ShortComplex.eq_liftCycles_homologyπ_up_to_refinements
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
hγ : Eq (α := A ⟶ S₂.homology) (γ ≫ homologyMap φ) 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
refine_2 : Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0
⊢ γ = 0

Tactic:
rw [← cancel_epi π₁, fac, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
hγ : Eq (α := A ⟶ S₂.homology) (γ ≫ homologyMap φ) 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
⊢ Eq (α := A₁ ⟶ S₂.homology) (π₁ ≫ γ ≫ homologyMap φ) (π₁ ≫ 0)

Tactic:
replace hγ := π₁ ≫= hγ
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
hγ : Eq (α := A₁ ⟶ S₂.homology) (π₁ ≫ γ ≫ homologyMap φ) (π₁ ≫ 0)
⊢ ∃ (A' : C) (π : A' ⟶ A₁) (_ : Epi π) (x₁ : A' ⟶ S₂.X₁),
    Eq (α := A' ⟶ S₂.cycles) (π ≫ S₂.liftCycles (z ≫ φ.τ₂) ⋯) (x₁ ≫ S₂.toCycles)

Tactic:
simp only [reassoc_of% fac, homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      comp_zero, comp_homologyπ_eq_zero_iff_up_to_refinements] at hγ

Premises used: CategoryTheory.ShortComplex.liftCycles_comp_cyclesMap_assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.homologyπ_naturality, CategoryTheory.ShortComplex.comp_homologyπ_eq_zero_iff_up_to_refinements
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
hγ :
  ∃ (A' : C) (π : A' ⟶ A₁) (_ : Epi π) (x₁ : A' ⟶ S₂.X₁),
    Eq (α := A' ⟶ S₂.cycles) (π ≫ S₂.liftCycles (z ≫ φ.τ₂) ⋯) (x₁ ≫ S₂.toCycles)
refine_2 :
  ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁) (hπ₂ : Epi π₂) (y : A₂ ⟶ S₂.X₁)
    (hy : Eq (α := A₂ ⟶ S₂.cycles) (π₂ ≫ S₂.liftCycles (z ≫ φ.τ₂) ⋯) (y ≫ S₂.toCycles)),
    Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0
⊢ Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0

Tactic:
obtain ⟨A₂, π₂, hπ₂, y, hy⟩ := hγ

Premises used: CategoryTheory.ShortComplex.π₂
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : Eq (α := A₂ ⟶ S₂.cycles) (π₂ ≫ S₂.liftCycles (z ≫ φ.τ₂) ⋯) (y ≫ S₂.toCycles)
⊢ CategoryStruct.comp (Y := S₂.cycles) (π₂ ≫ S₂.liftCycles (z ≫ φ.τ₂) ⋯) S₂.iCycles =
    CategoryStruct.comp (Y := S₂.cycles) (y ≫ S₂.toCycles) S₂.iCycles

Tactic:
replace hy := hy =≫ S₂.iCycles
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy :
  CategoryStruct.comp (Y := S₂.cycles) (π₂ ≫ S₂.liftCycles (z ≫ φ.τ₂) ⋯) S₂.iCycles =
    CategoryStruct.comp (Y := S₂.cycles) (y ≫ S₂.toCycles) S₂.iCycles
⊢ π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f

Tactic:
simp only [assoc, liftCycles_i, toCycles_i] at hy

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.liftCycles_i, CategoryTheory.ShortComplex.toCycles_i
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
rw : π₂ ≫ z ≫ S₁.g = 0
rw₁ : Eq (α := A₂ ⟶ S₁.X₃) (π₂ ≫ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := A₂ ⟶ S₁.X₃) 0 0
⊢ (π₂ ≫ z) ≫ S₁.g = 0

Tactic:
rw [assoc, hz, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero