-- Mathlib/CategoryTheory/Category/ReflQuiv.lean
theorem forget_faithful {C D : Cat.{v, u}} (F G : C ⥤ D)
    (hyp : forget.map F = forget.map G) : F = G

Proof state:
case mk.mk.refl
C D : Cat
toPrefunctor✝ : ↑C ⥤q ↑D
map_id✝¹ : ∀ (X : ↑C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝¹ :
  ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
map_id✝ : ∀ (X : ↑C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
rfl

Result:
no goals

Proof state:
case mk
C D : Cat
G : ↑C ⥤ ↑D
toPrefunctor✝ : ↑C ⥤q ↑D
map_id✝ : ∀ (X : ↑C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
hyp : forget.map { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ } = forget.map G
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ } = G

Tactic:
cases G

Result:
case mk.mk
C D : Cat
toPrefunctor✝¹ : ↑C ⥤q ↑D
map_id✝¹ : ∀ (X : ↑C), toPrefunctor✝¹.map (𝟙 X) = 𝟙 (toPrefunctor✝¹.obj X)
map_comp✝¹ :
  ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝¹.map (f ≫ g) = toPrefunctor✝¹.map f ≫ toPrefunctor✝¹.map g
toPrefunctor✝ : ↑C ⥤q ↑D
map_id✝ : ∀ (X : ↑C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
hyp :
  forget.map { toPrefunctor := toPrefunctor✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    forget.map { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }
⊢ { toPrefunctor := toPrefunctor✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }

Proof state:
C D : Cat
F G : ↑C ⥤ ↑D
hyp : forget.map F = forget.map G
⊢ F = G

Tactic:
cases F

Result:
case mk
C D : Cat
G : ↑C ⥤ ↑D
toPrefunctor✝ : ↑C ⥤q ↑D
map_id✝ : ∀ (X : ↑C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
hyp : forget.map { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ } = forget.map G
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ } = G

Proof state:
case mk.mk
C D : Cat
toPrefunctor✝¹ : ↑C ⥤q ↑D
map_id✝¹ : ∀ (X : ↑C), toPrefunctor✝¹.map (𝟙 X) = 𝟙 (toPrefunctor✝¹.obj X)
map_comp✝¹ :
  ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝¹.map (f ≫ g) = toPrefunctor✝¹.map f ≫ toPrefunctor✝¹.map g
toPrefunctor✝ : ↑C ⥤q ↑D
map_id✝ : ∀ (X : ↑C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
hyp :
  forget.map { toPrefunctor := toPrefunctor✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    forget.map { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }
⊢ { toPrefunctor := toPrefunctor✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
cases hyp

Result:
case mk.mk.refl
C D : Cat
toPrefunctor✝ : ↑C ⥤q ↑D
map_id✝¹ : ∀ (X : ↑C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝¹ :
  ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
map_id✝ : ∀ (X : ↑C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }