awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X_1 Y_1 : C
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
inst_3 : F.Full
inst_4 : F.Faithful
f : F.obj X ≅ F.obj Y
⊢ F.map (F.preimage f.inv ≫ F.preimage f.hom) = F.map (𝟙 Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_2 : F.Full
inst_3 : F.Faithful
f : X ≅ Y
w : (F.preimageIso (F.mapIso f)).hom = f.hom
⊢ F.preimageIso (F.mapIso f) = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_2 : F.Full
inst_3 : F.Faithful
f : X ≅ Y
⊢ (F.preimageIso (F.mapIso f)).hom = f.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X_1 Y_1 : C
F : Functor.{v₁, v₂, u₁, u₂} C D
X_2 Y_2 Z : C
hF : F.FullyFaithful
X Y : C
x : X ⟶ Y
⊢ hF.preimage (F.map x) = x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X_1 Y_1 : C
F : Functor.{v₁, v₂, u₁, u₂} C D
X_2 Y_2 Z : C
hF : F.FullyFaithful
X Y : C
x : F.obj X ⟶ F.obj Y
⊢ F.map (hF.preimage x) = x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X Y : C
f g : X ⟶ Y
h : F.map f = F.map g
⊢ f = g

Tactic:
hF.homEquiv.injective h

Premises used: CategoryTheory.Functor.FullyFaithful.homEquiv, Equiv.injective
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X Y : C
⊢ Function.Surjective (α := X ⟶ Y) F.map

Tactic:
hF.homEquiv.surjective

Premises used: CategoryTheory.Functor.FullyFaithful.homEquiv, Equiv.surjective
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X Y : C
⊢ Function.Bijective (α := X ⟶ Y) F.map

Tactic:
hF.homEquiv.bijective

Premises used: Equiv.bijective, CategoryTheory.Functor.FullyFaithful.homEquiv
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X : C
⊢ F.map (hF.preimage (𝟙 (F.obj X))) = F.map (𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X Y Z : C
f : F.obj X ⟶ F.obj Y
g : F.obj Y ⟶ F.obj Z
⊢ F.map (hF.preimage (f ≫ g)) = F.map (hF.preimage f ≫ hF.preimage g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X_1 Y_1 : C
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
hF h₁ h₂ : F.FullyFaithful
⊢ F.Faithful

Tactic:
have := h₁.faithful
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X_1 Y_1 : C
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map_1 : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
mk : @f₁ = @f₂
⊢ { preimage := @f₁, map_preimage := @hf₁, preimage_map := @preimage_map : F.FullyFaithful } =
    { preimage := @f₂, map_preimage := @hf₂, preimage_map := @preimage_map_1 }

Tactic:
simp only [Functor.FullyFaithful.mk.injEq]

Premises used: CategoryTheory.Functor.FullyFaithful.mk.injEq
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X_1 Y_1 : C
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map_1 : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
mk : ∀ (x x_1 : C) (x_2 : F.obj x ⟶ F.obj x_1), f₁ x_2 = f₂ x_2
⊢ @f₁ = @f₂

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X_1 Y_1 : C
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map_1 : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
x x_1 : C
x_2 : F.obj x ⟶ F.obj x_1
mk : F.map (f₁ x_2) = F.map (f₂ x_2)
⊢ f₁ x_2 = f₂ x_2

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X_1 Y_1 : C
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map_1 : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
x x_1 : C
x_2 : F.obj x ⟶ F.obj x_1
mk : x_2 = F.map (f₂ x_2)
mk₁ mk₂ : x_2 = x_2
⊢ F.map (f₁ x_2) = F.map (f₂ x_2)

Tactic:
rw [hf₁, hf₂]
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X_1 Y_1 : C
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
hF h₂ : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
mk :
  ∀ (f₂ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y) (hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f)
    (preimage_map_1 : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f),
    { preimage := @f₁, map_preimage := @hf₁, preimage_map := @preimage_map : F.FullyFaithful } =
      { preimage := @f₂, map_preimage := @hf₂, preimage_map := @preimage_map_1 }
⊢ { preimage := @f₁, map_preimage := @hf₁, preimage_map := @preimage_map : F.FullyFaithful } = h₂

Tactic:
cases h₂ with | mk f₂ hf₂ _ =>
    simp only [Functor.FullyFaithful.mk.injEq]
    ext
    apply F.map_injective
    rw [hf₁, hf₂]

Premises used: CategoryTheory.Functor.FullyFaithful.mk.injEq, CategoryTheory.Functor.map_injective, CategoryTheory.Functor.FullyFaithful.mk
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X_1 Y_1 : C
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
hF h₁ h₂ : F.FullyFaithful
this : F.Faithful
mk :
  ∀ (f₁ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y) (hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f)
    (preimage_map : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f),
    { preimage := @f₁, map_preimage := @hf₁, preimage_map := @preimage_map : F.FullyFaithful } = h₂
⊢ h₁ = h₂

Tactic:
cases h₁ with | mk f₁ hf₁ _ => cases h₂ with | mk f₂ hf₂ _ =>
    simp only [Functor.FullyFaithful.mk.injEq]
    ext
    apply F.map_injective
    rw [hf₁, hf₂]

Premises used: CategoryTheory.Functor.FullyFaithful.mk.injEq, CategoryTheory.Functor.map_injective, CategoryTheory.Functor.FullyFaithful.mk
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X_1 Y_1 : C
F : Functor.{v₁, v₂, u₁, u₂} C D
X_2 Y_2 Z : C
hF : F.FullyFaithful
X Y : C
e : F.obj X ≅ F.obj Y
⊢ F.map (hF.preimage e.hom ≫ hF.preimage e.inv) = F.map (𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X_1 Y_1 : C
F : Functor.{v₁, v₂, u₁, u₂} C D
X_2 Y_2 Z : C
hF : F.FullyFaithful
X Y : C
e : F.obj X ≅ F.obj Y
⊢ F.map (hF.preimage e.inv ≫ hF.preimage e.hom) = F.map (𝟙 Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X Y : C
f : X ⟶ Y
inst_2 : IsIso (F.map f)
⊢ IsIso f

Tactic:
simpa using (hF.preimageIso (asIso (F.map f))).isIso_hom

Premises used: CategoryTheory.Functor.map, CategoryTheory.Iso.isIso_hom, CategoryTheory.Functor.FullyFaithful.preimageIso, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X_1 Y_1 : C
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
hF : F.FullyFaithful
G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
X_2 Y_2 : C
f : G.obj X_2 ⟶ G.obj Y_2
⊢ G.map (hF.preimage (e.hom.app X_2 ≫ f ≫ e.inv.app Y_2)) = f

Tactic:
simp [← NatIso.naturality_1 e]

Premises used: CategoryTheory.NatIso.naturality_1
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : ∀ (X Y : C), Function.Bijective (α := X ⟶ Y) F.map
⊢ F.Faithful

Tactic:
have : F.Faithful := ⟨fun h ↦ (hF _ _).injective h⟩
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : ∀ (X Y : C), Function.Bijective (α := X ⟶ Y) F.map
this : F.Faithful
⊢ F.Full

Tactic:
have : F.Full := ⟨(hF _ _).surjective⟩
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : ∀ (X Y : C), Function.Bijective (α := X ⟶ Y) F.map
this_1 : F.Faithful
this : F.Full
⊢ Nonempty F.FullyFaithful

Tactic:
⟨.ofFullyFaithful _⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : ∀ (X Y : C), Function.Bijective (α := X ⟶ Y) F.map
this_1 : F.Faithful
this : F.Full
⊢ Nonempty F.FullyFaithful

Tactic:
exact ⟨.ofFullyFaithful _⟩
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : F.Faithful
X Y : C
f : X ⟶ Y
inst_4 : IsIso (F.map f)
⊢ F.map (f ≫ F.preimage (inv (F.map f))) = F.map (𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : F.Faithful
X Y : C
f : X ⟶ Y
inst_4 : IsIso (F.map f)
⊢ F.map (F.preimage (inv (F.map f)) ≫ f) = F.map (𝟙 Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ Faithful.{v₁, v₁, u₁, u₁} (𝟭 C)

Tactic:

Premises used: CategoryTheory.Functor.Faithful.mk
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : (F ⋙ G).Faithful
⊢ F.Faithful

Tactic:
{ map_injective := fun {_ _} => Function.Injective.of_comp (F ⋙ G).map_injective }

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.Faithful.mk, CategoryTheory.Functor.map_injective, Function.Injective.of_comp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F F' : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
α : F ≅ F'
X Y : C
f : F'.obj X ⟶ F'.obj Y
⊢ F'.map (F.preimage ((α.app X).hom ≫ f ≫ (α.app Y).inv)) = f

Tactic:
simp [← NatIso.naturality_1 α]

Premises used: CategoryTheory.NatIso.naturality_1
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F F' : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Faithful
α : F ≅ F'
X Y : C
a₁ a₂ : X ⟶ Y
h : F'.map a₁ = F'.map a₂
rw : α.symm.inv.app X ≫ F'.map a₁ ≫ α.symm.hom.app Y = F.map a₂
rw₁ : α.symm.inv.app X ≫ F'.map a₂ ≫ α.symm.hom.app Y = F.map a₂
rw₂ rw₃ : F.map a₂ = F.map a₂
⊢ F.map a₁ = F.map a₂

Tactic:
rw [← NatIso.naturality_1 α.symm, h, NatIso.naturality_1 α.symm]

Premises used: CategoryTheory.NatIso.naturality_1, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
H : Functor.{v₁, v₃, u₁, u₃} C E
inst_3 : H.Faithful
h : F ⋙ G ≅ H
⊢ F.Faithful

Tactic:
@Faithful.of_comp _ _ _ _ _ _ F G (Faithful.of_iso h.symm)

Premises used: CategoryTheory.Functor.Faithful.of_comp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
H : Functor.{v₁, v₃, u₁, u₃} C E
ℋ : H.Faithful
h : F ⋙ G = H
⊢ F.Faithful

Tactic:
@Faithful.of_comp _ _ _ _ _ _ F G (h.symm ▸ ℋ)

Premises used: CategoryTheory.Functor.Faithful.of_comp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F_1 F' : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
X : C
a : G.map (map (𝟙 X)) = G.map (𝟙 (obj X))
⊢ map (𝟙 X) = 𝟙 (obj X)

Tactic:
apply G.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F_1 F' : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
X : C
⊢ G.map (map (𝟙 X)) = G.map (𝟙 (obj X))

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F_1 F' : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₃, u₁, u₃} C E
inst_3 : F.Faithful
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
obtain :
  ∀ (F_obj : C → E) (map_1 : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)) (map_id : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (F_obj X))
    (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g)
    [{ obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.Faithful]
    (h_obj :
      ∀ (X : C),
        G.obj (obj X) =
          { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.obj X)
    (h_map :
      ∀ {X Y : C} {f : X ⟶ Y},
        G.map (map f) ≍
          { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.map
            f),
    Faithful.div { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }
          G obj h_obj @map @h_map ⋙
        G =
      { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp }
⊢ Faithful.div F G obj h_obj @map @h_map ⋙ G = F

Tactic:
obtain ⟨F_obj, _, _, _⟩ := F
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : G.Faithful
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_obj : C → E
map_1 : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (F_obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
inst_4 :
  { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.Faithful
h_obj :
  ∀ (X : C),
    G.obj (obj X) =
      { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    G.map (map f) ≍
      { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.map f
obtain :
  ∀ (G_obj : D → E) (map_2 : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y))
    (map_id_1 : ∀ (X : D), map_2 (𝟙 X) = 𝟙 (G_obj X))
    (map_comp_1 : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), map_2 (f ≫ g) = map_2 f ≫ map_2 g)
    [inst_5 :
      { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 :
          Functor.{v₂, v₃, u₂, u₃} D E }.Faithful]
    (h_obj :
      ∀ (X : C),
        { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.obj
            (obj X) =
          { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.obj X)
    (h_map :
      ∀ {X Y : C} {f : X ⟶ Y},
        { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.map
            (map f) ≍
          { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.map
            f),
    Faithful.div { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }
          { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }
          obj h_obj @map @h_map ⋙
        { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E } =
      { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp }
⊢ Faithful.div { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E } G
        obj h_obj @map @h_map ⋙
      G =
    { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp }

Tactic:
obtain ⟨G_obj, _, _, _⟩ := G
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_obj : C → E
map_1 : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (F_obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
inst_3 :
  { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.Faithful
G_obj : D → E
map_2 : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id_1 : ∀ (X : D), map_2 (𝟙 X) = 𝟙 (G_obj X)
map_comp_1 : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), map_2 (f ≫ g) = map_2 f ≫ map_2 g
inst_4 :
  { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.Faithful
h_obj :
  ∀ (X : C),
    { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.obj
        (obj X) =
      { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.map
        (map f) ≍
      { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.map f
unfold :
  {
      obj := fun (X : C) ↦
        { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.obj
          ({ obj := obj, map := @map, map_id := ⋯, map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D }.obj X),
      map := fun {X Y : C} (f : X ⟶ Y) ↦
        { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 }.map
          ({ obj := obj, map := @map, map_id := ⋯, map_comp := ⋯ }.map f),
      map_id := ⋯, map_comp := ⋯ } =
    { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }
⊢ Faithful.div { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }
        { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E } obj
        h_obj @map @h_map ⋙
      { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E } =
    { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp }

Tactic:
unfold Faithful.div Functor.comp

Premises used: CategoryTheory.Functor.Faithful.div, CategoryTheory.Functor.comp