awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_5 : S₁.HasHomology
inst_6 : S₂.HasHomology
inst_7 : HasHomology (Functor.obj F.mapShortComplex S₁)
inst_8 : HasHomology (Functor.obj F.mapShortComplex S₂)
inst_9 : F.PreservesRightHomologyOf S₁
inst_10 : F.PreservesRightHomologyOf S₂
inst_11 : F.ReflectsIsomorphisms
γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData
⊢ QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ) ↔ QuasiIso φ
have rw : IsIso (F.map γ.φH) ↔ IsIso γ.φH
Tactic: rw [γ.quasiIso_iff, (γ.map F).quasiIso_iff, RightHomologyMapData.map_φH]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_5 : S₁.HasHomology
inst_6 : S₂.HasHomology
inst_7 : HasHomology (Functor.obj F.mapShortComplex S₁)
inst_8 : HasHomology (Functor.obj F.mapShortComplex S₂)
inst_9 : F.PreservesRightHomologyOf S₁
inst_10 : F.PreservesRightHomologyOf S₂
inst_11 : F.ReflectsIsomorphisms
γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData
⊢ IsIso (F.map γ.φH) ↔ IsIso γ.φH
have mp : IsIso (F.map γ.φH) → IsIso γ.φH
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_5 : S₁.HasHomology
inst_6 : S₂.HasHomology
inst_7 : HasHomology (Functor.obj F.mapShortComplex S₁)
inst_8 : HasHomology (Functor.obj F.mapShortComplex S₂)
inst_9 : F.PreservesRightHomologyOf S₁
inst_10 : F.PreservesRightHomologyOf S₂
inst_11 : F.ReflectsIsomorphisms
γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData
mp : IsIso (F.map γ.φH) → IsIso γ.φH
⊢ IsIso (F.map γ.φH) ↔ IsIso γ.φH
have mpr : IsIso γ.φH → IsIso (F.map γ.φH)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S : ShortComplex.{v_1, u_1} C
hf : S.f = 0
inst_5 : PreservesLimit (parallelPair S.g 0) F
h : S.LeftHomologyData
⊢ h.f' = 0
have rw : h.f' ≫ h.i = 0 ≫ h.i
Tactic: rw [← cancel_mono h.i, h.f'_i, zero_comp, hf]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S : ShortComplex.{v_1, u_1} C
hf : S.f = 0
inst_5 : PreservesLimit (parallelPair S.g 0) F
h : S.LeftHomologyData
rw : h.f' ≫ h.i = 0 ≫ h.i
⊢ h.f' = 0
have rw₁ : S.f = 0 ≫ h.i
Tactic: rw [← cancel_mono h.i, h.f'_i, zero_comp, hf]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S : ShortComplex.{v_1, u_1} C
hf : S.f = 0
inst_5 : PreservesLimit (parallelPair S.g 0) F
h : S.LeftHomologyData
rw : h.f' ≫ h.i = 0 ≫ h.i
rw₁ : S.f = 0 ≫ h.i
rw₂ : S.f = 0
⊢ h.f' = 0
have rw₃ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
Tactic: rw [← cancel_mono h.i, h.f'_i, zero_comp, hf]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S : ShortComplex.{v_1, u_1} C
hg : S.g = 0
inst_5 : PreservesColimit (parallelPair S.f 0) F
h : S.RightHomologyData
⊢ h.g' = 0
have rw : h.p ≫ h.g' = h.p ≫ 0
Tactic: rw [← cancel_epi h.p, h.p_g', comp_zero, hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S : ShortComplex.{v_1, u_1} C
hg : S.g = 0
inst_5 : PreservesColimit (parallelPair S.f 0) F
h : S.RightHomologyData
rw : h.p ≫ h.g' = h.p ≫ 0
⊢ h.g' = 0
have rw₁ : S.g = h.p ≫ 0
Tactic: rw [← cancel_epi h.p, h.p_g', comp_zero, hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S : ShortComplex.{v_1, u_1} C
hg : S.g = 0
inst_5 : PreservesColimit (parallelPair S.f 0) F
h : S.RightHomologyData
rw : h.p ≫ h.g' = h.p ≫ 0
rw₁ : S.g = h.p ≫ 0
rw₂ : S.g = 0
⊢ h.g' = 0
have rw₃ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
Tactic: rw [← cancel_epi h.p, h.p_g', comp_zero, hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S : ShortComplex.{v_1, u_1} C
hg : S.g = 0
inst_5 : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
⊢ PreservesLimit (parallelPair S.g 0) F
have rw : PreservesLimit (parallelPair (X := S.X₂) (Y := S.X₃) 0 0) F
Tactic: rw [hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S : ShortComplex.{v_1, u_1} C
hg : S.g = 0
inst_5 : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
⊢ PreservesColimit (parallelPair h.f' 0) F
have this : IsIso h.i
Tactic: have := h.isIso_i hg
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S : ShortComplex.{v_1, u_1} C
hf : S.f = 0
inst_5 : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
⊢ PreservesColimit (parallelPair S.f 0) F
have rw : PreservesColimit (parallelPair (X := S.X₁) (Y := S.X₂) 0 0) F
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S : ShortComplex.{v_1, u_1} C
hf : S.f = 0
inst_5 : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
⊢ PreservesLimit (parallelPair h.g' 0) F
have this : IsIso h.p
Tactic: have := h.isIso_p hf
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F G : Functor.{v_1, v_2, u_1, u_2} C D
τ : F ⟶ G
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
inst_5 : F.PreservesZeroMorphisms
inst_6 : G.PreservesZeroMorphisms
inst_7 : F.PreservesLeftHomologyOf S
inst_8 : G.PreservesLeftHomologyOf S
inst_9 : F.PreservesRightHomologyOf S
inst_10 : G.PreservesRightHomologyOf S
⊢ Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (ShortComplex.homologyMap (S.mapNatTrans τ))
        (Iso.hom (S.mapHomologyIso G))))
have rw : Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
  (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map G))
      (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
        (τ.app S.homology ≫ Iso.inv (S.mapHomologyIso G)))
      (Iso.hom (S.mapHomologyIso G))))
Tactic: rw [ShortComplex.homologyMap_mapNatTrans, assoc, assoc, Iso.inv_hom_id,
    comp_id, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F G : Functor.{v_1, v_2, u_1, u_2} C D
τ : F ⟶ G
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
inst_5 : F.PreservesZeroMorphisms
inst_6 : G.PreservesZeroMorphisms
inst_7 : F.PreservesLeftHomologyOf S
inst_8 : G.PreservesLeftHomologyOf S
inst_9 : F.PreservesRightHomologyOf S
inst_10 : G.PreservesRightHomologyOf S
rw :
  Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := ShortComplex.homology (S.map G))
        (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
          (τ.app S.homology ≫ Iso.inv (S.mapHomologyIso G)))
        (Iso.hom (S.mapHomologyIso G))))
⊢ Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (ShortComplex.homologyMap (S.mapNatTrans τ))
        (Iso.hom (S.mapHomologyIso G))))
have rw₁ : Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
  (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
    (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (τ.app S.homology ≫ Iso.inv (S.mapHomologyIso G))
        (Iso.hom (S.mapHomologyIso G)))))
Tactic: rw [ShortComplex.homologyMap_mapNatTrans, assoc, assoc, Iso.inv_hom_id,
    comp_id, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F G : Functor.{v_1, v_2, u_1, u_2} C D
τ : F ⟶ G
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
inst_5 : F.PreservesZeroMorphisms
inst_6 : G.PreservesZeroMorphisms
inst_7 : F.PreservesLeftHomologyOf S
inst_8 : G.PreservesLeftHomologyOf S
inst_9 : F.PreservesRightHomologyOf S
inst_10 : G.PreservesRightHomologyOf S
rw :
  Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := ShortComplex.homology (S.map G))
        (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
          (τ.app S.homology ≫ Iso.inv (S.mapHomologyIso G)))
        (Iso.hom (S.mapHomologyIso G))))
rw₁ :
  Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
        (CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (τ.app S.homology ≫ Iso.inv (S.mapHomologyIso G))
          (Iso.hom (S.mapHomologyIso G)))))
⊢ Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (ShortComplex.homologyMap (S.mapNatTrans τ))
        (Iso.hom (S.mapHomologyIso G))))
have rw₂ : Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
  (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
    (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
      (τ.app S.homology ≫
        CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (Iso.inv (S.mapHomologyIso G))
          (Iso.hom (S.mapHomologyIso G)))))
Tactic: rw [ShortComplex.homologyMap_mapNatTrans, assoc, assoc, Iso.inv_hom_id,
    comp_id, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F G : Functor.{v_1, v_2, u_1, u_2} C D
τ : F ⟶ G
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
inst_5 : F.PreservesZeroMorphisms
inst_6 : G.PreservesZeroMorphisms
inst_7 : F.PreservesLeftHomologyOf S
inst_8 : G.PreservesLeftHomologyOf S
inst_9 : F.PreservesRightHomologyOf S
inst_10 : G.PreservesRightHomologyOf S
rw :
  Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := ShortComplex.homology (S.map G))
        (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
          (τ.app S.homology ≫ Iso.inv (S.mapHomologyIso G)))
        (Iso.hom (S.mapHomologyIso G))))
rw₁ :
  Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
        (CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (τ.app S.homology ≫ Iso.inv (S.mapHomologyIso G))
          (Iso.hom (S.mapHomologyIso G)))))
rw₂ :
  Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
        (τ.app S.homology ≫
          CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (Iso.inv (S.mapHomologyIso G))
            (Iso.hom (S.mapHomologyIso G)))))
⊢ Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (ShortComplex.homologyMap (S.mapNatTrans τ))
        (Iso.hom (S.mapHomologyIso G))))
have rw₃ : τ.app S.homology =
  CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
    (Iso.hom (S.mapHomologyIso F) ≫ τ.app S.homology ≫ 𝟙 (G.obj S.homology))
Tactic: rw [ShortComplex.homologyMap_mapNatTrans, assoc, assoc, Iso.inv_hom_id,
    comp_id, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F G : Functor.{v_1, v_2, u_1, u_2} C D
τ : F ⟶ G
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
inst_5 : F.PreservesZeroMorphisms
inst_6 : G.PreservesZeroMorphisms
inst_7 : F.PreservesLeftHomologyOf S
inst_8 : G.PreservesLeftHomologyOf S
inst_9 : F.PreservesRightHomologyOf S
inst_10 : G.PreservesRightHomologyOf S
rw :
  Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := ShortComplex.homology (S.map G))
        (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
          (τ.app S.homology ≫ Iso.inv (S.mapHomologyIso G)))
        (Iso.hom (S.mapHomologyIso G))))
rw₁ :
  Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
        (CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (τ.app S.homology ≫ Iso.inv (S.mapHomologyIso G))
          (Iso.hom (S.mapHomologyIso G)))))
rw₂ :
  Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
        (τ.app S.homology ≫
          CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (Iso.inv (S.mapHomologyIso G))
            (Iso.hom (S.mapHomologyIso G)))))
rw₃ :
  τ.app S.homology =
    CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (Iso.hom (S.mapHomologyIso F) ≫ τ.app S.homology ≫ 𝟙 (G.obj S.homology))
⊢ Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (ShortComplex.homologyMap (S.mapNatTrans τ))
        (Iso.hom (S.mapHomologyIso G))))
have rw₄ : Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
  (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
    (Iso.hom (S.mapHomologyIso F) ≫ τ.app S.homology))
Tactic: rw [ShortComplex.homologyMap_mapNatTrans, assoc, assoc, Iso.inv_hom_id,
    comp_id, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (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
F G : Functor.{v_1, v_2, u_1, u_2} C D
τ : F ⟶ G
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
inst_5 : F.PreservesZeroMorphisms
inst_6 : G.PreservesZeroMorphisms
inst_7 : F.PreservesLeftHomologyOf S
inst_8 : G.PreservesLeftHomologyOf S
inst_9 : F.PreservesRightHomologyOf S
inst_10 : G.PreservesRightHomologyOf S
rw :
  Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := ShortComplex.homology (S.map G))
        (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
          (τ.app S.homology ≫ Iso.inv (S.mapHomologyIso G)))
        (Iso.hom (S.mapHomologyIso G))))
rw₁ :
  Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
        (CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (τ.app S.homology ≫ Iso.inv (S.mapHomologyIso G))
          (Iso.hom (S.mapHomologyIso G)))))
rw₂ :
  Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
        (τ.app S.homology ≫
          CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (Iso.inv (S.mapHomologyIso G))
            (Iso.hom (S.mapHomologyIso G)))))
rw₃ :
  τ.app S.homology =
    CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (Iso.hom (S.mapHomologyIso F) ≫ τ.app S.homology ≫ 𝟙 (G.obj S.homology))
rw₄ :
  Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (Iso.hom (S.mapHomologyIso F) ≫ τ.app S.homology))
⊢ Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology)
    (CategoryStruct.comp (Y := ShortComplex.homology (S.map F)) (Iso.inv (S.mapHomologyIso F))
      (CategoryStruct.comp (Y := ShortComplex.homology (S.map G)) (ShortComplex.homologyMap (S.mapNatTrans τ))
        (Iso.hom (S.mapHomologyIso G))))
have rw₅ : Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology) (τ.app S.homology)
Tactic: rw [ShortComplex.homologyMap_mapNatTrans, assoc, assoc, Iso.inv_hom_id,
    comp_id, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ QuasiIso φ ↔ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
have mp : QuasiIso φ → IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
mp : QuasiIso φ → IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
⊢ QuasiIso φ ↔ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
have mpr : IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ) → QuasiIso φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
inst_5 : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
hφ' : QuasiIso φ'
⊢ QuasiIso (φ ≫ φ')
have rw : ∀ (hφ : IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ))
  (hφ' : IsIso (X := S₂.homology) (Y := S₃.homology) (homologyMap φ')),
  IsIso (X := S₁.homology) (Y := S₃.homology) (homologyMap (φ ≫ φ'))
Tactic: rw [quasiIso_iff] at hφ hφ' ⊢
Cleared hypotheses: hφ, hφ'
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
inst_5 : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
hφ' : IsIso (X := S₂.homology) (Y := S₃.homology) (homologyMap φ')
⊢ IsIso (X := S₁.homology) (Y := S₃.homology) (homologyMap (φ ≫ φ'))
have rw : IsIso (X := S₁.homology) (Y := S₃.homology) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (homologyMap φ'))
Tactic: rw [homologyMap_comp]