awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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.LeftHomologyData
h₂ : S.RightHomologyData
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₂
hl₁ : S₁.LeftHomologyData
hr₁ : S₁.RightHomologyData
hl₂ : S₂.LeftHomologyData
hr₂ : S₂.RightHomologyData
ψl : LeftHomologyMapData φ hl₁ hl₂
ψr : RightHomologyMapData φ hr₁ hr₂
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 : QuasiIso φ
γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData
⊢ IsIso γ.φH

Tactic:
have : IsIso γ.φH := by
    rw [← γ.quasiIso_iff]
    infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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.LeftHomologyData
h₂ : S.RightHomologyData
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₂
hl₁ : S₁.LeftHomologyData
hr₁ : S₁.RightHomologyData
hl₂ : S₂.LeftHomologyData
hr₂ : S₂.RightHomologyData
ψl : LeftHomologyMapData φ hl₁ hl₂
ψr : RightHomologyMapData φ hr₁ hr₂
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 : QuasiIso φ
γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData
this : IsIso γ.φH
rw : IsIso (F.map γ.φH)
⊢ QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ)

Tactic:
rw [(γ.map F).quasiIso_iff, RightHomologyMapData.map_φH]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.map, CategoryTheory.ShortComplex.RightHomologyMapData.map_φH, CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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.LeftHomologyData
h₂ : S.RightHomologyData
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₂
hl₁ : S₁.LeftHomologyData
hr₁ : S₁.RightHomologyData
hl₂ : S₂.LeftHomologyData
hr₂ : S₂.RightHomologyData
ψl : LeftHomologyMapData φ hl₁ hl₂
ψr : RightHomologyMapData φ hr₁ hr₂
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 : QuasiIso φ
γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData
this : IsIso γ.φH
⊢ IsIso (F.map γ.φH)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
have :
  ∀ (γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData),
    QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ) ↔ QuasiIso φ
⊢ QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ) ↔ QuasiIso φ

Tactic:
have γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData := default
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
rw : IsIso (F.map γ.φH) ↔ IsIso γ.φH
⊢ QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ) ↔ QuasiIso φ

Tactic:
rw [γ.quasiIso_iff, (γ.map F).quasiIso_iff, RightHomologyMapData.map_φH]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.map, CategoryTheory.ShortComplex.RightHomologyMapData.map_φH, CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
mpr : IsIso γ.φH → IsIso (F.map γ.φH)
⊢ IsIso (F.map γ.φH) ↔ IsIso γ.φH

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
h : IsIso (F.map γ.φH)
⊢ IsIso γ.φH

Tactic:
isIso_of_reflects_iso _ F

Premises used: CategoryTheory.isIso_of_reflects_iso
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
h : IsIso (F.map γ.φH)
⊢ IsIso γ.φH

Tactic:
exact isIso_of_reflects_iso _ F

Premises used: CategoryTheory.isIso_of_reflects_iso
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
h : IsIso γ.φH
⊢ IsIso (F.map γ.φH)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
⊢ PreservesLimit (parallelPair S.g 0) F

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
rw₃ rw₄ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
⊢ h.f' = 0

Tactic:
rw [← cancel_mono h.i, h.f'_i, zero_comp, hf]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.f'_i, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.LeftHomologyData.i
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
⊢ PreservesColimit (parallelPair S.f 0) F

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
rw₃ rw₄ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
⊢ h.g' = 0

Tactic:
rw [← cancel_epi h.p, h.p_g', comp_zero, hg]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p, CategoryTheory.ShortComplex.RightHomologyData.p_g'
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
rw : PreservesLimit (parallelPair (X := S.X₂) (Y := S.X₃) 0 0) F
⊢ PreservesLimit (parallelPair S.g 0) F

Tactic:
rw [hg]
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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 (X := S.X₂) (Y := S.X₃) 0 0) F

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
⊢ IsIso h.i

Tactic:
have := h.isIso_i hg
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
this : IsIso h.i
⊢ (parallelPair h.f' 0).map WalkingParallelPairHom.left ≫ (asIso h.i).hom =
    Iso.hom (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair S.f 0).map WalkingParallelPairHom.left

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
this : IsIso h.i
⊢ (parallelPair h.f' 0).map WalkingParallelPairHom.right ≫ (asIso h.i).hom =
    Iso.hom (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair S.f 0).map WalkingParallelPairHom.right

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
this : IsIso h.i
e : parallelPair h.f' 0 ≅ parallelPair S.f 0 :=
  parallelPair.ext (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)) (asIso h.i) ⋯ ⋯
⊢ PreservesColimit (parallelPair h.f' 0) F

Tactic:
Limits.preservesColimit_of_iso_diagram F e.symm

Premises used: CategoryTheory.Limits.preservesColimit_of_iso_diagram, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
this : IsIso h.i
e : parallelPair h.f' 0 ≅ parallelPair S.f 0 :=
  parallelPair.ext (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)) (asIso h.i) ⋯ ⋯
⊢ PreservesColimit (parallelPair h.f' 0) F

Tactic:
exact Limits.preservesColimit_of_iso_diagram F e.symm

Premises used: CategoryTheory.Limits.preservesColimit_of_iso_diagram, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
rw : PreservesColimit (parallelPair (X := S.X₁) (Y := S.X₂) 0 0) F
⊢ PreservesColimit (parallelPair S.f 0) F

Tactic:
rw [hf]
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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 (X := S.X₁) (Y := S.X₂) 0 0) F

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
⊢ IsIso h.p

Tactic:
have := h.isIso_p hf
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
this : IsIso h.p
⊢ (parallelPair S.g 0).map WalkingParallelPairHom.left ≫
      Iso.hom (Iso.refl ((parallelPair S.g 0).obj WalkingParallelPair.one)) =
    (asIso h.p).hom ≫ (parallelPair h.g' 0).map WalkingParallelPairHom.left

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
this : IsIso h.p
⊢ (parallelPair S.g 0).map WalkingParallelPairHom.right ≫
      Iso.hom (Iso.refl ((parallelPair S.g 0).obj WalkingParallelPair.one)) =
    (asIso h.p).hom ≫ (parallelPair h.g' 0).map WalkingParallelPairHom.right

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
this : IsIso h.p
e : parallelPair S.g 0 ≅ parallelPair h.g' 0 :=
  parallelPair.ext (asIso h.p) (Iso.refl ((parallelPair S.g 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ PreservesLimit (parallelPair h.g' 0) F

Tactic:
Limits.preservesLimit_of_iso_diagram F e

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
this : IsIso h.p
e : parallelPair S.g 0 ≅ parallelPair h.g' 0 :=
  parallelPair.ext (asIso h.p) (Iso.refl ((parallelPair S.g 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ PreservesLimit (parallelPair h.g' 0) F

Tactic:
exact Limits.preservesLimit_of_iso_diagram F e

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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))
rw₅ rw₆ : Eq (α := F.obj S.homology ⟶ G.obj S.homology) (τ.app S.homology) (τ.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))))

Tactic:
rw [ShortComplex.homologyMap_mapNatTrans, assoc, assoc, Iso.inv_hom_id,
    comp_id, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.homologyMap_mapNatTrans, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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₂
inst_6 : QuasiIso φ
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
QuasiIso.isIso'

Premises used: CategoryTheory.ShortComplex.QuasiIso.isIso'
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 φ)
mpr : IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ) → QuasiIso φ
⊢ QuasiIso φ ↔ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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₂
h : QuasiIso φ
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
infer_instance