awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.Restrict
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
iC : Functor.{v₁, v₃, u₁, u₃} C C'
iD : Functor.{v₂, v₄, u₂, u₄} D D'
L' : Functor.{v₃, v₄, u₃, u₄} C' D'
R' : Functor.{v₄, v₃, u₄, u₃} D' C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
suffices : R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g)
⊢ Eq (α := iC.obj X ⟶ iC.obj (R.obj Y))
    (iC.map
      ((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
            (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
              (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) hiD.homEquiv
                  ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y))))
                (adj.homEquiv (iC.obj X) (iD.obj Y)))
              (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
            (Equiv.symm hiC.homEquiv) :
          (a : L.obj X ⟶ Y) → X ⟶ R.obj Y)
        (f ≫ g)))
    (iC.map
      ((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
              (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                  (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) hiD.homEquiv
                    ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y'))))
                  (adj.homEquiv (iC.obj X) (iD.obj Y')))
                (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y')))
              (Equiv.symm hiC.homEquiv) :
            (a : L.obj X ⟶ Y') → X ⟶ R.obj Y')
          f ≫
        R.map g))

Tactic:
suffices R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g) by
          simp [Trans.trans, this]
-- Module: Mathlib.CategoryTheory.Adjunction.Restrict
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
iC : Functor.{v₁, v₃, u₁, u₃} C C'
iD : Functor.{v₂, v₄, u₂, u₄} D D'
L' : Functor.{v₃, v₄, u₃, u₄} C' D'
R' : Functor.{v₄, v₃, u₄, u₃} D' C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
⊢ R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g)

Tactic:
apply comm2.hom.naturality g

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Adjunction.Restrict
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
iC : Functor.{v₁, v₃, u₁, u₃} C C'
iD : Functor.{v₂, v₄, u₂, u₄} D D'
L' : Functor.{v₃, v₄, u₃, u₄} C' D'
R' : Functor.{v₄, v₃, u₄, u₃} D' C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
⊢ iC.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).unit.app X) =
    adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ comm2.hom.app (L.obj X)

Tactic:
simp [restrictFullyFaithful]

Premises used: CategoryTheory.Adjunction.restrictFullyFaithful
-- Module: Mathlib.CategoryTheory.Adjunction.Restrict
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
iC : Functor.{v₁, v₃, u₁, u₃} C C'
iD : Functor.{v₂, v₄, u₂, u₄} D D'
L' : Functor.{v₃, v₄, u₃, u₄} C' D'
R' : Functor.{v₄, v₃, u₄, u₃} D' C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : D
dsimp :
  iD.map
      (hiD.preimage
        (comm1.inv.app (R.obj X) ≫
          ((Equiv.symm (adj.homEquiv (iC.obj (R.obj X)) (iD.obj X)) :
                  Equiv.{v₃ + 1, v₄ + 1} (iC.obj (R.obj X) ⟶ R'.obj (iD.obj X))
                    (L'.obj (iC.obj (R.obj X)) ⟶ iD.obj X)) :
                (a : iC.obj (R.obj X) ⟶ R'.obj (iD.obj X)) → L'.obj (iC.obj (R.obj X)) ⟶ iD.obj X)
              (𝟙 (iC.obj (R.obj X)) ≫ iC.map (𝟙 (R.obj X)) ≫ comm2.inv.app X) ≫
            𝟙 (iD.obj X))) =
    comm1.inv.app (R.obj X) ≫ L'.map (comm2.inv.app X) ≫ adj.counit.app (iD.obj X)
⊢ iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X) =
    comm1.inv.app (R.obj X) ≫ L'.map (comm2.inv.app X) ≫ adj.counit.app (iD.obj X)

Tactic:
dsimp [restrictFullyFaithful]

Premises used: CategoryTheory.Adjunction.restrictFullyFaithful
-- Module: Mathlib.CategoryTheory.Adjunction.Restrict
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
iC : Functor.{v₁, v₃, u₁, u₃} C C'
iD : Functor.{v₂, v₄, u₂, u₄} D D'
L' : Functor.{v₃, v₄, u₃, u₄} C' D'
R' : Functor.{v₄, v₃, u₄, u₃} D' C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : D
⊢ iD.map
      (hiD.preimage
        (comm1.inv.app (R.obj X) ≫
          ((Equiv.symm (adj.homEquiv (iC.obj (R.obj X)) (iD.obj X)) :
                  Equiv.{v₃ + 1, v₄ + 1} (iC.obj (R.obj X) ⟶ R'.obj (iD.obj X))
                    (L'.obj (iC.obj (R.obj X)) ⟶ iD.obj X)) :
                (a : iC.obj (R.obj X) ⟶ R'.obj (iD.obj X)) → L'.obj (iC.obj (R.obj X)) ⟶ iD.obj X)
              (𝟙 (iC.obj (R.obj X)) ≫ iC.map (𝟙 (R.obj X)) ≫ comm2.inv.app X) ≫
            𝟙 (iD.obj X))) =
    comm1.inv.app (R.obj X) ≫ L'.map (comm2.inv.app X) ≫ adj.counit.app (iD.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Restrict
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
iC : Functor.{v₁, v₃, u₁, u₃} C C'
iD : Functor.{v₂, v₄, u₂, u₄} D D'
L' : Functor.{v₃, v₄, u₃, u₄} C' D'
R' : Functor.{v₄, v₃, u₄, u₃} D' C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y : D
f : L.obj X ⟶ Y
apply :
  iC.map (((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y : (a : L.obj X ⟶ Y) → X ⟶ R.obj Y) f) =
    iC.map (hiC.preimage (adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y))
⊢ ((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y : (a : L.obj X ⟶ Y) → X ⟶ R.obj Y) f =
    hiC.preimage (adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y)

Tactic:
apply hiC.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective
-- Module: Mathlib.CategoryTheory.Adjunction.Restrict
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
iC : Functor.{v₁, v₃, u₁, u₃} C C'
iD : Functor.{v₂, v₄, u₂, u₄} D D'
L' : Functor.{v₃, v₄, u₃, u₄} C' D'
R' : Functor.{v₄, v₃, u₄, u₃} D' C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y : D
f : L.obj X ⟶ Y
simp :
  adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ comm2.hom.app (L.obj X) ≫ iC.map (R.map f) =
    adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y
⊢ iC.map (((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y : (a : L.obj X ⟶ Y) → X ⟶ R.obj Y) f) =
    iC.map (hiC.preimage (adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y))

Tactic:
simp only [homEquiv_apply, Functor.comp_obj, Functor.map_comp, map_restrictFullyFaithful_unit_app,
    Functor.id_obj, assoc, Functor.FullyFaithful.map_preimage]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.id_obj, CategoryTheory.Adjunction.homEquiv_apply, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app, CategoryTheory.Functor.FullyFaithful.map_preimage
-- Module: Mathlib.CategoryTheory.Adjunction.Restrict
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
iC : Functor.{v₁, v₃, u₁, u₃} C C'
iD : Functor.{v₂, v₄, u₂, u₄} D D'
L' : Functor.{v₃, v₄, u₃, u₄} C' D'
R' : Functor.{v₄, v₃, u₄, u₃} D' C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y : D
f : L.obj X ⟶ Y
e_a : comm2.hom.app (L.obj X) ≫ iC.map (R.map f) = R'.map (iD.map f) ≫ comm2.hom.app Y
⊢ adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ comm2.hom.app (L.obj X) ≫ iC.map (R.map f) =
    adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y

Tactic:
congr 2
-- Module: Mathlib.CategoryTheory.Adjunction.Restrict
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
iC : Functor.{v₁, v₃, u₁, u₃} C C'
iD : Functor.{v₂, v₄, u₂, u₄} D D'
L' : Functor.{v₃, v₄, u₃, u₄} C' D'
R' : Functor.{v₄, v₃, u₄, u₃} D' C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y : D
f : L.obj X ⟶ Y
⊢ comm2.hom.app (L.obj X) ≫ iC.map (R.map f) = R'.map (iD.map f) ≫ comm2.hom.app Y

Tactic:
(comm2.hom.naturality _).symm

Premises used: CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Adjunction.Restrict
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
iC : Functor.{v₁, v₃, u₁, u₃} C C'
iD : Functor.{v₂, v₄, u₂, u₄} D D'
L' : Functor.{v₃, v₄, u₃, u₄} C' D'
R' : Functor.{v₄, v₃, u₄, u₃} D' C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y : D
f : L.obj X ⟶ Y
⊢ comm2.hom.app (L.obj X) ≫ iC.map (R.map f) = R'.map (iD.map f) ≫ comm2.hom.app Y

Tactic:
exact (comm2.hom.naturality _).symm

Premises used: CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
adj : F ⋙ G ⊣ H ⋙ G := t.adj₁.comp t.adj₂
mp : IsIso t.adj₁.unit → IsIso t.adj₂.counit
mpr : IsIso t.adj₂.counit → IsIso t.adj₁.unit
⊢ IsIso t.adj₁.unit ↔ IsIso t.adj₂.counit

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
adj : F ⋙ G ⊣ H ⋙ G := t.adj₁.comp t.adj₂
h : IsIso t.adj₁.unit
idAdj : 𝟭 C ⊣ H ⋙ G := adj.ofNatIsoLeft (asIso t.adj₁.unit).symm
⊢ IsIso t.adj₂.counit

Tactic:
t.adj₂.isIso_counit_of_iso (idAdj.rightAdjointUniq id)

Premises used: CategoryTheory.Adjunction.isIso_counit_of_iso, CategoryTheory.Adjunction.rightAdjointUniq, CategoryTheory.Adjunction.id, CategoryTheory.Adjunction.Triple.adj₂
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
adj : F ⋙ G ⊣ H ⋙ G := t.adj₁.comp t.adj₂
h : IsIso t.adj₁.unit
idAdj : 𝟭 C ⊣ H ⋙ G := adj.ofNatIsoLeft (asIso t.adj₁.unit).symm
⊢ IsIso t.adj₂.counit

Tactic:
exact t.adj₂.isIso_counit_of_iso (idAdj.rightAdjointUniq id)

Premises used: CategoryTheory.Adjunction.isIso_counit_of_iso, CategoryTheory.Adjunction.rightAdjointUniq, CategoryTheory.Adjunction.id, CategoryTheory.Adjunction.Triple.adj₂
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
adj : F ⋙ G ⊣ H ⋙ G := t.adj₁.comp t.adj₂
h : IsIso t.adj₂.counit
adjId : F ⋙ G ⊣ 𝟭 C := adj.ofNatIsoRight (asIso t.adj₂.counit)
⊢ IsIso t.adj₁.unit

Tactic:
t.adj₁.isIso_unit_of_iso (adjId.leftAdjointUniq id)

Premises used: CategoryTheory.Adjunction.Triple.adj₁, CategoryTheory.Adjunction.leftAdjointUniq, CategoryTheory.Adjunction.isIso_unit_of_iso, CategoryTheory.Adjunction.id
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
adj : F ⋙ G ⊣ H ⋙ G := t.adj₁.comp t.adj₂
h : IsIso t.adj₂.counit
adjId : F ⋙ G ⊣ 𝟭 C := adj.ofNatIsoRight (asIso t.adj₂.counit)
⊢ IsIso t.adj₁.unit

Tactic:
exact t.adj₁.isIso_unit_of_iso (adjId.leftAdjointUniq id)

Premises used: CategoryTheory.Adjunction.Triple.adj₁, CategoryTheory.Adjunction.leftAdjointUniq, CategoryTheory.Adjunction.isIso_unit_of_iso, CategoryTheory.Adjunction.id
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
h : F.FullyFaithful
this_1 : F.Full
this : F.Faithful
rw : IsIso t.adj₁.unit
⊢ IsIso t.adj₂.counit

Tactic:
rw [← t.isIso_unit_iff_isIso_counit]

Premises used: CategoryTheory.Adjunction.Triple.isIso_unit_iff_isIso_counit
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
h : F.FullyFaithful
this_1 : F.Full
this : F.Faithful
⊢ IsIso t.adj₁.unit

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
h : H.FullyFaithful
this_1 : H.Full
this : H.Faithful
rw : IsIso t.adj₂.counit
⊢ IsIso t.adj₁.unit

Tactic:
rw [t.isIso_unit_iff_isIso_counit]

Premises used: CategoryTheory.Adjunction.Triple.isIso_unit_iff_isIso_counit
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
h : H.FullyFaithful
this_1 : H.Full
this : H.Faithful
⊢ IsIso t.adj₂.counit

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
⊢ whiskerRight t.rightToLeft G = t.adj₂.counit ≫ t.adj₁.unit

Tactic:
((FullyFaithful.ofFullyFaithful G).whiskeringRight _).map_preimage _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.FullyFaithful.map_preimage, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful, CategoryTheory.Functor.FullyFaithful.whiskeringRight
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
X : C
⊢ G.map (t.rightToLeft.app X) = t.adj₂.counit.app X ≫ t.adj₁.unit.app X

Tactic:
congr_app t.whiskerRight_rightToLeft X

Premises used: CategoryTheory.Adjunction.Triple.whiskerRight_rightToLeft, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
w :
  ∀ (X : C),
    t.rightToLeft.app X =
      (H.leftUnitor.inv ≫
            whiskerRight t.adj₁.unit H ≫
              (F.associator G H).hom ≫ inv (F.whiskerLeft t.adj₂.unit) ≫ F.rightUnitor.hom).app
        X
⊢ t.rightToLeft =
    H.leftUnitor.inv ≫
      whiskerRight t.adj₁.unit H ≫ (F.associator G H).hom ≫ inv (F.whiskerLeft t.adj₂.unit) ≫ F.rightUnitor.hom

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
X : C
w :
  G.map (t.rightToLeft.app X) =
    G.map
      ((H.leftUnitor.inv ≫
            whiskerRight t.adj₁.unit H ≫
              (F.associator G H).hom ≫ inv (F.whiskerLeft t.adj₂.unit) ≫ F.rightUnitor.hom).app
        X)
⊢ t.rightToLeft.app X =
    (H.leftUnitor.inv ≫
          whiskerRight t.adj₁.unit H ≫ (F.associator G H).hom ≫ inv (F.whiskerLeft t.adj₂.unit) ≫ F.rightUnitor.hom).app
      X

Tactic:
apply G.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
X : C
⊢ G.map (t.rightToLeft.app X) =
    G.map
      ((H.leftUnitor.inv ≫
            whiskerRight t.adj₁.unit H ≫
              (F.associator G H).hom ≫ inv (F.whiskerLeft t.adj₂.unit) ≫ F.rightUnitor.hom).app
        X)

Tactic:
simp [rightToLeft]

Premises used: CategoryTheory.Adjunction.Triple.rightToLeft
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
w :
  ∀ (X : C),
    t.rightToLeft.app X =
      (H.rightUnitor.inv ≫
            inv (H.whiskerLeft t.adj₁.counit) ≫
              (H.associator G F).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom).app
        X
⊢ t.rightToLeft =
    H.rightUnitor.inv ≫
      inv (H.whiskerLeft t.adj₁.counit) ≫ (H.associator G F).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
X : C
w :
  G.map (t.rightToLeft.app X) =
    G.map
      ((H.rightUnitor.inv ≫
            inv (H.whiskerLeft t.adj₁.counit) ≫
              (H.associator G F).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom).app
        X)
⊢ t.rightToLeft.app X =
    (H.rightUnitor.inv ≫
          inv (H.whiskerLeft t.adj₁.counit) ≫
            (H.associator G F).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom).app
      X

Tactic:
apply G.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
X : C
⊢ G.map (t.rightToLeft.app X) =
    G.map
      ((H.rightUnitor.inv ≫
            inv (H.whiskerLeft t.adj₁.counit) ≫
              (H.associator G F).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom).app
        X)

Tactic:
simp [rightToLeft]

Premises used: CategoryTheory.Adjunction.Triple.rightToLeft
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
X : C
⊢ G.map (t.adj₁.counit.app (H.obj X) ≫ t.rightToLeft.app X) = G.map (F.map (t.adj₂.counit.app X))

Tactic:
simp [← cancel_epi (t.adj₁.unit.app _)]

Premises used: CategoryTheory.Adjunction.Triple.adj₁, CategoryTheory.Adjunction.unit, CategoryTheory.cancel_epi, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
X : C
⊢ G.map (t.rightToLeft.app X ≫ t.adj₂.unit.app (F.obj X)) = G.map (H.map (t.adj₁.unit.app X))

Tactic:
simp [← cancel_mono (t.adj₂.counit.app _)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Adjunction.counit, CategoryTheory.NatTrans.app, CategoryTheory.Adjunction.Triple.adj₂
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
w : ∀ (x : Cᵒᵖ), t.op.rightToLeft.app x = (NatTrans.op t.rightToLeft).app x
⊢ t.op.rightToLeft = NatTrans.op t.rightToLeft

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : G.Full
inst_3 : G.Faithful
x : Cᵒᵖ
w :
  (F.op.leftUnitor.inv ≫
          whiskerRight t.op.adj₁.unit F.op ≫
            (H.op.associator G.op F.op).hom ≫ inv (H.op.whiskerLeft t.op.adj₂.unit) ≫ H.op.rightUnitor.hom).app
      x =
    (NatTrans.op
          (H.rightUnitor.inv ≫
            inv (H.whiskerLeft t.adj₁.counit) ≫
              (H.associator G F).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom)).app
      x
⊢ t.op.rightToLeft.app x = (NatTrans.op t.rightToLeft).app x

Tactic:
rw [rightToLeft_eq_units, rightToLeft_eq_counits]

Premises used: CategoryTheory.Adjunction.Triple.rightToLeft_eq_units, CategoryTheory.Adjunction.Triple.rightToLeft_eq_counits