awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Faithful
X Y : D
f g : obj.{v₂, v₂, u₂, u₂} (𝟭 D) X ⟶ Y
hfg : h.counit.app X ≫ f = h.counit.app X ≫ g
⊢ Eq.{v₂ + 1} (α := L.obj (R.obj X) ⟶ Y)
    (((Equiv.symm (h.homEquiv (R.obj X) Y) : Equiv.{v₁ + 1, v₂ + 1} (R.obj X ⟶ R.obj Y) (L.obj (R.obj X) ⟶ Y)) :
          (a : R.obj X ⟶ R.obj Y) → L.obj (R.obj X) ⟶ Y)
        (R.map f) :
      L.obj (R.obj X) ⟶ Y)
    (((Equiv.symm (h.homEquiv (R.obj X) Y) : Equiv.{v₁ + 1, v₂ + 1} (R.obj X ⟶ R.obj Y) (L.obj (R.obj X) ⟶ Y)) :
          (a : R.obj X ⟶ R.obj Y) → L.obj (R.obj X) ⟶ Y)
        (R.map g) :
      L.obj (R.obj X) ⟶ Y)

Tactic:
simpa using hfg
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
X : D
⊢ h.counit.app X ≫ R.preimage (h.unit.app (R.obj X)) = 𝟙 ((R ⋙ L).obj X)

Tactic:
simp [← h.counit_naturality (R.preimage (h.unit.app (R.obj X)))]

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.Adjunction.unit, CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
X : D
⊢ IsSplitMono (h.counit.app X)

Tactic:
⟨⟨h.counitSplitMonoOfRFull X⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Adjunction.counitSplitMonoOfRFull, CategoryTheory.IsSplitMono.mk
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
X : D
⊢ IsIso (h.counit.app X)

Tactic:
isIso_of_epi_of_isSplitMono _

Premises used: CategoryTheory.isIso_of_epi_of_isSplitMono
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
⊢ IsIso h.counit

Tactic:
NatIso.isIso_of_isIso_app _

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : C
inst_2 : IsIso (h.unit.app X)
⊢ inv (L.map (h.unit.app X)) = h.counit.app (L.obj X)

Tactic:
IsIso.inv_eq_of_hom_inv_id (h.left_triangle_components X)

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id, CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : D
inst_2 : IsIso (h.counit.app X)
⊢ inv (R.map (h.counit.app X)) = h.unit.app (R.obj X)

Tactic:
IsIso.inv_eq_of_inv_hom_id (h.right_triangle_components X)

Premises used: CategoryTheory.Adjunction.right_triangle_components, CategoryTheory.IsIso.inv_eq_of_inv_hom_id
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
a : f ≫ h.unit.app Y = g ≫ h.unit.app Y
⊢ f = g

Tactic:
apply Mono.right_cancellation (f := h.unit.app Y)

Premises used: CategoryTheory.Mono.right_cancellation
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
a :
  Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Y)
    (((Equiv.symm (h.homEquiv X (L.obj Y)) : Equiv.{v₁ + 1, v₂ + 1} (X ⟶ R.obj (L.obj Y)) (L.obj X ⟶ L.obj Y)) :
          (a : X ⟶ R.obj (L.obj Y)) → L.obj X ⟶ L.obj Y)
        (f ≫ h.unit.app Y) :
      L.obj X ⟶ L.obj Y)
    (((Equiv.symm (h.homEquiv X (L.obj Y)) : Equiv.{v₁ + 1, v₂ + 1} (X ⟶ R.obj (L.obj Y)) (L.obj X ⟶ L.obj Y)) :
          (a : X ⟶ R.obj (L.obj Y)) → L.obj X ⟶ L.obj Y)
        (g ≫ h.unit.app Y) :
      L.obj X ⟶ L.obj Y)
⊢ f ≫ h.unit.app Y = g ≫ h.unit.app Y

Tactic:
apply (h.homEquiv X (L.obj Y)).symm.injective

Premises used: CategoryTheory.Adjunction.homEquiv, Equiv.injective, Equiv.symm, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
⊢ Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Y)
    (((Equiv.symm (h.homEquiv X (L.obj Y)) : Equiv.{v₁ + 1, v₂ + 1} (X ⟶ R.obj (L.obj Y)) (L.obj X ⟶ L.obj Y)) :
          (a : X ⟶ R.obj (L.obj Y)) → L.obj X ⟶ L.obj Y)
        (f ≫ h.unit.app Y) :
      L.obj X ⟶ L.obj Y)
    (((Equiv.symm (h.homEquiv X (L.obj Y)) : Equiv.{v₁ + 1, v₂ + 1} (X ⟶ R.obj (L.obj Y)) (L.obj X ⟶ L.obj Y)) :
          (a : X ⟶ R.obj (L.obj Y)) → L.obj X ⟶ L.obj Y)
        (g ≫ h.unit.app Y) :
      L.obj X ⟶ L.obj Y)

Tactic:
simpa using hfg
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
h₁ :
  L.map
      (((h.homEquiv X (L.obj Y) : Equiv.{v₂ + 1, v₁ + 1} (L.obj X ⟶ L.obj Y) (X ⟶ R.obj (L.obj Y))) :
            (a : L.obj X ⟶ L.obj Y) → X ⟶ R.obj (L.obj Y))
          f ≫
        section_ (h.unit.app Y)) =
    f
⊢ ∃ (a : X ⟶ Y), L.map a = f

Tactic:
use ((h.homEquiv X (L.obj Y)) f ≫ section_ (h.unit.app Y))

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.CategoryStruct.comp, CategoryTheory.section_, CategoryTheory.Adjunction.homEquiv, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
this : L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y)
⊢ L.map
      (((h.homEquiv X (L.obj Y) : Equiv.{v₂ + 1, v₁ + 1} (L.obj X ⟶ L.obj Y) (X ⟶ R.obj (L.obj Y))) :
            (a : L.obj X ⟶ L.obj Y) → X ⟶ R.obj (L.obj Y))
          f ≫
        section_ (h.unit.app Y)) =
    f

Tactic:
simp [this]
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
h₁ : L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y)
⊢ L.map
      (((h.homEquiv X (L.obj Y) : Equiv.{v₂ + 1, v₁ + 1} (L.obj X ⟶ L.obj Y) (X ⟶ R.obj (L.obj Y))) :
            (a : L.obj X ⟶ L.obj Y) → X ⟶ R.obj (L.obj Y))
          f ≫
        section_ (h.unit.app Y)) =
    f

Tactic:
suffices L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y) by simp [this]
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
h₁ : L.map (section_ (h.unit.app Y)) ≫ 𝟙 (L.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y)) = h.counit.app (L.obj Y)
⊢ L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y)

Tactic:
rw [← comp_id (L.map (section_ (h.unit.app Y)))]

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map, CategoryTheory.section_, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ L.map (section_ (h.unit.app Y)) ≫ 𝟙 (L.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y)) = h.counit.app (L.obj Y)

Tactic:
simp only [Functor.comp_obj, Functor.id_obj, ← h.left_triangle_components Y,
      ← assoc, ← Functor.map_comp, IsSplitEpi.id, Functor.map_id, id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.IsSplitEpi.id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.left_triangle_components, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : D), Epi (h.counit.app X)
X Y : D
f g : X ⟶ Y
hfg : R.map f = R.map g
a : h.counit.app X ≫ f = h.counit.app X ≫ g
⊢ f = g

Tactic:
apply Epi.left_cancellation (f := h.counit.app X)

Premises used: CategoryTheory.Epi.left_cancellation
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : D), Epi (h.counit.app X)
X Y : D
f g : X ⟶ Y
hfg : R.map f = R.map g
a :
  Eq.{v₁ + 1} (α := R.obj X ⟶ R.obj Y)
    (((h.homEquiv (R.obj X) Y : Equiv.{v₂ + 1, v₁ + 1} (L.obj (R.obj X) ⟶ Y) (R.obj X ⟶ R.obj Y)) :
          (a : L.obj (R.obj X) ⟶ Y) → R.obj X ⟶ R.obj Y)
        (h.counit.app X ≫ f) :
      R.obj X ⟶ R.obj Y)
    (((h.homEquiv (R.obj X) Y : Equiv.{v₂ + 1, v₁ + 1} (L.obj (R.obj X) ⟶ Y) (R.obj X ⟶ R.obj Y)) :
          (a : L.obj (R.obj X) ⟶ Y) → R.obj X ⟶ R.obj Y)
        (h.counit.app X ≫ g) :
      R.obj X ⟶ R.obj Y)
⊢ h.counit.app X ≫ f = h.counit.app X ≫ g

Tactic:
apply (h.homEquiv (R.obj X) Y).injective

Premises used: CategoryTheory.Adjunction.homEquiv, Equiv.injective, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : D), Epi (h.counit.app X)
X Y : D
f g : X ⟶ Y
hfg : R.map f = R.map g
⊢ Eq.{v₁ + 1} (α := R.obj X ⟶ R.obj Y)
    (((h.homEquiv (R.obj X) Y : Equiv.{v₂ + 1, v₁ + 1} (L.obj (R.obj X) ⟶ Y) (R.obj X ⟶ R.obj Y)) :
          (a : L.obj (R.obj X) ⟶ Y) → R.obj X ⟶ R.obj Y)
        (h.counit.app X ≫ f) :
      R.obj X ⟶ R.obj Y)
    (((h.homEquiv (R.obj X) Y : Equiv.{v₂ + 1, v₁ + 1} (L.obj (R.obj X) ⟶ Y) (R.obj X ⟶ R.obj Y)) :
          (a : L.obj (R.obj X) ⟶ Y) → R.obj X ⟶ R.obj Y)
        (h.counit.app X ≫ g) :
      R.obj X ⟶ R.obj Y)

Tactic:
simpa using hfg
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
h₁ :
  R.map
      (retraction (h.counit.app X) ≫
        ((Equiv.symm (h.homEquiv (R.obj X) Y) : Equiv.{v₁ + 1, v₂ + 1} (R.obj X ⟶ R.obj Y) (L.obj (R.obj X) ⟶ Y)) :
            (a : R.obj X ⟶ R.obj Y) → L.obj (R.obj X) ⟶ Y)
          f) =
    f
⊢ ∃ (a : X ⟶ Y), R.map a = f

Tactic:
use (retraction (h.counit.app X) ≫ (h.homEquiv (R.obj X) Y).symm f)

Premises used: CategoryTheory.retraction, CategoryTheory.Adjunction.counit, CategoryTheory.CategoryStruct.comp, CategoryTheory.Adjunction.homEquiv, Equiv.symm, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
this : R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)
⊢ R.map
      (retraction (h.counit.app X) ≫
        ((Equiv.symm (h.homEquiv (R.obj X) Y) : Equiv.{v₁ + 1, v₂ + 1} (R.obj X ⟶ R.obj Y) (L.obj (R.obj X) ⟶ Y)) :
            (a : R.obj X ⟶ R.obj Y) → L.obj (R.obj X) ⟶ Y)
          f) =
    f

Tactic:
simp [this]
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
h₁ : R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)
⊢ R.map
      (retraction (h.counit.app X) ≫
        ((Equiv.symm (h.homEquiv (R.obj X) Y) : Equiv.{v₁ + 1, v₂ + 1} (R.obj X ⟶ R.obj Y) (L.obj (R.obj X) ⟶ Y)) :
            (a : R.obj X ⟶ R.obj Y) → L.obj (R.obj X) ⟶ Y)
          f) =
    f

Tactic:
suffices R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X) by simp [this]
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
h₁ : 𝟙 (R.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)) ≫ R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)
⊢ R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)

Tactic:
rw [← id_comp (R.map (retraction (h.counit.app X)))]

Premises used: CategoryTheory.retraction, CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.NatTrans.app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
⊢ 𝟙 (R.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)) ≫ R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, ← h.right_triangle_components X,
      assoc, ← Functor.map_comp, IsSplitMono.id, Functor.map_id, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.IsSplitMono.id, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.right_triangle_components
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
⊢ whiskerRight h.unit L ≫ L.whiskerLeft h.counit = 𝟙 (𝟭 C ⋙ L)

Tactic:
have := h.left_triangle
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
this : whiskerRight h.unit L ≫ L.whiskerLeft h.counit = 𝟙 (𝟭 C ⋙ L)
⊢ L.whiskerLeft h.counit = inv (whiskerRight h.unit L) ≫ 𝟙 (𝟭 C ⋙ L)

Tactic:
rw [← IsIso.eq_inv_comp] at this

Premises used: CategoryTheory.IsIso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
this : L.whiskerLeft h.counit = inv (whiskerRight h.unit L) ≫ 𝟙 (𝟭 C ⋙ L)
rw : IsIso (inv (whiskerRight h.unit L) ≫ 𝟙 (𝟭 C ⋙ L))
⊢ IsIso (L.whiskerLeft h.counit)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
this : L.whiskerLeft h.counit = inv (whiskerRight h.unit L) ≫ 𝟙 (𝟭 C ⋙ L)
⊢ IsIso (inv (whiskerRight h.unit L) ≫ 𝟙 (𝟭 C ⋙ L))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
⊢ R.whiskerLeft h.unit ≫ whiskerRight h.counit R = 𝟙 (R ⋙ 𝟭 C)

Tactic:
have := h.right_triangle
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
this : R.whiskerLeft h.unit ≫ whiskerRight h.counit R = 𝟙 (R ⋙ 𝟭 C)
⊢ whiskerRight h.counit R = inv (R.whiskerLeft h.unit) ≫ 𝟙 (R ⋙ 𝟭 C)

Tactic:
rw [← IsIso.eq_inv_comp] at this

Premises used: CategoryTheory.IsIso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
this : whiskerRight h.counit R = inv (R.whiskerLeft h.unit) ≫ 𝟙 (R ⋙ 𝟭 C)
rw : IsIso (inv (R.whiskerLeft h.unit) ≫ 𝟙 (R ⋙ 𝟭 C))
⊢ IsIso (whiskerRight h.counit R)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
this : whiskerRight h.counit R = inv (R.whiskerLeft h.unit) ≫ 𝟙 (R ⋙ 𝟭 C)
⊢ IsIso (inv (R.whiskerLeft h.unit) ≫ 𝟙 (R ⋙ 𝟭 C))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
⊢ R.whiskerLeft h.unit ≫ whiskerRight h.counit R = 𝟙 (R ⋙ 𝟭 C)

Tactic:
have := h.right_triangle
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
this : R.whiskerLeft h.unit ≫ whiskerRight h.counit R = 𝟙 (R ⋙ 𝟭 C)
⊢ R.whiskerLeft h.unit = 𝟙 (R ⋙ 𝟭 C) ≫ inv (whiskerRight h.counit R)

Tactic:
rw [← IsIso.eq_comp_inv] at this

Premises used: CategoryTheory.IsIso.eq_comp_inv
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
this : R.whiskerLeft h.unit = 𝟙 (R ⋙ 𝟭 C) ≫ inv (whiskerRight h.counit R)
rw : IsIso (𝟙 (R ⋙ 𝟭 C) ≫ inv (whiskerRight h.counit R))
⊢ IsIso (R.whiskerLeft h.unit)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
this : R.whiskerLeft h.unit = 𝟙 (R ⋙ 𝟭 C) ≫ inv (whiskerRight h.counit R)
⊢ IsIso (𝟙 (R ⋙ 𝟭 C) ≫ inv (whiskerRight h.counit R))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
⊢ whiskerRight h.unit L ≫ L.whiskerLeft h.counit = 𝟙 (𝟭 C ⋙ L)

Tactic:
have := h.left_triangle
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
this : whiskerRight h.unit L ≫ L.whiskerLeft h.counit = 𝟙 (𝟭 C ⋙ L)
⊢ whiskerRight h.unit L = 𝟙 (𝟭 C ⋙ L) ≫ inv (L.whiskerLeft h.counit)

Tactic:
rw [← IsIso.eq_comp_inv] at this

Premises used: CategoryTheory.IsIso.eq_comp_inv
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
this : whiskerRight h.unit L = 𝟙 (𝟭 C ⋙ L) ≫ inv (L.whiskerLeft h.counit)
rw : IsIso (𝟙 (𝟭 C ⋙ L) ≫ inv (L.whiskerLeft h.counit))
⊢ IsIso (whiskerRight h.unit L)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : R.Full
inst_3 : R.Faithful
this : whiskerRight h.unit L = 𝟙 (𝟭 C ⋙ L) ≫ inv (L.whiskerLeft h.counit)
⊢ IsIso (𝟙 (𝟭 C ⋙ L) ≫ inv (L.whiskerLeft h.counit))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Faithful
inst_3 : L.Full
Y : C
⊢ IsIso (X := (R ⋙ L).obj (L.obj Y)) (h.counit.app (L.obj Y))

Tactic:
isIso_of_hom_comp_eq_id _ (h.left_triangle_components Y)

Premises used: CategoryTheory.isIso_of_hom_comp_eq_id, CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Faithful
inst_3 : L.Full
Y : D
⊢ IsIso (R.map (h.counit.app Y))

Tactic:
isIso_of_hom_comp_eq_id _ (h.right_triangle_components Y)

Premises used: CategoryTheory.Adjunction.right_triangle_components, CategoryTheory.isIso_of_hom_comp_eq_id
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Faithful
inst_3 : L.Full
X : D
mp : IsIso (h.counit.app X) → L.essImage X
mpr : L.essImage X → IsIso (h.counit.app X)
⊢ IsIso (h.counit.app X) ↔ L.essImage X

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Faithful
inst_3 : L.Full
X : D
h_1 : IsIso (h.counit.app X)
⊢ L.essImage X

Tactic:
⟨R.obj X, ⟨asIso (h.counit.app X)⟩⟩

Premises used: CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Adjunction.counit, Exists.intro, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.asIso