awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasKernel S.g
inst_4 : HasCokernel S.f
this : HasCokernel (Y := kernel S.g) (kernel.lift S.g S.f ⋯)
⊢ S.Exact ↔ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
have this₁ : HasKernel (X := cokernel S.f) (cokernel.desc S.f S.g sorry)
Tactic: haveI := HasRightHomology.hasKernel S
-- 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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
⊢ S.op.Exact
have obtain : ∀ (h : S.HomologyData) (z : IsZero.{v_1, u_1} h.left.H), S.op.Exact
Tactic: obtain ⟨h, z⟩ := h
Cleared hypotheses: h
-- 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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} Cᵒᵖ
h : S.Exact
⊢ S.unop.Exact
have obtain : ∀ (h : S.HomologyData) (z : IsZero.{v_1, u_1} h.left.H), S.unop.Exact
Tactic: obtain ⟨h, z⟩ := h
Cleared hypotheses: h
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.Exact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesLeftHomologyOf S
inst_6 : HasHomology (S.map F)
⊢ Exact (S.map F)
have this : S.HasHomology
Tactic: have := h.hasHomology
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.Exact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesLeftHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
⊢ Exact (S.map F)
have h₁ : Eq.{v_1 + 1} (α := S.leftHomologyData.H ⟶ S.leftHomologyData.H) (𝟙 S.leftHomologyData.H) 0
Tactic: rw [S.leftHomologyData.exact_iff, IsZero.iff_id_eq_zero] at h
Cleared hypotheses: h
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesLeftHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
h : Eq.{v_1 + 1} (α := S.leftHomologyData.H ⟶ S.leftHomologyData.H) (𝟙 S.leftHomologyData.H) 0
⊢ Exact (S.map F)
have rw : IsZero.{v_2, u_2} (F.obj S.leftHomologyData.H)
Tactic: rw [S.leftHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesLeftHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
h : Eq.{v_1 + 1} (α := S.leftHomologyData.H ⟶ S.leftHomologyData.H) (𝟙 S.leftHomologyData.H) 0
rw : IsZero.{v_2, u_2} (F.obj S.leftHomologyData.H)
⊢ Exact (S.map F)
have rw₁ : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (𝟙 (F.obj S.leftHomologyData.H)) 0
Tactic: rw [S.leftHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesLeftHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
h : Eq.{v_1 + 1} (α := S.leftHomologyData.H ⟶ S.leftHomologyData.H) (𝟙 S.leftHomologyData.H) 0
rw : IsZero.{v_2, u_2} (F.obj S.leftHomologyData.H)
rw₁ : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (𝟙 (F.obj S.leftHomologyData.H)) 0
⊢ Exact (S.map F)
have rw₂ : F.map (𝟙 S.leftHomologyData.H) = 0
Tactic: rw [S.leftHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesLeftHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
h : Eq.{v_1 + 1} (α := S.leftHomologyData.H ⟶ S.leftHomologyData.H) (𝟙 S.leftHomologyData.H) 0
rw : IsZero.{v_2, u_2} (F.obj S.leftHomologyData.H)
rw₁ : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (𝟙 (F.obj S.leftHomologyData.H)) 0
rw₂ : F.map (𝟙 S.leftHomologyData.H) = 0
⊢ Exact (S.map F)
have rw₃ : Eq (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (F.map 0) 0
Tactic: rw [S.leftHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesLeftHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
h : Eq.{v_1 + 1} (α := S.leftHomologyData.H ⟶ S.leftHomologyData.H) (𝟙 S.leftHomologyData.H) 0
rw : IsZero.{v_2, u_2} (F.obj S.leftHomologyData.H)
rw₁ : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (𝟙 (F.obj S.leftHomologyData.H)) 0
rw₂ : F.map (𝟙 S.leftHomologyData.H) = 0
rw₃ : Eq (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (F.map 0) 0
⊢ Exact (S.map F)
have rw₄ : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) 0 0
Tactic: rw [S.leftHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_zero]
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.Exact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesRightHomologyOf S
inst_6 : HasHomology (S.map F)
⊢ Exact (S.map F)
have this : S.HasHomology
Tactic: have : S.HasHomology := h.hasHomology
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.Exact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesRightHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
⊢ Exact (S.map F)
have h₁ : Eq.{v_1 + 1} (α := S.rightHomologyData.H ⟶ S.rightHomologyData.H) (𝟙 S.rightHomologyData.H) 0
Tactic: rw [S.rightHomologyData.exact_iff, IsZero.iff_id_eq_zero] at h
Cleared hypotheses: h
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesRightHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
h : Eq.{v_1 + 1} (α := S.rightHomologyData.H ⟶ S.rightHomologyData.H) (𝟙 S.rightHomologyData.H) 0
⊢ Exact (S.map F)
have rw : IsZero.{v_2, u_2} (F.obj S.rightHomologyData.H)
Tactic: rw [S.rightHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesRightHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
h : Eq.{v_1 + 1} (α := S.rightHomologyData.H ⟶ S.rightHomologyData.H) (𝟙 S.rightHomologyData.H) 0
rw : IsZero.{v_2, u_2} (F.obj S.rightHomologyData.H)
⊢ Exact (S.map F)
have rw₁ : Eq.{v_2 + 1} (α := F.obj S.rightHomologyData.H ⟶ F.obj S.rightHomologyData.H) (𝟙 (F.obj S.rightHomologyData.H)) 0
Tactic: rw [S.rightHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesRightHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
h : Eq.{v_1 + 1} (α := S.rightHomologyData.H ⟶ S.rightHomologyData.H) (𝟙 S.rightHomologyData.H) 0
rw : IsZero.{v_2, u_2} (F.obj S.rightHomologyData.H)
rw₁ : Eq.{v_2 + 1} (α := F.obj S.rightHomologyData.H ⟶ F.obj S.rightHomologyData.H) (𝟙 (F.obj S.rightHomologyData.H)) 0
⊢ Exact (S.map F)
have rw₂ : F.map (𝟙 S.rightHomologyData.H) = 0
Tactic: rw [S.rightHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesRightHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
h : Eq.{v_1 + 1} (α := S.rightHomologyData.H ⟶ S.rightHomologyData.H) (𝟙 S.rightHomologyData.H) 0
rw : IsZero.{v_2, u_2} (F.obj S.rightHomologyData.H)
rw₁ : Eq.{v_2 + 1} (α := F.obj S.rightHomologyData.H ⟶ F.obj S.rightHomologyData.H) (𝟙 (F.obj S.rightHomologyData.H)) 0
rw₂ : F.map (𝟙 S.rightHomologyData.H) = 0
⊢ Exact (S.map F)
have rw₃ : Eq (α := F.obj S.rightHomologyData.H ⟶ F.obj S.rightHomologyData.H) (F.map 0) 0
Tactic: rw [S.rightHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesRightHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
h : Eq.{v_1 + 1} (α := S.rightHomologyData.H ⟶ S.rightHomologyData.H) (𝟙 S.rightHomologyData.H) 0
rw : IsZero.{v_2, u_2} (F.obj S.rightHomologyData.H)
rw₁ : Eq.{v_2 + 1} (α := F.obj S.rightHomologyData.H ⟶ F.obj S.rightHomologyData.H) (𝟙 (F.obj S.rightHomologyData.H)) 0
rw₂ : F.map (𝟙 S.rightHomologyData.H) = 0
rw₃ : Eq (α := F.obj S.rightHomologyData.H ⟶ F.obj S.rightHomologyData.H) (F.map 0) 0
⊢ Exact (S.map F)
have rw₄ : Eq.{v_2 + 1} (α := F.obj S.rightHomologyData.H ⟶ F.obj S.rightHomologyData.H) 0 0
Tactic: rw [S.rightHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_zero]
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.Exact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesLeftHomologyOf S
inst_6 : F.PreservesRightHomologyOf S
⊢ Exact (S.map F)
have this : S.HasHomology
Tactic: have := h.hasHomology
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
inst_8 : F.Faithful
⊢ Exact (S.map F) ↔ S.Exact
have mp : Exact (S.map F) → S.Exact
Tactic: constructor
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
inst_8 : F.Faithful
mp : Exact (S.map F) → S.Exact
⊢ Exact (S.map F) ↔ S.Exact
have mpr : S.Exact → Exact (S.map F)
Tactic: constructor
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
inst_8 : F.Faithful
h : Exact (S.map F)
⊢ S.Exact
have mp : Eq.{v_1 + 1} (α := S.leftHomologyData.H ⟶ S.leftHomologyData.H) (𝟙 S.leftHomologyData.H) 0
Tactic: rw [S.leftHomologyData.exact_iff, IsZero.iff_id_eq_zero]
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
inst_8 : F.Faithful
h : Exact (S.map F)
⊢ Eq.{v_1 + 1} (α := S.leftHomologyData.H ⟶ S.leftHomologyData.H) (𝟙 S.leftHomologyData.H) 0
have h₁ : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (𝟙 (F.obj S.leftHomologyData.H)) 0
Tactic: rw [(S.leftHomologyData.map F).exact_iff, IsZero.iff_id_eq_zero,
      LeftHomologyData.map_H] at h
Cleared hypotheses: h
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
inst_8 : F.Faithful
h : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (𝟙 (F.obj S.leftHomologyData.H)) 0
⊢ Eq.{v_1 + 1} (α := S.leftHomologyData.H ⟶ S.leftHomologyData.H) (𝟙 S.leftHomologyData.H) 0
have mp : F.map (𝟙 S.leftHomologyData.H) = F.map 0
Tactic: apply F.map_injective
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
inst_8 : F.Faithful
h : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (𝟙 (F.obj S.leftHomologyData.H)) 0
⊢ F.map (𝟙 S.leftHomologyData.H) = F.map 0
have mp : 𝟙 (F.obj S.leftHomologyData.H) = F.map 0
Tactic: rw [F.map_id, F.map_zero, h]
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
inst_8 : F.Faithful
h : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (𝟙 (F.obj S.leftHomologyData.H)) 0
mp : 𝟙 (F.obj S.leftHomologyData.H) = F.map 0
mp₁ : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (𝟙 (F.obj S.leftHomologyData.H)) 0
⊢ F.map (𝟙 S.leftHomologyData.H) = F.map 0
have mp₂ : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) 0 0
Tactic: rw [F.map_id, F.map_zero, h]
-- 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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
⊢ a ≫ b = 0
have this : S.HasHomology
Tactic: have := h.hasHomology
-- 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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : S.Exact
⊢ a ≫ b = 0
have eq₁ : Eq (α := S.cycles ⟶ S.opcycles) (S.iCycles ≫ S.pOpcycles) 0
Tactic: rw [exact_iff_iCycles_pOpcycles_zero] at eq
Cleared hypotheses: eq
-- 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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : Eq (α := S.cycles ⟶ S.opcycles) (S.iCycles ≫ S.pOpcycles) 0
⊢ a ≫ b = 0
have rw : CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) S.iCycles ≫ b = 0
Tactic: rw [← S.liftCycles_i a ha, ← S.p_descOpcycles b hb, assoc, reassoc_of% eq,
    zero_comp, 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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : Eq (α := S.cycles ⟶ S.opcycles) (S.iCycles ≫ S.pOpcycles) 0
rw : CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) S.iCycles ≫ b = 0
⊢ a ≫ b = 0
have rw₁ : CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) S.iCycles ≫
    CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (S.descOpcycles b hb) =
  0
Tactic: rw [← S.liftCycles_i a ha, ← S.p_descOpcycles b hb, assoc, reassoc_of% eq,
    zero_comp, 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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : Eq (α := S.cycles ⟶ S.opcycles) (S.iCycles ≫ S.pOpcycles) 0
rw : CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) S.iCycles ≫ b = 0
rw₁ :
  CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) S.iCycles ≫
      CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (S.descOpcycles b hb) =
    0
⊢ a ≫ b = 0
have rw₂ : CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha)
    (S.iCycles ≫ CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (S.descOpcycles b hb)) =
  0
Tactic: rw [← S.liftCycles_i a ha, ← S.p_descOpcycles b hb, assoc, reassoc_of% eq,
    zero_comp, 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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : Eq (α := S.cycles ⟶ S.opcycles) (S.iCycles ≫ S.pOpcycles) 0
rw : CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) S.iCycles ≫ b = 0
rw₁ :
  CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) S.iCycles ≫
      CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (S.descOpcycles b hb) =
    0
rw₂ :
  CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha)
      (S.iCycles ≫ CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (S.descOpcycles b hb)) =
    0
⊢ a ≫ b = 0
have rw₃ : CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha)
    (CategoryStruct.comp (Y := S.opcycles) 0 (S.descOpcycles b hb)) =
  0
Tactic: rw [← S.liftCycles_i a ha, ← S.p_descOpcycles b hb, assoc, reassoc_of% eq,
    zero_comp, 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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : Eq (α := S.cycles ⟶ S.opcycles) (S.iCycles ≫ S.pOpcycles) 0
rw : CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) S.iCycles ≫ b = 0
rw₁ :
  CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) S.iCycles ≫
      CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (S.descOpcycles b hb) =
    0
rw₂ :
  CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha)
      (S.iCycles ≫ CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (S.descOpcycles b hb)) =
    0
rw₃ :
  CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha)
      (CategoryStruct.comp (Y := S.opcycles) 0 (S.descOpcycles b hb)) =
    0
⊢ a ≫ b = 0
have rw₄ : Eq (α := X ⟶ Y) (CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) 0) 0
Tactic: rw [← S.liftCycles_i a ha, ← S.p_descOpcycles b hb, assoc, reassoc_of% eq,
    zero_comp, 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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : Eq (α := S.cycles ⟶ S.opcycles) (S.iCycles ≫ S.pOpcycles) 0
rw : CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) S.iCycles ≫ b = 0
rw₁ :
  CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) S.iCycles ≫
      CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (S.descOpcycles b hb) =
    0
rw₂ :
  CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha)
      (S.iCycles ≫ CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (S.descOpcycles b hb)) =
    0
rw₃ :
  CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha)
      (CategoryStruct.comp (Y := S.opcycles) 0 (S.descOpcycles b hb)) =
    0
rw₄ : Eq (α := X ⟶ Y) (CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) 0) 0
⊢ a ≫ b = 0
have rw₅ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 0
Tactic: rw [← S.liftCycles_i a ha, ← S.p_descOpcycles b hb, assoc, reassoc_of% eq,
    zero_comp, comp_zero]