no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
⊢ F.obj X = G.obj X
rw [hX]
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
⊢ G.obj Y = F.obj Y
rw [hY]
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom (_ : F.obj X = G.obj X) ≫ G.map e.hom ≫ eqToHom (_ : G.obj Y = F.obj Y)
⊢ F.obj Y = G.obj Y
rw [hY]
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom (_ : F.obj X = G.obj X) ≫ G.map e.hom ≫ eqToHom (_ : G.obj Y = F.obj Y)
⊢ G.obj X = F.obj X
rw [hX]
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom (_ : F.obj X = G.obj X) ≫ G.map e.hom ≫ eqToHom (_ : G.obj Y = F.obj Y)
⊢ F.map e.inv = eqToHom (_ : F.obj Y = G.obj Y) ≫ G.map e.inv ≫ eqToHom (_ : G.obj X = F.obj X)
simp only [← IsIso.Iso.inv_hom e, Functor.map_inv, h₂, IsIso.inv_comp, inv_eqToHom,
  Category.assoc]