awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
G : Functor.{v₁, v, u₁, u} D C
inst_2 : HasLimits.{v₁, u₁} D
inst_3 : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
A : C
ι : Type v₁
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ (i : ι) (g : B i ⟶ X), f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun (i : ι) ↦ StructuredArrow.mk (f i)
hB' : ∀ (A' : StructuredArrow A G), ∃ (i : ι), Nonempty.{v₁ + 1} (B' i ⟶ A')
T : StructuredArrow A G
hT : ∀ (X : StructuredArrow A G), Nonempty.{v₁ + 1} (T ⟶ X)
⊢ HasInitial (StructuredArrow A G)

Tactic:
apply hasInitial_of_weakly_initial_and_hasWideEqualizers hT

Premises used: CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers
-- Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : HasLimits.{v, u'} D
inst_3 : WellPowered.{v, v, u'} D
P : ObjectProperty.{v, u'} D
inst_4 : ObjectProperty.Small.{v, v, u'} P
hP : P.IsCoseparating
G : Functor.{v, v, u', u} D C
inst_5 : PreservesLimits G
⊢ ∀ (A : C), HasInitial (StructuredArrow A G)

Tactic:
have : ∀ A, HasInitial (StructuredArrow A G) := fun A ↦
    hasInitial_of_isCoseparating.{v} (StructuredArrow.isCoseparating_inverseImage_proj A G hP)
-- Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : HasLimits.{v, u'} D
inst_3 : WellPowered.{v, v, u'} D
P : ObjectProperty.{v, u'} D
inst_4 : ObjectProperty.Small.{v, v, u'} P
hP : P.IsCoseparating
G : Functor.{v, v, u', u} D C
inst_5 : PreservesLimits G
this : ∀ (A : C), HasInitial (StructuredArrow A G)
⊢ G.IsRightAdjoint

Tactic:
isRightAdjointOfStructuredArrowInitials _

Premises used: CategoryTheory.isRightAdjointOfStructuredArrowInitials
-- Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : HasLimits.{v, u'} D
inst_3 : WellPowered.{v, v, u'} D
P : ObjectProperty.{v, u'} D
inst_4 : ObjectProperty.Small.{v, v, u'} P
hP : P.IsCoseparating
G : Functor.{v, v, u', u} D C
inst_5 : PreservesLimits G
this : ∀ (A : C), HasInitial (StructuredArrow A G)
⊢ G.IsRightAdjoint

Tactic:
exact isRightAdjointOfStructuredArrowInitials _

Premises used: CategoryTheory.isRightAdjointOfStructuredArrowInitials
-- Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : HasColimits.{v, u} C
inst_3 : WellPowered.{v, v, u} Cᵒᵖ
P : ObjectProperty.{v, u} C
inst_4 : ObjectProperty.Small.{v, v, u} P
h𝒢 : P.IsSeparating
F : Functor.{v, v, u, u'} C D
inst_5 : PreservesColimits F
⊢ F.IsLeftAdjoint

Tactic:
have : ∀ A, HasTerminal (CostructuredArrow F A) := fun A =>
    hasTerminal_of_isSeparating.{v} (CostructuredArrow.isSeparating_inverseImage_proj F A h𝒢)
  isLeftAdjoint_of_costructuredArrowTerminals _

Premises used: CategoryTheory.CostructuredArrow.isSeparating_inverseImage_proj, CategoryTheory.hasTerminal_of_isSeparating, CategoryTheory.isLeftAdjoint_of_costructuredArrowTerminals
-- Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
inst_2 : WellPowered.{v, v, u} C
P : ObjectProperty.{v, u} C
inst_3 : ObjectProperty.Small.{v, v, u} P
hP : P.IsCoseparating
⊢ HasColimits.{v, u} C

Tactic:
{ has_colimits_of_shape := fun _ _ =>
      hasColimitsOfShape_iff_isRightAdjoint_const.2
        (isRightAdjoint_of_preservesLimits_of_isCoseparating hP _) }

Premises used: Iff.mpr, CategoryTheory.Limits.hasColimitsOfShape_iff_isRightAdjoint_const, CategoryTheory.Limits.HasColimitsOfSize.mk, CategoryTheory.isRightAdjoint_of_preservesLimits_of_isCoseparating, CategoryTheory.Functor.const
-- Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
inst_2 : WellPowered.{v, v, u} Cᵒᵖ
P : ObjectProperty.{v, u} C
inst_3 : ObjectProperty.Small.{v, v, u} P
hP : P.IsSeparating
⊢ HasLimits.{v, u} C

Tactic:
{ has_limits_of_shape := fun _ _ =>
      hasLimitsOfShape_iff_isLeftAdjoint_const.2
        (isLeftAdjoint_of_preservesColimits_of_isSeparating hP _) }

Premises used: Iff.mpr, CategoryTheory.Limits.hasLimitsOfShape_iff_isLeftAdjoint_const, CategoryTheory.Limits.HasLimitsOfSize.mk, CategoryTheory.isLeftAdjoint_of_preservesColimits_of_isSeparating, CategoryTheory.Functor.const
-- Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
inst_2 : HasSeparator.{v, u} C
inst_3 : WellPowered.{v, v, u} Cᵒᵖ
⊢ HasLimits.{v, u} C

Tactic:
hasLimits_of_hasColimits_of_isSeparating <| isSeparator_separator C

Premises used: CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparating, CategoryTheory.isSeparator_separator
-- Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
inst_2 : HasCoseparator.{v, u} C
inst_3 : WellPowered.{v, v, u} C
⊢ HasColimits.{v, u} C

Tactic:
hasColimits_of_hasLimits_of_isCoseparating <| isCoseparator_coseparator C

Premises used: CategoryTheory.isCoseparator_coseparator, CategoryTheory.Limits.hasColimits_of_hasLimits_of_isCoseparating
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
X : C
Y : D
f : F.obj X ⟶ Y
dsimp : F.map (adj.unit.app X ≫ G.map f) ≫ adj.counit.app Y = f
⊢ (fun (g : X ⟶ G.obj Y) ↦ F.map g ≫ adj.counit.app Y) ((fun (f : F.obj X ⟶ Y) ↦ adj.unit.app X ≫ G.map f) f) = f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X)) ≫ map (𝟭 D) f = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
X : C
Y : D
g : X ⟶ G.obj Y
simp : adj.unit.app X ≫ G.map (F.map g) ≫ G.map (adj.counit.app Y) = g
⊢ (fun (f : F.obj X ⟶ Y) ↦ adj.unit.app X ≫ G.map f) ((fun (g : X ⟶ G.obj Y) ↦ F.map g ≫ adj.counit.app Y) g) = g

Tactic:
simp only [Functor.comp_obj, Functor.map_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
X : C
Y : D
g : X ⟶ G.obj Y
rw : (map (𝟭 C) g ≫ adj.unit.app (G.obj Y)) ≫ G.map (adj.counit.app Y) = g
⊢ adj.unit.app X ≫ G.map (F.map g) ≫ G.map (adj.counit.app Y) = g

Tactic:
rw [← assoc, ← Functor.comp_map, ← adj.unit.naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.unit, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
X : C
Y : D
g : X ⟶ G.obj Y
⊢ (map (𝟭 C) g ≫ adj.unit.app (G.obj Y)) ≫ G.map (adj.counit.app Y) = g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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 adj' : F ⊣ G
h : adj.unit = adj'.unit
h' : adj.counit = adj'.counit
mk :
  ∀ (unit : 𝟭 C ⟶ F ⋙ G) (counit : G ⋙ F ⟶ 𝟭 D)
    (left_triangle_components : ∀ (X : C), F.map (unit.app X) ≫ counit.app (F.obj X) = 𝟙 (F.obj X))
    (right_triangle_components : ∀ (Y : D), unit.app (G.obj Y) ≫ G.map (counit.app Y) = 𝟙 (G.obj Y))
    (h :
      { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
            right_triangle_components := right_triangle_components : F ⊣ G }.unit =
        adj'.unit)
    (h' :
      { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
            right_triangle_components := right_triangle_components : F ⊣ G }.counit =
        adj'.counit),
    { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
        right_triangle_components := right_triangle_components : F ⊣ G } =
      adj'
⊢ adj = adj'

Tactic:
cases adj
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
unit : 𝟭 C ⟶ F ⋙ G
counit : G ⋙ F ⟶ 𝟭 D
left_triangle_components : ∀ (X : C), F.map (unit.app X) ≫ counit.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components : ∀ (Y : D), unit.app (G.obj Y) ≫ G.map (counit.app Y) = 𝟙 (G.obj Y)
h :
  { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
        right_triangle_components := right_triangle_components : F ⊣ G }.unit =
    adj'.unit
h' :
  { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
        right_triangle_components := right_triangle_components : F ⊣ G }.counit =
    adj'.counit
mk :
  ∀ (unit_1 : 𝟭 C ⟶ F ⋙ G) (counit_1 : G ⋙ F ⟶ 𝟭 D)
    (left_triangle_components_1 : ∀ (X : C), F.map (unit_1.app X) ≫ counit_1.app (F.obj X) = 𝟙 (F.obj X))
    (right_triangle_components_1 : ∀ (Y : D), unit_1.app (G.obj Y) ≫ G.map (counit_1.app Y) = 𝟙 (G.obj Y))
    (h :
      { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
            right_triangle_components := right_triangle_components : F ⊣ G }.unit =
        { unit := unit_1, counit := counit_1, left_triangle_components := left_triangle_components_1,
            right_triangle_components := right_triangle_components_1 }.unit)
    (h' :
      { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
            right_triangle_components := right_triangle_components : F ⊣ G }.counit =
        { unit := unit_1, counit := counit_1, left_triangle_components := left_triangle_components_1,
            right_triangle_components := right_triangle_components_1 }.counit),
    { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
        right_triangle_components := right_triangle_components : F ⊣ G } =
      { unit := unit_1, counit := counit_1, left_triangle_components := left_triangle_components_1,
        right_triangle_components := right_triangle_components_1 }
⊢ { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
      right_triangle_components := right_triangle_components : F ⊣ G } =
    adj'

Tactic:
cases adj'
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
unit : 𝟭 C ⟶ F ⋙ G
counit : G ⋙ F ⟶ 𝟭 D
left_triangle_components : ∀ (X : C), F.map (unit.app X) ≫ counit.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components : ∀ (Y : D), unit.app (G.obj Y) ≫ G.map (counit.app Y) = 𝟙 (G.obj Y)
unit_1 : 𝟭 C ⟶ F ⋙ G
counit_1 : G ⋙ F ⟶ 𝟭 D
left_triangle_components_1 : ∀ (X : C), F.map (unit_1.app X) ≫ counit_1.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components_1 : ∀ (Y : D), unit_1.app (G.obj Y) ≫ G.map (counit_1.app Y) = 𝟙 (G.obj Y)
h :
  { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
        right_triangle_components := right_triangle_components : F ⊣ G }.unit =
    { unit := unit_1, counit := counit_1, left_triangle_components := left_triangle_components_1,
        right_triangle_components := right_triangle_components_1 }.unit
h' :
  { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
        right_triangle_components := right_triangle_components : F ⊣ G }.counit =
    { unit := unit_1, counit := counit_1, left_triangle_components := left_triangle_components_1,
        right_triangle_components := right_triangle_components_1 }.counit
⊢ { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
      right_triangle_components := right_triangle_components : F ⊣ G } =
    { unit := unit_1, counit := counit_1, left_triangle_components := left_triangle_components_1,
      right_triangle_components := right_triangle_components_1 }

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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 adj' : F ⊣ G
h : adj.unit = adj'.unit
suffices : adj.counit = adj'.counit
⊢ adj = adj'

Tactic:
suffices h' : adj.counit = adj'.counit by cases adj; cases adj'; aesop
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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 adj' : F ⊣ G
h : adj.unit = adj'.unit
w : ∀ (X : D), adj.counit.app X = adj'.counit.app X
⊢ adj.counit = adj'.counit

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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 adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
w :
  Eq.{v₁ + 1} (α := G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
    (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
              (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
          (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
        (adj.counit.app X) :
      G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
    (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
              (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
          (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
        (adj'.counit.app X) :
      G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
⊢ adj.counit.app X = adj'.counit.app X

Tactic:
apply (adj.homEquiv _ _).injective

Premises used: CategoryTheory.Adjunction.homEquiv, Equiv.injective
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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 adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
w :
  adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) =
    ((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
          Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
            (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
        (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
      (adj'.counit.app X)
w₁ : adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) = adj.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)
w₂ : 𝟙 (G.obj X) = adj.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)
w₃ : 𝟙 (G.obj X) = adj'.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)
w₄ w₅ : Eq.{v₁ + 1} (α := G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)) (𝟙 (G.obj X)) (𝟙 (G.obj X))
⊢ Eq.{v₁ + 1} (α := G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
    (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
              (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
          (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
        (adj.counit.app X) :
      G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
    (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
              (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
          (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
        (adj'.counit.app X) :
      G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))

Tactic:
rw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit,
    Adjunction.right_triangle_components, h, Adjunction.right_triangle_components]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.Adjunction.right_triangle_components
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
⊢ F.IsLeftAdjoint

Tactic:
⟨_, ⟨adj⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
⊢ G.IsRightAdjoint

Tactic:
⟨_, ⟨adj⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : R.IsRightAdjoint
⊢ R.leftAdjoint.IsLeftAdjoint

Tactic:
(ofIsRightAdjoint R).isLeftAdjoint

Premises used: CategoryTheory.Adjunction.isLeftAdjoint, CategoryTheory.Adjunction.ofIsRightAdjoint
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLeftAdjoint
⊢ L.rightAdjoint.IsRightAdjoint

Tactic:
(ofIsLeftAdjoint L).isRightAdjoint

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.Adjunction.isRightAdjoint
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
X : C
⊢ ((adj.homEquiv X (F.obj X) : Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ F.obj X) (X ⟶ G.obj (F.obj X))) :
        (a : F.obj X ⟶ F.obj X) → X ⟶ G.obj (F.obj X))
      (𝟙 (F.obj X)) =
    adj.unit.app X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
X : D
⊢ ((Equiv.symm (adj.homEquiv (G.obj X) X) : Equiv.{v₁ + 1, v₂ + 1} (G.obj X ⟶ G.obj X) (F.obj (G.obj X) ⟶ X)) :
        (a : G.obj X ⟶ G.obj X) → F.obj (G.obj X) ⟶ X)
      (𝟙 (G.obj X)) =
    adj.counit.app X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
X : C
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj X)
    (((Equiv.symm (adj.homEquiv X (F.obj X)) : Equiv.{v₁ + 1, v₂ + 1} (X ⟶ G.obj (F.obj X)) (F.obj X ⟶ F.obj X)) :
          (a : X ⟶ G.obj (F.obj X)) → F.obj X ⟶ F.obj X)
        (adj.unit.app X) :
      F.obj X ⟶ F.obj X)
    (𝟙 (F.obj X) : F.obj X ⟶ F.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
⊢ Eq.{v₂ + 1} (α := F.obj X' ⟶ Y)
    (((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y) (f ≫ g) : F.obj X' ⟶ Y)
    (F.map f ≫ ((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) g : F.obj X' ⟶ Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
rw :
  F.map f ≫ g =
    ((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y)
      (f ≫ (adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g)
⊢ Eq.{v₁ + 1} (α := X' ⟶ G.obj Y) ((adj.homEquiv X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G.obj Y) (F.map f ≫ g) : X' ⟶ G.obj Y)
    (f ≫ (adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g : X' ⟶ G.obj Y)

Tactic:
rw [← Equiv.eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g =
    ((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y)
      (f ≫ (adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g)

Tactic:
simp only [Equiv.symm_apply_apply, homEquiv_naturality_left_symm]

Premises used: Equiv.symm_apply_apply, CategoryTheory.Adjunction.homEquiv_naturality_left_symm
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
X : C
Y Y' : D
f : F.obj X ⟶ Y
g : Y ⟶ Y'
⊢ Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((adj.homEquiv X Y' : (a : F.obj X ⟶ Y') → X ⟶ G.obj Y') (f ≫ g) : X ⟶ G.obj Y')
    ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) f ≫ G.map g : X ⟶ G.obj Y')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
rw :
  f ≫ G.map g =
    (adj.homEquiv X Y' : (a : F.obj X ⟶ Y') → X ⟶ G.obj Y')
      (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f ≫ g)
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ Y')
    (((adj.homEquiv X Y').symm : (a : X ⟶ G.obj Y') → F.obj X ⟶ Y') (f ≫ G.map g) : F.obj X ⟶ Y')
    (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f ≫ g : F.obj X ⟶ Y')

Tactic:
rw [Equiv.symm_apply_eq]

Premises used: Equiv.symm_apply_eq
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
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
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g =
    (adj.homEquiv X Y' : (a : F.obj X ⟶ Y') → X ⟶ G.obj Y')
      (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f ≫ g)

Tactic:
simp only [homEquiv_naturality_right, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, CategoryTheory.Adjunction.homEquiv_naturality_right