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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasHomology
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
w :
  ∀ (γ : HomologyMapData (S₁ := S.map F) (𝟙 (S.map F)) (homologyData (S.map F)) (S.homologyData.map F)),
    Eq (α := homology (S.map F) ⟶ F.obj S.homology)
      (Iso.hom (HomologyData.iso (homologyData (S.map F))) ≫
          rightHomologyMap' (𝟙 (S.map F)) (HomologyData.right (homologyData (S.map F))) (S.homologyData.right.map F) ≫
            F.map S.homologyData.iso.inv :
        homology (S.map F) ⟶ F.obj S.homology)
      (leftHomologyMap' (𝟙 (S.map F)) (HomologyData.left (homologyData (S.map F))) (S.homologyData.left.map F) :
        LeftHomologyData.H (S := S.map F) (HomologyData.left (homologyData (S.map F))) ⟶
          LeftHomologyData.H (S := S.map F) (S.homologyData.left.map F))
⊢ Eq (α := homology (S.map F) ⟶ F.obj S.homology)
    (Iso.hom (HomologyData.iso (homologyData (S.map F))) ≫
        rightHomologyMap' (𝟙 (S.map F)) (HomologyData.right (homologyData (S.map F))) (S.homologyData.right.map F) ≫
          F.map S.homologyData.iso.inv :
      homology (S.map F) ⟶ F.obj S.homology)
    (leftHomologyMap' (𝟙 (S.map F)) (HomologyData.left (homologyData (S.map F))) (S.homologyData.left.map F) :
      LeftHomologyData.H (S := S.map F) (HomologyData.left (homologyData (S.map F))) ⟶
        LeftHomologyData.H (S := S.map F) (S.homologyData.left.map F))

Tactic:
have γ : HomologyMapData (𝟙 (S.map F)) (map S F).homologyData (S.homologyData.map F) := 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
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 : S.HasHomology
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
γ : HomologyMapData (S₁ := S.map F) (𝟙 (S.map F)) (homologyData (S.map F)) (S.homologyData.map F)
⊢ γ.left.φH ≫ Iso.hom (HomologyData.iso (S.homologyData.map F)) =
    Iso.hom (HomologyData.iso (homologyData (S.map F))) ≫ γ.right.φH

Tactic:
have eq := γ.comm
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasHomology
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
γ : HomologyMapData (S₁ := S.map F) (𝟙 (S.map F)) (homologyData (S.map F)) (S.homologyData.map F)
eq :
  γ.left.φH ≫ Iso.hom (HomologyData.iso (S.homologyData.map F)) =
    Iso.hom (HomologyData.iso (homologyData (S.map F))) ≫ γ.right.φH
⊢ Eq (α :=
    LeftHomologyData.H (S := S.map F) (HomologyData.left (homologyData (S.map F))) ⟶
      RightHomologyData.H (S := S.map F) (HomologyData.right (S.homologyData.map F)))
    (leftHomologyMap' (𝟙 (S.map F)) (HomologyData.left (homologyData (S.map F)))
        (HomologyData.left (S.homologyData.map F)) ≫
      Iso.hom (HomologyData.iso (S.homologyData.map F)))
    (Iso.hom (HomologyData.iso (homologyData (S.map F))) ≫
      rightHomologyMap' (𝟙 (S.map F)) (HomologyData.right (homologyData (S.map F)))
        (HomologyData.right (S.homologyData.map F)))

Tactic:
rw [← γ.left.leftHomologyMap'_eq, ← γ.right.rightHomologyMap'_eq] at eq

Premises used: CategoryTheory.ShortComplex.HomologyMapData.right, CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq, CategoryTheory.ShortComplex.HomologyMapData.left, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasHomology
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
γ : HomologyMapData (S₁ := S.map F) (𝟙 (S.map F)) (homologyData (S.map F)) (S.homologyData.map F)
eq :
  Eq (α :=
    LeftHomologyData.H (S := S.map F) (HomologyData.left (homologyData (S.map F))) ⟶ F.obj S.homologyData.right.H)
    (leftHomologyMap' (𝟙 (S.map F)) (HomologyData.left (homologyData (S.map F))) (S.homologyData.left.map F) ≫
        F.map S.homologyData.iso.hom :
      LeftHomologyData.H (S := S.map F) (HomologyData.left (homologyData (S.map F))) ⟶ F.obj S.homologyData.right.H)
    (Iso.hom (HomologyData.iso (homologyData (S.map F))) ≫
        rightHomologyMap' (𝟙 (S.map F)) (HomologyData.right (homologyData (S.map F))) (S.homologyData.right.map F) :
      LeftHomologyData.H (S := S.map F) (HomologyData.left (homologyData (S.map F))) ⟶ F.obj S.homologyData.right.H)
⊢ Eq (α := homology (S.map F) ⟶ F.obj S.homology)
    (Iso.hom (HomologyData.iso (homologyData (S.map F))) ≫
        rightHomologyMap' (𝟙 (S.map F)) (HomologyData.right (homologyData (S.map F))) (S.homologyData.right.map F) ≫
          F.map S.homologyData.iso.inv :
      homology (S.map F) ⟶ F.obj S.homology)
    (leftHomologyMap' (𝟙 (S.map F)) (HomologyData.left (homologyData (S.map F))) (S.homologyData.left.map F) :
      LeftHomologyData.H (S := S.map F) (HomologyData.left (homologyData (S.map F))) ⟶
        LeftHomologyData.H (S := S.map F) (S.homologyData.left.map F))

Tactic:
simp only [← reassoc_of% eq, ← F.map_comp, Iso.hom_inv_id, F.map_id, comp_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- 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
F G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : G.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : G.PreservesLeftHomologyOf S
inst_8 : F.PreservesRightHomologyOf S
inst_9 : G.PreservesRightHomologyOf S
inst_10 : S.HasHomology
τ : F ⟶ G
⊢ Eq (α := homology (S.map F) ⟶ homology (S.map G)) (homologyMap (S.mapNatTrans τ))
    (CategoryStruct.comp (Y := F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
      (τ.app S.homology ≫ Iso.inv (S.mapHomologyIso G)))

Tactic:
(LeftHomologyMapData.natTransApp S.homologyData.left τ).homologyMap_eq

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_eq, CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp, CategoryTheory.ShortComplex.homologyData
-- 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₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
ψl : LeftHomologyMapData φ hl₁ hl₂
inst_5 : HasHomology (Functor.obj F.mapShortComplex S₁)
inst_6 : HasHomology (Functor.obj F.mapShortComplex S₂)
inst_7 : hl₁.IsPreservedBy F
inst_8 : hl₂.IsPreservedBy F
⊢ QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ) ↔ IsIso (F.map ψl.φH)

Tactic:
(ψl.map F).quasiIso_iff

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff, CategoryTheory.ShortComplex.LeftHomologyMapData.map
-- 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₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
ψr : RightHomologyMapData φ hr₁ hr₂
inst_5 : HasHomology (Functor.obj F.mapShortComplex S₁)
inst_6 : HasHomology (Functor.obj F.mapShortComplex S₂)
inst_7 : hr₁.IsPreservedBy F
inst_8 : hr₂.IsPreservedBy F
⊢ QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ) ↔ IsIso (F.map ψr.φH)

Tactic:
(ψr.map F).quasiIso_iff

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.map, 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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : QuasiIso φ
have :
  ∀ (γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData),
    QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ)
⊢ QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ)

Tactic:
have γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData := 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
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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : QuasiIso φ
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
rw : QuasiIso φ
⊢ IsIso γ.φH

Tactic:
rw [← γ.quasiIso_iff]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : QuasiIso φ
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
⊢ QuasiIso φ

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
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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : QuasiIso φ
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
⊢ 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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : QuasiIso φ
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
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, LeftHomologyMapData.map_φH]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.map_φH, CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff, CategoryTheory.ShortComplex.LeftHomologyMapData.map
-- 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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : QuasiIso φ
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : F.ReflectsIsomorphisms
have :
  ∀ (γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData),
    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 γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData := 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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : F.ReflectsIsomorphisms
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
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, LeftHomologyMapData.map_φH]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.map_φH, CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff, CategoryTheory.ShortComplex.LeftHomologyMapData.map
-- 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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : F.ReflectsIsomorphisms
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : F.ReflectsIsomorphisms
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : F.ReflectsIsomorphisms
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : F.ReflectsIsomorphisms
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
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
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 φ
have :
  ∀ (γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData),
    QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ)
⊢ QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ)

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
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
rw : QuasiIso φ
⊢ IsIso γ.φH

Tactic:
rw [← γ.quasiIso_iff]

Premises used: 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
⊢ QuasiIso φ

Tactic:
infer_instance