C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H : g ≫ G.map f = h ≫ G.map f
⊢ g = h
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
⊢ ∀ {Z : C} (g h : Z ⟶ G.obj X), g ≫ G.map f = h ≫ G.map f → g = h
intro Z g h H
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H : ↑(Adjunction.homEquiv adj Z Y).symm (g ≫ G.map f) = ↑(Adjunction.homEquiv adj Z Y).symm (h ≫ G.map f)
⊢ g = h
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H : g ≫ G.map f = h ≫ G.map f
⊢ g = h
replace H := congr_arg (adj.homEquiv Z Y).symm H
no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H : ↑(Adjunction.homEquiv adj Z Y).symm (g ≫ G.map f) = ↑(Adjunction.homEquiv adj Z Y).symm (h ≫ G.map f)
⊢ g = h
rwa [adj.homEquiv_naturality_right_symm, adj.homEquiv_naturality_right_symm, cancel_mono,
  Equiv.apply_eq_iff_eq] at H