awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
x₁ : (↑S.X₁ : Type u)
h :
  Eq (α := (↑S.X₃ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.g :
            (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) S.f :
                (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
              x₁ :
            (↑S.X₂ : Type u)) :
        (↑S.X₃ : Type u))
      (0 : (↑S.X₃ : Type u)) →
    ∃ (x₁_1 : (↑S.X₁ : Type u)),
      Eq (α := (↑S.X₂ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁_1 :
          (↑S.X₂ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ :
          (↑S.X₂ : Type u))
⊢ Eq (α := (↑S.X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) S.g :
          (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ :
          (↑S.X₂ : Type u)) :
      (↑S.X₃ : Type u))
    (0 : (↑S.X₃ : Type u))

Tactic:
simp only [ab_zero_apply]

Premises used: CategoryTheory.ShortComplex.ab_zero_apply
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
⊢ S.Exact ↔ (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range

Tactic:
S.ab_exact_iff

Premises used: Set.Mem, setOf, CategoryTheory.ShortComplex.ab_exact_iff, Set.preimage, Set.singleton, Set.range
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
rw :
  (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range ↔
    (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker
⊢ S.Exact ↔ (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker

Tactic:
rw [ab_exact_iff_ker_le_range]

Premises used: CategoryTheory.ShortComplex.ab_exact_iff_ker_le_range
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
mp :
  (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range →
    (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker
mpr :
  (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker →
    (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range
⊢ (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range ↔
    (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
h : (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range
⊢ (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker

Tactic:
le_antisymm ?_ h

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
h : (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range
mp : (AddCommGrpCat.Hom.hom S.f).range ≤ (AddCommGrpCat.Hom.hom S.g).ker
⊢ (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker

Tactic:
refine le_antisymm ?_ h

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
h : (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range
x₁ : (↑S.X₁ : Type u)
mp :
  Eq (α := (↑S.X₃ : Type u))
    ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
            (fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) AddCommGrpCat.carrier _ _ S.X₁ S.X₃ 0 :
          (a : (↑S.X₁ : Type u)) → (↑S.X₃ : Type u))
        x₁ :
      (↑S.X₃ : Type u))
    (0 : (↑S.X₃ : Type u))
⊢ Membership.mem (α := (↑S.X₂ : Type u)) (AddCommGrpCat.Hom.hom S.g).ker
    ((AddCommGrpCat.Hom.hom S.f : (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u)) x₁ : (↑S.X₂ : Type u))

Tactic:
rw [AddMonoidHom.mem_ker, ← ConcreteCategory.comp_apply, S.zero]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.ShortComplex.zero, AddMonoidHom.mem_ker
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
h : (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range
x₁ : (↑S.X₁ : Type u)
⊢ Eq (α := (↑S.X₃ : Type u))
    ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
            (fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) AddCommGrpCat.carrier _ _ S.X₁ S.X₃ 0 :
          (a : (↑S.X₁ : Type u)) → (↑S.X₃ : Type u))
        x₁ :
      (↑S.X₃ : Type u))
    (0 : (↑S.X₃ : Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
h : (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker
mpr mpr₁ : (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.g).ker
⊢ (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
hS : S.Exact
inst : Finite.{u + 1} (↑S.X₁ : Type u)
inst_1 : Finite.{u + 1} (↑S.X₃ : Type u)
⊢ Finite.{u + 1} ↥(AddCommGrpCat.Hom.hom S.f).range

Tactic:
have : Finite S.f.hom.range := Set.finite_range _
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
hS : S.Exact
inst : Finite.{u + 1} (↑S.X₁ : Type u)
inst_1 : Finite.{u + 1} (↑S.X₃ : Type u)
this : Finite.{u + 1} ↥(AddCommGrpCat.Hom.hom S.f).range
rw : Finite.{u + 1} ((↑S.X₂ : Type u) ⧸ (AddCommGrpCat.Hom.hom S.g).ker)
⊢ Finite.{u + 1} ((↑S.X₂ : Type u) ⧸ (AddCommGrpCat.Hom.hom S.f).range)

Tactic:
rw [hS.ab_range_eq_ker]

Premises used: CategoryTheory.ShortComplex.Exact.ab_range_eq_ker
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
hS : S.Exact
inst : Finite.{u + 1} (↑S.X₁ : Type u)
inst_1 : Finite.{u + 1} (↑S.X₃ : Type u)
this : Finite.{u + 1} ↥(AddCommGrpCat.Hom.hom S.f).range
⊢ Finite.{u + 1} ((↑S.X₂ : Type u) ⧸ (AddCommGrpCat.Hom.hom S.g).ker)

Tactic:
.of_equiv _ (QuotientAddGroup.quotientKerEquivRange _).toEquiv.symm

Premises used: Finite.of_equiv, QuotientAddGroup.quotientKerEquivRange, AddEquiv.toEquiv, Equiv.symm
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
hS : S.Exact
inst : Finite.{u + 1} (↑S.X₁ : Type u)
inst_1 : Finite.{u + 1} (↑S.X₃ : Type u)
this : Finite.{u + 1} ↥(AddCommGrpCat.Hom.hom S.f).range
⊢ Finite.{u + 1} ((↑S.X₂ : Type u) ⧸ (AddCommGrpCat.Hom.hom S.g).ker)

Tactic:
exact .of_equiv _ (QuotientAddGroup.quotientKerEquivRange _).toEquiv.symm
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
hS : S.Exact
inst : Finite.{u + 1} (↑S.X₁ : Type u)
inst_1 : Finite.{u + 1} (↑S.X₃ : Type u)
this : Finite.{u + 1} ↥(AddCommGrpCat.Hom.hom S.f).range
⊢ Finite.{u + 1} ((↑S.X₂ : Type u) ⧸ (AddCommGrpCat.Hom.hom S.f).range)

Tactic:
have : Finite (S.X₂ ⧸ S.f.hom.range) := by
    rw [hS.ab_range_eq_ker]
    exact .of_equiv _ (QuotientAddGroup.quotientKerEquivRange _).toEquiv.symm
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
hS : S.Exact
inst : Finite.{u + 1} (↑S.X₁ : Type u)
inst_1 : Finite.{u + 1} (↑S.X₃ : Type u)
this_1 : Finite.{u + 1} ↥(AddCommGrpCat.Hom.hom S.f).range
this : Finite.{u + 1} ((↑S.X₂ : Type u) ⧸ (AddCommGrpCat.Hom.hom S.f).range)
⊢ Finite.{u + 1} (↑S.X₂ : Type u)

Tactic:
.of_addSubgroup_quotient (H := S.f.hom.range)

Premises used: AddMonoidHom.range, Finite.of_addSubgroup_quotient, AddCommGrpCat.Hom.hom, CategoryTheory.ShortComplex.f
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
hS : S.Exact
inst : Finite.{u + 1} (↑S.X₁ : Type u)
inst_1 : Finite.{u + 1} (↑S.X₃ : Type u)
this_1 : Finite.{u + 1} ↥(AddCommGrpCat.Hom.hom S.f).range
this : Finite.{u + 1} ((↑S.X₂ : Type u) ⧸ (AddCommGrpCat.Hom.hom S.f).range)
⊢ Finite.{u + 1} (↑S.X₂ : Type u)

Tactic:
exact .of_addSubgroup_quotient (H := S.f.hom.range)
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
hS : S.ShortExact
⊢ Function.Injective (α := (↑S.X₁ : Type u)) (β := (↑S.X₂ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) S.f) :
      (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))

Tactic:
(AddCommGrpCat.mono_iff_injective _).1 hS.mono_f

Premises used: CategoryTheory.ShortComplex.ShortExact.mono_f, AddCommGrpCat.mono_iff_injective, Iff.mp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
hS : S.ShortExact
⊢ Function.Surjective (α := (↑S.X₂ : Type u)) (β := (↑S.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))

Tactic:
(AddCommGrpCat.epi_iff_surjective _).1 hS.epi_g

Premises used: CategoryTheory.ShortComplex.ShortExact.epi_g, AddCommGrpCat.epi_iff_surjective, Iff.mp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
f g : S₁ ⟶ S₂
h₁ : f.τ₁ = g.τ₁
h₂ : f.τ₂ = g.τ₂
h₃ : f.τ₃ = g.τ₃
⊢ f = g

Tactic:
Hom.ext h₁ h₂ h₃

Premises used: CategoryTheory.ShortComplex.Hom.ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
⊢ Hom.τ₁ (𝟙 S) = 𝟙 S.X₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
⊢ Hom.τ₂ (𝟙 S) = 𝟙 S.X₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
⊢ Hom.τ₃ (𝟙 S) = 𝟙 S.X₃

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁₂ : S₁ ⟶ S₂
φ₂₃ : S₂ ⟶ S₃
⊢ (φ₁₂ ≫ φ₂₃).τ₁ = φ₁₂.τ₁ ≫ φ₂₃.τ₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁₂ : S₁ ⟶ S₂
φ₂₃ : S₂ ⟶ S₃
⊢ (φ₁₂ ≫ φ₂₃).τ₂ = φ₁₂.τ₂ ≫ φ₂₃.τ₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁₂ : S₁ ⟶ S₂
φ₂₃ : S₂ ⟶ S₃
⊢ (φ₁₂ ≫ φ₂₃).τ₃ = φ₁₂.τ₃ ≫ φ₂₃.τ₃

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
⊢ Eq.{v_1 + 1} (α := S₁.X₁ ⟶ S₂.X₁) (Hom.τ₁ 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
⊢ Eq.{v_1 + 1} (α := S₁.X₂ ⟶ S₂.X₂) (Hom.τ₂ 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
⊢ Eq.{v_1 + 1} (α := S₁.X₃ ⟶ S₂.X₃) (Hom.τ₃ 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
f : S₁ ⟶ S₂
inst_6 : IsIso f
⊢ IsIso f.τ₁

Tactic:
(inferInstance : IsIso (π₁.mapIso (asIso f)).hom)

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
f : S₁ ⟶ S₂
inst_6 : IsIso f
⊢ IsIso f.τ₂

Tactic:
(inferInstance : IsIso (π₂.mapIso (asIso f)).hom)

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
f : S₁ ⟶ S₂
inst_6 : IsIso f
⊢ IsIso f.τ₃

Tactic:
(inferInstance : IsIso (π₃.mapIso (asIso f)).hom)

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.PreservesZeroMorphisms
rw : F.map (S.f ≫ S.g) = 0
rw₁ : Eq (α := F.obj S.X₁ ⟶ F.obj S.X₃) (F.map 0) 0
rw₂ rw₃ : Eq.{v_2 + 1} (α := F.obj S.X₁ ⟶ F.obj S.X₃) 0 0
⊢ F.map S.f ≫ F.map S.g = 0

Tactic:
rw [← F.map_comp, S.zero, F.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.ShortComplex.zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
⊢ S.map (𝟭 C) = S

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.map, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.PreservesZeroMorphisms
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.PreservesZeroMorphisms
⊢ Eq (α := ShortComplex.{v_3, u_3} E) (S.map (F ⋙ G)) (map (S.map F) G)

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.map, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.PreservesZeroMorphisms
X Y : ShortComplex.{v_1, u_1} C
φ : X ⟶ Y
dsimp : F.map φ.τ₁ ≫ F.map Y.f = F.map X.f ≫ F.map φ.τ₂
⊢ Eq (α := X₁ (X.map F) ⟶ X₂ (Y.map F)) (F.map φ.τ₁ ≫ f (Y.map F)) (f (X.map F) ≫ F.map φ.τ₂)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.PreservesZeroMorphisms
X Y : ShortComplex.{v_1, u_1} C
φ : X ⟶ Y
⊢ F.map φ.τ₁ ≫ F.map Y.f = F.map X.f ≫ F.map φ.τ₂

Tactic:
simp only [← F.map_comp, φ.comm₁₂]

Premises used: CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.PreservesZeroMorphisms
X Y : ShortComplex.{v_1, u_1} C
φ : X ⟶ Y
dsimp : F.map φ.τ₂ ≫ F.map Y.g = F.map X.g ≫ F.map φ.τ₃
⊢ Eq (α := X₂ (X.map F) ⟶ X₃ (Y.map F)) (F.map φ.τ₂ ≫ g (Y.map F)) (g (X.map F) ≫ F.map φ.τ₃)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.PreservesZeroMorphisms
X Y : ShortComplex.{v_1, u_1} C
φ : X ⟶ Y
⊢ F.map φ.τ₂ ≫ F.map Y.g = F.map X.g ≫ F.map φ.τ₃

Tactic:
simp only [← F.map_comp, φ.comm₂₃]

Premises used: CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
rw : (e₁.inv ≫ S₁.f) ≫ e₂.hom = (S₂.f ≫ e₂.inv) ≫ e₂.hom
rw₁ : e₁.inv ≫ S₁.f ≫ e₂.hom = (S₂.f ≫ e₂.inv) ≫ e₂.hom
rw₂ : e₁.inv ≫ S₁.f ≫ e₂.hom = S₂.f ≫ e₂.inv ≫ e₂.hom
rw₃ : e₁.inv ≫ S₁.f ≫ e₂.hom = S₂.f ≫ 𝟙 S₂.X₂
rw₄ : e₁.inv ≫ S₁.f ≫ e₂.hom = S₂.f
rw₅ : e₁.inv ≫ e₁.hom ≫ S₂.f = S₂.f
rw₆ rw₇ : S₂.f = S₂.f
⊢ e₁.inv ≫ S₁.f = S₂.f ≫ e₂.inv

Tactic:
rw [← cancel_mono e₂.hom, assoc, assoc, e₂.inv_hom_id, comp_id,
          ← comm₁₂, e₁.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
rw : (e₂.inv ≫ S₁.g) ≫ e₃.hom = (S₂.g ≫ e₃.inv) ≫ e₃.hom
rw₁ : e₂.inv ≫ S₁.g ≫ e₃.hom = (S₂.g ≫ e₃.inv) ≫ e₃.hom
rw₂ : e₂.inv ≫ S₁.g ≫ e₃.hom = S₂.g ≫ e₃.inv ≫ e₃.hom
rw₃ : e₂.inv ≫ S₁.g ≫ e₃.hom = S₂.g ≫ 𝟙 S₂.X₃
rw₄ : e₂.inv ≫ S₁.g ≫ e₃.hom = S₂.g
rw₅ : e₂.inv ≫ e₂.hom ≫ S₂.g = S₂.g
rw₆ rw₇ : S₂.g = S₂.g
⊢ e₂.inv ≫ S₁.g = S₂.g ≫ e₃.inv

Tactic:
rw [← cancel_mono e₃.hom, assoc, assoc, e₃.inv_hom_id, comp_id,
          ← comm₂₃, e₂.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
f : S₁ ⟶ S₂
inst_2 : IsIso f.τ₁
inst_3 : IsIso f.τ₂
inst_4 : IsIso f.τ₃
⊢ IsIso f

Tactic:
(isoMk (asIso f.τ₁) (asIso f.τ₂) (asIso f.τ₃)).isIso_hom

Premises used: CategoryTheory.ShortComplex.Hom.τ₁, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.Iso.isIso_hom, CategoryTheory.ShortComplex.isoMk, CategoryTheory.ShortComplex.Hom.τ₃, CategoryTheory.asIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
f : S₁ ⟶ S₂
⊢ IsIso f ↔ IsIso f.τ₁ ∧ IsIso f.τ₂ ∧ IsIso f.τ₃

Tactic:
⟨fun _ ↦ ⟨inferInstance, inferInstance, inferInstance⟩, ?_⟩

Premises used: inferInstance, And.intro, Iff.intro
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
f : S₁ ⟶ S₂
refine : IsIso f.τ₁ ∧ IsIso f.τ₂ ∧ IsIso f.τ₃ → IsIso f
⊢ IsIso f ↔ IsIso f.τ₁ ∧ IsIso f.τ₂ ∧ IsIso f.τ₃

Tactic:
refine ⟨fun _ ↦ ⟨inferInstance, inferInstance, inferInstance⟩, ?_⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
f : S₁ ⟶ S₂
left : IsIso f.τ₁
left_1 : IsIso f.τ₂
right : IsIso f.τ₃
⊢ IsIso f

Tactic:
apply isIso_of_isIso

Premises used: CategoryTheory.ShortComplex.isIso_of_isIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
simp : Eq.{v_1 + 1} (α := Opposite.op S.X₃ ⟶ Opposite.op S.X₁) (Quiver.Hom.op 0) 0
⊢ Eq.{v_1 + 1} (α := Opposite.op S.X₃ ⟶ Opposite.op S.X₁) (S.g.op ≫ S.f.op) 0

Tactic:
simp only [← op_comp, S.zero]

Premises used: CategoryTheory.op_comp, CategoryTheory.ShortComplex.zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
⊢ Eq.{v_1 + 1} (α := Opposite.op S.X₃ ⟶ Opposite.op S.X₁) (Quiver.Hom.op 0) 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
dsimp : Eq.{v_1 + 1} (α := Opposite.op S₂.X₃ ⟶ Opposite.op S₁.X₂) (φ.τ₃.op ≫ S₁.g.op) (S₂.g.op ≫ φ.τ₂.op)
⊢ φ.τ₃.op ≫ S₁.op.f = S₂.op.f ≫ φ.τ₂.op

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
⊢ Eq.{v_1 + 1} (α := Opposite.op S₂.X₃ ⟶ Opposite.op S₁.X₂) (φ.τ₃.op ≫ S₁.g.op) (S₂.g.op ≫ φ.τ₂.op)

Tactic:
simp only [← op_comp, φ.comm₂₃]

Premises used: CategoryTheory.op_comp, CategoryTheory.ShortComplex.Hom.comm₂₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.Basic
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasZeroMorphisms.{v_2, u_2} D
inst_5 : HasZeroMorphisms.{v_3, u_3} E
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
dsimp : Eq.{v_1 + 1} (α := Opposite.op S₂.X₂ ⟶ Opposite.op S₁.X₁) (φ.τ₂.op ≫ S₁.f.op) (S₂.f.op ≫ φ.τ₁.op)
⊢ φ.τ₂.op ≫ S₁.op.g = S₂.op.g ≫ φ.τ₁.op

Tactic:
dsimp