awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.QuasiIso
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
⊢ 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:
exact ShortComplex.quasiIso_map_iff_of_preservesLeftHomology F
    ((shortComplexFunctor C₁ c i).map φ)

Premises used: HomologicalComplex.shortComplexFunctor, CategoryTheory.Functor.map, CategoryTheory.ShortComplex.quasiIso_map_iff_of_preservesLeftHomology
-- Module: Mathlib.Algebra.Homology.QuasiIso
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
inst_6 : ∀ (i : ι), K.HasHomology i
inst_7 : ∀ (i : ι), L.HasHomology i
inst_8 : ∀ (i : ι), HasHomology (Functor.obj (F.mapHomologicalComplex c) K) i
inst_9 : ∀ (i : ι), HasHomology (Functor.obj (F.mapHomologicalComplex c) L) i
inst_10 : F.ReflectsIsomorphisms
⊢ QuasiIso (K := Functor.obj (F.mapHomologicalComplex c) K) (CategoryTheory.Functor.map (F.mapHomologicalComplex c) φ) ↔
    QuasiIso φ

Tactic:
simp only [quasiIso_iff, quasiIsoAt_map_iff_of_preservesHomology φ F]

Premises used: quasiIso_iff, HomologicalComplex.quasiIsoAt_map_iff_of_preservesHomology
-- Module: Mathlib.Algebra.Homology.QuasiIso
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
inst_2 : CategoryWithHomology.{v, u} C
f : K ⟶ L
⊢ quasiIso C c f ↔ QuasiIso f

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 : HomologicalComplex.{v, u, u_1} C c
⊢ QuasiIso (𝟙 x)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 x

Tactic:
rw [mem_quasiIso_iff] at hf hg ⊢

Premises used: HomologicalComplex.mem_quasiIso_iff
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 x_1

Tactic:
rw [mem_quasiIso_iff] at hf hg ⊢

Premises used: HomologicalComplex.mem_quasiIso_iff
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 x
hg : QuasiIso x_1
⊢ QuasiIso (x ≫ x_1)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 g

Tactic:
rw [mem_quasiIso_iff] at hg hfg ⊢

Premises used: HomologicalComplex.mem_quasiIso_iff
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 (f ≫ g)

Tactic:
rw [mem_quasiIso_iff] at hg hfg ⊢

Premises used: HomologicalComplex.mem_quasiIso_iff
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 g
hfg : QuasiIso (f ≫ g)
rwa rwa₁ rwa₂ rwa₃ : QuasiIso (f ≫ g)
⊢ QuasiIso f

Tactic:
rwa [← quasiIso_iff_comp_right f g]

Premises used: quasiIso_iff_comp_right
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 f

Tactic:
rw [mem_quasiIso_iff] at hf hfg ⊢

Premises used: HomologicalComplex.mem_quasiIso_iff
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 (f ≫ g)

Tactic:
rw [mem_quasiIso_iff] at hf hfg ⊢

Premises used: HomologicalComplex.mem_quasiIso_iff
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 f
hfg : QuasiIso (f ≫ g)
rwa rwa₁ rwa₂ rwa₃ : QuasiIso (f ≫ g)
⊢ QuasiIso g

Tactic:
rwa [← quasiIso_iff_comp_left f g]

Premises used: quasiIso_iff_comp_left
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 g

Tactic:
rw [mem_quasiIso_iff] at hg ⊢

Premises used: HomologicalComplex.mem_quasiIso_iff
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 g
⊢ QuasiIso f

Tactic:
quasiIso_of_retractArrow h

Premises used: quasiIso_of_retractArrow
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 g
⊢ QuasiIso f

Tactic:
exact quasiIso_of_retractArrow h

Premises used: quasiIso_of_retractArrow
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 x_1 : HomologicalComplex.{v, u, u_1} C c
x_2 : x ⟶ x_1
h : IsIso x_2
⊢ QuasiIso x_2

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.QuasiIso
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 :
  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))
⊢ QuasiIsoAt e.hom n

Tactic:
rw [quasiIsoAt_iff, ShortComplex.quasiIso_iff]

Premises used: CategoryTheory.ShortComplex.quasiIso_iff, quasiIsoAt_iff
-- Module: Mathlib.Algebra.Homology.QuasiIso
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
⊢ 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:
(e.toHomologyIso n).isIso_hom

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.Iso.isIso_hom, CategoryTheory.ShortComplex.homologyMap', HomotopyEquiv.toHomologyIso, HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.QuasiIso
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
⊢ 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:
exact (e.toHomologyIso n).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, HomotopyEquiv.toHomologyIso
-- Module: Mathlib.Algebra.Homology.QuasiIso
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)
rw₁ rw₂ 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))
⊢ QuasiIsoAt e.hom n

Tactic:
classical
  rw [quasiIsoAt_iff, ShortComplex.quasiIso_iff]
  exact (e.toHomologyIso n).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, HomotopyEquiv.toHomologyIso, CategoryTheory.ShortComplex.quasiIso_iff, quasiIsoAt_iff
-- Module: Mathlib.Algebra.Homology.QuasiIso
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.inv n

Tactic:
e.symm.quasiIsoAt_hom n

Premises used: HomotopyEquiv.symm, HomotopyEquiv.quasiIsoAt_hom
-- Module: Mathlib.Algebra.Homology.QuasiIso
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
inst_2 : ∀ (n : ι), K.HasHomology n
inst_3 : ∀ (n : ι), L.HasHomology n
⊢ QuasiIso e.hom

Tactic:
⟨fun _ => inferInstance⟩

Premises used: inferInstance, QuasiIso.mk
-- Module: Mathlib.Algebra.Homology.QuasiIso
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
inst_2 : ∀ (n : ι), K.HasHomology n
inst_3 : ∀ (n : ι), L.HasHomology n
⊢ QuasiIso e.inv

Tactic:
⟨fun _ => inferInstance⟩

Premises used: inferInstance, QuasiIso.mk
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
c : ComplexShape ι
inst_2 : CategoryWithHomology.{v, u} C
K L : HomologicalComplex.{v, u, u_1} C c
e : HomotopyEquiv K L
⊢ QuasiIso e.hom

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
x : (↑S.X₁ : Type u)
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))
⊢ 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))

Tactic:
rw [← ConcreteCategory.comp_apply, S.zero]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.ShortComplex.zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
x : (↑S.X₁ : Type u)
⊢ 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:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
⊢ ∀ (a b : (↑S.X₁ : Type u)),
    (fun (x : (↑S.X₁ : Type u)) ↦
          (Subtype.mk (p := fun (x : (↑S.X₂ : Type u)) ↦ x ∈ (AddCommGrpCat.Hom.hom S.g).ker)
              ((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)
              ⋯ :
            ↥(AddCommGrpCat.Hom.hom S.g).ker))
        (a + b) =
      HAdd.hAdd (α := ↥(AddCommGrpCat.Hom.hom S.g).ker)
        ((fun (x : (↑S.X₁ : Type u)) ↦
            (Subtype.mk (p := fun (x : (↑S.X₂ : Type u)) ↦ x ∈ (AddCommGrpCat.Hom.hom S.g).ker)
                ((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)
                ⋯ :
              ↥(AddCommGrpCat.Hom.hom S.g).ker))
          a)
        ((fun (x : (↑S.X₁ : Type u)) ↦
            (Subtype.mk (p := fun (x : (↑S.X₂ : Type u)) ↦ x ∈ (AddCommGrpCat.Hom.hom S.g).ker)
                ((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)
                ⋯ :
              ↥(AddCommGrpCat.Hom.hom S.g).ker))
          b)

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
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))
⊢ AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom S.g).ker.subtype ≫ S.g = 0

Tactic:
ext ⟨_, hx⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
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:
hx

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
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:
exact hx
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
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 ⋯) ≫
                AddCommGrpCat.ofHom (QuotientAddGroup.mk' S.abToCycles.range)) :
            (a : (↑(Limits.KernelFork.ofι S.f ⋯).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 ⋯).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))
⊢ 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

Tactic:
ext (x : S.X₁)

Premises used: CategoryTheory.ShortComplex.X₁
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
x : (↑S.X₁ : Type u)
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 ⋯)) :
              (↑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)
⊢ 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))

Tactic:
rw [QuotientAddGroup.eq_zero_iff, AddMonoidHom.mem_range]

Premises used: QuotientAddGroup.eq_zero_iff, AddMonoidHom.mem_range
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
x : (↑S.X₁ : Type u)
⊢ ∃ (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 ⋯)) :
              (↑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:
apply exists_apply_eq_apply

Premises used: exists_apply_eq_apply
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
⊢ S.abLeftHomologyData.f' = AddCommGrpCat.ofHom S.abToCycles

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.abToCycles, CategoryTheory.ShortComplex.LeftHomologyData.f', CategoryTheory.ShortComplex.LeftHomologyData.liftK, AddMonoidHom.codRestrict, AddMonoidHom.mk', rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
x : ↥(AddCommGrpCat.Hom.hom S.g).ker
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))
⊢ (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))

Tactic:
rw [← ConcreteCategory.comp_apply, S.abLeftHomologyData.cyclesIso_inv_comp_iCycles]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.ShortComplex.abLeftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
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) 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:
rfl