awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology
have refine_1 : (homologyMap φ ≫ z) ≫ S₁.homologyι = 𝟙 S₁.homology ≫ S₁.homologyι
Tactic: rw [← cancel_mono S₁.homologyι, id_comp, assoc, hz, homologyι_naturality_assoc,
      IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_1 : (homologyMap φ ≫ z) ≫ S₁.homologyι = 𝟙 S₁.homology ≫ S₁.homologyι
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology
have refine_1₁ : Eq (α := S₁.homology ⟶ S₁.opcycles) ((homologyMap φ ≫ z) ≫ S₁.homologyι) S₁.homologyι
Tactic: rw [← cancel_mono S₁.homologyι, id_comp, assoc, hz, homologyι_naturality_assoc,
      IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_1 : (homologyMap φ ≫ z) ≫ S₁.homologyι = 𝟙 S₁.homology ≫ S₁.homologyι
refine_1₁ : Eq (α := S₁.homology ⟶ S₁.opcycles) ((homologyMap φ ≫ z) ≫ S₁.homologyι) S₁.homologyι
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology
have refine_1₂ : Eq (α := S₁.homology ⟶ S₁.opcycles) (homologyMap φ ≫ z ≫ S₁.homologyι) S₁.homologyι
Tactic: rw [← cancel_mono S₁.homologyι, id_comp, assoc, hz, homologyι_naturality_assoc,
      IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_1 : (homologyMap φ ≫ z) ≫ S₁.homologyι = 𝟙 S₁.homology ≫ S₁.homologyι
refine_1₁ : Eq (α := S₁.homology ⟶ S₁.opcycles) ((homologyMap φ ≫ z) ≫ S₁.homologyι) S₁.homologyι
refine_1₂ : Eq (α := S₁.homology ⟶ S₁.opcycles) (homologyMap φ ≫ z ≫ S₁.homologyι) S₁.homologyι
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology
have refine_1₃ : Eq (α := S₁.homology ⟶ S₁.opcycles)
  (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (S₂.homologyι ≫ inv (opcyclesMap φ))) S₁.homologyι
Tactic: rw [← cancel_mono S₁.homologyι, id_comp, assoc, hz, homologyι_naturality_assoc,
      IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_1 : (homologyMap φ ≫ z) ≫ S₁.homologyι = 𝟙 S₁.homology ≫ S₁.homologyι
refine_1₁ : Eq (α := S₁.homology ⟶ S₁.opcycles) ((homologyMap φ ≫ z) ≫ S₁.homologyι) S₁.homologyι
refine_1₂ : Eq (α := S₁.homology ⟶ S₁.opcycles) (homologyMap φ ≫ z ≫ S₁.homologyι) S₁.homologyι
refine_1₃ :
  Eq (α := S₁.homology ⟶ S₁.opcycles)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (S₂.homologyι ≫ inv (opcyclesMap φ))) S₁.homologyι
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology
have refine_1₄ : Eq (α := S₁.homology ⟶ S₁.opcycles)
  (S₁.homologyι ≫ CategoryStruct.comp (Y := S₂.opcycles) (opcyclesMap φ) (inv (opcyclesMap φ))) S₁.homologyι
Tactic: rw [← cancel_mono S₁.homologyι, id_comp, assoc, hz, homologyι_naturality_assoc,
      IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_1 : (homologyMap φ ≫ z) ≫ S₁.homologyι = 𝟙 S₁.homology ≫ S₁.homologyι
refine_1₁ : Eq (α := S₁.homology ⟶ S₁.opcycles) ((homologyMap φ ≫ z) ≫ S₁.homologyι) S₁.homologyι
refine_1₂ : Eq (α := S₁.homology ⟶ S₁.opcycles) (homologyMap φ ≫ z ≫ S₁.homologyι) S₁.homologyι
refine_1₃ :
  Eq (α := S₁.homology ⟶ S₁.opcycles)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (S₂.homologyι ≫ inv (opcyclesMap φ))) S₁.homologyι
refine_1₄ :
  Eq (α := S₁.homology ⟶ S₁.opcycles)
    (S₁.homologyι ≫ CategoryStruct.comp (Y := S₂.opcycles) (opcyclesMap φ) (inv (opcyclesMap φ))) S₁.homologyι
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology
have refine_1₅ : Eq (α := S₁.homology ⟶ S₁.opcycles) (S₁.homologyι ≫ 𝟙 S₁.opcycles) S₁.homologyι
Tactic: rw [← cancel_mono S₁.homologyι, id_comp, assoc, hz, homologyι_naturality_assoc,
      IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_1 : (homologyMap φ ≫ z) ≫ S₁.homologyι = 𝟙 S₁.homology ≫ S₁.homologyι
refine_1₁ : Eq (α := S₁.homology ⟶ S₁.opcycles) ((homologyMap φ ≫ z) ≫ S₁.homologyι) S₁.homologyι
refine_1₂ : Eq (α := S₁.homology ⟶ S₁.opcycles) (homologyMap φ ≫ z ≫ S₁.homologyι) S₁.homologyι
refine_1₃ :
  Eq (α := S₁.homology ⟶ S₁.opcycles)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (S₂.homologyι ≫ inv (opcyclesMap φ))) S₁.homologyι
refine_1₄ :
  Eq (α := S₁.homology ⟶ S₁.opcycles)
    (S₁.homologyι ≫ CategoryStruct.comp (Y := S₂.opcycles) (opcyclesMap φ) (inv (opcyclesMap φ))) S₁.homologyι
refine_1₅ : Eq (α := S₁.homology ⟶ S₁.opcycles) (S₁.homologyι ≫ 𝟙 S₁.opcycles) S₁.homologyι
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology
have refine_1₆ : Eq (α := S₁.homology ⟶ S₁.opcycles) S₁.homologyι S₁.homologyι
Tactic: rw [← cancel_mono S₁.homologyι, id_comp, assoc, hz, homologyι_naturality_assoc,
      IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology
have refine_2 : CategoryStruct.comp (Y := S₂.homology) (z ≫ homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
Tactic: rw [← cancel_mono S₂.homologyι, assoc, homologyι_naturality, reassoc_of% hz,
      IsIso.inv_hom_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_2 : CategoryStruct.comp (Y := S₂.homology) (z ≫ homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology
have refine_2₁ : z ≫ CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
Tactic: rw [← cancel_mono S₂.homologyι, assoc, homologyι_naturality, reassoc_of% hz,
      IsIso.inv_hom_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_2 : CategoryStruct.comp (Y := S₂.homology) (z ≫ homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₁ : z ≫ CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology
have refine_2₂ : z ≫ S₁.homologyι ≫ opcyclesMap φ = 𝟙 S₂.homology ≫ S₂.homologyι
Tactic: rw [← cancel_mono S₂.homologyι, assoc, homologyι_naturality, reassoc_of% hz,
      IsIso.inv_hom_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_2 : CategoryStruct.comp (Y := S₂.homology) (z ≫ homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₁ : z ≫ CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₂ : z ≫ S₁.homologyι ≫ opcyclesMap φ = 𝟙 S₂.homology ≫ S₂.homologyι
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology
have refine_2₃ : S₂.homologyι ≫ CategoryStruct.comp (Y := S₁.opcycles) (inv (opcyclesMap φ)) (opcyclesMap φ) =
  𝟙 S₂.homology ≫ S₂.homologyι
Tactic: rw [← cancel_mono S₂.homologyι, assoc, homologyι_naturality, reassoc_of% hz,
      IsIso.inv_hom_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_2 : CategoryStruct.comp (Y := S₂.homology) (z ≫ homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₁ : z ≫ CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₂ : z ≫ S₁.homologyι ≫ opcyclesMap φ = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₃ :
  S₂.homologyι ≫ CategoryStruct.comp (Y := S₁.opcycles) (inv (opcyclesMap φ)) (opcyclesMap φ) =
    𝟙 S₂.homology ≫ S₂.homologyι
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology
have refine_2₄ : S₂.homologyι ≫ 𝟙 S₂.opcycles = 𝟙 S₂.homology ≫ S₂.homologyι
Tactic: rw [← cancel_mono S₂.homologyι, assoc, homologyι_naturality, reassoc_of% hz,
      IsIso.inv_hom_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_2 : CategoryStruct.comp (Y := S₂.homology) (z ≫ homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₁ : z ≫ CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₂ : z ≫ S₁.homologyι ≫ opcyclesMap φ = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₃ :
  S₂.homologyι ≫ CategoryStruct.comp (Y := S₁.opcycles) (inv (opcyclesMap φ)) (opcyclesMap φ) =
    𝟙 S₂.homology ≫ S₂.homologyι
refine_2₄ : S₂.homologyι ≫ 𝟙 S₂.opcycles = 𝟙 S₂.homology ≫ S₂.homologyι
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology
have refine_2₅ : S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
Tactic: rw [← cancel_mono S₂.homologyι, assoc, homologyι_naturality, reassoc_of% hz,
      IsIso.inv_hom_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_2 : CategoryStruct.comp (Y := S₂.homology) (z ≫ homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₁ : z ≫ CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₂ : z ≫ S₁.homologyι ≫ opcyclesMap φ = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₃ :
  S₂.homologyι ≫ CategoryStruct.comp (Y := S₁.opcycles) (inv (opcyclesMap φ)) (opcyclesMap φ) =
    𝟙 S₂.homology ≫ S₂.homologyι
refine_2₄ : S₂.homologyι ≫ 𝟙 S₂.opcycles = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₅ : S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology
have refine_2₆ : Eq (α := S₂.homology ⟶ S₂.opcycles) S₂.homologyι S₂.homologyι
Tactic: rw [← cancel_mono S₂.homologyι, assoc, homologyι_naturality, reassoc_of% hz,
      IsIso.inv_hom_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hf : S.f = 0
inst_2 : S.HasHomology
⊢ IsIso (X := S.cycles) (Y := S.homology) S.homologyπ
have this : IsIso (X := S.cycles) S.leftHomologyπ
Tactic: have := S.isIso_leftHomologyπ hf
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hf : S.f = 0
inst_2 : S.HasHomology
this : IsIso (X := S.cycles) S.leftHomologyπ
⊢ IsIso (X := S.cycles) (Y := S.homology) S.homologyπ
have dsimp : IsIso (X := S.cycles) (Y := S.homology) (S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso)
Tactic: dsimp only [homologyπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hg : S.g = 0
inst_2 : S.HasHomology
⊢ IsIso (X := S.homology) S.homologyι
have this : IsIso (X := S.rightHomology) S.rightHomologyι
Tactic: have := S.isIso_rightHomologyι hg
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hg : S.g = 0
inst_2 : S.HasHomology
this : IsIso (X := S.rightHomology) S.rightHomologyι
⊢ IsIso (X := S.homology) S.homologyι
have dsimp : IsIso (X := S.homology) (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι)
Tactic: dsimp only [homologyι]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
hf : S.f = 0
inst_2 : S.HasHomology
⊢ S.cycles ≅ S.homology
have this : IsIso (X := S.cycles) (Y := S.homology) S.homologyπ
Tactic: have := S.isIso_homologyπ hf
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
hg : S.g = 0
inst_2 : S.HasHomology
⊢ S.homology ≅ S.opcycles
have this : IsIso (X := S.homology) S.homologyι
Tactic: have := S.isIso_homologyι hg
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h : Mono (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
⊢ Mono (X := S₁.homology) (Y := S₂.opcycles)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι : S₁.homology ⟶ S₂.opcycles)
have rw : Mono (X := S₁.homology) (Y := S₂.opcycles) (S₁.homologyι ≫ opcyclesMap φ)
Tactic: rw [homologyι_naturality φ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h : Mono (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
⊢ Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
have this : Mono (X := S₁.homology) (Y := S₂.opcycles)
  (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι : S₁.homology ⟶ S₂.opcycles)
Tactic: have : Mono (homologyMap φ ≫ S₂.homologyι) := by
    rw [homologyι_naturality φ]
    apply mono_comp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h : Epi (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
⊢ Epi (X := S₁.cycles) (Y := S₂.homology)
    (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ) : S₁.cycles ⟶ S₂.homology)
have rw : Epi (X := S₁.cycles) (Y := S₂.homology) (cyclesMap φ ≫ S₂.homologyπ)
Tactic: rw [homologyπ_naturality φ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h : Epi (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
⊢ Epi (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
have this : Epi (X := S₁.cycles) (Y := S₂.homology)
  (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ) : S₁.cycles ⟶ S₂.homology)
Tactic: have : Epi (S₁.homologyπ ≫ homologyMap φ) := by
    rw [homologyπ_naturality φ]
    apply epi_comp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ k ≫ S.g = 0
have rw : (x ≫ S.f) ≫ S.g = 0
Tactic: rw [hx, assoc, S.zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
rw : (x ≫ S.f) ≫ S.g = 0
⊢ k ≫ S.g = 0
have rw₁ : x ≫ S.f ≫ S.g = 0
Tactic: rw [hx, assoc, S.zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
rw : (x ≫ S.f) ≫ S.g = 0
rw₁ : x ≫ S.f ≫ S.g = 0
⊢ k ≫ S.g = 0
have rw₂ : Eq (α := A ⟶ S.X₃) (x ≫ 0) 0
Tactic: rw [hx, assoc, S.zero, comp_zero]