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 : L.Faithful
inst_3 : L.Full
X : D
h_1 : IsIso (h.counit.app X)
⊢ L.essImage X

Tactic:
exact ⟨R.obj X, ⟨asIso (h.counit.app X)⟩⟩
-- 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
w : C
i : L.obj w ≅ X
mpr : IsIso (X := (R ⋙ L).obj (L.obj w)) (h.counit.app (L.obj w))
⊢ IsIso (h.counit.app X)

Tactic:
rw [NatTrans.isIso_app_iff_of_iso _ i.symm]

Premises used: CategoryTheory.NatTrans.isIso_app_iff_of_iso, CategoryTheory.Iso.symm
-- 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
w : C
i : L.obj w ≅ X
⊢ IsIso (X := (R ⋙ L).obj (L.obj w)) (h.counit.app (L.obj w))

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
A : D
inst_2 : IsIso (h.counit.app A)
⊢ L.essImage A

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

Premises used: CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Adjunction.counit, Exists.intro, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- 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
Y : C
e : X ≅ L.obj Y
⊢ IsIso (h.counit.app X)

Tactic:
(isIso_counit_app_iff_mem_essImage h).mpr ⟨Y, ⟨e.symm⟩⟩

Premises used: Iff.mpr, Nonempty.intro, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage
-- 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
inst_3 : R.Full
Y : D
⊢ IsIso (X := obj.{v₁, v₁, u₁, u₁} (𝟭 C) (R.obj Y)) (h.unit.app (R.obj Y))

Tactic:
isIso_of_comp_hom_eq_id _ (h.right_triangle_components Y)

Premises used: CategoryTheory.isIso_of_comp_hom_eq_id, 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 : R.Faithful
inst_3 : R.Full
X : C
⊢ IsIso (L.map (h.unit.app X))

Tactic:
isIso_of_comp_hom_eq_id _ (h.left_triangle_components X)

Premises used: CategoryTheory.isIso_of_comp_hom_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 : R.Faithful
inst_3 : R.Full
Y : C
mp : IsIso (h.unit.app Y) → R.essImage Y
mpr : R.essImage Y → IsIso (h.unit.app Y)
⊢ IsIso (h.unit.app Y) ↔ R.essImage Y

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 : R.Faithful
inst_3 : R.Full
Y : C
h_1 : IsIso (h.unit.app Y)
⊢ R.essImage Y

Tactic:
⟨L.obj Y, ⟨(asIso (h.unit.app Y)).symm⟩⟩

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.Functor.essImage, Nonempty.intro, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- 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
inst_3 : R.Full
Y : C
h_1 : IsIso (h.unit.app Y)
⊢ R.essImage Y

Tactic:
exact ⟨L.obj Y, ⟨(asIso (h.unit.app Y)).symm⟩⟩
-- 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
inst_3 : R.Full
Y : C
w : D
i : R.obj w ≅ Y
mpr : IsIso (X := obj.{v₁, v₁, u₁, u₁} (𝟭 C) (R.obj w)) (h.unit.app (R.obj w))
⊢ IsIso (h.unit.app Y)

Tactic:
rw [NatTrans.isIso_app_iff_of_iso _ i.symm]

Premises used: CategoryTheory.NatTrans.isIso_app_iff_of_iso, CategoryTheory.Iso.symm
-- 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
inst_3 : R.Full
Y : C
w : D
i : R.obj w ≅ Y
⊢ IsIso (X := obj.{v₁, v₁, u₁, u₁} (𝟭 C) (R.obj w)) (h.unit.app (R.obj w))

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
A : C
inst_2 : IsIso (h.unit.app A)
⊢ R.essImage A

Tactic:
⟨L.obj A, ⟨(asIso (h.unit.app A)).symm⟩⟩

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.Functor.essImage, Nonempty.intro, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- 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
inst_3 : R.Full
X : D
Y : C
e : Y ≅ R.obj X
⊢ IsIso (h.unit.app Y)

Tactic:
(isIso_unit_app_iff_mem_essImage h).mpr ⟨X, ⟨e.symm⟩⟩

Premises used: Iff.mpr, CategoryTheory.Adjunction.isIso_unit_app_iff_mem_essImage, Nonempty.intro, Exists.intro, CategoryTheory.Iso.symm
-- 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.IsEquivalence
⊢ ∀ (Y : C), IsIso (h.unit.app Y)

Tactic:
have := fun Y => isIso_unit_app_of_iso h (R.objObjPreimageIso Y).symm
-- 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.IsEquivalence
this : ∀ (Y : C), IsIso (h.unit.app Y)
⊢ IsIso h.unit

Tactic:
apply 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
inst_2 : L.IsEquivalence
⊢ ∀ (X : D), IsIso (h.counit.app X)

Tactic:
have := fun X => isIso_counit_app_of_iso h (L.objObjPreimageIso X).symm
-- 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.IsEquivalence
this : ∀ (X : D), IsIso (h.counit.app X)
⊢ IsIso h.counit

Tactic:
apply 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
inst_2 : R.IsEquivalence
⊢ L.IsEquivalence

Tactic:
h.toEquivalence.isEquivalence_functor

Premises used: CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Adjunction.toEquivalence
-- 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.IsEquivalence
⊢ R.IsEquivalence

Tactic:
h.toEquivalence.isEquivalence_inverse

Premises used: CategoryTheory.Equivalence.isEquivalence_inverse, CategoryTheory.Adjunction.toEquivalence
-- 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.IsEquivalence
⊢ R.IsEquivalence

Tactic:
have := h.isEquivalence_right_of_isEquivalence_left
-- 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.IsEquivalence
this : R.IsEquivalence
⊢ IsIso h.unit

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.IsEquivalence
⊢ L.IsEquivalence

Tactic:
have := h.isEquivalence_left_of_isEquivalence_right
-- 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.IsEquivalence
this : L.IsEquivalence
⊢ IsIso 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
E : Type u_1
inst_2 : Category.{v_1, u_1} E
T : Functor.{v₁, v_1, u₁, u_1} C E
S : Functor.{v_1, v₂, u_1, u₂} E D
X : C
adj2 : T ⊣ S ⋙ R
inst_3 : R.Faithful
inst_4 : R.Full
FF : R.FullyFaithful := FullyFaithful.ofFullyFaithful R
hf :
  ∀ (T_1 : E),
    Function.Bijective (β := T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ T_1) fun (x : T.obj ((L ⋙ R).obj X) ⟶ T_1) ↦
      T.map (h.unit.app X) ≫ x
⊢ IsIso (T.map (h.unit.app X))

Tactic:
apply isIso_of_coyoneda_map_bijective

Premises used: CategoryTheory.isIso_of_coyoneda_map_bijective
-- 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
E : Type u_1
inst_2 : Category.{v_1, u_1} E
T : Functor.{v₁, v_1, u₁, u_1} C E
S : Functor.{v_1, v₂, u_1, u₂} E D
X : C
adj2 : T ⊣ S ⋙ R
inst_3 : R.Faithful
inst_4 : R.Full
FF : R.FullyFaithful := FullyFaithful.ofFullyFaithful R
Y : E
⊢ Function.Bijective (α := T.obj (R.obj (L.obj X)) ⟶ Y) (β := T.obj X ⟶ Y)
    (⇑(Equiv.trans (adj2.homEquiv (R.obj (L.obj X)) Y)
          (Equiv.trans (Equiv.symm FF.homEquiv) (Equiv.trans (h.homEquiv X (S.obj Y)) (adj2.homEquiv X Y).symm))) :
      (a : T.obj (R.obj (L.obj X)) ⟶ Y) → T.obj X ⟶ Y)

Tactic:
((adj2.homEquiv (R.obj (L.obj X)) Y).trans <|
        FF.homEquiv.symm.trans <|
          (h.homEquiv X (S.obj Y)).trans (adj2.homEquiv X Y).symm).bijective

Premises used: Equiv.bijective, Equiv.trans, CategoryTheory.Functor.FullyFaithful.homEquiv, CategoryTheory.Adjunction.homEquiv, 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
E : Type u_1
inst_2 : Category.{v_1, u_1} E
T : Functor.{v₁, v_1, u₁, u_1} C E
S : Functor.{v_1, v₂, u_1, u₂} E D
X : C
adj2 : T ⊣ S ⋙ R
inst_3 : R.Faithful
inst_4 : R.Full
FF : R.FullyFaithful := FullyFaithful.ofFullyFaithful R
Y : E
h₁ :
  (T.obj ((L ⋙ R).obj X) ⟶ Y) = (T.obj (R.obj (L.obj X)) ⟶ Y) →
    (T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ Y) = (T.obj X ⟶ Y) →
      Eq (α := (T.obj ((L ⋙ R).obj X) ⟶ Y) → (T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ Y))
        (fun (x : T.obj ((L ⋙ R).obj X) ⟶ Y) ↦ T.map (h.unit.app X) ≫ x)
        (⇑(Equiv.trans (adj2.homEquiv (R.obj (L.obj X)) Y)
              (Equiv.trans (Equiv.symm FF.homEquiv) (Equiv.trans (h.homEquiv X (S.obj Y)) (adj2.homEquiv X Y).symm))) :
          (a : T.obj (R.obj (L.obj X)) ⟶ Y) → T.obj X ⟶ Y)
⊢ Function.Bijective (β := T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ Y) fun (x : T.obj ((L ⋙ R).obj X) ⟶ Y) ↦
    T.map (h.unit.app X) ≫ x

Tactic:
convert!
    ((adj2.homEquiv (R.obj (L.obj X)) Y).trans <|
        FF.homEquiv.symm.trans <|
          (h.homEquiv X (S.obj Y)).trans (adj2.homEquiv X Y).symm).bijective using 1

Premises used: Equiv.bijective, Equiv.trans, CategoryTheory.Functor.FullyFaithful.homEquiv, CategoryTheory.Adjunction.homEquiv, 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
E : Type u_1
inst_2 : Category.{v_1, u_1} E
T : Functor.{v₁, v_1, u₁, u_1} C E
S : Functor.{v_1, v₂, u_1, u₂} E D
X : C
adj2 : T ⊣ S ⋙ R
inst_3 : R.Faithful
inst_4 : R.Full
FF : R.FullyFaithful := FullyFaithful.ofFullyFaithful R
Y : E
e_1 : (T.obj ((L ⋙ R).obj X) ⟶ Y) = (T.obj (R.obj (L.obj X)) ⟶ Y)
e_2 : (T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ Y) = (T.obj X ⟶ Y)
h₁ :
  ∀ (x : T.obj ((L ⋙ R).obj X) ⟶ Y),
    T.map (h.unit.app X) ≫ x =
      (Equiv.trans (adj2.homEquiv (R.obj (L.obj X)) Y)
            (Equiv.trans (Equiv.symm FF.homEquiv) (Equiv.trans (h.homEquiv X (S.obj Y)) (adj2.homEquiv X Y).symm)) :
          (a : T.obj (R.obj (L.obj X)) ⟶ Y) → T.obj X ⟶ Y)
        x
⊢ Eq (α := (T.obj ((L ⋙ R).obj X) ⟶ Y) → (T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ Y))
    (fun (x : T.obj ((L ⋙ R).obj X) ⟶ Y) ↦ T.map (h.unit.app X) ≫ x)
    (⇑(Equiv.trans (adj2.homEquiv (R.obj (L.obj X)) Y)
          (Equiv.trans (Equiv.symm FF.homEquiv) (Equiv.trans (h.homEquiv X (S.obj Y)) (adj2.homEquiv X Y).symm))) :
      (a : T.obj (R.obj (L.obj X)) ⟶ Y) → T.obj X ⟶ Y)

Tactic:
ext x
-- 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
E : Type u_1
inst_2 : Category.{v_1, u_1} E
T : Functor.{v₁, v_1, u₁, u_1} C E
S : Functor.{v_1, v₂, u_1, u₂} E D
X : C
adj2 : T ⊣ S ⋙ R
inst_3 : R.Faithful
inst_4 : R.Full
FF : R.FullyFaithful := FullyFaithful.ofFullyFaithful R
Y : E
e_1 : (T.obj ((L ⋙ R).obj X) ⟶ Y) = (T.obj (R.obj (L.obj X)) ⟶ Y)
e_2 : (T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ Y) = (T.obj X ⟶ Y)
x : T.obj ((L ⋙ R).obj X) ⟶ Y
⊢ T.map ((S ⋙ R).map x) ≫ adj2.counit.app Y = adj2.counit.app (T.obj ((L ⋙ R).obj X)) ≫ x

Tactic:
have := adj2.counit_naturality x
-- 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
E : Type u_1
inst_2 : Category.{v_1, u_1} E
T : Functor.{v₁, v_1, u₁, u_1} C E
S : Functor.{v_1, v₂, u_1, u₂} E D
X : C
adj2 : T ⊣ S ⋙ R
inst_3 : R.Faithful
inst_4 : R.Full
FF : R.FullyFaithful := FullyFaithful.ofFullyFaithful R
Y : E
e_1 : (T.obj ((L ⋙ R).obj X) ⟶ Y) = (T.obj (R.obj (L.obj X)) ⟶ Y)
e_2 : (T.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ Y) = (T.obj X ⟶ Y)
x : T.obj ((L ⋙ R).obj X) ⟶ Y
this : T.map ((S ⋙ R).map x) ≫ adj2.counit.app Y = adj2.counit.app (T.obj ((L ⋙ R).obj X)) ≫ x
⊢ T.map (h.unit.app X) ≫ x =
    (Equiv.trans (adj2.homEquiv (R.obj (L.obj X)) Y)
          (Equiv.trans (Equiv.symm FF.homEquiv) (Equiv.trans (h.homEquiv X (S.obj Y)) (adj2.homEquiv X Y).symm)) :
        (a : T.obj (R.obj (L.obj X)) ⟶ Y) → T.obj X ⟶ Y)
      x

Tactic:
simp_all [Adjunction.homEquiv]

Premises used: CategoryTheory.Adjunction.homEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₂, v₃, u₂, u₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
rw : F'.map (𝟙 (U.obj X)) = 𝟙 (F'.obj (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)))
⊢ F'.map (adj₁.unit.app (U.obj X)) ≫ F'.map (U.map (adj₁.counit.app X)) =
    𝟙 (F'.obj (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)))

Tactic:
rw [← F'.map_comp, adj₁.right_triangle_components]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.right_triangle_components
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₂, v₃, u₂, u₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (𝟙 (U.obj X)) = 𝟙 (F'.obj (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)))

Tactic:
apply F'.map_id

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₂, v₃, u₂, u₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
dsimp :
  F'.map (adj₁.unit.app (U.obj X)) ≫
      F'.map (U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
        adj₂.counit.app (F'.obj (U.1 X)) =
    𝟙 (F'.obj (U.obj X))
⊢ F'.map (adj₁.unit.app (U.obj X)) ≫ otherMap R F' adj₁ adj₂ X =
    𝟙 (F'.obj (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)))

Tactic:
dsimp [otherMap]

Premises used: CategoryTheory.LiftLeftAdjoint.otherMap
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₂, v₃, u₂, u₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
rw :
  F'.map (adj₁.unit.app (U.obj X) ≫ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
      adj₂.counit.app (F'.obj (U.1 X)) =
    𝟙 (F'.obj (U.obj X))
rw₁ :
  F'.map
        (adj₁.unit.app (U.obj X) ≫
          U.map (F.map (adj₂.unit.app (U.1 X))) ≫ U.map (adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
      adj₂.counit.app (F'.obj (U.1 X)) =
    𝟙 (F'.obj (U.obj X))
rw₂ :
  F'.map
        (adj₂.unit.app (U.1 X) ≫
          adj₁.unit.app (U.obj (R.obj (F'.obj (U.1 X)))) ≫ U.map (adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
      adj₂.counit.app (F'.obj (U.1 X)) =
    𝟙 (F'.obj (U.obj X))
rw₃ :
  F'.map (adj₂.unit.app (U.1 X) ≫ 𝟙 (U.obj (R.obj (F'.obj (U.1 X))))) ≫ adj₂.counit.app (F'.obj (U.1 X)) =
    𝟙 (F'.obj (U.obj X))
rw₄ : F'.map (adj₂.unit.app (U.1 X)) ≫ adj₂.counit.app (F'.obj (U.1 X)) = 𝟙 (F'.obj (U.obj X))
rw₅ rw₆ : Eq.{v₁ + 1} (α := F'.obj (U.obj X) ⟶ F'.obj (U.obj X)) (𝟙 (F'.obj (U.obj X))) (𝟙 (F'.obj (U.obj X)))
⊢ F'.map (adj₁.unit.app (U.obj X)) ≫
      F'.map (U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
        adj₂.counit.app (F'.obj (U.1 X)) =
    𝟙 (F'.obj (U.obj X))

Tactic:
rw [← F'.map_comp_assoc, U.map_comp, adj₁.unit_naturality_assoc,
        adj₁.right_triangle_components, comp_id, adj₂.left_triangle_components]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.right_triangle_components, CategoryTheory.Adjunction.left_triangle_components, CategoryTheory.Adjunction.unit_naturality_assoc
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₂, v₃, u₂, u₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
apply :
  ∀ (a : F'.obj (U.obj X) ⟶ Y),
    F'.map (U.map (adj₁.counit.app X)) ≫ a = otherMap R F' adj₁ adj₂ X ≫ a ↔
      Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R.obj Y)))
        (U.map
          (F.map
              (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
                  (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
                a) ≫
            adj₁.counit.app (R.obj Y)))
        (U.map (adj₁.counit.app X) ≫
          ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
              (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
            a)
⊢ Equiv.{v₁ + 1, max 1 (v₃ + 1)}
    { f : F'.obj (U.obj X) ⟶ Y // F'.map (U.map (adj₁.counit.app X)) ≫ f = otherMap R F' adj₁ adj₂ X ≫ f }
    { g : U.obj X ⟶ U.obj (R.obj Y) // U.map (F.map g ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ g }

Tactic:
apply (adj₂.homEquiv _ _).subtypeEquiv _

Premises used: Equiv.subtypeEquiv, CategoryTheory.Adjunction.homEquiv