awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
Q : Functor.{v₁, v₂, u₁, u₂} A B
V : Functor.{v₂, v₄, u₂, u₄} B D
U : Functor.{v₁, v₃, u₁, u₃} A C
L : Functor.{v₃, v₄, u₃, u₄} C D
comm : U ⋙ L ≅ Q ⋙ V
inst_4 : U.IsLeftAdjoint
inst_5 : ComonadicLeftAdjoint V
inst_6 : L.IsLeftAdjoint
inst_7 : HasCoreflexiveEqualizers.{v₁, u₁} A
⊢ Q.IsLeftAdjoint

Tactic:
have := ((Adjunction.ofIsLeftAdjoint (U ⋙ L)).ofNatIsoLeft comm).isLeftAdjoint
  isLeftAdjoint_triangle_lift_comonadic V

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.isLeftAdjoint, CategoryTheory.isLeftAdjoint_triangle_lift_comonadic, CategoryTheory.Adjunction.ofNatIsoLeft
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₁, u, u₁} J C
inst_3 : HasColimitsOfShape.{v, u, v₁, u₁} J C
⊢ PreservesColimits (C := Functor.{v, v₁, u, u₁} J C) colim

Tactic:
colimConstAdj.leftAdjoint_preservesColimits

Premises used: CategoryTheory.Adjunction.leftAdjoint_preservesColimits, CategoryTheory.Limits.colimConstAdj
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₁, u, u₁} J C
E : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : E.IsEquivalence
⊢ PreservesColimitsOfSize.{v, u, v₁, v₂, u₁, u₂} E

Tactic:
leftAdjoint_preservesColimits E.adjunction

Premises used: CategoryTheory.Functor.adjunction, CategoryTheory.Adjunction.leftAdjoint_preservesColimits
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₁, u, u₁} J C
E : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : E.IsEquivalence
inst_4 : HasColimit K
⊢ HasColimit (K ⋙ E)

Tactic:
HasColimit.mk
    { cocone := E.mapCocone (colimit.cocone K)
      isColimit := isColimitOfPreserves _ (colimit.isColimit K) }

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₁, u, u₁} J C
E : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : E.IsEquivalence
inst_4 : HasColimit (K ⋙ E)
rw : HasColimit (K ⋙ E.asEquivalence.functor ⋙ E.asEquivalence.inverse)
⊢ HasColimit K

Tactic:
rw [hasColimit_iff_of_iso
    ((Functor.rightUnitor _).symm ≪≫ isoWhiskerLeft K E.asEquivalence.unitIso)]

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Limits.hasColimit_iff_of_iso, CategoryTheory.Functor.rightUnitor, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₁, u, u₁} J C
E : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : E.IsEquivalence
inst_4 : HasColimit (K ⋙ E)
⊢ HasColimit (K ⋙ E.asEquivalence.functor ⋙ E.asEquivalence.inverse)

Tactic:
hasColimit_comp_equivalence (K ⋙ E) E.inv

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.Functor.comp, CategoryTheory.Functor.objPreimage, Classical.choose, CategoryTheory.Functor.inv, CategoryTheory.Adjunction.hasColimit_comp_equivalence, CategoryTheory.Functor.essImage.witness
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₁, u, u₁} J C
E : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : E.IsEquivalence
inst_4 : HasColimit (K ⋙ E)
⊢ HasColimit (K ⋙ E.asEquivalence.functor ⋙ E.asEquivalence.inverse)

Tactic:
exact hasColimit_comp_equivalence (K ⋙ E) E.inv

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.inv, CategoryTheory.Adjunction.hasColimit_comp_equivalence
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
E : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : E.IsEquivalence
inst_4 : HasColimitsOfShape.{v, u, v₂, u₂} J D
⊢ HasColimitsOfShape.{v, u, v₁, u₁} J C

Tactic:
⟨fun F => hasColimit_of_comp_equivalence F E⟩

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.Adjunction.hasColimit_of_comp_equivalence
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : E.IsEquivalence
inst_3 : HasColimitsOfSize.{v, u, v₂, u₂} D
⊢ HasColimitsOfSize.{v, u, v₁, u₁} C

Tactic:
⟨fun _ _ => hasColimitsOfShape_of_equivalence E⟩

Premises used: CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence, CategoryTheory.Limits.HasColimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₂, u, u₂} J D
inst_3 : HasLimitsOfShape.{v, u, v₁, u₁} J C
⊢ PreservesLimits (C := Functor.{v, v₁, u, u₁} J C) lim

Tactic:
constLimAdj.rightAdjoint_preservesLimits

Premises used: CategoryTheory.Adjunction.rightAdjoint_preservesLimits, CategoryTheory.Limits.constLimAdj
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₂, u, u₂} J D
E : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : E.IsEquivalence
⊢ PreservesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E

Tactic:
rightAdjoint_preservesLimits E.asEquivalence.symm.toAdjunction

Premises used: CategoryTheory.Functor.asEquivalence, CategoryTheory.Adjunction.rightAdjoint_preservesLimits, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₂, u, u₂} J D
E : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : E.IsEquivalence
inst_4 : HasLimit K
⊢ HasLimit (K ⋙ E)

Tactic:
HasLimit.mk
    { cone := E.mapCone (limit.cone K)
      isLimit := isLimitOfPreserves _ (limit.isLimit K) }

Premises used: CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Functor.mapCone, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₂, u, u₂} J D
E : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : E.IsEquivalence
inst_4 : HasLimit (K ⋙ E)
rw : HasLimit (K ⋙ E.asEquivalence.functor ⋙ E.asEquivalence.inverse)
⊢ HasLimit K

Tactic:
rw [← hasLimit_iff_of_iso
    (isoWhiskerLeft K E.asEquivalence.unitIso.symm ≪≫ Functor.rightUnitor _)]

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Limits.hasLimit_iff_of_iso, CategoryTheory.Functor.rightUnitor, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₂, u, u₂} J D
E : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : E.IsEquivalence
inst_4 : HasLimit (K ⋙ E)
⊢ HasLimit (K ⋙ E.asEquivalence.functor ⋙ E.asEquivalence.inverse)

Tactic:
hasLimit_comp_equivalence (K ⋙ E) E.inv

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.Functor.comp, CategoryTheory.Functor.objPreimage, CategoryTheory.Adjunction.hasLimit_comp_equivalence, Classical.choose, CategoryTheory.Functor.inv, CategoryTheory.Functor.essImage.witness
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₂, u, u₂} J D
E : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : E.IsEquivalence
inst_4 : HasLimit (K ⋙ E)
⊢ HasLimit (K ⋙ E.asEquivalence.functor ⋙ E.asEquivalence.inverse)

Tactic:
exact hasLimit_comp_equivalence (K ⋙ E) E.inv

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Adjunction.hasLimit_comp_equivalence, CategoryTheory.Functor.inv
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
E : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : E.IsEquivalence
inst_4 : HasLimitsOfShape.{v, u, v₁, u₁} J C
⊢ HasLimitsOfShape.{v, u, v₂, u₂} J D

Tactic:
⟨fun F => hasLimit_of_comp_equivalence F E⟩

Premises used: CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Adjunction.hasLimit_of_comp_equivalence
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : E.IsEquivalence
inst_3 : HasLimitsOfSize.{v, u, v₁, u₁} C
⊢ HasLimitsOfSize.{v, u, v₂, u₂} D

Tactic:
⟨fun _ _ => hasLimitsOfShape_of_equivalence E⟩

Premises used: CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence, CategoryTheory.Limits.HasLimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₁, u, u₁} J C
Y : D
t : (obj (cocones J D) (op (K ⋙ F))).obj Y
j j' : J
f : j ⟶ j'
rw :
  Eq.{v₁ + 1} (α := (unop (op (unop (op K)))).obj j ⟶ obj.{v, v₁, u, u₁} (obj (const J) (G.obj Y)) j')
    (((adj.homEquiv ((unop (op (unop (op K)))).obj j) Y :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj ((unop (op (unop (op K)))).obj j) ⟶ Y)
              ((unop (op (unop (op K)))).obj j ⟶ G.obj Y)) :
          (a : F.obj ((unop (op (unop (op K)))).obj j) ⟶ Y) → (unop (op (unop (op K)))).obj j ⟶ G.obj Y)
        (t.app j ≫ map (obj (const J) Y) f) :
      (unop (op (unop (op K)))).obj j ⟶ G.obj Y)
    (((adj.homEquiv (K.obj j) Y : Equiv.{v₂ + 1, v₁ + 1} (F.obj (K.obj j) ⟶ Y) (K.obj j ⟶ G.obj Y)) :
            (a : F.obj (K.obj j) ⟶ Y) → K.obj j ⟶ G.obj Y)
          (t.app j) ≫
        map (obj (const J) (G.obj Y)) f :
      (unop (op (unop (op K)))).obj j ⟶ obj.{v, v₁, u, u₁} (obj (const J) (G.obj Y)) j')
⊢ Eq (α := (unop (op (unop (op K)))).obj j ⟶ obj.{v, v₁, u, u₁} (obj (const J) (G.obj Y)) j')
    ((unop (op (unop (op K)))).map f ≫
      ((adj.homEquiv (K.obj j') Y : Equiv.{v₂ + 1, v₁ + 1} (F.obj (K.obj j') ⟶ Y) (K.obj j' ⟶ G.obj Y)) :
          (a : F.obj (K.obj j') ⟶ Y) → K.obj j' ⟶ G.obj Y)
        (t.app j'))
    (((adj.homEquiv (K.obj j) Y : Equiv.{v₂ + 1, v₁ + 1} (F.obj (K.obj j) ⟶ Y) (K.obj j ⟶ G.obj Y)) :
          (a : F.obj (K.obj j) ⟶ Y) → K.obj j ⟶ G.obj Y)
        (t.app j) ≫
      map (obj (const J) (G.obj Y)) f)

Tactic:
rw [← adj.homEquiv_naturality_left, ← Functor.comp_map, t.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.comp_map, CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₁, u, u₁} J C
Y : D
t : (obj (cocones J D) (op (K ⋙ F))).obj Y
j j' : J
f : j ⟶ j'
⊢ Eq.{v₁ + 1} (α := (unop (op (unop (op K)))).obj j ⟶ obj.{v, v₁, u, u₁} (obj (const J) (G.obj Y)) j')
    (((adj.homEquiv ((unop (op (unop (op K)))).obj j) Y :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj ((unop (op (unop (op K)))).obj j) ⟶ Y)
              ((unop (op (unop (op K)))).obj j ⟶ G.obj Y)) :
          (a : F.obj ((unop (op (unop (op K)))).obj j) ⟶ Y) → (unop (op (unop (op K)))).obj j ⟶ G.obj Y)
        (t.app j ≫ map (obj (const J) Y) f) :
      (unop (op (unop (op K)))).obj j ⟶ G.obj Y)
    (((adj.homEquiv (K.obj j) Y : Equiv.{v₂ + 1, v₁ + 1} (F.obj (K.obj j) ⟶ Y) (K.obj j ⟶ G.obj Y)) :
            (a : F.obj (K.obj j) ⟶ Y) → K.obj j ⟶ G.obj Y)
          (t.app j) ≫
        map (obj (const J) (G.obj Y)) f :
      (unop (op (unop (op K)))).obj j ⟶ obj.{v, v₁, u, u₁} (obj (const J) (G.obj Y)) j')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₁, u, u₁} J C
Y : D
t : (G ⋙ obj (cocones J C) (op K)).obj Y
j j' : J
f : j ⟶ j'
⊢ Eq.{v₂ + 1} (α := (unop (op (unop (op (K ⋙ F))))).obj j ⟶ obj.{v, v₂, u, u₂} (obj (const J) Y) j')
    (((Equiv.symm (adj.homEquiv (K.obj j) (obj.{v, v₂, u, u₂} (obj (const J) Y) j')) :
            Equiv.{v₁ + 1, v₂ + 1} (K.obj j ⟶ G.obj (obj.{v, v₂, u, u₂} (obj (const J) Y) j'))
              (F.obj (K.obj j) ⟶ obj.{v, v₂, u, u₂} (obj (const J) Y) j')) :
          (a : K.obj j ⟶ G.obj (((const J).obj Y).obj j')) → F.obj (K.obj j) ⟶ ((const J).obj Y).obj j')
        (t.app j ≫ map (obj (const J) (G.obj Y)) f) :
      F.obj (K.obj j) ⟶ obj.{v, v₂, u, u₂} (obj (const J) Y) j')
    (((Equiv.symm (adj.homEquiv (K.obj j) (obj.{v, v₂, u, u₂} (obj (const J) Y) j')) :
            Equiv.{v₁ + 1, v₂ + 1} (K.obj j ⟶ G.obj (obj.{v, v₂, u, u₂} (obj (const J) Y) j'))
              (F.obj (K.obj j) ⟶ obj.{v, v₂, u, u₂} (obj (const J) Y) j')) :
          (a : K.obj j ⟶ G.obj (((const J).obj Y).obj j')) → F.obj (K.obj j) ⟶ ((const J).obj Y).obj j')
        (t.app j ≫ G.map (map (obj (const J) Y) f)) :
      F.obj (K.obj j) ⟶ obj.{v, v₂, u, u₂} (obj (const J) Y) j')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₂, u, u₂} J D
X : Cᵒᵖ
t : (F.op ⋙ obj (cones J D) K).obj X
j j' : J
f : j ⟶ j'
erw :
  Eq.{v₁ + 1} (α := obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j ⟶ (K ⋙ G).obj j')
    (((adj.homEquiv (unop X) (K.obj j') :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (unop X) ⟶ K.obj j') (unop X ⟶ G.obj (K.obj j'))) :
          (a : F.obj (unop X) ⟶ K.obj j') → unop X ⟶ G.obj (K.obj j'))
        (t.app j') :
      unop X ⟶ G.obj (K.obj j'))
    (((adj.homEquiv (obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j) (K.obj j') :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j) ⟶ K.obj j')
              (obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j ⟶ G.obj (K.obj j'))) :
          (a : F.obj ((unop ((const J).op.obj X)).obj j) ⟶ K.obj j') →
            (unop ((const J).op.obj X)).obj j ⟶ G.obj (K.obj j'))
        (t.app j') :
      obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j ⟶ G.obj (K.obj j'))
⊢ Eq.{v₁ + 1} (α := obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j ⟶ (K ⋙ G).obj j')
    (map (unop (obj (Functor.op (const J)) X)) f ≫
      ((adj.homEquiv (unop X) (K.obj j') :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (unop X) ⟶ K.obj j') (unop X ⟶ G.obj (K.obj j'))) :
          (a : F.obj (unop X) ⟶ K.obj j') → unop X ⟶ G.obj (K.obj j'))
        (t.app j'))
    (((adj.homEquiv (unop X) (K.obj j) : Equiv.{v₂ + 1, v₁ + 1} (F.obj (unop X) ⟶ K.obj j) (unop X ⟶ G.obj (K.obj j))) :
          (a : F.obj (unop X) ⟶ K.obj j) → unop X ⟶ G.obj (K.obj j))
        (t.app j) ≫
      (K ⋙ G).map f)

Tactic:
erw [← adj.homEquiv_naturality_right, ← t.naturality, Category.id_comp, Category.id_comp]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Adjunction.homEquiv_naturality_right, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₂, u, u₂} J D
X : Cᵒᵖ
t : (F.op ⋙ obj (cones J D) K).obj X
j j' : J
f : j ⟶ j'
⊢ Eq.{v₁ + 1} (α := obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j ⟶ (K ⋙ G).obj j')
    (((adj.homEquiv (unop X) (K.obj j') :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (unop X) ⟶ K.obj j') (unop X ⟶ G.obj (K.obj j'))) :
          (a : F.obj (unop X) ⟶ K.obj j') → unop X ⟶ G.obj (K.obj j'))
        (t.app j') :
      unop X ⟶ G.obj (K.obj j'))
    (((adj.homEquiv (obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j) (K.obj j') :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j) ⟶ K.obj j')
              (obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j ⟶ G.obj (K.obj j'))) :
          (a : F.obj ((unop ((const J).op.obj X)).obj j) ⟶ K.obj j') →
            (unop ((const J).op.obj X)).obj j ⟶ G.obj (K.obj j'))
        (t.app j') :
      obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j ⟶ G.obj (K.obj j'))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
F : Functor.{v_2, v_3, u_2, u_3} C D
inst_3 : F.IsLeftAdjoint
⊢ PreservesColimitsOfShape.{v_1, u_1, v_2, v_3, u_2, u_3} J F

Tactic:
(Adjunction.ofIsLeftAdjoint F).leftAdjoint_preservesColimits.preservesColimitsOfShape

Premises used: CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape
-- Module: Mathlib.CategoryTheory.Adjunction.Limits
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
F : Functor.{v_2, v_3, u_2, u_3} C D
inst_3 : F.IsRightAdjoint
⊢ PreservesLimitsOfShape.{v_1, u_1, v_2, v_3, u_2, u_3} J F

Tactic:
(Adjunction.ofIsRightAdjoint F).rightAdjoint_preservesLimits.preservesLimitsOfShape

Premises used: CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
h :
  ∀ (X : C),
    app
        (natTrans
          ((fun (β : TwoSquare R₁ H G R₂) ↦
              TwoSquare.mk G L₁ L₂ H
                ((G ⋙ L₂).leftUnitor.inv ≫
                  whiskerRight adj₁.unit (G ⋙ L₂) ≫
                    ((L₁ ⋙ R₁).associator G L₂).inv ≫
                      whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                        whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                          whiskerRight (L₁.associator H R₂).inv L₂ ≫
                            ((L₁ ⋙ H).associator R₂ L₂).hom ≫
                              (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
            ((fun (α : TwoSquare G L₁ L₂ H) ↦
                TwoSquare.mk R₁ H G R₂
                  ((R₁ ⋙ G).rightUnitor.inv ≫
                    (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                      (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                        R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                          R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                            R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                              (R₁.associator L₁ (H ⋙ R₂)).inv ≫
                                whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
              α)))
        X =
      α.natTrans.app X
⊢ (fun (β : TwoSquare R₁ H G R₂) ↦
        TwoSquare.mk G L₁ L₂ H
          ((G ⋙ L₂).leftUnitor.inv ≫
            whiskerRight adj₁.unit (G ⋙ L₂) ≫
              ((L₁ ⋙ R₁).associator G L₂).inv ≫
                whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                  whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                    whiskerRight (L₁.associator H R₂).inv L₂ ≫
                      ((L₁ ⋙ H).associator R₂ L₂).hom ≫ (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
      ((fun (α : TwoSquare G L₁ L₂ H) ↦
          TwoSquare.mk R₁ H G R₂
            ((R₁ ⋙ G).rightUnitor.inv ≫
              (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                  R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                    R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                      R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                        (R₁.associator L₁ (H ⋙ R₂)).inv ≫ whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
        α) =
    α

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X : C
h : α.natTrans.app X ≫ 𝟙 (H.obj (L₁.obj X)) = α.natTrans.app X
⊢ L₂.map (G.map (adj₁.unit.app X)) ≫ α.natTrans.app (R₁.obj (L₁.obj X)) ≫ H.map (adj₁.counit.app (L₁.obj X)) =
    α.natTrans.app X

Tactic:
rw [← assoc, ← Functor.comp_map, α.natTrans.naturality, Functor.comp_map, assoc, ← H.map_comp,
      left_triangle_components, map_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.TwoSquare.natTrans, CategoryTheory.Functor.comp_map, CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X : C
⊢ α.natTrans.app X ≫ 𝟙 (H.obj (L₁.obj X)) = α.natTrans.app X

Tactic:
simp only [comp_obj, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.comp_id