C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_3
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X Y : C
f : X ⟶ Y
⊢ (MorphismProperty.Q W ⋙ lift G hG).map f =
    eqToHom (_ : (MorphismProperty.Q W ⋙ lift G hG).obj X = (MorphismProperty.Q W ⋙ lift G hG).obj X) ≫
      G.map f ≫ eqToHom (_ : G.obj Y = (MorphismProperty.Q W ⋙ lift G hG).obj Y)
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_3
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
⊢ ∀ (X Y : C) (f : X ⟶ Y),
    (MorphismProperty.Q W ⋙ lift G hG).map f =
      eqToHom (_ : (MorphismProperty.Q W ⋙ lift G hG).obj X = (MorphismProperty.Q W ⋙ lift G hG).obj X) ≫
        G.map f ≫ eqToHom (_ : G.obj Y = (MorphismProperty.Q W ⋙ lift G hG).obj Y)
intro X Y f
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_3
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X Y : C
f : X ⟶ Y
⊢ (lift G hG).map ((MorphismProperty.Q W).map f) = G.map f
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_3
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X Y : C
f : X ⟶ Y
⊢ (MorphismProperty.Q W ⋙ lift G hG).map f =
    eqToHom (_ : (MorphismProperty.Q W ⋙ lift G hG).obj X = (MorphismProperty.Q W ⋙ lift G hG).obj X) ≫
      G.map f ≫ eqToHom (_ : G.obj Y = (MorphismProperty.Q W ⋙ lift G hG).obj Y)
simp only [Functor.comp_map, eqToHom_refl, comp_id, id_comp]
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_3
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X Y : C
f : X ⟶ Y
⊢ composePath (Quiver.Hom.toPath (G.map f)) = G.map f
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_3
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X Y : C
f : X ⟶ Y
⊢ (lift G hG).map ((MorphismProperty.Q W).map f) = G.map f
dsimp [MorphismProperty.Q, Quot.liftOn]
no goals
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_3
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X Y : C
f : X ⟶ Y
⊢ composePath (Quiver.Hom.toPath (G.map f)) = G.map f
rw [composePath_toPath]