awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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ᵒᵖ
⊢ (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

Tactic:
simp
-- 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
rw : Epi (t.rightToLeft.app X ≫ t.adj₂.unit.app (F.obj X)) ↔ Epi (H.map (t.adj₁.unit.app X))
rw₁ rw₂ : Epi (H.map (t.adj₁.unit.app X)) ↔ Epi (H.map (t.adj₁.unit.app X))
⊢ Epi (t.rightToLeft.app X) ↔ Epi (H.map (t.adj₁.unit.app X))

Tactic:
rw [← epi_comp_iff_of_isIso _ (t.adj₂.unit.app (F.obj X)), rightToLeft_app_adj₂_unit_app]

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.epi_comp_iff_of_isIso, CategoryTheory.Adjunction.Triple.rightToLeft_app_adj₂_unit_app, CategoryTheory.Functor.obj, 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
X : C
rw : Epi (t.adj₁.counit.app (H.obj X) ≫ t.rightToLeft.app X) ↔ Epi (F.map (t.adj₂.counit.app X))
rw₁ rw₂ : Epi (F.map (t.adj₂.counit.app X)) ↔ Epi (F.map (t.adj₂.counit.app X))
⊢ Epi (t.rightToLeft.app X) ↔ Epi (F.map (t.adj₂.counit.app X))

Tactic:
rw [← epi_comp_iff_of_epi (t.adj₁.counit.app (H.obj X)), adj₁_counit_app_rightToLeft_app]

Premises used: CategoryTheory.epi_comp_iff_of_epi, CategoryTheory.Adjunction.Triple.adj₁_counit_app_rightToLeft_app, CategoryTheory.Adjunction.Triple.adj₁, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.obj, 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
inst_4 : H.PreservesEpimorphisms
X : C
⊢ G.IsLeftAdjoint

Tactic:
have _ := t.adj₂.isLeftAdjoint
-- 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
inst_4 : H.PreservesEpimorphisms
X : C
h_1 : G.IsLeftAdjoint
h : Epi (t.rightToLeft.app X)
rw : Epi (G.map (t.rightToLeft.app X))
⊢ Epi (t.adj₂.counit.app X ≫ t.adj₁.unit.app X)

Tactic:
rw [← map_rightToLeft_app]

Premises used: CategoryTheory.Adjunction.Triple.map_rightToLeft_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
inst_4 : H.PreservesEpimorphisms
X : C
h_1 : G.IsLeftAdjoint
h : Epi (t.rightToLeft.app X)
⊢ Epi (G.map (t.rightToLeft.app X))

Tactic:
G.map_epi _

Premises used: CategoryTheory.Functor.map_epi
-- 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
inst_4 : H.PreservesEpimorphisms
X : C
h_1 : G.IsLeftAdjoint
h : Epi (t.rightToLeft.app X)
⊢ Epi (G.map (t.rightToLeft.app X))

Tactic:
exact G.map_epi _

Premises used: CategoryTheory.Functor.map_epi
-- 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
inst_4 : H.PreservesEpimorphisms
X : C
h : G.IsLeftAdjoint
refine : ∀ (h : Epi (t.adj₂.counit.app X ≫ t.adj₁.unit.app X)), Epi (t.rightToLeft.app X)
⊢ Epi (t.rightToLeft.app X) ↔ Epi (t.adj₂.counit.app X ≫ t.adj₁.unit.app X)

Tactic:
refine ⟨fun h ↦ by rw [← map_rightToLeft_app]; exact G.map_epi _, fun h ↦ ?_⟩
-- 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
inst_4 : H.PreservesEpimorphisms
X : C
h_1 : G.IsLeftAdjoint
h : Epi (t.adj₂.counit.app X ≫ t.adj₁.unit.app X)
rw : Epi (H.map (t.adj₁.unit.app X))
⊢ Epi (t.rightToLeft.app X)

Tactic:
rw [epi_rightToLeft_app_iff_epi_map_adj₁_unit_app]

Premises used: CategoryTheory.Adjunction.Triple.epi_rightToLeft_app_iff_epi_map_adj₁_unit_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
inst_4 : H.PreservesEpimorphisms
X : C
h_1 : G.IsLeftAdjoint
h : Epi (t.adj₂.counit.app X ≫ t.adj₁.unit.app X)
⊢ Epi (H.map (t.adj₁.unit.app X))

Tactic:
simpa using epi_comp (t.adj₂.unit.app (H.obj X)) (H.map (t.adj₂.counit.app X ≫ t.adj₁.unit.app X))

Premises used: CategoryTheory.epi_comp, CategoryTheory.Adjunction.Triple.adj₁, CategoryTheory.Adjunction.unit, CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.obj, 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 : F.Full
inst_3 : F.Faithful
X : C
⊢ t.leftToRight.app X = t.adj₂.unit.app (F.obj X) ≫ inv (H.map (t.adj₁.unit.app X))

Tactic:
simp [leftToRight]

Premises used: CategoryTheory.Adjunction.Triple.leftToRight
-- 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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
w :
  ∀ (X : C),
    t.leftToRight.app X =
      (F.leftUnitor.inv ≫
            inv (whiskerRight t.adj₂.counit F) ≫
              (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.rightUnitor.hom).app
        X
⊢ t.leftToRight =
    F.leftUnitor.inv ≫
      inv (whiskerRight t.adj₂.counit F) ≫ (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
w :
  𝟙 (F.obj X) ≫
      t.adj₂.unit.app (F.obj X) ≫ 𝟙 (H.obj (G.obj (F.obj X))) ≫ (inv (whiskerRight t.adj₁.unit H)).app X ≫ 𝟙 (H.obj X) =
    𝟙 (F.obj X) ≫
      (inv (whiskerRight t.adj₂.counit F)).app X ≫
        𝟙 (F.obj (G.obj (H.obj X))) ≫ t.adj₁.counit.app (H.obj X) ≫ 𝟙 (H.obj X)
⊢ t.leftToRight.app X =
    (F.leftUnitor.inv ≫
          inv (whiskerRight t.adj₂.counit F) ≫
            (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.rightUnitor.hom).app
      X

Tactic:
dsimp [leftToRight]

Premises used: CategoryTheory.Adjunction.Triple.leftToRight
-- 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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
w :
  t.adj₂.unit.app (F.obj X) ≫ inv ((whiskerRight t.adj₁.unit H).app X) =
    inv ((whiskerRight t.adj₂.counit F).app X) ≫ t.adj₁.counit.app (H.obj X)
⊢ 𝟙 (F.obj X) ≫
      t.adj₂.unit.app (F.obj X) ≫ 𝟙 (H.obj (G.obj (F.obj X))) ≫ (inv (whiskerRight t.adj₁.unit H)).app X ≫ 𝟙 (H.obj X) =
    𝟙 (F.obj X) ≫
      (inv (whiskerRight t.adj₂.counit F)).app X ≫
        𝟙 (F.obj (G.obj (H.obj X))) ≫ t.adj₁.counit.app (H.obj X) ≫ 𝟙 (H.obj X)

Tactic:
simp only [Category.id_comp, Category.comp_id, NatIso.isIso_inv_app]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.NatIso.isIso_inv_app, CategoryTheory.Category.id_comp
-- 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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
w :
  (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    t.adj₁.counit.app (H.obj X) ≫ (whiskerRight t.adj₁.unit H).app X
⊢ t.adj₂.unit.app (F.obj X) ≫ inv ((whiskerRight t.adj₁.unit H).app X) =
    inv ((whiskerRight t.adj₂.counit F).app X) ≫ t.adj₁.counit.app (H.obj X)

Tactic:
rw [IsIso.comp_inv_eq, Category.assoc, IsIso.eq_inv_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.eq_inv_comp, CategoryTheory.IsIso.comp_inv_eq
-- 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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    t.adj₁.counit.app (H.obj X) ≫ (whiskerRight t.adj₁.unit H).app X

Tactic:
Eq.trans ?_ (t.adj₁.counit_naturality <| (whiskerRight t.adj₁.unit H).app X)

Premises used: CategoryTheory.Adjunction.Triple.adj₁, CategoryTheory.Adjunction.unit, CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Functor.whiskerRight, CategoryTheory.NatTrans.app, Eq.trans
-- 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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
w :
  (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    F.map (G.map ((whiskerRight t.adj₁.unit H).app X)) ≫ t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    t.adj₁.counit.app (H.obj X) ≫ (whiskerRight t.adj₁.unit H).app X

Tactic:
refine Eq.trans ?_ (t.adj₁.counit_naturality <| (whiskerRight t.adj₁.unit H).app X)

Premises used: CategoryTheory.Adjunction.Triple.adj₁, CategoryTheory.Adjunction.unit, CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Functor.whiskerRight, CategoryTheory.NatTrans.app, Eq.trans
-- 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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
w :
  (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    F.map
        ((t.adj₂.counit.app (obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ≫ t.adj₁.unit.app X) ≫
          G.map (t.adj₂.unit.app (F.obj X))) ≫
      t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    F.map (G.map ((whiskerRight t.adj₁.unit H).app X)) ≫ t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)

Tactic:
rw [whiskerRight_app _ H, (asIso (t.adj₂.counit.app (G.obj _))).eq_comp_inv.2
      (t.adj₂.counit_naturality (t.adj₁.unit.app X)),
    ← (asIso _).comp_hom_eq_id.1 <| t.adj₂.left_triangle_components (F.obj X)]

Premises used: Iff.mpr, CategoryTheory.Iso.eq_comp_inv, CategoryTheory.Adjunction.Triple.adj₁, CategoryTheory.Iso.comp_hom_eq_id, CategoryTheory.Adjunction.unit, CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.whiskerRight_app, Iff.mp, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.Adjunction.Triple.adj₂, CategoryTheory.Adjunction.left_triangle_components, CategoryTheory.asIso
-- 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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    F.map
        ((t.adj₂.counit.app (obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ≫ t.adj₁.unit.app X) ≫
          G.map (t.adj₂.unit.app (F.obj X))) ≫
      t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)

Tactic:
simp
-- 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 : F.Full
inst_3 : F.Faithful
X : D
⊢ t.leftToRight.app (G.obj X) = t.adj₁.counit.app X ≫ t.adj₂.unit.app X

Tactic:
(((t.adj₂.homEquiv _ _).apply_symm_apply _).symm.trans ?_).symm

Premises used: Equiv.apply_symm_apply, CategoryTheory.Adjunction.homEquiv, Eq.symm, CategoryTheory.Adjunction.Triple.adj₂, Eq.trans
-- 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 : F.Full
inst_3 : F.Faithful
X : D
refine :
  Eq.{v_2 + 1} (α := F.obj (G.obj X) ⟶ H.obj (G.obj X))
    (((t.adj₂.homEquiv (F.obj (G.obj X)) (G.obj X) :
            Equiv.{v_1 + 1, v_2 + 1} (G.obj (F.obj (G.obj X)) ⟶ G.obj X) (F.obj (G.obj X) ⟶ H.obj (G.obj X))) :
          (a : G.obj (F.obj (G.obj X)) ⟶ G.obj X) → F.obj (G.obj X) ⟶ H.obj (G.obj X))
        (((Equiv.symm (t.adj₂.homEquiv (F.obj (G.obj X)) (G.obj X)) :
              Equiv.{v_2 + 1, v_1 + 1} (F.obj (G.obj X) ⟶ H.obj (G.obj X)) (G.obj (F.obj (G.obj X)) ⟶ G.obj X)) :
            (a : F.obj (G.obj X) ⟶ H.obj (G.obj X)) → G.obj (F.obj (G.obj X)) ⟶ G.obj X)
          (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)) :
      F.obj (G.obj X) ⟶ H.obj (G.obj X))
    (t.leftToRight.app (G.obj X) : F.obj (G.obj X) ⟶ H.obj (G.obj X))
⊢ t.leftToRight.app (G.obj X) = t.adj₁.counit.app X ≫ t.adj₂.unit.app X

Tactic:
refine (((t.adj₂.homEquiv _ _).apply_symm_apply _).symm.trans ?_).symm

Premises used: Equiv.apply_symm_apply, CategoryTheory.Adjunction.homEquiv, Eq.symm, CategoryTheory.Adjunction.Triple.adj₂, Eq.trans
-- 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 : F.Full
inst_3 : F.Faithful
X : D
rw :
  t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X)) =
    t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (inv (t.adj₁.unit.app (G.obj X)))
⊢ Eq.{v_2 + 1} (α := F.obj (G.obj X) ⟶ H.obj (G.obj X))
    (((t.adj₂.homEquiv (F.obj (G.obj X)) (G.obj X) :
            Equiv.{v_1 + 1, v_2 + 1} (G.obj (F.obj (G.obj X)) ⟶ G.obj X) (F.obj (G.obj X) ⟶ H.obj (G.obj X))) :
          (a : G.obj (F.obj (G.obj X)) ⟶ G.obj X) → F.obj (G.obj X) ⟶ H.obj (G.obj X))
        (((Equiv.symm (t.adj₂.homEquiv (F.obj (G.obj X)) (G.obj X)) :
              Equiv.{v_2 + 1, v_1 + 1} (F.obj (G.obj X) ⟶ H.obj (G.obj X)) (G.obj (F.obj (G.obj X)) ⟶ G.obj X)) :
            (a : F.obj (G.obj X) ⟶ H.obj (G.obj X)) → G.obj (F.obj (G.obj X)) ⟶ G.obj X)
          (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)) :
      F.obj (G.obj X) ⟶ H.obj (G.obj X))
    (t.leftToRight.app (G.obj X) : F.obj (G.obj X) ⟶ H.obj (G.obj X))

Tactic:
rw [homEquiv_symm_apply, map_comp, Category.assoc, left_triangle_components,
    homEquiv_apply, leftToRight_app, ← H.map_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_inv, CategoryTheory.Adjunction.homEquiv_apply, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.Triple.leftToRight_app, CategoryTheory.Adjunction.left_triangle_components, CategoryTheory.Adjunction.homEquiv_symm_apply
-- 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 : F.Full
inst_3 : F.Faithful
X : D
e_a : G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X) = inv (t.adj₁.unit.app (G.obj X))
⊢ t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X)) =
    t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (inv (t.adj₁.unit.app (G.obj X)))

Tactic:
congr
-- 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 : F.Full
inst_3 : F.Faithful
X : D
⊢ G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X) = inv (t.adj₁.unit.app (G.obj X))

Tactic:
simpa using IsIso.eq_inv_of_hom_inv_id (t.adj₁.right_triangle_components _)

Premises used: CategoryTheory.Adjunction.Triple.adj₁, CategoryTheory.IsIso.eq_inv_of_hom_inv_id, CategoryTheory.Adjunction.right_triangle_components
-- 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 : F.Full
inst_3 : F.Faithful
w : ∀ (X : D), (G.whiskerLeft t.leftToRight).app X = (t.adj₁.counit ≫ t.adj₂.unit).app X
⊢ G.whiskerLeft t.leftToRight = t.adj₁.counit ≫ t.adj₂.unit

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 : F.Full
inst_3 : F.Faithful
X : D
⊢ (G.whiskerLeft t.leftToRight).app X = (t.adj₁.counit ≫ t.adj₂.unit).app X

Tactic:
t.leftToRight_app_obj

Premises used: CategoryTheory.Adjunction.Triple.leftToRight_app_obj
-- 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 : F.Full
inst_3 : F.Faithful
X : D
⊢ (G.whiskerLeft t.leftToRight).app X = (t.adj₁.counit ≫ t.adj₂.unit).app X

Tactic:
exact t.leftToRight_app_obj

Premises used: CategoryTheory.Adjunction.Triple.leftToRight_app_obj
-- 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 : F.Full
inst_3 : F.Faithful
X : C
⊢ F.map (t.adj₂.counit.app X) ≫ t.leftToRight.app X = t.adj₁.counit.app (H.obj X)

Tactic:
simp
-- 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 : F.Full
inst_3 : F.Faithful
X : C
⊢ t.leftToRight.app X ≫ H.map (t.adj₁.unit.app X) = t.adj₂.unit.app (F.obj X)

Tactic:
simp [leftToRight_app]

Premises used: CategoryTheory.Adjunction.Triple.leftToRight_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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
w : ∀ (x : Cᵒᵖ), t.op.leftToRight.app x = (NatTrans.op t.leftToRight).app x
⊢ t.op.leftToRight = NatTrans.op t.leftToRight

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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
x : Cᵒᵖ
w :
  (H.op.rightUnitor.inv ≫
          H.op.whiskerLeft t.op.adj₂.unit ≫
            (H.op.associator G.op F.op).inv ≫ inv (whiskerRight t.op.adj₁.unit F.op) ≫ F.op.leftUnitor.hom).app
      x =
    (NatTrans.op
          (F.leftUnitor.inv ≫
            inv (whiskerRight t.adj₂.counit F) ≫
              (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.rightUnitor.hom)).app
      x
⊢ t.op.leftToRight.app x = (NatTrans.op t.leftToRight).app x

Tactic:
rw [leftToRight, leftToRight_eq_counits]

Premises used: CategoryTheory.Adjunction.Triple.leftToRight_eq_counits, CategoryTheory.Adjunction.Triple.leftToRight
-- 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 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
x : Cᵒᵖ
⊢ (H.op.rightUnitor.inv ≫
          H.op.whiskerLeft t.op.adj₂.unit ≫
            (H.op.associator G.op F.op).inv ≫ inv (whiskerRight t.op.adj₁.unit F.op) ≫ F.op.leftUnitor.hom).app
      x =
    (NatTrans.op
          (F.leftUnitor.inv ≫
            inv (whiskerRight t.adj₂.counit F) ≫
              (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.rightUnitor.hom)).app
      x

Tactic:
simp