awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst_3 : HasZeroObject.{v, u_1} C
e_a :
  (mappingCone.triangle g).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
        (mappingCone.inr f) =
    HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g) ≫
      (mappingCone.triangle (K := mappingCone f) (L := mappingCone (f ≫ g))
          (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g))).mor₃
⊢ Eq (α :=
    Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone g) ⟶
      Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone f)))
    (CategoryStruct.comp (Y :=
      Functor.obj (quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          (mappingCone f)))
      (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
        ((mappingCone.triangle g).mor₃ ≫
          CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
            (mappingCone.inr f)))
      (NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1)) (mappingCone f)))
    (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
        (HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g) ≫
          (mappingCone.triangle (K := mappingCone f) (L := mappingCone (f ≫ g))
              (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g))).mor₃) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1)) (mappingCone f))

Tactic:
congr 2
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst_3 : HasZeroObject.{v, u_1} C
⊢ (mappingCone.triangle g).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
        (mappingCone.inr f) =
    HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g) ≫
      (mappingCone.triangle (K := mappingCone f) (L := mappingCone (f ≫ g))
          (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g))).mor₃

Tactic:
(mappingConeCompHomotopyEquiv_comm₂ f g).symm

Premises used: CochainComplex.mappingCone, CochainComplex.mappingCone.map, CochainComplex.HomComplex.Cocycle.homOf, HomologicalComplex.homotopyCofiber, CochainComplex.mappingConeCompHomotopyEquiv_comm₂, CochainComplex.mappingCone.desc, Eq.symm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst_3 : HasZeroObject.{v, u_1} C
⊢ (mappingCone.triangle g).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
        (mappingCone.inr f) =
    HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g) ≫
      (mappingCone.triangle (K := mappingCone f) (L := mappingCone (f ≫ g))
          (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g))).mor₃

Tactic:
exact (mappingConeCompHomotopyEquiv_comm₂ f g).symm

Premises used: CochainComplex.mappingConeCompHomotopyEquiv_comm₂, Eq.symm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
X Y : HomologicalComplex.{v, u, u_2} V c
f₁ f₂ g₁ g₂ : X ⟶ Y
h : Homotopy f₁ f₂
h' : Homotopy g₁ g₂
⊢ homotopic V c (f₁ + g₁) (f₂ + g₂)

Tactic:
⟨Homotopy.add h h'⟩

Premises used: Nonempty.intro, homotopic, Homotopy.add
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
X Y : HomologicalComplex.{v, u, u_2} V c
f₁ f₂ g₁ g₂ : X ⟶ Y
h : Homotopy f₁ f₂
h' : Homotopy g₁ g₂
⊢ homotopic V c (f₁ + g₁) (f₂ + g₂)

Tactic:
exact ⟨Homotopy.add h h'⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
⊢ Functor.Full (C := HomologicalComplex.{v, u, u_2} V c) (quotient V c)

Tactic:
Quotient.full_functor _

Premises used: CategoryTheory.Quotient.full_functor, HomotopyCategory, HomotopyCategory.quotient
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
⊢ Functor.EssSurj (C := HomologicalComplex.{v, u, u_2} V c) (quotient V c)

Tactic:
Quotient.essSurj_functor _

Premises used: CategoryTheory.Quotient.essSurj_functor, HomotopyCategory, HomotopyCategory.quotient
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
inst_3 : Linear.{u_1, v, u} R V
⊢ Functor.Linear R (C := HomologicalComplex.{v, u, u_2} V c) (quotient V c)

Tactic:
Quotient.linear_functor _ (homotopic V c) _

Premises used: CategoryTheory.Quotient.linear_functor, homotopic, HomotopyCategory.instPreadditive._aux_1, HomotopyCategory, HomotopyCategory.quotient
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
inst_3 : HasZeroObject.{v, u} V
rw :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0) (Functor.obj (quotient V c) 0))
    (𝟙 (Functor.obj (quotient V c) 0)) 0
rw₁ :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0) (Functor.obj (quotient V c) 0))
    (CategoryTheory.Functor.map (quotient V c) (𝟙 0)) 0
rw₂ :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0) (Functor.obj (quotient V c) 0))
    (CategoryTheory.Functor.map (quotient V c) 0) 0
rw₃ rw₄ :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0) (Functor.obj (quotient V c) 0)) 0
    0
⊢ IsZero (C := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0)

Tactic:
rw [IsZero.iff_id_eq_zero, ← (quotient V c).map_id, id_zero, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.id_zero, CategoryTheory.Functor.map_id, HomotopyCategory.quotient, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
D : Type u_3
inst_3 : Category.{v_1, u_3} D
⊢ Functor.Full (C := HomotopyCategory.{v, u, u_2} V c ⥤ D)
    (Functor.obj (Functor.whiskeringLeft (HomologicalComplex.{v, u, u_2} V c) (HomotopyCategory.{v, u, u_2} V c) D)
      (quotient V c))

Tactic:
Quotient.full_whiskeringLeft_functor _ _

Premises used: CategoryTheory.Quotient.full_whiskeringLeft_functor, HomotopyCategory, HomotopyCategory.quotient
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
D : Type u_3
inst_3 : Category.{v_1, u_3} D
⊢ Functor.Faithful (C := HomotopyCategory.{v, u, u_2} V c ⥤ D)
    (Functor.obj (Functor.whiskeringLeft (HomologicalComplex.{v, u, u_2} V c) (HomotopyCategory.{v, u, u_2} V c) D)
      (quotient V c))

Tactic:
Quotient.faithful_whiskeringLeft_functor _ _

Premises used: CategoryTheory.Quotient.faithful_whiskeringLeft_functor, HomotopyCategory, HomotopyCategory.quotient
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
X : HomotopyCategory.{v, u, u_2} V c
⊢ ∃ (K : HomologicalComplex.{v, u, u_2} V c), Functor.obj (quotient V c) K = X

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_2} V c
⊢ (Functor.obj (quotient V c) C).as (r := homotopic V c) = C

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomotopyCategory.{v, u, u_2} V c
f : C ⟶ D
⊢ CategoryTheory.Functor.map (quotient V c) (Quot.out (r := HomRel.CompClosure (homotopic V c)) f) = f

Tactic:
Quot.out_eq _

Premises used: Quot.out_eq, CategoryTheory.Quotient.Hom
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f : C ⟶ D
⊢ Eq (α := Quot (α := C ⟶ D) (HomRel.CompClosure (homotopic V c))) (Quot.mk (HomRel.CompClosure (homotopic V c)) f)
    (CategoryTheory.Functor.map (quotient V c) f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f g : C ⟶ D
h : Homotopy f g
⊢ Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) D) (CategoryTheory.Functor.map (quotient V c) f)
    (CategoryTheory.Functor.map (quotient V c) g)

Tactic:
CategoryTheory.Quotient.sound _ ⟨h⟩

Premises used: Nonempty.intro, CategoryTheory.Quotient.sound
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f : C ⟶ D
h :
  Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) D) (CategoryTheory.Functor.map (quotient V c) f) 0
⊢ Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) D) (CategoryTheory.Functor.map (quotient V c) f)
    (CategoryTheory.Functor.map (quotient V c) 0)

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f : C ⟶ D
h_1 : Nonempty (Homotopy f 0)
h : Homotopy f 0
⊢ Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) D) (CategoryTheory.Functor.map (quotient V c) f) 0

Tactic:
simpa using eq_of_homotopy _ _ h

Premises used: HomotopyCategory.eq_of_homotopy
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f : C ⟶ D
w :
  Eq (α :=
    Functor.obj (quotient V c) ((Functor.obj (quotient V c) C).as (r := homotopic V c)) ⟶
      Functor.obj (quotient V c) ((Functor.obj (quotient V c) D).as (r := homotopic V c)))
    (CategoryTheory.Functor.map (quotient V c)
      (Quot.out (r := HomRel.CompClosure (homotopic V c)) (CategoryTheory.Functor.map (quotient V c) f)))
    (CategoryTheory.Functor.map (quotient V c) f)
⊢ Homotopy (Quot.out (r := HomRel.CompClosure (homotopic V c)) (CategoryTheory.Functor.map (quotient V c) f)) f

Tactic:
apply homotopyOfEq

Premises used: HomotopyCategory.homotopyOfEq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f : C ⟶ D
⊢ Eq (α :=
    Functor.obj (quotient V c) ((Functor.obj (quotient V c) C).as (r := homotopic V c)) ⟶
      Functor.obj (quotient V c) ((Functor.obj (quotient V c) D).as (r := homotopic V c)))
    (CategoryTheory.Functor.map (quotient V c)
      (Quot.out (r := HomRel.CompClosure (homotopic V c)) (CategoryTheory.Functor.map (quotient V c) f)))
    (CategoryTheory.Functor.map (quotient V c) f)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomotopyCategory.{v, u, u_2} V c
f : C ⟶ D
g : D ⟶ E
⊢ CategoryTheory.Functor.map (quotient V c)
      (Quot.out (r := HomRel.CompClosure (homotopic V c)) f ≫ Quot.out (r := HomRel.CompClosure (homotopic V c)) g) =
    f ≫ g

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f : HomotopyEquiv C D
rw :
  Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C)
    (CategoryTheory.Functor.map (quotient V c) (f.hom ≫ f.inv)) (CategoryTheory.Functor.map (quotient V c) (𝟙 C))
⊢ CategoryTheory.Functor.map (quotient V c) f.hom ≫ CategoryTheory.Functor.map (quotient V c) f.inv =
    𝟙 (Functor.obj (quotient V c) C)

Tactic:
rw [← (quotient V c).map_comp, ← (quotient V c).map_id]

Premises used: CategoryTheory.Functor.map_id, HomotopyCategory.quotient, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f : HomotopyEquiv C D
⊢ Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C)
    (CategoryTheory.Functor.map (quotient V c) (f.hom ≫ f.inv)) (CategoryTheory.Functor.map (quotient V c) (𝟙 C))

Tactic:
eq_of_homotopy _ _ f.homotopyHomInvId

Premises used: HomotopyCategory.eq_of_homotopy, HomotopyEquiv.homotopyHomInvId
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f : HomotopyEquiv C D
⊢ Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C)
    (CategoryTheory.Functor.map (quotient V c) (f.hom ≫ f.inv)) (CategoryTheory.Functor.map (quotient V c) (𝟙 C))

Tactic:
exact eq_of_homotopy _ _ f.homotopyHomInvId

Premises used: HomotopyCategory.eq_of_homotopy, HomotopyEquiv.homotopyHomInvId
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f : HomotopyEquiv C D
rw :
  Eq (α := Functor.obj (quotient V c) D ⟶ Functor.obj (quotient V c) D)
    (CategoryTheory.Functor.map (quotient V c) (f.inv ≫ f.hom)) (CategoryTheory.Functor.map (quotient V c) (𝟙 D))
⊢ CategoryTheory.Functor.map (quotient V c) f.inv ≫ CategoryTheory.Functor.map (quotient V c) f.hom =
    𝟙 (Functor.obj (quotient V c) D)

Tactic:
rw [← (quotient V c).map_comp, ← (quotient V c).map_id]

Premises used: CategoryTheory.Functor.map_id, HomotopyCategory.quotient, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f : HomotopyEquiv C D
⊢ Eq (α := Functor.obj (quotient V c) D ⟶ Functor.obj (quotient V c) D)
    (CategoryTheory.Functor.map (quotient V c) (f.inv ≫ f.hom)) (CategoryTheory.Functor.map (quotient V c) (𝟙 D))

Tactic:
eq_of_homotopy _ _ f.homotopyInvHomId

Premises used: HomotopyCategory.eq_of_homotopy, HomotopyEquiv.homotopyInvHomId
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f : HomotopyEquiv C D
⊢ Eq (α := Functor.obj (quotient V c) D ⟶ Functor.obj (quotient V c) D)
    (CategoryTheory.Functor.map (quotient V c) (f.inv ≫ f.hom)) (CategoryTheory.Functor.map (quotient V c) (𝟙 D))

Tactic:
exact eq_of_homotopy _ _ f.homotopyInvHomId

Premises used: HomotopyCategory.eq_of_homotopy, HomotopyEquiv.homotopyInvHomId
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
i : Functor.obj (quotient V c) C ≅ Functor.obj (quotient V c) D
rw : i.hom ≫ i.inv = CategoryTheory.Functor.map (quotient V c) (𝟙 C)
rw₁ : 𝟙 (Functor.obj (quotient V c) C) = CategoryTheory.Functor.map (quotient V c) (𝟙 C)
rw₂ rw₃ : 𝟙 (Functor.obj (quotient V c) C) = 𝟙 (Functor.obj (quotient V c) C)
⊢ Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C)
    (CategoryTheory.Functor.map (quotient V c)
      (Quot.out (r := HomRel.CompClosure (homotopic V c)) i.hom ≫
        Quot.out (r := HomRel.CompClosure (homotopic V c)) i.inv))
    (CategoryTheory.Functor.map (quotient V c) (𝟙 C))

Tactic:
rw [quotient_map_out_comp_out, i.hom_inv_id, (quotient V c).map_id]

Premises used: HomotopyCategory.quotient_map_out_comp_out, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Functor.map_id, HomotopyCategory.quotient
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
i : Functor.obj (quotient V c) C ≅ Functor.obj (quotient V c) D
rw : i.inv ≫ i.hom = CategoryTheory.Functor.map (quotient V c) (𝟙 D)
rw₁ : 𝟙 (Functor.obj (quotient V c) D) = CategoryTheory.Functor.map (quotient V c) (𝟙 D)
rw₂ rw₃ : 𝟙 (Functor.obj (quotient V c) D) = 𝟙 (Functor.obj (quotient V c) D)
⊢ Eq (α := Functor.obj (quotient V c) D ⟶ Functor.obj (quotient V c) D)
    (CategoryTheory.Functor.map (quotient V c)
      (Quot.out (r := HomRel.CompClosure (homotopic V c)) i.inv ≫
        Quot.out (r := HomRel.CompClosure (homotopic V c)) i.hom))
    (CategoryTheory.Functor.map (quotient V c) (𝟙 D))

Tactic:
rw [quotient_map_out_comp_out, i.inv_hom_id, (quotient V c).map_id]

Premises used: HomotopyCategory.quotient_map_out_comp_out, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.map_id, HomotopyCategory.quotient
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_2} V c
e : HomotopyEquiv K L
⊢ IsIso (isoOfHomotopyEquiv e).hom

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
h :
  ∀ ⦃K L : HomologicalComplex.{v, u, u_2} V c⦄ (f : K ⟶ L),
    MorphismProperty.inverseImage (MorphismProperty.isomorphisms (HomotopyCategory.{v, u, u_2} V c)) (quotient V c) f ↔
      homotopyEquivalences V c f
⊢ Eq (α := MorphismProperty (HomologicalComplex.{v, u, u_2} V c))
    (MorphismProperty.inverseImage (MorphismProperty.isomorphisms (HomotopyCategory.{v, u, u_2} V c)) (quotient V c))
    (homotopyEquivalences V c)

Tactic:
ext K L f
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_2} V c
f : K ⟶ L
⊢ IsIso (X := Functor.obj (quotient V c) K) (CategoryTheory.Functor.map (quotient V c) f) ↔ homotopyEquivalences V c f

Tactic:
⟨fun _ ↦ ?_, fun hf ↦ quotient_inverts_homotopyEquivalences _ _ _ hf⟩

Premises used: HomotopyCategory.quotient_inverts_homotopyEquivalences, Iff.intro
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_2} V c
f : K ⟶ L
h : IsIso (X := Functor.obj (quotient V c) K) (CategoryTheory.Functor.map (quotient V c) f) → homotopyEquivalences V c f
⊢ IsIso (X := Functor.obj (quotient V c) K) (CategoryTheory.Functor.map (quotient V c) f) ↔ homotopyEquivalences V c f

Tactic:
refine ⟨fun _ ↦ ?_, fun hf ↦ quotient_inverts_homotopyEquivalences _ _ _ hf⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_2} V c
f : K ⟶ L
h_1 : IsIso (X := Functor.obj (quotient V c) K) (CategoryTheory.Functor.map (quotient V c) f)
h :
  ∀ (g : L ⟶ K)
    (hg :
      Eq (α := Functor.obj (quotient V c) L ⟶ Functor.obj (quotient V c) K)
        (CategoryTheory.Functor.map (quotient V c) g) (inv (CategoryTheory.Functor.map (quotient V c) f))),
    homotopyEquivalences V c f
⊢ homotopyEquivalences V c f

Tactic:
obtain ⟨g, hg⟩ := (quotient V c).map_surjective (inv ((quotient _ _).map f))

Premises used: CategoryTheory.Functor.map, HomotopyCategory.quotient, CategoryTheory.inv, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_2} V c
f : K ⟶ L
h : IsIso (X := Functor.obj (quotient V c) K) (CategoryTheory.Functor.map (quotient V c) f)
g : L ⟶ K
hg :
  Eq (α := Functor.obj (quotient V c) L ⟶ Functor.obj (quotient V c) K) (CategoryTheory.Functor.map (quotient V c) g)
    (inv (CategoryTheory.Functor.map (quotient V c) f))
⊢ Eq (α := Functor.obj (quotient V c) K ⟶ Functor.obj (quotient V c) K)
    (CategoryTheory.Functor.map (quotient V c) (f ≫ g)) (CategoryTheory.Functor.map (quotient V c) (𝟙 K))

Tactic:
simp [hg]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_2} V c
f : K ⟶ L
h : IsIso (X := Functor.obj (quotient V c) K) (CategoryTheory.Functor.map (quotient V c) f)
g : L ⟶ K
hg :
  Eq (α := Functor.obj (quotient V c) L ⟶ Functor.obj (quotient V c) K) (CategoryTheory.Functor.map (quotient V c) g)
    (inv (CategoryTheory.Functor.map (quotient V c) f))
⊢ Eq (α := Functor.obj (quotient V c) L ⟶ Functor.obj (quotient V c) L)
    (CategoryTheory.Functor.map (quotient V c) (g ≫ f)) (CategoryTheory.Functor.map (quotient V c) (𝟙 L))

Tactic:
simp [hg]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_2} V c
f : K ⟶ L
h : IsIso (X := Functor.obj (quotient V c) K) (CategoryTheory.Functor.map (quotient V c) f)
g : L ⟶ K
hg :
  Eq (α := Functor.obj (quotient V c) L ⟶ Functor.obj (quotient V c) K) (CategoryTheory.Functor.map (quotient V c) g)
    (inv (CategoryTheory.Functor.map (quotient V c) f))
⊢ homotopyEquivalences V c f

Tactic:
exact ⟨{
    hom := f
    inv := g
    homotopyHomInvId := homotopyOfEq _ _ (by simp [hg])
    homotopyInvHomId := homotopyOfEq _ _ (by simp [hg]) }, rfl⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_2} V c
rw :
  Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C) (𝟙 (Functor.obj (quotient V c) C)) 0 ↔
    Nonempty (Homotopy (𝟙 C) 0)
⊢ IsZero (Functor.obj (quotient V c) C) ↔ Nonempty (Homotopy (𝟙 C) 0)

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero