[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
