awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
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)
have rw : Finite.{u + 1} ((↑S.X₂ : Type u) ⧸ (AddCommGrpCat.Hom.hom S.g).ker)
Tactic: rw [hS.ab_range_eq_ker]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (hypothesis)
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)
have this₁ : 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
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ F.map S.f ≫ F.map S.g = 0
have rw : F.map (S.f ≫ S.g) = 0
Tactic: rw [← F.map_comp, S.zero, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ F.map S.f ≫ F.map S.g = 0
have rw₁ : Eq (α := F.obj S.X₁ ⟶ F.obj S.X₃) (F.map 0) 0
Tactic: rw [← F.map_comp, S.zero, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ F.map S.f ≫ F.map S.g = 0
have rw₂ : Eq.{v_2 + 1} (α := F.obj S.X₁ ⟶ F.obj S.X₃) 0 0
Tactic: rw [← F.map_comp, S.zero, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ Eq (α := X₁ (X.map F) ⟶ X₂ (Y.map F)) (F.map φ.τ₁ ≫ f (Y.map F)) (f (X.map F) ≫ F.map φ.τ₂)
have dsimp : F.map φ.τ₁ ≫ F.map Y.f = F.map X.f ≫ F.map φ.τ₂
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ Eq (α := X₂ (X.map F) ⟶ X₃ (Y.map F)) (F.map φ.τ₂ ≫ g (Y.map F)) (g (X.map F) ≫ F.map φ.τ₃)
have dsimp : F.map φ.τ₂ ≫ F.map Y.g = F.map X.g ≫ F.map φ.τ₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ e₁.inv ≫ S₁.f = S₂.f ≫ e₂.inv
have rw : (e₁.inv ≫ S₁.f) ≫ e₂.hom = (S₂.f ≫ e₂.inv) ≫ e₂.hom
Tactic: rw [← cancel_mono e₂.hom, assoc, assoc, e₂.inv_hom_id, comp_id,
          ← comm₁₂, e₁.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ e₁.inv ≫ S₁.f = S₂.f ≫ e₂.inv
have rw₁ : e₁.inv ≫ S₁.f ≫ e₂.hom = (S₂.f ≫ e₂.inv) ≫ e₂.hom
Tactic: rw [← cancel_mono e₂.hom, assoc, assoc, e₂.inv_hom_id, comp_id,
          ← comm₁₂, e₁.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ e₁.inv ≫ S₁.f = S₂.f ≫ e₂.inv
have rw₂ : e₁.inv ≫ S₁.f ≫ e₂.hom = S₂.f ≫ e₂.inv ≫ e₂.hom
Tactic: rw [← cancel_mono e₂.hom, assoc, assoc, e₂.inv_hom_id, comp_id,
          ← comm₁₂, e₁.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ e₁.inv ≫ S₁.f = S₂.f ≫ e₂.inv
have rw₃ : e₁.inv ≫ S₁.f ≫ e₂.hom = S₂.f ≫ 𝟙 S₂.X₂
Tactic: rw [← cancel_mono e₂.hom, assoc, assoc, e₂.inv_hom_id, comp_id,
          ← comm₁₂, e₁.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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₂
⊢ e₁.inv ≫ S₁.f = S₂.f ≫ e₂.inv
have rw₄ : e₁.inv ≫ S₁.f ≫ e₂.hom = S₂.f
Tactic: rw [← cancel_mono e₂.hom, assoc, assoc, e₂.inv_hom_id, comp_id,
          ← comm₁₂, e₁.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ e₁.inv ≫ S₁.f = S₂.f ≫ e₂.inv
have rw₅ : e₁.inv ≫ e₁.hom ≫ S₂.f = S₂.f
Tactic: rw [← cancel_mono e₂.hom, assoc, assoc, e₂.inv_hom_id, comp_id,
          ← comm₁₂, e₁.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ e₁.inv ≫ S₁.f = S₂.f ≫ e₂.inv
have rw₆ : S₂.f = S₂.f
Tactic: rw [← cancel_mono e₂.hom, assoc, assoc, e₂.inv_hom_id, comp_id,
          ← comm₁₂, e₁.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ e₂.inv ≫ S₁.g = S₂.g ≫ e₃.inv
have rw : (e₂.inv ≫ S₁.g) ≫ e₃.hom = (S₂.g ≫ e₃.inv) ≫ e₃.hom
Tactic: rw [← cancel_mono e₃.hom, assoc, assoc, e₃.inv_hom_id, comp_id,
          ← comm₂₃, e₂.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ e₂.inv ≫ S₁.g = S₂.g ≫ e₃.inv
have rw₁ : e₂.inv ≫ S₁.g ≫ e₃.hom = (S₂.g ≫ e₃.inv) ≫ e₃.hom
Tactic: rw [← cancel_mono e₃.hom, assoc, assoc, e₃.inv_hom_id, comp_id,
          ← comm₂₃, e₂.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ e₂.inv ≫ S₁.g = S₂.g ≫ e₃.inv
have rw₂ : e₂.inv ≫ S₁.g ≫ e₃.hom = S₂.g ≫ e₃.inv ≫ e₃.hom
Tactic: rw [← cancel_mono e₃.hom, assoc, assoc, e₃.inv_hom_id, comp_id,
          ← comm₂₃, e₂.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ e₂.inv ≫ S₁.g = S₂.g ≫ e₃.inv
have rw₃ : e₂.inv ≫ S₁.g ≫ e₃.hom = S₂.g ≫ 𝟙 S₂.X₃
Tactic: rw [← cancel_mono e₃.hom, assoc, assoc, e₃.inv_hom_id, comp_id,
          ← comm₂₃, e₂.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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₃
⊢ e₂.inv ≫ S₁.g = S₂.g ≫ e₃.inv
have rw₄ : e₂.inv ≫ S₁.g ≫ e₃.hom = S₂.g
Tactic: rw [← cancel_mono e₃.hom, assoc, assoc, e₃.inv_hom_id, comp_id,
          ← comm₂₃, e₂.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ e₂.inv ≫ S₁.g = S₂.g ≫ e₃.inv
have rw₅ : e₂.inv ≫ e₂.hom ≫ S₂.g = S₂.g
Tactic: rw [← cancel_mono e₃.hom, assoc, assoc, e₃.inv_hom_id, comp_id,
          ← comm₂₃, e₂.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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
⊢ e₂.inv ≫ S₁.g = S₂.g ≫ e₃.inv
have rw₆ : S₂.g = S₂.g
Tactic: rw [← cancel_mono e₃.hom, assoc, assoc, e₃.inv_hom_id, comp_id,
          ← comm₂₃, e₂.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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.τ₃
have refine : IsIso f.τ₁ ∧ IsIso f.τ₂ ∧ IsIso f.τ₃ → IsIso f
Tactic: refine ⟨fun _ ↦ ⟨inferInstance, inferInstance, inferInstance⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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₁) (S.g.op ≫ S.f.op) 0
have simp : Eq.{v_1 + 1} (α := Opposite.op S.X₃ ⟶ Opposite.op S.X₁) (Quiver.Hom.op 0) 0
Tactic: simp only [← op_comp, S.zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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₂
⊢ φ.τ₃.op ≫ S₁.op.f = S₂.op.f ≫ φ.τ₂.op
have dsimp : Eq.{v_1 + 1} (α := Opposite.op S₂.X₃ ⟶ Opposite.op S₁.X₂) (φ.τ₃.op ≫ S₁.g.op) (S₂.g.op ≫ φ.τ₂.op)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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₂
⊢ φ.τ₂.op ≫ S₁.op.g = S₂.op.g ≫ φ.τ₁.op
have dsimp : Eq.{v_1 + 1} (α := Opposite.op S₂.X₂ ⟶ Opposite.op S₁.X₁) (φ.τ₂.op ≫ S₁.f.op) (S₂.f.op ≫ φ.τ₁.op)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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_1 S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} Cᵒᵖ
⊢ S.g.unop ≫ S.f.unop = 0
have simp : Eq.{v_1 + 1} (α := Opposite.unop S.X₃ ⟶ Opposite.unop S.X₁) (Quiver.Hom.unop 0) 0
Tactic: simp only [← unop_comp, S.zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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₁_1 S₂_1 S₃ : ShortComplex.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
φ : S₁ ⟶ S₂
⊢ φ.τ₃.unop ≫ S₁.unop.f = S₂.unop.f ≫ φ.τ₂.unop
have dsimp : φ.τ₃.unop ≫ S₁.g.unop = S₂.g.unop ≫ φ.τ₂.unop
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Basic (goal)
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₁_1 S₂_1 S₃ : ShortComplex.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
φ : S₁ ⟶ S₂
⊢ φ.τ₂.unop ≫ S₁.unop.g = S₂.unop.g ≫ φ.τ₁.unop
have dsimp : φ.τ₂.unop ≫ S₁.f.unop = S₂.f.unop ≫ φ.τ₁.unop
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 :
  HasForget₂.{w, v, u, u_1, w, w + 1, w} C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)
inst_4 : Preadditive.{v, u} C
inst_5 :
  Functor.Additive.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_7 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Mono f ↔
    Function.Injective (α :=
      (↑(Functor.obj.{v, w, u, w + 1}
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
              (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
            X) :
        Type w))
      (β :=
      (↑(Functor.obj.{v, w, u, w + 1}
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
              (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
            Y) :
        Type w))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj.{v, w, u, w + 1}
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
              X)
            (Functor.map
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
              f)) :
        (a : (↑((forget₂ C Ab).obj X) : Type w)) → (↑((forget₂ C Ab).obj Y) : Type w))
have rw : Mono f ↔
  Mono (X :=
    Functor.obj.{v, w, u, w + 1}
      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
        (CD := AddCommGrpCat.carrier))
      X)
    (Functor.map
      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
        (CD := AddCommGrpCat.carrier))
      f)
Tactic: rw [← AddCommGrpCat.mono_iff_injective]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 :
  HasForget₂.{w, v, u, u_1, w, w + 1, w} C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)
inst_4 : Preadditive.{v, u} C
inst_5 :
  Functor.Additive.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_7 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Mono f ↔
    Mono (X :=
      Functor.obj.{v, w, u, w + 1}
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        X)
      (Functor.map
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        f)
have mp : Mono f →
  Mono (X :=
    Functor.obj.{v, w, u, w + 1}
      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
        (CD := AddCommGrpCat.carrier))
      X)
    (Functor.map
      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
        (CD := AddCommGrpCat.carrier))
      f)
Tactic: constructor