awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hL : L.ExactAt i
⊢ QuasiIsoAt f i ↔ K.ExactAt i
have simp : ∀ (hL : IsZero.{v, u} (L.sc i).homology),
  IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) ↔
    IsZero.{v, u} (K.sc i).homology
Tactic: simp only [quasiIsoAt_iff, ShortComplex.quasiIso_iff, exactAt_iff,
    ShortComplex.exact_iff_isZero_homology] at hL ⊢
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hL : IsZero.{v, u} (L.sc i).homology
⊢ IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) ↔
    IsZero.{v, u} (K.sc i).homology
have mp : IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
    (Functor.obj (shortComplexFunctor C c i) L).homology)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) →
  IsZero.{v, u} (K.sc i).homology
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hL : IsZero.{v, u} (L.sc i).homology
mp :
  IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) →
    IsZero.{v, u} (K.sc i).homology
⊢ IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) ↔
    IsZero.{v, u} (K.sc i).homology
have mpr : IsZero.{v, u} (K.sc i).homology →
  IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
    (Functor.obj (shortComplexFunctor C c i) L).homology)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M K' L' : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ : QuasiIsoAt φ i
hφ' : QuasiIsoAt φ' i
⊢ QuasiIsoAt (φ ≫ φ') i
have rw : ∀
  (hφ :
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
  (hφ' :
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) L)
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ')),
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ ≫ φ'))
Tactic: rw [quasiIsoAt_iff] at hφ hφ' ⊢
Cleared hypotheses: hφ, hφ'
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M K' L' : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ)
hφ' :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) L)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ')
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ ≫ φ'))
have rw : ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
  (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ ≫ CategoryTheory.Functor.map (shortComplexFunctor C c i) φ')
Tactic: rw [Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ : QuasiIsoAt φ i
hφφ' : QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt φ' i
have rw : ∀ (hφ : IsIso (X := K.homology i) (Y := L.homology i) (homologyMap φ i))
  (hφφ' : IsIso (X := K.homology i) (Y := M.homology i) (homologyMap (φ ≫ φ') i)),
  IsIso (X := L.homology i) (Y := M.homology i) (homologyMap φ' i)
Tactic: rw [quasiIsoAt_iff_isIso_homologyMap] at hφ hφφ' ⊢
Cleared hypotheses: hφ, hφφ'
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (hypothesis)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ : IsIso (X := K.homology i) (Y := L.homology i) (homologyMap φ i)
hφφ' : IsIso (X := K.homology i) (Y := M.homology i) (homologyMap (φ ≫ φ') i)
⊢ IsIso (X := L.homology i) (Y := M.homology i) (homologyMap φ' i)
have hφφ'₁ : IsIso (X := K.homology i) (Y := M.homology i)
  (CategoryStruct.comp (Y := L.homology i) (homologyMap φ i) (homologyMap φ' i))
Tactic: rw [homologyMap_comp] at hφφ'
Cleared hypotheses: hφφ'
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ : QuasiIsoAt φ i
⊢ QuasiIsoAt (φ ≫ φ') i ↔ QuasiIsoAt φ' i
have mp : QuasiIsoAt (φ ≫ φ') i → QuasiIsoAt φ' i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ : QuasiIsoAt φ i
mp : QuasiIsoAt (φ ≫ φ') i → QuasiIsoAt φ' i
⊢ QuasiIsoAt (φ ≫ φ') i ↔ QuasiIsoAt φ' i
have mpr : QuasiIsoAt φ' i → QuasiIsoAt (φ ≫ φ') i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ' : QuasiIsoAt φ' i
hφφ' : QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt φ i
have rw : ∀ (hφ' : IsIso (X := L.homology i) (Y := M.homology i) (homologyMap φ' i))
  (hφφ' : IsIso (X := K.homology i) (Y := M.homology i) (homologyMap (φ ≫ φ') i)),
  IsIso (X := K.homology i) (Y := L.homology i) (homologyMap φ i)
Tactic: rw [quasiIsoAt_iff_isIso_homologyMap] at hφ' hφφ' ⊢
Cleared hypotheses: hφ', hφφ'
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (hypothesis)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ' : IsIso (X := L.homology i) (Y := M.homology i) (homologyMap φ' i)
hφφ' : IsIso (X := K.homology i) (Y := M.homology i) (homologyMap (φ ≫ φ') i)
⊢ IsIso (X := K.homology i) (Y := L.homology i) (homologyMap φ i)
have hφφ'₁ : IsIso (X := K.homology i) (Y := M.homology i)
  (CategoryStruct.comp (Y := L.homology i) (homologyMap φ i) (homologyMap φ' i))
Tactic: rw [homologyMap_comp] at hφφ'
Cleared hypotheses: hφφ'
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ' : QuasiIsoAt φ' i
⊢ QuasiIsoAt (φ ≫ φ') i ↔ QuasiIsoAt φ i
have mp : QuasiIsoAt (φ ≫ φ') i → QuasiIsoAt φ i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ' : QuasiIsoAt φ' i
mp : QuasiIsoAt (φ ≫ φ') i → QuasiIsoAt φ i
⊢ QuasiIsoAt (φ ≫ φ') i ↔ QuasiIsoAt φ i
have mpr : QuasiIsoAt φ i → QuasiIsoAt (φ ≫ φ') i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K_1 L_1 M K' L' : HomologicalComplex.{v, u, u_1} C c
C₁ : Type u_2
C₂ : Type u_3
inst_2 : Category.{v_1, u_2} C₁
inst_3 : Category.{v_2, u_3} C₂
inst_4 : Preadditive.{v_1, u_2} C₁
inst_5 : Preadditive.{v_2, u_3} C₂
K L : HomologicalComplex.{v_1, u_2, u_1} C₁ c
φ : K ⟶ L
F : CategoryTheory.Functor.{v_1, v_2, u_2, u_3} C₁ C₂
inst_6 : F.Additive
inst_7 : F.PreservesHomology
i : ι
inst_8 : K.HasHomology i
inst_9 : L.HasHomology i
inst_10 : HasHomology (Functor.obj (F.mapHomologicalComplex c) K) i
inst_11 : HasHomology (Functor.obj (F.mapHomologicalComplex c) L) i
hφ : QuasiIsoAt φ i
⊢ QuasiIsoAt (K := Functor.obj (F.mapHomologicalComplex c) K) (CategoryTheory.Functor.map (F.mapHomologicalComplex c) φ)
    i
have rw : ∀
  (hφ :
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C₁ c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C₁ c i) φ)),
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C₂ c i) (Functor.obj (F.mapHomologicalComplex c) K))
    (CategoryTheory.Functor.map (shortComplexFunctor C₂ c i) (CategoryTheory.Functor.map (F.mapHomologicalComplex c) φ))
Tactic: rw [quasiIsoAt_iff] at hφ ⊢
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
c : ComplexShape ι
C₁ : Type u_2
C₂ : Type u_3
inst : Category.{v_1, u_2} C₁
inst_1 : Category.{v_2, u_3} C₂
inst_2 : Preadditive.{v_1, u_2} C₁
inst_3 : Preadditive.{v_2, u_3} C₂
K L : HomologicalComplex.{v_1, u_2, u_1} C₁ c
φ : K ⟶ L
F : CategoryTheory.Functor.{v_1, v_2, u_2, u_3} C₁ C₂
inst_4 : F.Additive
inst_5 : F.PreservesHomology
i : ι
inst_6 : K.HasHomology i
inst_7 : L.HasHomology i
inst_8 : HasHomology (Functor.obj (F.mapHomologicalComplex c) K) i
inst_9 : HasHomology (Functor.obj (F.mapHomologicalComplex c) L) i
inst_10 : F.ReflectsIsomorphisms
⊢ QuasiIsoAt (K := Functor.obj (F.mapHomologicalComplex c) K) (CategoryTheory.Functor.map (F.mapHomologicalComplex c) φ)
      i ↔
    QuasiIsoAt φ i
have simp : ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C₂ c i) (Functor.obj (F.mapHomologicalComplex c) K))
    (CategoryTheory.Functor.map (shortComplexFunctor C₂ c i)
      (CategoryTheory.Functor.map (F.mapHomologicalComplex c) φ)) ↔
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C₁ c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C₁ c i) φ)
Tactic: simp only [quasiIsoAt_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (hypothesis)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M K' L' : HomologicalComplex.{v, u, u_1} C c
inst_2 : CategoryWithHomology.{v, u} C
X Y Z : HomologicalComplex.{v, u, u_1} C c
x : X ⟶ Y
x_1 : Y ⟶ Z
hf : quasiIso C c x
hg : quasiIso C c x_1
⊢ quasiIso C c (x ≫ x_1)
have hf₁ : QuasiIso x
Tactic: rw [mem_quasiIso_iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (hypothesis)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M K' L' : HomologicalComplex.{v, u, u_1} C c
inst_2 : CategoryWithHomology.{v, u} C
X Y Z : HomologicalComplex.{v, u, u_1} C c
x : X ⟶ Y
x_1 : Y ⟶ Z
hf : quasiIso C c x
hg : quasiIso C c x_1
hf₁ : QuasiIso x
⊢ quasiIso C c (x ≫ x_1)
have hg₁ : QuasiIso x_1
Tactic: rw [mem_quasiIso_iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (hypothesis)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M K' L' : HomologicalComplex.{v, u, u_1} C c
inst_2 : CategoryWithHomology.{v, u} C
X Y Z : HomologicalComplex.{v, u, u_1} C c
f : X ⟶ Y
g : Y ⟶ Z
hg : quasiIso C c g
hfg : quasiIso C c (f ≫ g)
⊢ quasiIso C c f
have hg₁ : QuasiIso g
Tactic: rw [mem_quasiIso_iff] at hg hfg ⊢
Cleared hypotheses: hg, hfg
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (hypothesis)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M K' L' : HomologicalComplex.{v, u, u_1} C c
inst_2 : CategoryWithHomology.{v, u} C
X Y Z : HomologicalComplex.{v, u, u_1} C c
f : X ⟶ Y
g : Y ⟶ Z
hg : quasiIso C c g
hfg : quasiIso C c (f ≫ g)
hg₁ : QuasiIso g
⊢ quasiIso C c f
have hfg₁ : QuasiIso (f ≫ g)
Tactic: rw [mem_quasiIso_iff] at hg hfg ⊢
Cleared hypotheses: hg, hfg
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (hypothesis)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M K' L' : HomologicalComplex.{v, u, u_1} C c
inst_2 : CategoryWithHomology.{v, u} C
X Y Z : HomologicalComplex.{v, u, u_1} C c
f : X ⟶ Y
g : Y ⟶ Z
hf : quasiIso C c f
hfg : quasiIso C c (f ≫ g)
⊢ quasiIso C c g
have hf₁ : QuasiIso f
Tactic: rw [mem_quasiIso_iff] at hf hfg ⊢
Cleared hypotheses: hf, hfg
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (hypothesis)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M K' L' : HomologicalComplex.{v, u, u_1} C c
inst_2 : CategoryWithHomology.{v, u} C
X Y Z : HomologicalComplex.{v, u, u_1} C c
f : X ⟶ Y
g : Y ⟶ Z
hf : quasiIso C c f
hfg : quasiIso C c (f ≫ g)
hf₁ : QuasiIso f
⊢ quasiIso C c g
have hfg₁ : QuasiIso (f ≫ g)
Tactic: rw [mem_quasiIso_iff] at hf hfg ⊢
Cleared hypotheses: hf, hfg
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (hypothesis)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M K' L' : HomologicalComplex.{v, u, u_1} C c
inst_2 : CategoryWithHomology.{v, u} C
X Y Z W : HomologicalComplex.{v, u, u_1} C c
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
hg : quasiIso C c g
⊢ quasiIso C c f
have hg₁ : QuasiIso g
Tactic: rw [mem_quasiIso_iff] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} C c
e : HomotopyEquiv K L
n : ι
inst_2 : K.HasHomology n
inst_3 : L.HasHomology n
⊢ QuasiIsoAt e.hom n
have rw : IsIso (X := (Functor.obj (shortComplexFunctor C c n) K).homology) (Y :=
  (Functor.obj (shortComplexFunctor C c n) L).homology)
  (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c n) e.hom))
Tactic: rw [quasiIsoAt_iff, ShortComplex.quasiIso_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} C c
e : HomotopyEquiv K L
n : ι
inst_2 : K.HasHomology n
inst_3 : L.HasHomology n
⊢ QuasiIsoAt e.hom n
have rw : ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c n) K)
  (CategoryTheory.Functor.map (shortComplexFunctor C c n) e.hom)
Tactic: classical
  rw [quasiIsoAt_iff, ShortComplex.quasiIso_iff]
  exact (e.toHomologyIso n).isIso_hom
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} C c
e : HomotopyEquiv K L
n : ι
inst_2 : K.HasHomology n
inst_3 : L.HasHomology n
rw :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c n) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c n) e.hom)
⊢ QuasiIsoAt e.hom n
have rw₁ : IsIso (X := (Functor.obj (shortComplexFunctor C c n) K).homology) (Y :=
  (Functor.obj (shortComplexFunctor C c n) L).homology)
  (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c n) e.hom))
Tactic: classical
  rw [quasiIsoAt_iff, ShortComplex.quasiIso_iff]
  exact (e.toHomologyIso n).isIso_hom
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
x : (↑S.X₁ : Type u)
⊢ Eq (α := (↑S.X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) S.g :
          (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x :
          (↑S.X₂ : Type u)) :
      (↑S.X₃ : Type u))
    (0 : (↑S.X₃ : Type u))
have rw : Eq (α := (↑S.X₃ : Type u))
  ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
          (fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) AddCommGrpCat.carrier _ _ S.X₁ S.X₃ 0 :
        (a : (↑S.X₁ : Type u)) → (↑S.X₃ : Type u))
      x :
    (↑S.X₃ : Type u))
  (0 : (↑S.X₃ : Type u))
Tactic: rw [← ConcreteCategory.comp_apply, S.zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
⊢ AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom S.g).ker.subtype ≫ S.g = 0
have hf : ∀ (val : (↑S.X₂ : Type u)) (hx : val ∈ (AddCommGrpCat.Hom.hom S.g).ker),
  Eq (α := (↑S.X₃ : Type u))
    ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom S.g).ker.subtype ≫ S.g) :
          (a : (↑(AddCommGrpCat.of ↥(AddCommGrpCat.Hom.hom S.g).ker) : Type u)) → (↑S.X₃ : Type u))
        (Subtype.mk (p := fun (x : (↑S.X₂ : Type u)) ↦ x ∈ (AddCommGrpCat.Hom.hom S.g).ker) val hx) :
      (↑S.X₃ : Type u))
    ((AddCommGrpCat.Hom.hom 0 :
          (a : (↑(AddCommGrpCat.of ↥(AddCommGrpCat.Hom.hom S.g).ker) : Type u)) → (↑S.X₃ : Type u))
        (Subtype.mk (p := fun (x : (↑S.X₂ : Type u)) ↦ x ∈ (AddCommGrpCat.Hom.hom S.g).ker) val hx) :
      (↑S.X₃ : Type u))
Tactic: ext ⟨_, hx⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
⊢ Eq (α := (Limits.KernelFork.ofι S.f ⋯).pt ⟶ AddCommGrpCat.of (↥(AddCommGrpCat.Hom.hom S.g).ker ⧸ S.abToCycles.range))
    ((AddCommGrpCat.kernelIsLimit S.g).lift (Limits.KernelFork.ofι S.f ⋯) ≫
      AddCommGrpCat.ofHom (QuotientAddGroup.mk' S.abToCycles.range))
    0
have hf : ∀ (x : (↑S.X₁ : Type u)),
  Eq (α := (↑(AddCommGrpCat.of (↥(AddCommGrpCat.Hom.hom S.g).ker ⧸ S.abToCycles.range)) : Type u))
    ((AddCommGrpCat.Hom.hom
            ((AddCommGrpCat.kernelIsLimit S.g).lift (Limits.KernelFork.ofι S.f sorry) ≫
              AddCommGrpCat.ofHom (QuotientAddGroup.mk' S.abToCycles.range)) :
          (a : (↑(Limits.KernelFork.ofι S.f sorry).pt : Type u)) →
            (↑(AddCommGrpCat.of (↥(AddCommGrpCat.Hom.hom S.g).ker ⧸ S.abToCycles.range)) : Type u))
        x :
      (↑(AddCommGrpCat.of (↥(AddCommGrpCat.Hom.hom S.g).ker ⧸ S.abToCycles.range)) : Type u))
    ((AddCommGrpCat.Hom.hom 0 :
          (a : (↑(Limits.KernelFork.ofι S.f sorry).pt : Type u)) →
            (↑(AddCommGrpCat.of (↥(AddCommGrpCat.Hom.hom S.g).ker ⧸ S.abToCycles.range)) : Type u))
        x :
      (↑(AddCommGrpCat.of (↥(AddCommGrpCat.Hom.hom S.g).ker ⧸ S.abToCycles.range)) : Type u))
Tactic: ext (x : S.X₁)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
x : (↑S.X₁ : Type u)
⊢ Eq (α := ↥(AddCommGrpCat.Hom.hom S.g).ker ⧸ S.abToCycles.range)
    ((↑(((AddCommGrpCat.Hom.hom ((AddCommGrpCat.kernelIsLimit S.g).lift (Limits.KernelFork.ofι S.f ⋯)) :
                (↑S.X₁ : Type u) →+ (↑(AddCommGrpCat.of ↥(AddCommGrpCat.Hom.hom S.g).ker) : Type u)) :
              (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker)
            x) :
        ↥(AddCommGrpCat.Hom.hom S.g).ker ⧸ S.abToCycles.range) :
      ↥(AddCommGrpCat.Hom.hom S.g).ker ⧸ S.abToCycles.range)
    (0 : (↑(AddCommGrpCat.of (↥(AddCommGrpCat.Hom.hom S.g).ker ⧸ S.abToCycles.range)) : Type u))
have hf : ∃ (x_1 : (↑S.X₁ : Type u)),
  Eq (α := ↥(AddCommGrpCat.Hom.hom S.g).ker)
    ((S.abToCycles : (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker) x_1 : ↥(AddCommGrpCat.Hom.hom S.g).ker)
    (((AddCommGrpCat.Hom.hom ((AddCommGrpCat.kernelIsLimit S.g).lift (Limits.KernelFork.ofι S.f sorry)) :
            (↑S.X₁ : Type u) →+ (↑(AddCommGrpCat.of ↥(AddCommGrpCat.Hom.hom S.g).ker) : Type u)) :
          (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker)
        x :
      ↥(AddCommGrpCat.Hom.hom S.g).ker)
Tactic: rw [QuotientAddGroup.eq_zero_iff, AddMonoidHom.mem_range]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
x : ↥(AddCommGrpCat.Hom.hom S.g).ker
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (X := S.cycles) S.iCycles :
        (a : (↑S.cycles : Type u)) → (↑S.X₂ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) (Y := S.cycles) (Iso.inv S.abLeftHomologyData.cyclesIso) :
            (a : ↥(AddCommGrpCat.Hom.hom S.g).ker) → (↑S.cycles : Type u))
          x :
        (↑S.cycles : Type u)) =
    (↑x : (↑S.X₂ : Type u))
have rw : (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
        AddCommGrpCat.carrier) S.abLeftHomologyData.i :
      (a : (↑(AddCommGrpCat.of ↥(AddCommGrpCat.Hom.hom S.g).ker) : Type u)) → (↑S.X₂ : Type u))
    x =
  (↑x : (↑S.X₂ : Type u))
Tactic: rw [← ConcreteCategory.comp_apply, S.abLeftHomologyData.cyclesIso_inv_comp_iCycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
⊢ S.Exact ↔
    Function.Surjective (α := (↑S.X₁ : Type u)) (β := ↥(AddCommGrpCat.Hom.hom S.g).ker)
      (⇑S.abToCycles : (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker)
have rw : Function.Surjective (α := (↑S.X₁ : Type u)) (β := (↑S.abLeftHomologyData.K : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (AddCommGrpCat.ofHom S.abToCycles)) :
      (a : (↑S.X₁ : Type u)) → (↑S.abLeftHomologyData.K : Type u)) ↔
  Function.Surjective (α := (↑S.X₁ : Type u)) (β := ↥(AddCommGrpCat.Hom.hom S.g).ker)
    (⇑S.abToCycles : (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker)
Tactic: rw [S.abLeftHomologyData.exact_iff_epi_f', abLeftHomologyData_f',
    AddCommGrpCat.epi_iff_surjective]