awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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₂ ≫ φ.τ₂
⊢ CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯) = 𝟙 S₁.X₂
have mpr₄ : φ.τ₂ = φ.τ₂
Tactic: rw [← cancel_mono φ.τ₂, assoc, h₁.lift_f, liftCycles_i, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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 φ.τ₂
⊢ h₁.lift S₂.iCycles ⋯ ≫ S₂.liftCycles φ.τ₂ ⋯ = 𝟙 S₂.cycles
have mpr : CategoryStruct.comp (Y := S₂.cycles) (h₁.lift S₂.iCycles sorry ≫ S₂.liftCycles φ.τ₂ sorry) S₂.iCycles = 𝟙 S₂.cycles ≫ S₂.iCycles
Tactic: rw [← cancel_mono S₂.iCycles, assoc, liftCycles_i, h₁.lift_f, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ h₁.lift S₂.iCycles ⋯ ≫ S₂.liftCycles φ.τ₂ ⋯ = 𝟙 S₂.cycles
have mpr₁ : h₁.lift S₂.iCycles sorry ≫ CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ sorry) S₂.iCycles = 𝟙 S₂.cycles ≫ S₂.iCycles
Tactic: rw [← cancel_mono S₂.iCycles, assoc, liftCycles_i, h₁.lift_f, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ h₁.lift S₂.iCycles ⋯ ≫ S₂.liftCycles φ.τ₂ ⋯ = 𝟙 S₂.cycles
have mpr₂ : h₁.lift S₂.iCycles sorry ≫ φ.τ₂ = 𝟙 S₂.cycles ≫ S₂.iCycles
Tactic: rw [← cancel_mono S₂.iCycles, assoc, liftCycles_i, h₁.lift_f, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ h₁.lift S₂.iCycles ⋯ ≫ S₂.liftCycles φ.τ₂ ⋯ = 𝟙 S₂.cycles
have mpr₃ : S₂.iCycles = 𝟙 S₂.cycles ≫ S₂.iCycles
Tactic: rw [← cancel_mono S₂.iCycles, assoc, liftCycles_i, h₁.lift_f, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ h₁.lift S₂.iCycles ⋯ ≫ S₂.liftCycles φ.τ₂ ⋯ = 𝟙 S₂.cycles
have mpr₄ : Eq (α := S₂.cycles ⟶ S₂.X₂) S₂.iCycles S₂.iCycles
Tactic: rw [← cancel_mono S₂.iCycles, assoc, liftCycles_i, h₁.lift_f, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S₁.f ≫ φ.τ₂ = 0
have rw : φ.τ₁ ≫ S₂.f = 0
Tactic: rw [← φ.comm₁₂, hf₂, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S₁.f ≫ φ.τ₂ = 0
have rw₁ : Eq (α := S₁.X₁ ⟶ S₂.X₂) (φ.τ₁ ≫ 0) 0
Tactic: rw [← φ.comm₁₂, hf₂, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S₁.f ≫ φ.τ₂ = 0
have rw₂ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ S₂.X₂) 0 0
Tactic: rw [← φ.comm₁₂, hf₂, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ QuasiIso φ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Epi φ.τ₂
have rw : Exact { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := sorry } ∧
    Mono (opMap φ).τ₂ ↔
  { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := sorry : ShortComplex.{v_1, u_1} C }.Exact ∧
    Epi φ.τ₂
Tactic: rw [← quasiIso_opMap_iff, quasiIso_iff_of_zeros]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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 φ.τ₂
⊢ QuasiIso φ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Epi φ.τ₂
have hf₁ : S₂.op.f = 0
Tactic: rw [← quasiIso_opMap_iff, quasiIso_iff_of_zeros]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ QuasiIso φ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Epi φ.τ₂
have hg₃ : S₂.op.g = 0
Tactic: rw [← quasiIso_opMap_iff, quasiIso_iff_of_zeros]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ QuasiIso φ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Epi φ.τ₂
have hf₃ : S₁.op.f = 0
Tactic: rw [← quasiIso_opMap_iff, quasiIso_iff_of_zeros]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S₂.op.f = 0
have hf₁ : S₂.g.op = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S₂.g.op = 0
have hf₁ : Eq.{v_1 + 1} (α := Opposite.op S₂.X₃ ⟶ Opposite.op S₂.X₂) (Quiver.Hom.op 0) 0
Tactic: rw [hg₂, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S₂.g.op = 0
have hf₃ : Eq.{v_1 + 1} (α := Opposite.op S₂.X₃ ⟶ Opposite.op S₂.X₂) 0 0
Tactic: rw [hg₂, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S₂.op.g = 0
have hg₃ : S₂.f.op = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S₂.f.op = 0
have hg₃ : Eq.{v_1 + 1} (α := Opposite.op S₂.X₂ ⟶ Opposite.op S₂.X₁) (Quiver.Hom.op 0) 0
Tactic: rw [hf₂, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S₂.f.op = 0
have hg₄ : Eq.{v_1 + 1} (α := Opposite.op S₂.X₂ ⟶ Opposite.op S₂.X₁) 0 0
Tactic: rw [hf₂, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S₁.op.f = 0
have hf₃ : S₁.g.op = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S₁.g.op = 0
have hf₃ : Eq.{v_1 + 1} (α := Opposite.op S₁.X₃ ⟶ Opposite.op S₁.X₂) (Quiver.Hom.op 0) 0
Tactic: rw [hg₁, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S₁.g.op = 0
have hf₄ : Eq.{v_1 + 1} (α := Opposite.op S₁.X₃ ⟶ Opposite.op S₁.X₂) 0 0
Tactic: rw [hg₁, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ 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 φ.τ₂
have rw : Exact (unop { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := sorry }) ∧
    Mono (opMap φ).τ₂ ↔
  { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := sorry : ShortComplex.{v_1, u_1} C }.Exact ∧
    Epi φ.τ₂
Tactic: rw [← exact_unop_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
⊢ 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 φ.τ₂
have this : 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 _⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
⊢ S.X₃ ⟶ J
have this : Mono (X := S.opcycles) S.fromOpcycles
Tactic: have := hS.mono_fromOpcycles
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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 ≫ hS.descToInjective f hf = f
have dsimp : S.g ≫ Injective.factorThru (X := S.opcycles) (S.descOpcycles f hf) S.fromOpcycles = f
Tactic: dsimp [descToInjective]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
⊢ P ⟶ S.X₁
have this : Epi (Y := S.cycles) S.toCycles
Tactic: have := hS.epi_toCycles
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ hS.liftFromProjective f hf ≫ S.f = f
have dsimp : Projective.factorThru (X := S.cycles) (S.liftCycles f hf) S.toCycles ≫ S.f = f
Tactic: dsimp [liftFromProjective]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ Projective.factorThru (X := S.cycles) (S.liftCycles f hf) S.toCycles ≫ S.f = f
have rw : Projective.factorThru (X := S.cycles) (S.liftCycles f hf) S.toCycles ≫
    CategoryStruct.comp (Y := S.cycles) S.toCycles S.iCycles =
  f
Tactic: rw [← toCycles_i, Projective.factorThru_comp_assoc, liftCycles_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ Projective.factorThru (X := S.cycles) (S.liftCycles f hf) S.toCycles ≫ S.f = f
have rw₁ : CategoryStruct.comp (Y := S.cycles) (S.liftCycles f hf) S.iCycles = f
Tactic: rw [← toCycles_i, Projective.factorThru_comp_assoc, liftCycles_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ Projective.factorThru (X := S.cycles) (S.liftCycles f hf) S.toCycles ≫ S.f = f
have rw₂ : f = f
Tactic: rw [← toCycles_i, Projective.factorThru_comp_assoc, liftCycles_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯ = 𝟙 S.X₁
have rw : (S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) sorry) ≫ S.f = 𝟙 S.X₁ ≫ S.f
Tactic: rw [← cancel_mono S.f, assoc, Exact.lift_f, comp_sub, comp_id,
    zero_assoc, zero_comp, sub_zero, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯ = 𝟙 S.X₁
have rw₁ : S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) sorry ≫ S.f = 𝟙 S.X₁ ≫ S.f
Tactic: rw [← cancel_mono S.f, assoc, Exact.lift_f, comp_sub, comp_id,
    zero_assoc, zero_comp, sub_zero, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯ = 𝟙 S.X₁
have rw₂ : S.f ≫ (𝟙 S.X₂ - S.g ≫ s) = 𝟙 S.X₁ ≫ S.f
Tactic: rw [← cancel_mono S.f, assoc, Exact.lift_f, comp_sub, comp_id,
    zero_assoc, zero_comp, sub_zero, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯ = 𝟙 S.X₁
have rw₃ : S.f ≫ 𝟙 S.X₂ - S.f ≫ S.g ≫ s = 𝟙 S.X₁ ≫ S.f
Tactic: rw [← cancel_mono S.f, assoc, Exact.lift_f, comp_sub, comp_id,
    zero_assoc, zero_comp, sub_zero, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯ = 𝟙 S.X₁
have rw₄ : S.f - S.f ≫ S.g ≫ s = 𝟙 S.X₁ ≫ S.f
Tactic: rw [← cancel_mono S.f, assoc, Exact.lift_f, comp_sub, comp_id,
    zero_assoc, zero_comp, sub_zero, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯ = 𝟙 S.X₁
have rw₅ : S.f - 0 ≫ s = 𝟙 S.X₁ ≫ S.f
Tactic: rw [← cancel_mono S.f, assoc, Exact.lift_f, comp_sub, comp_id,
    zero_assoc, zero_comp, sub_zero, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯ = 𝟙 S.X₁
have rw₆ : S.f - 0 = 𝟙 S.X₁ ≫ S.f
Tactic: rw [← cancel_mono S.f, assoc, Exact.lift_f, comp_sub, comp_id,
    zero_assoc, zero_comp, sub_zero, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯ = 𝟙 S.X₁
have rw₇ : S.f = 𝟙 S.X₁ ≫ S.f
Tactic: rw [← cancel_mono S.f, assoc, Exact.lift_f, comp_sub, comp_id,
    zero_assoc, zero_comp, sub_zero, id_comp]