C : Type u_2
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X Y : C
f : X ⟶ Y
⊢ (lift r F H).map ((functor r).map f) =
    (lift.isLift r F H).inv.app X ≫ (functor r ⋙ lift r F H).map f ≫ (lift.isLift r F H).hom.app Y
C : Type u_2
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X Y : C
f : X ⟶ Y
⊢ (lift r F H).map ((functor r).map f) = F.map f
rw [← NatIso.naturality_1 (lift.isLift r F H)]
C : Type u_2
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X Y : C
f : X ⟶ Y
⊢ Quot.liftOn (Quot.mk (CompClosure r) f) (fun f => F.map f)
      (_ :
        ∀ (a b : ((functor r).obj X).as ⟶ ((functor r).obj Y).as),
          CompClosure r a b → (fun f => F.map f) a = (fun f => F.map f) b) =
    𝟙 (F.obj X) ≫
      Quot.liftOn (Quot.mk (CompClosure r) f) (fun f => F.map f)
          (_ :
            ∀ (a b : ((functor r).obj X).as ⟶ ((functor r).obj Y).as),
              CompClosure r a b → (fun f => F.map f) a = (fun f => F.map f) b) ≫
        𝟙 (F.obj Y)
C : Type u_2
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X Y : C
f : X ⟶ Y
⊢ (lift r F H).map ((functor r).map f) =
    (lift.isLift r F H).inv.app X ≫ (functor r ⋙ lift r F H).map f ≫ (lift.isLift r F H).hom.app Y
dsimp
no goals
C : Type u_2
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X Y : C
f : X ⟶ Y
⊢ Quot.liftOn (Quot.mk (CompClosure r) f) (fun f => F.map f)
      (_ :
        ∀ (a b : ((functor r).obj X).as ⟶ ((functor r).obj Y).as),
          CompClosure r a b → (fun f => F.map f) a = (fun f => F.map f) b) =
    𝟙 (F.obj X) ≫
      Quot.liftOn (Quot.mk (CompClosure r) f) (fun f => F.map f)
          (_ :
            ∀ (a b : ((functor r).obj X).as ⟶ ((functor r).obj Y).as),
              CompClosure r a b → (fun f => F.map f) a = (fun f => F.map f) b) ≫
        𝟙 (F.obj Y)
simp