[GOAL]
C : Type u_1
inst✝ : Bicategory C
X : C
⊢ ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : EndMonoidal X} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (fun {X₁ Y₁ X₂ Y₂} f g => f ▷ X₂ ≫ Y₁ ◁ g) (f₁ ≫ g₁) (f₂ ≫ g₂) =
      (fun {X₁ Y₁ X₂ Y₂} f g => f ▷ X₂ ≫ Y₁ ◁ g) f₁ f₂ ≫ (fun {X₁ Y₁ X₂ Y₂} f g => f ▷ X₂ ≫ Y₁ ◁ g) g₁ g₂
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
inst✝ : Bicategory C
X : C
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : EndMonoidal X
f₁✝ : X₁✝ ⟶ Y₁✝
f₂✝ : X₂✝ ⟶ Y₂✝
g₁✝ : Y₁✝ ⟶ Z₁✝
g₂✝ : Y₂✝ ⟶ Z₂✝
⊢ (fun {X₁ Y₁ X₂ Y₂} f g => f ▷ X₂ ≫ Y₁ ◁ g) (f₁✝ ≫ g₁✝) (f₂✝ ≫ g₂✝) =
    (fun {X₁ Y₁ X₂ Y₂} f g => f ▷ X₂ ≫ Y₁ ◁ g) f₁✝ f₂✝ ≫ (fun {X₁ Y₁ X₂ Y₂} f g => f ▷ X₂ ≫ Y₁ ◁ g) g₁✝ g₂✝
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝ : Bicategory C
X : C
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : EndMonoidal X
f₁✝ : X₁✝ ⟶ Y₁✝
f₂✝ : X₂✝ ⟶ Y₂✝
g₁✝ : Y₁✝ ⟶ Z₁✝
g₂✝ : Y₂✝ ⟶ Z₂✝
⊢ (f₁✝ ≫ g₁✝) ▷ X₂✝ ≫ Z₁✝ ◁ (f₂✝ ≫ g₂✝) = (f₁✝ ▷ X₂✝ ≫ Y₁✝ ◁ f₂✝) ≫ g₁✝ ▷ Y₂✝ ≫ Z₁✝ ◁ g₂✝
[PROOFSTEP]
rw [Bicategory.whiskerLeft_comp, Bicategory.comp_whiskerRight, Category.assoc, Category.assoc,
  Bicategory.whisker_exchange_assoc]


[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
apply Discrete.ext
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ ((f ≫ g) ≫ h).as = (f ≫ g ≫ h).as
[PROOFSTEP]
change (f.as ≫ g.as) ≫ h.as = f.as ≫ (g.as ≫ h.as)
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ (f.as ≫ g.as) ≫ h.as = f.as ≫ g.as ≫ h.as
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ 𝟙 a✝ ≫ f = f
[PROOFSTEP]
apply Discrete.ext
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ (𝟙 a✝ ≫ f).as = f.as
[PROOFSTEP]
change 𝟙 _ ≫ _ = _
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ 𝟙 a✝ ≫ f.as = f.as
[PROOFSTEP]
rw [Category.id_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ f ≫ 𝟙 b✝ = f
[PROOFSTEP]
apply Discrete.ext
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ (f ≫ 𝟙 b✝).as = f.as
[PROOFSTEP]
change _ ≫ 𝟙 _ = _
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ f.as ≫ 𝟙 b✝ = f.as
[PROOFSTEP]
rw [Category.comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : LocallyDiscrete C} (f : a ⟶ b), 𝟙 a ≫ f = f
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f✝ : a✝ ⟶ b✝
⊢ 𝟙 a✝ ≫ f✝ = f✝
[PROOFSTEP]
apply Discrete.ext
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f✝ : a✝ ⟶ b✝
⊢ (𝟙 a✝ ≫ f✝).as = f✝.as
[PROOFSTEP]
apply Category.id_comp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : LocallyDiscrete C} (f : a ⟶ b), f ≫ 𝟙 b = f
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f✝ : a✝ ⟶ b✝
⊢ f✝ ≫ 𝟙 b✝ = f✝
[PROOFSTEP]
apply Discrete.ext
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f✝ : a✝ ⟶ b✝
⊢ (f✝ ≫ 𝟙 b✝).as = f✝.as
[PROOFSTEP]
apply Category.comp_id
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b c d : LocallyDiscrete C} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : LocallyDiscrete C
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
[PROOFSTEP]
apply Discrete.ext
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : LocallyDiscrete C
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ ((f✝ ≫ g✝) ≫ h✝).as = (f✝ ≫ g✝ ≫ h✝).as
[PROOFSTEP]
apply Category.assoc


[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X✝ Y✝ : C
F : C ⥤ D
inst✝ : Full F
X Y : C
f : F.obj X ⟶ F.obj Y
⊢ F.map (F.preimage f) = f
[PROOFSTEP]
unfold preimage
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X✝ Y✝ : C
F : C ⥤ D
inst✝ : Full F
X Y : C
f : F.obj X ⟶ F.obj Y
⊢ F.map (Full.preimage f) = f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
F : C ⥤ D
h : ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, F.map p = f
⊢ Full F
[PROOFSTEP]
choose p hp using h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
F : C ⥤ D
p : (X Y : C) → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hp : ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), F.map (p X Y f) = f
⊢ Full F
[PROOFSTEP]
exact ⟨@p, @hp⟩
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
X Y Z : C
⊢ F.map (F.preimage (𝟙 (F.obj X))) = F.map (𝟙 X)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
X Y Z : C
f : F.obj X ⟶ F.obj Y
g : F.obj Y ⟶ F.obj Z
⊢ F.map (F.preimage (f ≫ g)) = F.map (F.preimage f ≫ F.preimage g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
X Y Z : C
f : X ⟶ Y
⊢ F.map (F.preimage (F.map f)) = F.map f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
X Y Z : C
f : F.obj X ≅ F.obj Y
⊢ F.map (F.preimage f.hom ≫ F.preimage f.inv) = F.map (𝟙 X)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
X Y Z : C
f : F.obj X ≅ F.obj Y
⊢ F.map (F.preimage f.inv ≫ F.preimage f.hom) = F.map (𝟙 Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
X Y Z : C
f : X ≅ Y
⊢ preimageIso F (F.mapIso f) = f
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
X Y Z : C
f : X ≅ Y
⊢ (preimageIso F (F.mapIso f)).hom = f.hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : Full F
inst✝¹ : Faithful F
X Y Z : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ F.map (f ≫ F.preimage (inv (F.map f))) = F.map (𝟙 X)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : Full F
inst✝¹ : Faithful F
X Y Z : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ F.map (F.preimage (inv (F.map f)) ≫ f) = F.map (𝟙 Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
X✝ Y✝ Z X Y : C
f : X ⟶ Y
⊢ (fun f => F.preimage f) ((fun f => F.map f) f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
X✝ Y✝ Z X Y : C
f : F.obj X ⟶ F.obj Y
⊢ (fun f => F.map f) ((fun f => F.preimage f) f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
X✝ Y✝ Z X Y : C
f : X ≅ Y
⊢ (fun f => Functor.preimageIso F f) ((fun f => F.mapIso f) f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
X✝ Y✝ Z X Y : C
f : F.obj X ≅ F.obj Y
⊢ (fun f => F.mapIso f) ((fun f => Functor.preimageIso F f) f) = f
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
X✝ Y✝ Z X Y : C
f : F.obj X ≅ F.obj Y
⊢ ((fun f => F.mapIso f) ((fun f => Functor.preimageIso F f) f)).hom = f.hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{?u.9765, u_1} E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
α : F ⋙ H ⟶ G ⋙ H
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ (fun X => ↑(equivOfFullyFaithful H).symm (NatTrans.app α X)) Y =
    (fun X => ↑(equivOfFullyFaithful H).symm (NatTrans.app α X)) X ≫ G.map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{?u.9765, u_1} E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
α : F ⋙ H ⟶ G ⋙ H
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ H.preimage (NatTrans.app α Y) = H.preimage (NatTrans.app α X) ≫ G.map f
[PROOFSTEP]
apply H.map_injective
[GOAL]
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{?u.9765, u_1} E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
α : F ⋙ H ⟶ G ⋙ H
X Y : C
f : X ⟶ Y
⊢ H.map (F.map f ≫ H.preimage (NatTrans.app α Y)) = H.map (H.preimage (NatTrans.app α X) ≫ G.map f)
[PROOFSTEP]
simpa using α.naturality f
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{?u.11855, u_1} E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
i : F ⋙ H ≅ G ⋙ H
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ F.map f ≫ ((fun X => ↑(isoEquivOfFullyFaithful H).symm (i.app X)) Y✝).hom =
    ((fun X => ↑(isoEquivOfFullyFaithful H).symm (i.app X)) X✝).hom ≫ G.map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{?u.11855, u_1} E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
i : F ⋙ H ≅ G ⋙ H
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ F.map f ≫ H.preimage (NatTrans.app i.hom Y✝) = H.preimage (NatTrans.app i.hom X✝) ≫ G.map f
[PROOFSTEP]
apply H.map_injective
[GOAL]
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{?u.11855, u_1} E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
i : F ⋙ H ≅ G ⋙ H
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ H.map (F.map f ≫ H.preimage (NatTrans.app i.hom Y✝)) = H.map (H.preimage (NatTrans.app i.hom X✝) ≫ G.map f)
[PROOFSTEP]
simpa using i.hom.naturality f
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
i : F ⋙ H ≅ G ⋙ H
⊢ (natIsoOfCompFullyFaithful H i).hom = natTransOfCompFullyFaithful H i.hom
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
i : F ⋙ H ≅ G ⋙ H
x✝ : C
⊢ NatTrans.app (natIsoOfCompFullyFaithful H i).hom x✝ = NatTrans.app (natTransOfCompFullyFaithful H i.hom) x✝
[PROOFSTEP]
simp [natIsoOfCompFullyFaithful]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
i : F ⋙ H ≅ G ⋙ H
⊢ (natIsoOfCompFullyFaithful H i).inv = natTransOfCompFullyFaithful H i.inv
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
i : F ⋙ H ≅ G ⋙ H
x✝ : C
⊢ NatTrans.app (natIsoOfCompFullyFaithful H i).inv x✝ = NatTrans.app (natTransOfCompFullyFaithful H i.inv) x✝
[PROOFSTEP]
simp [← preimage_comp]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{?u.17323, u_1} E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
⊢ Function.LeftInverse (natTransOfCompFullyFaithful H) fun α => α ◫ 𝟙 H
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{?u.17323, u_1} E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
⊢ Function.RightInverse (natTransOfCompFullyFaithful H) fun α => α ◫ 𝟙 H
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{?u.20694, u_1} E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
⊢ Function.LeftInverse (natIsoOfCompFullyFaithful H) fun e => hcomp e (Iso.refl H)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{?u.20694, u_1} E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
⊢ Function.RightInverse (natIsoOfCompFullyFaithful H) fun e => hcomp e (Iso.refl H)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F F' : C ⥤ D
G : D ⥤ E
inst✝ : Full F
α : F ≅ F'
X✝ Y✝ : C
f : F'.obj X✝ ⟶ F'.obj Y✝
⊢ F'.map ((fun {X Y} f => F.preimage ((α.app X).hom ≫ f ≫ (α.app Y).inv)) f) = f
[PROOFSTEP]
simp [← NatIso.naturality_1 α]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F F' : C ⥤ D
G : D ⥤ E
inst✝ : Faithful F
α : F ≅ F'
X✝ Y✝ : C
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F'.map a₁✝ = F'.map a₂✝
⊢ F.map a₁✝ = F.map a₂✝
[PROOFSTEP]
rw [← NatIso.naturality_1 α.symm, h, NatIso.naturality_1 α.symm]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
⊢ ∀ (X : C), { obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
[PROOFSTEP]
intros X
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X : C
⊢ { obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
[PROOFSTEP]
apply G.map_injective
[GOAL]
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X : C
⊢ G.map ({ obj := obj, map := map }.map (𝟙 X)) = G.map (𝟙 ({ obj := obj, map := map }.obj X))
[PROOFSTEP]
apply eq_of_heq
[GOAL]
case a.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X : C
⊢ HEq (G.map ({ obj := obj, map := map }.map (𝟙 X))) (G.map (𝟙 ({ obj := obj, map := map }.obj X)))
[PROOFSTEP]
trans F.map (𝟙 X)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X : C
⊢ HEq (G.map ({ obj := obj, map := map }.map (𝟙 X))) (F.map (𝟙 X))
[PROOFSTEP]
exact h_map
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X : C
⊢ HEq (F.map (𝟙 X)) (G.map (𝟙 ({ obj := obj, map := map }.obj X)))
[PROOFSTEP]
rw [F.map_id, G.map_id, h_obj X]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := obj, map := map }.map (f ≫ g) = { obj := obj, map := map }.map f ≫ { obj := obj, map := map }.map g
[PROOFSTEP]
intros X Y Z f g
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ { obj := obj, map := map }.map (f ≫ g) = { obj := obj, map := map }.map f ≫ { obj := obj, map := map }.map g
[PROOFSTEP]
refine G.map_injective <| eq_of_heq <| h_map.trans ?_
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ HEq (F.map (f ≫ g)) (G.map ({ obj := obj, map := map }.map f ≫ { obj := obj, map := map }.map g))
[PROOFSTEP]
simp only [Functor.map_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ HEq (F.map f ≫ F.map g) (G.map (map f) ≫ G.map (map g))
[PROOFSTEP]
convert HEq.refl (F.map f ≫ F.map g)
[GOAL]
case h.e'_3.h.e'_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ G.obj (obj X) = F.obj X
case h.e'_3.h.e'_4
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ G.obj (obj Z) = F.obj Z
case h.e'_4.e'_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
⊢ G.obj (obj X) = F.obj X
case h.e'_4.e'_4
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
⊢ G.obj (obj Y) = F.obj Y
case h.e'_4.e'_5
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
⊢ G.obj (obj Z) = F.obj Z
case h.e'_4.e'_6
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝¹ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
e_3✝ : G.obj (obj X) = F.obj X
e_4✝ : G.obj (obj Y) = F.obj Y
⊢ HEq (G.map (map f)) (F.map f)
case h.e'_4.e'_7
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
e_4✝ : G.obj (obj Y) = F.obj Y
e_5✝ : G.obj (obj Z) = F.obj Z
⊢ HEq (G.map (map g)) (F.map g)
[PROOFSTEP]
all_goals
  {first
  | apply h_obj
  | apply h_map
}
[GOAL]
case h.e'_3.h.e'_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ G.obj (obj X) = F.obj X
[PROOFSTEP]
{first
  | apply h_obj
  | apply h_map
}
[GOAL]
case h.e'_3.h.e'_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ G.obj (obj X) = F.obj X
[PROOFSTEP]
first
| apply h_obj
| apply h_map
[GOAL]
case h.e'_3.h.e'_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ G.obj (obj X) = F.obj X
[PROOFSTEP]
apply h_obj
[GOAL]
case h.e'_3.h.e'_4
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ G.obj (obj Z) = F.obj Z
[PROOFSTEP]
{first
  | apply h_obj
  | apply h_map
}
[GOAL]
case h.e'_3.h.e'_4
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ G.obj (obj Z) = F.obj Z
[PROOFSTEP]
first
| apply h_obj
| apply h_map
[GOAL]
case h.e'_3.h.e'_4
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ G.obj (obj Z) = F.obj Z
[PROOFSTEP]
apply h_obj
[GOAL]
case h.e'_4.e'_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
⊢ G.obj (obj X) = F.obj X
[PROOFSTEP]
{first
  | apply h_obj
  | apply h_map
}
[GOAL]
case h.e'_4.e'_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
⊢ G.obj (obj X) = F.obj X
[PROOFSTEP]
first
| apply h_obj
| apply h_map
[GOAL]
case h.e'_4.e'_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
⊢ G.obj (obj X) = F.obj X
[PROOFSTEP]
apply h_obj
[GOAL]
case h.e'_4.e'_4
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
⊢ G.obj (obj Y) = F.obj Y
[PROOFSTEP]
{first
  | apply h_obj
  | apply h_map
}
[GOAL]
case h.e'_4.e'_4
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
⊢ G.obj (obj Y) = F.obj Y
[PROOFSTEP]
first
| apply h_obj
| apply h_map
[GOAL]
case h.e'_4.e'_4
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
⊢ G.obj (obj Y) = F.obj Y
[PROOFSTEP]
apply h_obj
[GOAL]
case h.e'_4.e'_5
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
⊢ G.obj (obj Z) = F.obj Z
[PROOFSTEP]
{first
  | apply h_obj
  | apply h_map
}
[GOAL]
case h.e'_4.e'_5
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
⊢ G.obj (obj Z) = F.obj Z
[PROOFSTEP]
first
| apply h_obj
| apply h_map
[GOAL]
case h.e'_4.e'_5
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
⊢ G.obj (obj Z) = F.obj Z
[PROOFSTEP]
apply h_obj
[GOAL]
case h.e'_4.e'_6
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝¹ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
e_3✝ : G.obj (obj X) = F.obj X
e_4✝ : G.obj (obj Y) = F.obj Y
⊢ HEq (G.map (map f)) (F.map f)
[PROOFSTEP]
{first
  | apply h_obj
  | apply h_map
}
[GOAL]
case h.e'_4.e'_6
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝¹ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
e_3✝ : G.obj (obj X) = F.obj X
e_4✝ : G.obj (obj Y) = F.obj Y
⊢ HEq (G.map (map f)) (F.map f)
[PROOFSTEP]
first
| apply h_obj
| apply h_map
[GOAL]
case h.e'_4.e'_6
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝¹ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
e_3✝ : G.obj (obj X) = F.obj X
e_4✝ : G.obj (obj Y) = F.obj Y
⊢ HEq (G.map (map f)) (F.map f)
[PROOFSTEP]
apply h_obj
[GOAL]
case h.e'_4.e'_6
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝¹ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
e_3✝ : G.obj (obj X) = F.obj X
e_4✝ : G.obj (obj Y) = F.obj Y
⊢ HEq (G.map (map f)) (F.map f)
[PROOFSTEP]
apply h_map
[GOAL]
case h.e'_4.e'_7
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
e_4✝ : G.obj (obj Y) = F.obj Y
e_5✝ : G.obj (obj Z) = F.obj Z
⊢ HEq (G.map (map g)) (F.map g)
[PROOFSTEP]
{first
  | apply h_obj
  | apply h_map
}
[GOAL]
case h.e'_4.e'_7
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
e_4✝ : G.obj (obj Y) = F.obj Y
e_5✝ : G.obj (obj Z) = F.obj Z
⊢ HEq (G.map (map g)) (F.map g)
[PROOFSTEP]
first
| apply h_obj
| apply h_map
[GOAL]
case h.e'_4.e'_7
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
e_4✝ : G.obj (obj Y) = F.obj Y
e_5✝ : G.obj (obj Z) = F.obj Z
⊢ HEq (G.map (map g)) (F.map g)
[PROOFSTEP]
apply h_obj
[GOAL]
case h.e'_4.e'_7
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e_3✝ : (G.obj (obj X) ⟶ G.obj (obj Z)) = (F.obj X ⟶ F.obj Z)
e_4✝ : G.obj (obj Y) = F.obj Y
e_5✝ : G.obj (obj Z) = F.obj Z
⊢ HEq (G.map (map g)) (F.map g)
[PROOFSTEP]
apply h_map
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
inst✝¹ : Faithful F
G : D ⥤ E
inst✝ : Faithful G
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
⊢ Faithful.div F G obj h_obj map h_map ⋙ G = F
[PROOFSTEP]
cases' F with F_pre _ _
[GOAL]
case mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F F' : C ⥤ D
G✝ G : D ⥤ E
inst✝¹ : Faithful G
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_pre : C ⥤q E
map_id✝ : ∀ (X : C), F_pre.map (𝟙 X) = 𝟙 (F_pre.obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), F_pre.map (f ≫ g) = F_pre.map f ≫ F_pre.map g
inst✝ : Faithful (Functor.mk F_pre)
h_obj : ∀ (X : C), G.obj (obj X) = (Functor.mk F_pre).obj X
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) ((Functor.mk F_pre).map f)
⊢ Faithful.div (Functor.mk F_pre) G obj h_obj map h_map ⋙ G = Functor.mk F_pre
[PROOFSTEP]
cases' G with G_pre _ _
[GOAL]
case mk.mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F F' : C ⥤ D
G : D ⥤ E
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_pre : C ⥤q E
map_id✝¹ : ∀ (X : C), F_pre.map (𝟙 X) = 𝟙 (F_pre.obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), F_pre.map (f ≫ g) = F_pre.map f ≫ F_pre.map g
inst✝¹ : Faithful (Functor.mk F_pre)
G_pre : D ⥤q E
map_id✝ : ∀ (X : D), G_pre.map (𝟙 X) = 𝟙 (G_pre.obj X)
map_comp✝ : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), G_pre.map (f ≫ g) = G_pre.map f ≫ G_pre.map g
inst✝ : Faithful (Functor.mk G_pre)
h_obj : ∀ (X : C), (Functor.mk G_pre).obj (obj X) = (Functor.mk F_pre).obj X
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq ((Functor.mk G_pre).map (map f)) ((Functor.mk F_pre).map f)
⊢ Faithful.div (Functor.mk F_pre) (Functor.mk G_pre) obj h_obj map h_map ⋙ Functor.mk G_pre = Functor.mk F_pre
[PROOFSTEP]
cases' F_pre with F_obj _
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F F' : C ⥤ D
G : D ⥤ E
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
G_pre : D ⥤q E
map_id✝¹ : ∀ (X : D), G_pre.map (𝟙 X) = 𝟙 (G_pre.obj X)
map_comp✝¹ : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), G_pre.map (f ≫ g) = G_pre.map f ≫ G_pre.map g
inst✝¹ : Faithful (Functor.mk G_pre)
F_obj : C → E
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), { obj := F_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝ }.map (f ≫ g) =
      { obj := F_obj, map := map✝ }.map f ≫ { obj := F_obj, map := map✝ }.map g
inst✝ : Faithful (Functor.mk { obj := F_obj, map := map✝ })
h_obj : ∀ (X : C), (Functor.mk G_pre).obj (obj X) = (Functor.mk { obj := F_obj, map := map✝ }).obj X
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq ((Functor.mk G_pre).map (map f)) ((Functor.mk { obj := F_obj, map := map✝ }).map f)
⊢ Faithful.div (Functor.mk { obj := F_obj, map := map✝ }) (Functor.mk G_pre) obj h_obj map h_map ⋙ Functor.mk G_pre =
    Functor.mk { obj := F_obj, map := map✝ }
[PROOFSTEP]
cases' G_pre with G_obj _
[GOAL]
case mk.mk.mk.mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F F' : C ⥤ D
G : D ⥤ E
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_obj : C → E
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
inst✝¹ : Faithful (Functor.mk { obj := F_obj, map := map✝¹ })
G_obj : D → E
map✝ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ : ∀ (X : D), { obj := G_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj, map := map✝ }.map (f ≫ g) =
      { obj := G_obj, map := map✝ }.map f ≫ { obj := G_obj, map := map✝ }.map g
inst✝ : Faithful (Functor.mk { obj := G_obj, map := map✝ })
h_obj :
  ∀ (X : C), (Functor.mk { obj := G_obj, map := map✝ }).obj (obj X) = (Functor.mk { obj := F_obj, map := map✝¹ }).obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    HEq ((Functor.mk { obj := G_obj, map := map✝ }).map (map f)) ((Functor.mk { obj := F_obj, map := map✝¹ }).map f)
⊢ Faithful.div (Functor.mk { obj := F_obj, map := map✝¹ }) (Functor.mk { obj := G_obj, map := map✝ }) obj h_obj map
        h_map ⋙
      Functor.mk { obj := G_obj, map := map✝ } =
    Functor.mk { obj := F_obj, map := map✝¹ }
[PROOFSTEP]
unfold Faithful.div Functor.comp
[GOAL]
case mk.mk.mk.mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F F' : C ⥤ D
G : D ⥤ E
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_obj : C → E
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
inst✝¹ : Faithful (Functor.mk { obj := F_obj, map := map✝¹ })
G_obj : D → E
map✝ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ : ∀ (X : D), { obj := G_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj, map := map✝ }.map (f ≫ g) =
      { obj := G_obj, map := map✝ }.map f ≫ { obj := G_obj, map := map✝ }.map g
inst✝ : Faithful (Functor.mk { obj := G_obj, map := map✝ })
h_obj :
  ∀ (X : C), (Functor.mk { obj := G_obj, map := map✝ }).obj (obj X) = (Functor.mk { obj := F_obj, map := map✝¹ }).obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    HEq ((Functor.mk { obj := G_obj, map := map✝ }).map (map f)) ((Functor.mk { obj := F_obj, map := map✝¹ }).map f)
⊢ Functor.mk
      { obj := fun X => (Functor.mk { obj := G_obj, map := map✝ }).obj ((Functor.mk { obj := obj, map := map }).obj X),
        map := fun {X Y} f =>
          (Functor.mk { obj := G_obj, map := map✝ }).map ((Functor.mk { obj := obj, map := map }).map f) } =
    Functor.mk { obj := F_obj, map := map✝¹ }
[PROOFSTEP]
have : F_obj = G_obj ∘ obj := (funext h_obj).symm
[GOAL]
case mk.mk.mk.mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F F' : C ⥤ D
G : D ⥤ E
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_obj : C → E
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
inst✝¹ : Faithful (Functor.mk { obj := F_obj, map := map✝¹ })
G_obj : D → E
map✝ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ : ∀ (X : D), { obj := G_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj, map := map✝ }.map (f ≫ g) =
      { obj := G_obj, map := map✝ }.map f ≫ { obj := G_obj, map := map✝ }.map g
inst✝ : Faithful (Functor.mk { obj := G_obj, map := map✝ })
h_obj :
  ∀ (X : C), (Functor.mk { obj := G_obj, map := map✝ }).obj (obj X) = (Functor.mk { obj := F_obj, map := map✝¹ }).obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    HEq ((Functor.mk { obj := G_obj, map := map✝ }).map (map f)) ((Functor.mk { obj := F_obj, map := map✝¹ }).map f)
this : F_obj = G_obj ∘ obj
⊢ Functor.mk
      { obj := fun X => (Functor.mk { obj := G_obj, map := map✝ }).obj ((Functor.mk { obj := obj, map := map }).obj X),
        map := fun {X Y} f =>
          (Functor.mk { obj := G_obj, map := map✝ }).map ((Functor.mk { obj := obj, map := map }).map f) } =
    Functor.mk { obj := F_obj, map := map✝¹ }
[PROOFSTEP]
subst this
[GOAL]
case mk.mk.mk.mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F F' : C ⥤ D
G : D ⥤ E
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
G_obj : D → E
map✝¹ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : D), { obj := G_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := G_obj, map := map✝¹ }.map f ≫ { obj := G_obj, map := map✝¹ }.map g
inst✝¹ : Faithful (Functor.mk { obj := G_obj, map := map✝¹ })
map✝ : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)
map_id✝ : ∀ (X : C), { obj := G_obj ∘ obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj ∘ obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj ∘ obj, map := map✝ }.map (f ≫ g) =
      { obj := G_obj ∘ obj, map := map✝ }.map f ≫ { obj := G_obj ∘ obj, map := map✝ }.map g
inst✝ : Faithful (Functor.mk { obj := G_obj ∘ obj, map := map✝ })
h_obj :
  ∀ (X : C),
    (Functor.mk { obj := G_obj, map := map✝¹ }).obj (obj X) = (Functor.mk { obj := G_obj ∘ obj, map := map✝ }).obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    HEq ((Functor.mk { obj := G_obj, map := map✝¹ }).map (map f))
      ((Functor.mk { obj := G_obj ∘ obj, map := map✝ }).map f)
⊢ Functor.mk
      { obj := fun X => (Functor.mk { obj := G_obj, map := map✝¹ }).obj ((Functor.mk { obj := obj, map := map }).obj X),
        map := fun {X Y} f =>
          (Functor.mk { obj := G_obj, map := map✝¹ }).map ((Functor.mk { obj := obj, map := map }).map f) } =
    Functor.mk { obj := G_obj ∘ obj, map := map✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.mk.mk.e_toPrefunctor.e_map
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F F' : C ⥤ D
G : D ⥤ E
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
G_obj : D → E
map✝¹ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : D), { obj := G_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := G_obj, map := map✝¹ }.map f ≫ { obj := G_obj, map := map✝¹ }.map g
inst✝¹ : Faithful (Functor.mk { obj := G_obj, map := map✝¹ })
map✝ : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)
map_id✝ : ∀ (X : C), { obj := G_obj ∘ obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj ∘ obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj ∘ obj, map := map✝ }.map (f ≫ g) =
      { obj := G_obj ∘ obj, map := map✝ }.map f ≫ { obj := G_obj ∘ obj, map := map✝ }.map g
inst✝ : Faithful (Functor.mk { obj := G_obj ∘ obj, map := map✝ })
h_obj :
  ∀ (X : C),
    (Functor.mk { obj := G_obj, map := map✝¹ }).obj (obj X) = (Functor.mk { obj := G_obj ∘ obj, map := map✝ }).obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    HEq ((Functor.mk { obj := G_obj, map := map✝¹ }).map (map f))
      ((Functor.mk { obj := G_obj ∘ obj, map := map✝ }).map f)
⊢ (fun {X Y} f => (Functor.mk { obj := G_obj, map := map✝¹ }).map ((Functor.mk { obj := obj, map := map }).map f)) =
    map✝
[PROOFSTEP]
simp only [Function.comp_apply, heq_eq_eq] at h_map
[GOAL]
case mk.mk.mk.mk.e_toPrefunctor.e_map
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F F' : C ⥤ D
G : D ⥤ E
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
G_obj : D → E
map✝¹ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : D), { obj := G_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := G_obj, map := map✝¹ }.map f ≫ { obj := G_obj, map := map✝¹ }.map g
inst✝¹ : Faithful (Functor.mk { obj := G_obj, map := map✝¹ })
map✝ : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)
map_id✝ : ∀ (X : C), { obj := G_obj ∘ obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj ∘ obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj ∘ obj, map := map✝ }.map (f ≫ g) =
      { obj := G_obj ∘ obj, map := map✝ }.map f ≫ { obj := G_obj ∘ obj, map := map✝ }.map g
inst✝ : Faithful (Functor.mk { obj := G_obj ∘ obj, map := map✝ })
h_obj :
  ∀ (X : C),
    (Functor.mk { obj := G_obj, map := map✝¹ }).obj (obj X) = (Functor.mk { obj := G_obj ∘ obj, map := map✝ }).obj X
h_map✝ :
  ∀ {X Y : C} {f : X ⟶ Y},
    HEq ((Functor.mk { obj := G_obj, map := map✝¹ }).map (map f))
      ((Functor.mk { obj := G_obj ∘ obj, map := map✝ }).map f)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, map✝¹ (map f) = map✝ f
⊢ (fun {X Y} f => (Functor.mk { obj := G_obj, map := map✝¹ }).map ((Functor.mk { obj := obj, map := map }).map f)) =
    map✝
[PROOFSTEP]
ext
[GOAL]
case mk.mk.mk.mk.e_toPrefunctor.e_map.h.h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F F' : C ⥤ D
G : D ⥤ E
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
G_obj : D → E
map✝¹ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : D), { obj := G_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := G_obj, map := map✝¹ }.map f ≫ { obj := G_obj, map := map✝¹ }.map g
inst✝¹ : Faithful (Functor.mk { obj := G_obj, map := map✝¹ })
map✝ : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)
map_id✝ : ∀ (X : C), { obj := G_obj ∘ obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj ∘ obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj ∘ obj, map := map✝ }.map (f ≫ g) =
      { obj := G_obj ∘ obj, map := map✝ }.map f ≫ { obj := G_obj ∘ obj, map := map✝ }.map g
inst✝ : Faithful (Functor.mk { obj := G_obj ∘ obj, map := map✝ })
h_obj :
  ∀ (X : C),
    (Functor.mk { obj := G_obj, map := map✝¹ }).obj (obj X) = (Functor.mk { obj := G_obj ∘ obj, map := map✝ }).obj X
h_map✝ :
  ∀ {X Y : C} {f : X ⟶ Y},
    HEq ((Functor.mk { obj := G_obj, map := map✝¹ }).map (map f))
      ((Functor.mk { obj := G_obj ∘ obj, map := map✝ }).map f)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, map✝¹ (map f) = map✝ f
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ (Functor.mk { obj := G_obj, map := map✝¹ }).map ((Functor.mk { obj := obj, map := map }).map x✝) = map✝ x✝
[PROOFSTEP]
exact h_map
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
comp_iso : F ⋙ H ≅ G ⋙ H
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ H.map (F.map f ≫ ((fun X => Functor.preimageIso H (comp_iso.app X)) Y✝).hom) =
    H.map (((fun X => Functor.preimageIso H (comp_iso.app X)) X✝).hom ≫ G.map f)
[PROOFSTEP]
simpa using comp_iso.hom.naturality f


[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (leftDerived F n).map f =
    (leftDerivedObjIso F n P).hom ≫
      (homologyFunctor D (ComplexShape.down ℕ) n).map ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) ≫
        (leftDerivedObjIso F n Q).inv
[PROOFSTEP]
dsimp only [Functor.leftDerived, Functor.leftDerivedObjIso]
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (projectiveResolutions C ⋙
          mapHomotopyCategory F (ComplexShape.down ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      f =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).mapIso
            (HomotopyCategory.isoOfHomotopyEquiv
              (mapHomotopyEquiv F (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P))) ≪≫
          (HomotopyCategory.homologyFactors D (ComplexShape.down ℕ) n).app
            ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)).hom ≫
      (homologyFunctor D (ComplexShape.down ℕ) n).map ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) ≫
        ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).mapIso
              (HomotopyCategory.isoOfHomotopyEquiv
                (mapHomotopyEquiv F (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q))) ≪≫
            (HomotopyCategory.homologyFactors D (ComplexShape.down ℕ) n).app
              ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex)).inv
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.down ℕ)).map ((projectiveResolutions C).map f)) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
              (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom)) ≫
        𝟙
          ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).obj
            ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
              ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)))) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n =
              0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) n =
              0)
          (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n)
          (HomologicalComplex.Hom.sqFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n)
          (_ :
            (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n).right =
              (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n).right) ≫
        𝟙 (HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) n) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
            ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
              ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
                (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv))
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp]
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.down ℕ)).map ((projectiveResolutions C).map f)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
          ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
            (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom)) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n =
              0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) n =
              0)
          (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n)
          (HomologicalComplex.Hom.sqFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n)
          (_ :
            (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n).right =
              (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n).right) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
              (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv))
[PROOFSTEP]
rw [← homologyFunctor_map, HomotopyCategory.homologyFunctor_map_factors]
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.down ℕ)).map ((projectiveResolutions C).map f)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
          ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
            (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom)) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
              (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv))
[PROOFSTEP]
simp only [← Functor.map_comp]
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.down ℕ)).map ((projectiveResolutions C).map f)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
          ((ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
            g ≫ (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv)))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (mapHomotopyCategory F (ComplexShape.down ℕ)).map ((projectiveResolutions C).map f) =
    (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
      ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
        ((ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
          g ≫ (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv))
[PROOFSTEP]
apply HomotopyCategory.eq_of_homotopy
[GOAL]
case e_a.h
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ Homotopy ((mapHomologicalComplex F (ComplexShape.down ℕ)).map (projectiveResolution.lift f))
    ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
      ((ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
        g ≫ (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv))
[PROOFSTEP]
apply Functor.mapHomotopy
[GOAL]
case e_a.h.h
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ Homotopy (projectiveResolution.lift f)
    ((ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
      g ≫ (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv)
[PROOFSTEP]
apply ProjectiveResolution.liftHomotopy f
[GOAL]
case e_a.h.h.g_comm
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ projectiveResolution.lift f ≫ (projectiveResolution Y).π = (projectiveResolution X).π ≫ (ChainComplex.single₀ C).map f
[PROOFSTEP]
simp
[GOAL]
case e_a.h.h.h_comm
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ ((ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
        g ≫ (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv) ≫
      (projectiveResolution Y).π =
    (projectiveResolution X).π ≫ (ChainComplex.single₀ C).map f
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Functor.Additive F
n : ℕ
⊢ leftDerived (𝟙 F) n = 𝟙 (Functor.leftDerived F n)
[PROOFSTEP]
simp [NatTrans.leftDerived]
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Functor.Additive F
n : ℕ
⊢ 𝟙
      (projectiveResolutions C ⋙
        Functor.mapHomotopyCategory F (ComplexShape.down ℕ) ⋙
          HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) =
    𝟙 (Functor.leftDerived F n)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹⁴ : Category.{v, u} C
D : Type u_1
inst✝¹³ : Category.{u_2, u_1} D
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasEqualizers C
inst✝⁹ : HasImages C
inst✝⁸ : HasProjectiveResolutions C
inst✝⁷ : Preadditive D
inst✝⁶ : HasEqualizers D
inst✝⁵ : HasCokernels D
inst✝⁴ : HasImages D
inst✝³ : HasImageMaps D
F G H : C ⥤ D
inst✝² : Functor.Additive F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Additive H
α : F ⟶ G
β : G ⟶ H
n : ℕ
⊢ leftDerived (α ≫ β) n = leftDerived α n ≫ leftDerived β n
[PROOFSTEP]
simp [NatTrans.leftDerived]
[GOAL]
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ app (leftDerived α n) X =
    (Functor.leftDerivedObjIso F n P).hom ≫
      (homologyFunctor D (ComplexShape.down ℕ) n).map (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) ≫
        (Functor.leftDerivedObjIso G n P).inv
[PROOFSTEP]
symm
[GOAL]
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ (Functor.leftDerivedObjIso F n P).hom ≫
      (homologyFunctor D (ComplexShape.down ℕ) n).map (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) ≫
        (Functor.leftDerivedObjIso G n P).inv =
    app (leftDerived α n) X
[PROOFSTEP]
dsimp [NatTrans.leftDerived, Functor.leftDerivedObjIso]
[GOAL]
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map
              (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom)) ≫
        𝟙
          ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).obj
            ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
              ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)))) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n ≫
                HomologicalComplex.dFrom ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n =
              0)
          (_ :
            HomologicalComplex.dTo ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj P.complex) n ≫
                HomologicalComplex.dFrom ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj P.complex) n =
              0)
          (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n)
          (HomologicalComplex.Hom.sqFrom (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n)
          (_ :
            (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n).right =
              (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n).right) ≫
        𝟙 (HomologicalComplex.homology ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj P.complex) n) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
            ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
              ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
                (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as))
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp]
[GOAL]
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
          ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map
            (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom)) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n ≫
                HomologicalComplex.dFrom ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n =
              0)
          (_ :
            HomologicalComplex.dTo ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj P.complex) n ≫
                HomologicalComplex.dFrom ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj P.complex) n =
              0)
          (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n)
          (HomologicalComplex.Hom.sqFrom (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n)
          (_ :
            (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n).right =
              (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n).right) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
              (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as))
[PROOFSTEP]
rw [← homologyFunctor_map, HomotopyCategory.homologyFunctor_map_factors]
[GOAL]
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
          ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map
            (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom)) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
              (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as))
[PROOFSTEP]
simp only [← Functor.map_comp]
[GOAL]
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map
            (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
          app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex ≫
            (Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
              (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
      ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map
          (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
        app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex ≫
          (Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
            (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv) =
    (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
      (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as)
[PROOFSTEP]
apply HomotopyCategory.eq_of_homotopy
[GOAL]
case e_a.h
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ Homotopy
    ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map
        (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
      app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex ≫
        (Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
          (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv)
    (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as)
[PROOFSTEP]
simp only [NatTrans.mapHomologicalComplex_naturality_assoc, ← Functor.map_comp]
[GOAL]
case e_a.h
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ Homotopy
    (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as ≫
      (Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
        ((ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
          (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv))
    (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as)
[PROOFSTEP]
apply Homotopy.compLeftId
[GOAL]
case e_a.h.h
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ Homotopy
    ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
      ((ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
        (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv))
    (𝟙 ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as))
[PROOFSTEP]
refine' (Functor.mapHomotopy _ (HomotopyEquiv.homotopyHomInvId _)).trans _
[GOAL]
case e_a.h.h
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ Homotopy ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map (𝟙 ((projectiveResolutions C).obj X).as))
    (𝟙 ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as))
[PROOFSTEP]
apply Homotopy.ofEq
[GOAL]
case e_a.h.h.h
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ (Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map (𝟙 ((projectiveResolutions C).obj X).as) =
    𝟙 ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as)
[PROOFSTEP]
simp only [Functor.map_id]


[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.73, u_1} C
inst✝ : MonoidalCategory C
⊢ Inhabited (MonoidalSingleObj C)
[PROOFSTEP]
unfold MonoidalSingleObj
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.73, u_1} C
inst✝ : MonoidalCategory C
⊢ Inhabited PUnit
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.162, u_1} C
inst✝ : MonoidalCategory C
a✝ b✝ : MonoidalSingleObj C
f✝ g✝ : a✝ ⟶ b✝
x✝ : f✝ ⟶ g✝
⊢ (fun {a b c} X Y Z f => 𝟙 X ⊗ f) (𝟙 a✝) f✝ g✝ x✝ =
    ((fun {a b} X => λ_ X) f✝).hom ≫ x✝ ≫ ((fun {a b} X => λ_ X) g✝).inv
[PROOFSTEP]
simp_rw [leftUnitor_inv_naturality, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.162, u_1} C
inst✝ : MonoidalCategory C
a✝ b✝ c✝ d✝ : MonoidalSingleObj C
x✝⁴ : a✝ ⟶ b✝
x✝³ : b✝ ⟶ c✝
x✝² x✝¹ : c✝ ⟶ d✝
x✝ : x✝² ⟶ x✝¹
⊢ (fun {a b c} X Y Z f => 𝟙 X ⊗ f) (x✝⁴ ≫ x✝³) x✝² x✝¹ x✝ =
    ((fun {a b c d} X Y Z => α_ X Y Z) x✝⁴ x✝³ x✝²).hom ≫
      (fun {a b c} X Y Z f => 𝟙 X ⊗ f) x✝⁴ (x✝³ ≫ x✝²) (x✝³ ≫ x✝¹) ((fun {a b c} X Y Z f => 𝟙 X ⊗ f) x✝³ x✝² x✝¹ x✝) ≫
        ((fun {a b c d} X Y Z => α_ X Y Z) x✝⁴ x✝³ x✝¹).inv
[PROOFSTEP]
simp_rw [associator_inv_naturality, Iso.hom_inv_id_assoc, tensor_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.162, u_1} C
inst✝ : MonoidalCategory C
a✝ b✝ : MonoidalSingleObj C
f✝ g✝ : a✝ ⟶ b✝
x✝ : f✝ ⟶ g✝
⊢ (fun {a b c} {f g} f_1 Z => f_1 ⊗ 𝟙 Z) x✝ (𝟙 b✝) =
    ((fun {a b} X => ρ_ X) f✝).hom ≫ x✝ ≫ ((fun {a b} X => ρ_ X) g✝).inv
[PROOFSTEP]
simp_rw [rightUnitor_inv_naturality, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.162, u_1} C
inst✝ : MonoidalCategory C
a✝ b✝ c✝ d✝ : MonoidalSingleObj C
f✝ f'✝ : a✝ ⟶ b✝
x✝² : f✝ ⟶ f'✝
x✝¹ : b✝ ⟶ c✝
x✝ : c✝ ⟶ d✝
⊢ (fun {a b c} {f g} f_1 Z => f_1 ⊗ 𝟙 Z) x✝² (x✝¹ ≫ x✝) =
    ((fun {a b c d} X Y Z => α_ X Y Z) f✝ x✝¹ x✝).inv ≫
      (fun {a b c} {f g} f_1 Z => f_1 ⊗ 𝟙 Z) ((fun {a b c} {f g} f_1 Z => f_1 ⊗ 𝟙 Z) x✝² x✝¹) x✝ ≫
        ((fun {a b c d} X Y Z => α_ X Y Z) f'✝ x✝¹ x✝).hom
[PROOFSTEP]
simp_rw [← tensor_id, associator_naturality, Iso.inv_hom_id_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.162, u_1} C
inst✝ : MonoidalCategory C
a✝ b✝ c✝ d✝ : MonoidalSingleObj C
x✝⁴ : a✝ ⟶ b✝
x✝³ x✝² : b✝ ⟶ c✝
x✝¹ : x✝³ ⟶ x✝²
x✝ : c✝ ⟶ d✝
⊢ (fun {a b c} {f g} f_1 Z => f_1 ⊗ 𝟙 Z) ((fun {a b c} X Y Z f => 𝟙 X ⊗ f) x✝⁴ x✝³ x✝² x✝¹) x✝ =
    ((fun {a b c d} X Y Z => α_ X Y Z) x✝⁴ x✝³ x✝).hom ≫
      (fun {a b c} X Y Z f => 𝟙 X ⊗ f) x✝⁴ (x✝³ ≫ x✝) (x✝² ≫ x✝) ((fun {a b c} {f g} f_1 Z => f_1 ⊗ 𝟙 Z) x✝¹ x✝) ≫
        ((fun {a b c d} X Y Z => α_ X Y Z) x✝⁴ x✝² x✝).inv
[PROOFSTEP]
simp_rw [associator_inv_naturality, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.162, u_1} C
inst✝ : MonoidalCategory C
a✝ b✝ c✝ d✝ e✝ : MonoidalSingleObj C
x✝³ : a✝ ⟶ b✝
x✝² : b✝ ⟶ c✝
x✝¹ : c✝ ⟶ d✝
x✝ : d✝ ⟶ e✝
⊢ (fun {a b c} {f g} f_1 Z => f_1 ⊗ 𝟙 Z) ((fun {a b c d} X Y Z => α_ X Y Z) x✝³ x✝² x✝¹).hom x✝ ≫
      ((fun {a b c d} X Y Z => α_ X Y Z) x✝³ (x✝² ≫ x✝¹) x✝).hom ≫
        (fun {a b c} X Y Z f => 𝟙 X ⊗ f) x✝³ ((x✝² ≫ x✝¹) ≫ x✝) (x✝² ≫ x✝¹ ≫ x✝)
          ((fun {a b c d} X Y Z => α_ X Y Z) x✝² x✝¹ x✝).hom =
    ((fun {a b c d} X Y Z => α_ X Y Z) (x✝³ ≫ x✝²) x✝¹ x✝).hom ≫
      ((fun {a b c d} X Y Z => α_ X Y Z) x✝³ x✝² (x✝¹ ≫ x✝)).hom
[PROOFSTEP]
simp_rw [pentagon]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.14692, u_1} C
inst✝ : MonoidalCategory C
X✝ Y✝ X'✝ Y'✝ : EndMonoidal (MonoidalSingleObj.star C)
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
⊢ ((Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).map f ⊗
        (Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).map g) ≫
      (fun X Y =>
          𝟙
            ((Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).obj X ⊗
              (Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).obj Y))
        Y✝ Y'✝ =
    (fun X Y =>
          𝟙
            ((Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).obj X ⊗
              (Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).obj Y))
        X✝ X'✝ ≫
      (Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).map (f ⊗ g)
[PROOFSTEP]
simp_rw [Category.id_comp, Category.comp_id]
  -- Should we provide further simp lemmas so this goal becomes visible?
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.14692, u_1} C
inst✝ : MonoidalCategory C
X✝ Y✝ X'✝ Y'✝ : EndMonoidal (MonoidalSingleObj.star C)
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
⊢ f ⊗ g = f ⊗ g
[PROOFSTEP]
exact (tensor_id_comp_id_tensor _ _).symm


[GOAL]
C : Type u_1
inst✝ : Category.{?u.598, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
hip : HasLiftingProperty i p
⊢ CommSq.HasLift sq
[PROOFSTEP]
apply hip.sq_hasLift
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
h : HasLiftingProperty i p
f : Opposite.op Y ⟶ Opposite.op B
g : Opposite.op X ⟶ Opposite.op A
sq : CommSq f p.op i.op g
⊢ CommSq.HasLift sq
[PROOFSTEP]
simp only [CommSq.HasLift.iff_unop, Quiver.Hom.unop_op]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
h : HasLiftingProperty i p
f : Opposite.op Y ⟶ Opposite.op B
g : Opposite.op X ⟶ Opposite.op A
sq : CommSq f p.op i.op g
⊢ CommSq.HasLift (_ : CommSq g.unop i p f.unop)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Y.unop ⟶ B.unop
g : X.unop ⟶ A.unop
sq : CommSq f p.unop i.unop g
⊢ CommSq.HasLift sq
[PROOFSTEP]
rw [CommSq.HasLift.iff_op]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Y.unop ⟶ B.unop
g : X.unop ⟶ A.unop
sq : CommSq f p.unop i.unop g
⊢ CommSq.HasLift (_ : CommSq g.op i.unop.op p.unop.op f.op)
[PROOFSTEP]
simp only [Quiver.Hom.op_unop]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Y.unop ⟶ B.unop
g : X.unop ⟶ A.unop
sq : CommSq f p.unop i.unop g
⊢ CommSq.HasLift (_ : CommSq g.op i p f.op)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.3772, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝ : IsIso i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ i ≫ inv i ≫ f = f
[PROOFSTEP]
simp only [IsIso.hom_inv_id_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.3772, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝ : IsIso i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ (inv i ≫ f) ≫ p = g
[PROOFSTEP]
simp only [sq.w, assoc, IsIso.inv_hom_id_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4638, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝ : IsIso p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ i ≫ g ≫ inv p = f
[PROOFSTEP]
simp only [← sq.w_assoc, IsIso.hom_inv_id, comp_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4638, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝ : IsIso p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ (g ≫ inv p) ≫ p = g
[PROOFSTEP]
simp only [assoc, IsIso.inv_hom_id, comp_id]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.5681, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
⊢ CommSq.HasLift sq
[PROOFSTEP]
have fac := sq.w
[GOAL]
C : Type u_1
inst✝² : Category.{?u.5681, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = (i ≫ i') ≫ g
⊢ CommSq.HasLift sq
[PROOFSTEP]
rw [assoc] at fac
[GOAL]
C : Type u_1
inst✝² : Category.{?u.5681, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = i ≫ i' ≫ g
⊢ CommSq.HasLift sq
[PROOFSTEP]
exact
  CommSq.HasLift.mk'
    { l := (CommSq.mk (CommSq.mk fac).fac_right).lift
      fac_left := by simp only [assoc, CommSq.fac_left]
      fac_right := by simp only [CommSq.fac_right] }
[GOAL]
C : Type u_1
inst✝² : Category.{?u.5681, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = i ≫ i' ≫ g
⊢ (i ≫ i') ≫ CommSq.lift (_ : CommSq (CommSq.lift (_ : CommSq f i p (i' ≫ g))) i' p g) = f
[PROOFSTEP]
simp only [assoc, CommSq.fac_left]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.5681, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = i ≫ i' ≫ g
⊢ CommSq.lift (_ : CommSq (CommSq.lift (_ : CommSq f i p (i' ≫ g))) i' p g) ≫ p = g
[PROOFSTEP]
simp only [CommSq.fac_right]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.7264, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i p'
f : A ⟶ X
g : B ⟶ Y'
sq : CommSq f i (p ≫ p') g
⊢ CommSq.HasLift sq
[PROOFSTEP]
have fac := sq.w
[GOAL]
C : Type u_1
inst✝² : Category.{?u.7264, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i p'
f : A ⟶ X
g : B ⟶ Y'
sq : CommSq f i (p ≫ p') g
fac : f ≫ p ≫ p' = i ≫ g
⊢ CommSq.HasLift sq
[PROOFSTEP]
rw [← assoc] at fac
[GOAL]
C : Type u_1
inst✝² : Category.{?u.7264, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i p'
f : A ⟶ X
g : B ⟶ Y'
sq : CommSq f i (p ≫ p') g
fac : (f ≫ p) ≫ p' = i ≫ g
⊢ CommSq.HasLift sq
[PROOFSTEP]
let _ := (CommSq.mk (CommSq.mk fac).fac_left.symm).lift
[GOAL]
C : Type u_1
inst✝² : Category.{?u.7264, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i p'
f : A ⟶ X
g : B ⟶ Y'
sq : CommSq f i (p ≫ p') g
fac : (f ≫ p) ≫ p' = i ≫ g
x✝ : B ⟶ X := CommSq.lift (_ : CommSq f i p (CommSq.lift (_ : CommSq (f ≫ p) i p' g)))
⊢ CommSq.HasLift sq
[PROOFSTEP]
exact
  CommSq.HasLift.mk'
    { l := (CommSq.mk (CommSq.mk fac).fac_left.symm).lift
      fac_left := by simp only [CommSq.fac_left]
      fac_right := by simp only [CommSq.fac_right_assoc, CommSq.fac_right] }
[GOAL]
C : Type u_1
inst✝² : Category.{?u.7264, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i p'
f : A ⟶ X
g : B ⟶ Y'
sq : CommSq f i (p ≫ p') g
fac : (f ≫ p) ≫ p' = i ≫ g
x✝ : B ⟶ X := CommSq.lift (_ : CommSq f i p (CommSq.lift (_ : CommSq (f ≫ p) i p' g)))
⊢ i ≫ CommSq.lift (_ : CommSq f i p (CommSq.lift (_ : CommSq (f ≫ p) i p' g))) = f
[PROOFSTEP]
simp only [CommSq.fac_left]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.7264, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i p'
f : A ⟶ X
g : B ⟶ Y'
sq : CommSq f i (p ≫ p') g
fac : (f ≫ p) ≫ p' = i ≫ g
x✝ : B ⟶ X := CommSq.lift (_ : CommSq f i p (CommSq.lift (_ : CommSq (f ≫ p) i p' g)))
⊢ CommSq.lift (_ : CommSq f i p (CommSq.lift (_ : CommSq (f ≫ p) i p' g))) ≫ p ≫ p' = g
[PROOFSTEP]
simp only [CommSq.fac_right_assoc, CommSq.fac_right]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B'✝ X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i'✝ : B✝ ⟶ B'✝
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i' p
[PROOFSTEP]
rw [Arrow.iso_w' e]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B'✝ X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i'✝ : B✝ ⟶ B'✝
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
hip : HasLiftingProperty i p
⊢ HasLiftingProperty (e.inv.left ≫ i ≫ e.hom.right) p
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y'✝ : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p'✝ : Y✝ ⟶ Y'✝
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i p'
[PROOFSTEP]
rw [Arrow.iso_w' e]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y'✝ : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p'✝ : Y✝ ⟶ Y'✝
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i (e.inv.left ≫ p ≫ e.hom.right)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B'✝ X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i'✝ : B✝ ⟶ B'✝
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
⊢ HasLiftingProperty i p ↔ HasLiftingProperty i' p
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B'✝ X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i'✝ : B✝ ⟶ B'✝
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
⊢ HasLiftingProperty i p → HasLiftingProperty i' p
[PROOFSTEP]
intro
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B'✝ X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i'✝ : B✝ ⟶ B'✝
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
⊢ HasLiftingProperty i' p → HasLiftingProperty i p
[PROOFSTEP]
intro
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B'✝ X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i'✝ : B✝ ⟶ B'✝
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
a✝ : HasLiftingProperty i p
⊢ HasLiftingProperty i' p
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B'✝ X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i'✝ : B✝ ⟶ B'✝
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
a✝ : HasLiftingProperty i' p
⊢ HasLiftingProperty i p
[PROOFSTEP]
exacts [of_arrow_iso_left e p, of_arrow_iso_left e.symm p]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y'✝ : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p'✝ : Y✝ ⟶ Y'✝
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
⊢ HasLiftingProperty i p ↔ HasLiftingProperty i p'
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y'✝ : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p'✝ : Y✝ ⟶ Y'✝
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
⊢ HasLiftingProperty i p → HasLiftingProperty i p'
[PROOFSTEP]
intro
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y'✝ : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p'✝ : Y✝ ⟶ Y'✝
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
⊢ HasLiftingProperty i p' → HasLiftingProperty i p
[PROOFSTEP]
intro
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y'✝ : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p'✝ : Y✝ ⟶ Y'✝
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
a✝ : HasLiftingProperty i p
⊢ HasLiftingProperty i p'
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y'✝ : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p'✝ : Y✝ ⟶ Y'✝
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
a✝ : HasLiftingProperty i p'
⊢ HasLiftingProperty i p
[PROOFSTEP]
exacts [of_arrow_iso_right i e, of_arrow_iso_right i e.symm]


[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g = h
⊢ f ◁ eqToHom η = eqToHom (_ : f ≫ g = f ≫ h)
[PROOFSTEP]
cases η
[GOAL]
case refl
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ eqToHom (_ : g = g) = eqToHom (_ : f ≫ g = f ≫ g)
[PROOFSTEP]
simp only [whiskerLeft_id, eqToHom_refl]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
η : f = g
h : b ⟶ c
⊢ eqToHom η ▷ h = eqToHom (_ : f ≫ h = g ≫ h)
[PROOFSTEP]
cases η
[GOAL]
case refl
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
h : b ⟶ c
⊢ eqToHom (_ : f = f) ▷ h = eqToHom (_ : f ≫ h = f ≫ h)
[PROOFSTEP]
simp only [id_whiskerRight, eqToHom_refl]