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
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S₁.HasHomology
inst_6 : S₂.HasHomology
inst_7 : HasHomology (S₁.map F)
inst_8 : HasHomology (S₂.map F)
inst_9 : F.PreservesRightHomologyOf S₁
inst_10 : F.PreservesRightHomologyOf S₂
rw :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F))
      (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso' F))))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F))
      (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso' F))
        (homologyMap (Functor.map F.mapShortComplex φ))))
rw₁ :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := homology (S₂.map F)) (homologyMap (Functor.map F.mapShortComplex φ))
        (CategoryStruct.comp (Y := F.obj S₂.homology) (Iso.hom (S₂.mapHomologyIso' F))
          (Iso.inv (S₂.mapHomologyIso' F))) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F))
        (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso' F))
          (homologyMap (Functor.map F.mapShortComplex φ))) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
⊢ Eq (α := F.obj S₁.homology ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso' F)))
    (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso' F))
      (homologyMap (Functor.map F.mapShortComplex φ)))
have rw₂ : Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
  (homologyMap (Functor.map F.mapShortComplex φ) ≫ 𝟙 (homology (S₂.map F)) : homology (S₁.map F) ⟶ homology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F))
      (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso' F))
        (homologyMap (Functor.map F.mapShortComplex φ))) :
    homology (S₁.map F) ⟶ homology (S₂.map F))
Tactic: rw [← cancel_epi (S₁.mapHomologyIso' F).hom, ← mapHomologyIso'_hom_naturality_assoc,
    Iso.hom_inv_id, comp_id, Iso.hom_inv_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
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S₁.HasHomology
inst_6 : S₂.HasHomology
inst_7 : HasHomology (S₁.map F)
inst_8 : HasHomology (S₂.map F)
inst_9 : F.PreservesRightHomologyOf S₁
inst_10 : F.PreservesRightHomologyOf S₂
rw :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F))
      (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso' F))))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F))
      (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso' F))
        (homologyMap (Functor.map F.mapShortComplex φ))))
rw₁ :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := homology (S₂.map F)) (homologyMap (Functor.map F.mapShortComplex φ))
        (CategoryStruct.comp (Y := F.obj S₂.homology) (Iso.hom (S₂.mapHomologyIso' F))
          (Iso.inv (S₂.mapHomologyIso' F))) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F))
        (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso' F))
          (homologyMap (Functor.map F.mapShortComplex φ))) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
rw₂ :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (homologyMap (Functor.map F.mapShortComplex φ) ≫ 𝟙 (homology (S₂.map F)) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F))
        (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso' F))
          (homologyMap (Functor.map F.mapShortComplex φ))) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
⊢ Eq (α := F.obj S₁.homology ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso' F)))
    (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso' F))
      (homologyMap (Functor.map F.mapShortComplex φ)))
have rw₃ : Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
  (homologyMap (Functor.map F.mapShortComplex φ) : homology (S₁.map F) ⟶ homology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F))
      (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso' F))
        (homologyMap (Functor.map F.mapShortComplex φ))) :
    homology (S₁.map F) ⟶ homology (S₂.map F))
Tactic: rw [← cancel_epi (S₁.mapHomologyIso' F).hom, ← mapHomologyIso'_hom_naturality_assoc,
    Iso.hom_inv_id, comp_id, Iso.hom_inv_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
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
⊢ Eq (α := homology (S.map F) ≅ F.obj S.homology) (S.mapHomologyIso' F) (S.mapHomologyIso F)
have w : Eq (α := homology (S.map F) ⟶ F.obj S.homology) (Iso.hom (S.mapHomologyIso' F)) (Iso.hom (S.mapHomologyIso F))
Tactic: ext
-- 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
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
⊢ Eq (α := homology (S.map F) ⟶ F.obj S.homology) (Iso.hom (S.mapHomologyIso' F)) (Iso.hom (S.mapHomologyIso F))
have w : Eq (α := homology (S.map F) ⟶ F.obj S.homology)
  (Iso.hom
    (Iso.trans (Y := RightHomologyData.H (S := S.map F) (S.homologyData.right.map F))
      (RightHomologyData.homologyIso (S.homologyData.right.map F))
      (F.mapIso (Iso.symm S.homologyData.right.homologyIso))))
  (Iso.hom
    (Iso.trans (Y := LeftHomologyData.H (S := S.map F) (S.homologyData.left.map F))
      (LeftHomologyData.homologyIso (S.homologyData.left.map F)) (F.mapIso (Iso.symm S.homologyData.left.homologyIso))))
Tactic: rw [S.homologyData.left.mapHomologyIso_eq F, S.homologyData.right.mapHomologyIso'_eq F]
-- 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
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
⊢ 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))
have 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))
Tactic: have γ : HomologyMapData (𝟙 (S.map F)) (map S F).homologyData (S.homologyData.map F) := default
-- 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
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 (α := 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))
have eq : γ.left.φH ≫ Iso.hom (HomologyData.iso (S.homologyData.map F)) =
  Iso.hom (HomologyData.iso (homologyData (S.map F))) ≫ γ.right.φH
Tactic: have eq := γ.comm
-- 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
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 (α := 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))
have eq₁ : 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
Cleared hypotheses: eq
-- 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
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 φ
⊢ QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ)
have have : ∀ (γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData),
  QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ)
Tactic: have γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData := default
-- 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
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 (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ)
have this : IsIso γ.φH
Tactic: have : IsIso γ.φH := by
    rw [← γ.quasiIso_iff]
    infer_instance
-- 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
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
⊢ QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ)
have rw : IsIso (F.map γ.φH)
Tactic: rw [(γ.map F).quasiIso_iff, LeftHomologyMapData.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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : F.ReflectsIsomorphisms
⊢ QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ) ↔ QuasiIso φ
have have : ∀ (γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData),
  QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ) ↔ QuasiIso φ
Tactic: have γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData := default
-- 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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : F.ReflectsIsomorphisms
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
⊢ 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, LeftHomologyMapData.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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : F.ReflectsIsomorphisms
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
⊢ 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.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
inst_11 : F.ReflectsIsomorphisms
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
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
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 φ
⊢ QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ)
have have : ∀ (γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData),
  QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ)
Tactic: have γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData := default
-- 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
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 (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ)
have this : IsIso γ.φH
Tactic: have : IsIso γ.φH := by
    rw [← γ.quasiIso_iff]
    infer_instance
-- 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
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
⊢ QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ)
have rw : IsIso (F.map γ.φH)
Tactic: rw [(γ.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
⊢ QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ) ↔ QuasiIso φ
have have : ∀ (γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData),
  QuasiIso (S₁ := Functor.obj F.mapShortComplex S₁) (Functor.map F.mapShortComplex φ) ↔ QuasiIso φ
Tactic: have γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData := default