[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
ι✝ : Type ?u.1725
v : ComplexShape ι✝
⊢ Category.{?u.1722, max (max u v) ?u.1725} (HomotopyCategory V v)
[PROOFSTEP]
dsimp only [HomotopyCategory]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
ι✝ : Type ?u.1725
v : ComplexShape ι✝
⊢ Category.{?u.1722, max (max u v) ?u.1725} (CategoryTheory.Quotient (homotopic V v))
[PROOFSTEP]
infer_instance
  -- TODO the homotopy_category is preadditive
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
⊢ Homotopy (Quot.out ((quotient V c).map f)) f
[PROOFSTEP]
apply homotopyOfEq
[GOAL]
case w
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
⊢ (quotient V c).map (Quot.out ((quotient V c).map f)) = (quotient V c).map f
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomotopyCategory V c
f : C ⟶ D
g : D ⟶ E
⊢ (quotient V c).map (Quot.out f ≫ Quot.out g) = f ≫ g
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map f.hom ≫ (quotient V c).map f.inv = 𝟙 ((quotient V c).obj C)
[PROOFSTEP]
rw [← (quotient V c).map_comp, ← (quotient V c).map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map (f.hom ≫ f.inv) = (quotient V c).map (𝟙 C)
[PROOFSTEP]
exact eq_of_homotopy _ _ f.homotopyHomInvId
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map f.inv ≫ (quotient V c).map f.hom = 𝟙 ((quotient V c).obj D)
[PROOFSTEP]
rw [← (quotient V c).map_comp, ← (quotient V c).map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map (f.inv ≫ f.hom) = (quotient V c).map (𝟙 D)
[PROOFSTEP]
exact eq_of_homotopy _ _ f.homotopyInvHomId
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
i : (quotient V c).obj C ≅ (quotient V c).obj D
⊢ (quotient V c).map (Quot.out i.hom ≫ Quot.out i.inv) = (quotient V c).map (𝟙 C)
[PROOFSTEP]
rw [quotient_map_out_comp_out, i.hom_inv_id, (quotient V c).map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
i : (quotient V c).obj C ≅ (quotient V c).obj D
⊢ (quotient V c).map (Quot.out i.inv ≫ Quot.out i.hom) = (quotient V c).map (𝟙 D)
[PROOFSTEP]
rw [quotient_map_out_comp_out, i.inv_hom_id, (quotient V c).map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c✝ : ComplexShape ι
W : Type u_2
inst✝³ : Category.{?u.46796, u_2} W
inst✝² : Preadditive W
F G : V ⥤ W
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
c : ComplexShape ι
⊢ ∀ ⦃X Y : HomotopyCategory V c⦄ (f : X ⟶ Y),
    (Functor.mapHomotopyCategory F c).map f ≫
        (fun C => (HomotopyCategory.quotient W c).map (app (mapHomologicalComplex α c) C.as)) Y =
      (fun C => (HomotopyCategory.quotient W c).map (app (mapHomologicalComplex α c) C.as)) X ≫
        (Functor.mapHomotopyCategory G c).map f
[PROOFSTEP]
rintro ⟨C⟩ ⟨D⟩ ⟨f : C ⟶ D⟩
[GOAL]
case mk.mk.mk
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c✝ : ComplexShape ι
W : Type u_2
inst✝³ : Category.{?u.46796, u_2} W
inst✝² : Preadditive W
F G : V ⥤ W
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
c : ComplexShape ι
C D : HomologicalComplex V c
f✝ : { as := C } ⟶ { as := D }
f : C ⟶ D
⊢ (Functor.mapHomotopyCategory F c).map (Quot.mk (Quotient.CompClosure (homotopic V c)) f) ≫
      (fun C => (HomotopyCategory.quotient W c).map (app (mapHomologicalComplex α c) C.as)) { as := D } =
    (fun C => (HomotopyCategory.quotient W c).map (app (mapHomologicalComplex α c) C.as)) { as := C } ≫
      (Functor.mapHomotopyCategory G c).map (Quot.mk (Quotient.CompClosure (homotopic V c)) f)
[PROOFSTEP]
simp only [HomotopyCategory.quot_mk_eq_quotient_map, Functor.mapHomotopyCategory_map, ← Functor.map_comp,
  NatTrans.naturality]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
c : ComplexShape ι
F : V ⥤ W
inst✝ : Functor.Additive F
⊢ mapHomotopyCategory (𝟙 F) c = 𝟙 (Functor.mapHomotopyCategory F c)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
W : Type u_2
inst✝⁴ : Category.{u_3, u_2} W
inst✝³ : Preadditive W
c : ComplexShape ι
F G H : V ⥤ W
inst✝² : Functor.Additive F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Additive H
α : F ⟶ G
β : G ⟶ H
⊢ mapHomotopyCategory (α ≫ β) c = mapHomotopyCategory α c ≫ mapHomotopyCategory β c
[PROOFSTEP]
aesop_cat
