awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Exact (cokernelSequence f)

Tactic:
exact_of_g_is_cokernel _ (cokernelIsCokernel f)

Premises used: CategoryTheory.ShortComplex.exact_of_g_is_cokernel, CategoryTheory.Limits.cokernelIsCokernel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
rw : S₁.g ≫ φ.τ₃ = 0
rw₁ : Eq (α := S₁.X₂ ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₁.X₂ ⟶ S₂.X₃) 0 0
⊢ φ.τ₂ ≫ S₂.g = 0

Tactic:
rw [φ.comm₂₃, hg₁, zero_comp]

Premises used: CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
rw : S₁.g ≫ φ.τ₃ = 0
rw₁ : Eq (α := S₁.X₂ ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₁.X₂ ⟶ S₂.X₃) 0 0
⊢ φ.τ₂ ≫ S₂.g = 0

Tactic:
rw [φ.comm₂₃, hg₁, zero_comp]

Premises used: CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ φ.τ₂ ≫ S₂.g = 0

Tactic:
have w : φ.τ₂ ≫ S₂.g = 0 := by rw [φ.comm₂₃, hg₁, zero_comp]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
rw :
  IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) ↔
    { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Mono φ.τ₂
⊢ QuasiIso φ ↔
    { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Mono φ.τ₂

Tactic:
rw [quasiIso_iff_isIso_liftCycles φ hf₁ hg₁ hf₂]

Premises used: CategoryTheory.ShortComplex.quasiIso_iff_isIso_liftCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
mp :
  IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) →
    { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Mono φ.τ₂
mpr :
  { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Mono φ.τ₂ →
    IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
⊢ IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) ↔
    { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Mono φ.τ₂

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
rw : Mono (CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ w) S₂.iCycles)
⊢ Mono φ.τ₂

Tactic:
rw [← S₂.liftCycles_i φ.τ₂ w]

Premises used: CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.ShortComplex.liftCycles_i
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
⊢ Mono (CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ w) S₂.iCycles)

Tactic:
apply mono_comp

Premises used: CategoryTheory.mono_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
⊢ Mono φ.τ₂

Tactic:
have : Mono φ.τ₂ := by
      rw [← S₂.liftCycles_i φ.τ₂ w]
      apply mono_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
    Mono φ.τ₂

Tactic:
⟨?_, this⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
mp : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
⊢ { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
    Mono φ.τ₂

Tactic:
refine ⟨?_, this⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
mp :
  IsLimit
    (KernelFork.ofι
      { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.f ⋯)
⊢ { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact

Tactic:
apply exact_of_f_is_kernel

Premises used: CategoryTheory.ShortComplex.exact_of_f_is_kernel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ Iso.hom (Iso.symm (asIso (S₂.liftCycles φ.τ₂ w))) ≫
      Fork.ι
        (KernelFork.ofι
          { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.f ⋯) =
    Fork.ι (KernelFork.ofι (Z := S₂.cycles) S₂.iCycles ⋯)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ IsLimit
    (KernelFork.ofι
      { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.f ⋯)

Tactic:
exact IsLimit.ofIsoLimit S₂.cyclesIsKernel
      (Fork.ext (asIso (S₂.liftCycles φ.τ₂ w)).symm (by simp))
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
h₂ : Mono φ.τ₂
⊢ Eq (α :=
    S₂.cycles ⟶
      { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₃)
    (S₂.iCycles ≫
      { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g)
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
h₂ : Mono φ.τ₂
mpr : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯) = 𝟙 S₁.X₂
mpr₁ : h₁.lift S₂.iCycles ⋯ ≫ S₂.liftCycles φ.τ₂ ⋯ = 𝟙 S₂.cycles
⊢ IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)

Tactic:
refine ⟨⟨h₁.lift S₂.iCycles (by simp), ?_, ?_⟩⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
h₂ : Mono φ.τ₂
mpr : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯) ≫ φ.τ₂ = 𝟙 S₁.X₂ ≫ φ.τ₂
mpr₁ : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯ ≫ φ.τ₂) = 𝟙 S₁.X₂ ≫ φ.τ₂
mpr₂ : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) S₂.iCycles = 𝟙 S₁.X₂ ≫ φ.τ₂
mpr₃ : φ.τ₂ = 𝟙 S₁.X₂ ≫ φ.τ₂
mpr₄ mpr₅ : φ.τ₂ = φ.τ₂
⊢ CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯) = 𝟙 S₁.X₂

Tactic:
rw [← cancel_mono φ.τ₂, assoc, h₁.lift_f, liftCycles_i, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.ShortComplex.liftCycles_i, CategoryTheory.ShortComplex.Exact.lift_f, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
h₂ : Mono φ.τ₂
mpr :
  CategoryStruct.comp (Y := S₂.cycles) (h₁.lift S₂.iCycles ⋯ ≫ S₂.liftCycles φ.τ₂ ⋯) S₂.iCycles =
    𝟙 S₂.cycles ≫ S₂.iCycles
mpr₁ :
  h₁.lift S₂.iCycles ⋯ ≫ CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) S₂.iCycles =
    𝟙 S₂.cycles ≫ S₂.iCycles
mpr₂ : h₁.lift S₂.iCycles ⋯ ≫ φ.τ₂ = 𝟙 S₂.cycles ≫ S₂.iCycles
mpr₃ : S₂.iCycles = 𝟙 S₂.cycles ≫ S₂.iCycles
mpr₄ mpr₅ : Eq (α := S₂.cycles ⟶ S₂.X₂) S₂.iCycles S₂.iCycles
⊢ h₁.lift S₂.iCycles ⋯ ≫ S₂.liftCycles φ.τ₂ ⋯ = 𝟙 S₂.cycles

Tactic:
rw [← cancel_mono S₂.iCycles, assoc, liftCycles_i, h₁.lift_f, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.liftCycles_i, CategoryTheory.ShortComplex.iCycles, CategoryTheory.ShortComplex.Exact.lift_f, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
rw : φ.τ₁ ≫ S₂.f = 0
rw₁ : Eq (α := S₁.X₁ ⟶ S₂.X₂) (φ.τ₁ ≫ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ S₂.X₂) 0 0
⊢ S₁.f ≫ φ.τ₂ = 0

Tactic:
rw [← φ.comm₁₂, hf₂, comp_zero]

Premises used: CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.Limits.comp_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
rw :
  Exact { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := ⋯ } ∧
      Mono (opMap φ).τ₂ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Epi φ.τ₂
hf₁ : S₂.op.f = 0
hg₃ : S₂.op.g = 0
hf₃ : S₁.op.f = 0
⊢ QuasiIso φ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Epi φ.τ₂

Tactic:
rw [← quasiIso_opMap_iff, quasiIso_iff_of_zeros]

Premises used: CategoryTheory.ShortComplex.quasiIso_iff_of_zeros, CategoryTheory.ShortComplex.quasiIso_opMap_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
hf₁ : S₂.g.op = 0
⊢ S₂.op.f = 0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
hf₁ : Eq.{v_1 + 1} (α := Opposite.op S₂.X₃ ⟶ Opposite.op S₂.X₂) (Quiver.Hom.op 0) 0
hf₃ hf₄ : Eq.{v_1 + 1} (α := Opposite.op S₂.X₃ ⟶ Opposite.op S₂.X₂) 0 0
⊢ S₂.g.op = 0

Tactic:
rw [hg₂, op_zero]

Premises used: CategoryTheory.Limits.op_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
hg₃ : S₂.f.op = 0
⊢ S₂.op.g = 0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
hg₃ : Eq.{v_1 + 1} (α := Opposite.op S₂.X₂ ⟶ Opposite.op S₂.X₁) (Quiver.Hom.op 0) 0
hg₄ hg₅ : Eq.{v_1 + 1} (α := Opposite.op S₂.X₂ ⟶ Opposite.op S₂.X₁) 0 0
⊢ S₂.f.op = 0

Tactic:
rw [hf₂, op_zero]

Premises used: CategoryTheory.Limits.op_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
hf₃ : S₁.g.op = 0
⊢ S₁.op.f = 0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
hf₃ : Eq.{v_1 + 1} (α := Opposite.op S₁.X₃ ⟶ Opposite.op S₁.X₂) (Quiver.Hom.op 0) 0
hf₄ hf₅ : Eq.{v_1 + 1} (α := Opposite.op S₁.X₃ ⟶ Opposite.op S₁.X₂) 0 0
⊢ S₁.g.op = 0

Tactic:
rw [hg₁, op_zero]

Premises used: CategoryTheory.Limits.op_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
rw :
  Exact (unop { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := ⋯ }) ∧
      Mono (opMap φ).τ₂ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Epi φ.τ₂
⊢ Exact { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := ⋯ } ∧
      Mono (opMap φ).τ₂ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Epi φ.τ₂

Tactic:
rw [← exact_unop_iff]

Premises used: CategoryTheory.ShortComplex.exact_unop_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ Mono.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.X₂) (Y := Opposite.op S₁.X₂) φ.τ₂.op ↔ Epi φ.τ₂

Tactic:
have : Mono φ.τ₂.op ↔ Epi φ.τ₂ :=
    ⟨fun _ => unop_epi_of_mono φ.τ₂.op, fun _ => op_mono_of_epi _⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
J : C
f : S.X₂ ⟶ J
inst_3 : Injective.{v_1, u_1} J
hf : S.f ≫ f = 0
⊢ Mono (X := S.opcycles) S.fromOpcycles

Tactic:
have := hS.mono_fromOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
J : C
f : S.X₂ ⟶ J
inst_3 : Injective.{v_1, u_1} J
hf : S.f ≫ f = 0
this : Mono (X := S.opcycles) S.fromOpcycles
⊢ S.X₃ ⟶ J

Tactic:
exact Injective.factorThru (S.descOpcycles f hf) S.fromOpcycles

Premises used: CategoryTheory.ShortComplex.descOpcycles, CategoryTheory.Injective.factorThru, CategoryTheory.ShortComplex.fromOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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
hS : S.Exact
J : C
f : S.X₂ ⟶ J
inst_2 : Injective.{v_1, u_1} J
hf : S.f ≫ f = 0
dsimp : S.g ≫ Injective.factorThru (X := S.opcycles) (S.descOpcycles f hf) S.fromOpcycles = f
⊢ S.g ≫ hS.descToInjective f hf = f

Tactic:
dsimp [descToInjective]

Premises used: CategoryTheory.ShortComplex.Exact.descToInjective
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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
hS : S.Exact
J : C
f : S.X₂ ⟶ J
inst_2 : Injective.{v_1, u_1} J
hf : S.f ≫ f = 0
⊢ S.g ≫ Injective.factorThru (X := S.opcycles) (S.descOpcycles f hf) S.fromOpcycles = f

Tactic:
simp only [← p_fromOpcycles, assoc, Injective.comp_factorThru, p_descOpcycles]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.p_fromOpcycles, CategoryTheory.Injective.comp_factorThru, CategoryTheory.ShortComplex.p_descOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst_3 : Projective.{v_1, u_1} P
hf : f ≫ S.g = 0
⊢ Epi (Y := S.cycles) S.toCycles

Tactic:
have := hS.epi_toCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst_3 : Projective.{v_1, u_1} P
hf : f ≫ S.g = 0
this : Epi (Y := S.cycles) S.toCycles
⊢ P ⟶ S.X₁

Tactic:
exact Projective.factorThru (S.liftCycles f hf) S.toCycles

Premises used: CategoryTheory.Projective.factorThru, CategoryTheory.ShortComplex.liftCycles, CategoryTheory.ShortComplex.toCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst_2 : Projective.{v_1, u_1} P
hf : f ≫ S.g = 0
dsimp : Projective.factorThru (X := S.cycles) (S.liftCycles f hf) S.toCycles ≫ S.f = f
⊢ hS.liftFromProjective f hf ≫ S.f = f

Tactic:
dsimp [liftFromProjective]

Premises used: CategoryTheory.ShortComplex.Exact.liftFromProjective
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
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
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst_2 : Projective.{v_1, u_1} P
hf : f ≫ S.g = 0
rw :
  Projective.factorThru (X := S.cycles) (S.liftCycles f hf) S.toCycles ≫
      CategoryStruct.comp (Y := S.cycles) S.toCycles S.iCycles =
    f
rw₁ : CategoryStruct.comp (Y := S.cycles) (S.liftCycles f hf) S.iCycles = f
rw₂ rw₃ : f = f
⊢ Projective.factorThru (X := S.cycles) (S.liftCycles f hf) S.toCycles ≫ S.f = f

Tactic:
rw [← toCycles_i, Projective.factorThru_comp_assoc, liftCycles_i]

Premises used: CategoryTheory.Projective.factorThru_comp_assoc, CategoryTheory.ShortComplex.liftCycles_i, CategoryTheory.ShortComplex.toCycles_i
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : F.PreservesZeroMorphisms
inst_7 : F.PreservesHomology
X Y : C
f : X ⟶ Y
hf : Mono f
S : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := X) 0 f ⋯
⊢ Eq (α := ShortComplex.X₁ (S.map F) ⟶ ShortComplex.X₂ (S.map F)) (ShortComplex.f (S.map F)) 0

Tactic:
simp [S]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : F.PreservesZeroMorphisms
inst_7 : F.PreservesHomology
X Y : C
f : X ⟶ Y
hf : Mono f
S : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := X) 0 f ⋯
⊢ Mono (F.map f)

Tactic:
exact ((S.map F).exact_iff_mono (by simp [S])).1
      (((S.exact_iff_mono rfl).2 hf).map F)

Premises used: Iff.mpr, CategoryTheory.ShortComplex.Exact.map, CategoryTheory.ShortComplex.exact_iff_mono, Iff.mp, CategoryTheory.ShortComplex.map, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : F.PreservesZeroMorphisms
inst_7 : F.PreservesHomology
X Y : C
f : X ⟶ Y
hf : Epi f
S : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₃ := Y) f 0 ⋯
⊢ Eq (α := ShortComplex.X₂ (S.map F) ⟶ ShortComplex.X₃ (S.map F)) (ShortComplex.g (S.map F)) 0

Tactic:
simp [S]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : F.PreservesZeroMorphisms
inst_7 : F.PreservesHomology
X Y : C
f : X ⟶ Y
hf : Epi f
S : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₃ := Y) f 0 ⋯
⊢ Epi (F.map f)

Tactic:
exact ((S.map F).exact_iff_epi (by simp [S])).1
      (((S.exact_iff_epi rfl).2 hf).map F)

Premises used: Iff.mpr, CategoryTheory.ShortComplex.Exact.map, Iff.mp, CategoryTheory.ShortComplex.map, CategoryTheory.ShortComplex.exact_iff_epi, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
s : S.X₃ ⟶ S.X₂
s_g : s ≫ S.g = 𝟙 S.X₃
hf : Mono S.f
⊢ (𝟙 S.X₂ - S.g ≫ s) ≫ S.g = 0

Tactic:
simp [s_g]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
s : S.X₃ ⟶ S.X₂
s_g : s ≫ S.g = 𝟙 S.X₃
hf : Mono S.f
rw : (S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯) ≫ S.f = 𝟙 S.X₁ ≫ S.f
rw₁ : S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯ ≫ S.f = 𝟙 S.X₁ ≫ S.f
rw₂ : S.f ≫ (𝟙 S.X₂ - S.g ≫ s) = 𝟙 S.X₁ ≫ S.f
rw₃ : S.f ≫ 𝟙 S.X₂ - S.f ≫ S.g ≫ s = 𝟙 S.X₁ ≫ S.f
rw₄ : S.f - S.f ≫ S.g ≫ s = 𝟙 S.X₁ ≫ S.f
rw₅ : S.f - 0 ≫ s = 𝟙 S.X₁ ≫ S.f
rw₆ : S.f - 0 = 𝟙 S.X₁ ≫ S.f
rw₇ : S.f = 𝟙 S.X₁ ≫ S.f
rw₈ rw₉ : S.f = S.f
⊢ S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯ = 𝟙 S.X₁

Tactic:
rw [← cancel_mono S.f, assoc, Exact.lift_f, comp_sub, comp_id,
    zero_assoc, zero_comp, sub_zero, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.zero_assoc, sub_zero, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.zero_comp, CategoryTheory.Preadditive.comp_sub, CategoryTheory.ShortComplex.Exact.lift_f, CategoryTheory.Category.id_comp