awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : G.Additive
X Y : C
f g : X ⟶ Y
⊢ Eq.{v₁ + 1} (α := X ⟶ G.obj (F.obj Y))
    (((adj.homEquiv X (F.obj Y) : Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ F.obj Y) (X ⟶ G.obj (F.obj Y))) :
          (a : F.obj X ⟶ F.obj Y) → X ⟶ G.obj (F.obj Y))
        (F.map (f + g)) :
      X ⟶ G.obj (F.obj Y))
    (((adj.homEquiv X (F.obj Y) : Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ F.obj Y) (X ⟶ G.obj (F.obj Y))) :
          (a : F.obj X ⟶ F.obj Y) → X ⟶ G.obj (F.obj Y))
        (F.map f + F.map g) :
      X ⟶ G.obj (F.obj Y))

Tactic:
simp [homEquiv_unit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : C
Y : D
x x_1 : F.obj X ⟶ Y
⊢ G.Additive

Tactic:
have := adj.right_adjoint_additive
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : C
Y : D
x x_1 : F.obj X ⟶ Y
this : G.Additive
⊢ (adj.homEquiv X Y).toFun (x + x_1) = (adj.homEquiv X Y).toFun x + (adj.homEquiv X Y).toFun x_1

Tactic:
simp [homEquiv_apply]

Premises used: CategoryTheory.Adjunction.homEquiv_apply
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : C
Y : D
f : F.obj X ⟶ Y
⊢ Eq.{v₁ + 1} (α := X ⟶ G.obj Y)
    (((adj.homAddEquiv X Y : AddEquiv.{v₂, v₁} (F.obj X ⟶ Y) (X ⟶ G.obj Y)) : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) f :
      X ⟶ G.obj Y)
    ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) f : X ⟶ G.obj Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : C
Y : D
f : X ⟶ G.obj Y
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ Y)
    (((AddEquiv.symm (adj.homAddEquiv X Y) : AddEquiv.{v₁, v₂} (X ⟶ G.obj Y) (F.obj X ⟶ Y)) :
          (a : X ⟶ G.obj Y) → F.obj X ⟶ Y)
        f :
      F.obj X ⟶ Y)
    (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f : F.obj X ⟶ Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : C
Y : D
⊢ Eq.{v₁ + 1} (α := X ⟶ G.obj Y) ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) 0) 0

Tactic:
map_zero (adj.homAddEquiv X Y)

Premises used: map_zero, CategoryTheory.Adjunction.homAddEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : C
Y : D
f f' : F.obj X ⟶ Y
⊢ (adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) (f + f') =
    HAdd.hAdd (α := X ⟶ G.obj Y) (β := X ⟶ G.obj Y)
      ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) f : X ⟶ G.obj Y)
      ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) f' : X ⟶ G.obj Y)

Tactic:
map_add (adj.homAddEquiv X Y) _ _

Premises used: map_add, CategoryTheory.Adjunction.homAddEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : C
Y : D
f f' : F.obj X ⟶ Y
⊢ (adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) (f - f') =
    HSub.hSub (α := X ⟶ G.obj Y) (β := X ⟶ G.obj Y)
      ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) f : X ⟶ G.obj Y)
      ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) f' : X ⟶ G.obj Y)

Tactic:
map_sub (adj.homAddEquiv X Y) _ _

Premises used: map_sub, CategoryTheory.Adjunction.homAddEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : C
Y : D
f : F.obj X ⟶ Y
⊢ Eq.{v₁ + 1} (α := X ⟶ G.obj Y) ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) (-f) : X ⟶ G.obj Y)
    (-(adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) f : X ⟶ G.obj Y)

Tactic:
map_neg (adj.homAddEquiv X Y) _

Premises used: map_neg, CategoryTheory.Adjunction.homAddEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : C
Y : D
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ Y) (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) 0) 0

Tactic:
map_zero (adj.homAddEquiv X Y).symm

Premises used: map_zero, CategoryTheory.Adjunction.homAddEquiv, AddEquiv.symm
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : C
Y : D
f f' : X ⟶ G.obj Y
⊢ ((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) (f + f') =
    HAdd.hAdd (α := F.obj X ⟶ Y) (β := F.obj X ⟶ Y)
      (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f : F.obj X ⟶ Y)
      (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f' : F.obj X ⟶ Y)

Tactic:
map_add (adj.homAddEquiv X Y).symm _ _

Premises used: map_add, CategoryTheory.Adjunction.homAddEquiv, AddEquiv.symm
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : C
Y : D
f f' : X ⟶ G.obj Y
⊢ ((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) (f - f') =
    HSub.hSub (α := F.obj X ⟶ Y) (β := F.obj X ⟶ Y)
      (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f : F.obj X ⟶ Y)
      (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f' : F.obj X ⟶ Y)

Tactic:
map_sub (adj.homAddEquiv X Y).symm _ _

Premises used: map_sub, CategoryTheory.Adjunction.homAddEquiv, AddEquiv.symm
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : C
Y : D
f : 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) : F.obj X ⟶ Y)
    (-((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f : F.obj X ⟶ Y)

Tactic:
map_neg (adj.homAddEquiv X Y).symm _

Premises used: map_neg, CategoryTheory.Adjunction.homAddEquiv, AddEquiv.symm
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : Cᵒᵖ
Y : D
a : ULift.{max v₁ v₂, v₁} (Opposite.unop X ⟶ G.obj Y)
⊢ Eq (α :=
    (↑(((preadditiveYoneda ⋙
                  obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                    obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
              Y).obj
          X) :
      Type (max v₁ v₂)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max v₁ v₂)) →+ (↑x2 : Type (max v₁ v₂)))
            (CC := AddCommGrpCat.carrier) (X :=
            ((G ⋙
                      preadditiveYoneda ⋙
                        obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                  Y).obj
              X)
            (Y :=
            ((preadditiveYoneda ⋙
                      obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                        obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                  Y).obj
              X)
            (NatTrans.app (NatTrans.app (Iso.hom adj.compPreadditiveYonedaIso) Y) X) :
          (a :
              (↑(((G ⋙
                            preadditiveYoneda ⋙
                              (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                        Y).obj
                    X) :
                Type (max v₁ v₂))) →
            (↑(((preadditiveYoneda ⋙
                          (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op ⋙
                            (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                      Y).obj
                  X) :
              Type (max v₁ v₂)))
        a :
      (↑(((preadditiveYoneda ⋙
                    obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                      obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                Y).obj
            X) :
        Type (max v₁ v₂)))
    ({
        down :=
          ((Equiv.symm (adj.homEquiv (Opposite.unop X) Y) :
                Equiv.{v₁ + 1, v₂ + 1} (Opposite.unop X ⟶ G.obj Y) (F.obj (Opposite.unop X) ⟶ Y)) :
              (a : Opposite.unop X ⟶ G.obj Y) → F.obj (Opposite.unop X) ⟶ Y)
            ((AddEquiv.ulift : (a : ULift.{max v₁ v₂, v₁} (Opposite.unop X ⟶ G.obj Y)) → Opposite.unop X ⟶ G.obj Y)
              a) } :
      ULift.{max v₁ v₂, v₂} (F.obj (Opposite.unop X) ⟶ Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : Cᵒᵖ
Y : D
a : ULift.{max v₁ v₂, v₂} (F.obj (Opposite.unop X) ⟶ Y)
⊢ Eq (α :=
    (↑(((G ⋙ preadditiveYoneda ⋙ obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
              Y).obj
          X) :
      Type (max v₁ v₂)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max v₁ v₂)) →+ (↑x2 : Type (max v₁ v₂)))
            (CC := AddCommGrpCat.carrier) (X :=
            ((preadditiveYoneda ⋙
                      obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                        obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                  Y).obj
              X)
            (Y :=
            ((G ⋙
                      preadditiveYoneda ⋙
                        obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                  Y).obj
              X)
            (NatTrans.app (NatTrans.app (Iso.inv adj.compPreadditiveYonedaIso) Y) X) :
          (a :
              (↑(((preadditiveYoneda ⋙
                            (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op ⋙
                              (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                        Y).obj
                    X) :
                Type (max v₁ v₂))) →
            (↑(((G ⋙
                          preadditiveYoneda ⋙
                            (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                      Y).obj
                  X) :
              Type (max v₁ v₂)))
        a :
      (↑(((G ⋙ preadditiveYoneda ⋙ obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                Y).obj
            X) :
        Type (max v₁ v₂)))
    ({
        down :=
          ((adj.homEquiv (Opposite.unop X) Y :
                Equiv.{v₂ + 1, v₁ + 1} (F.obj (Opposite.unop X) ⟶ Y) (Opposite.unop X ⟶ G.obj Y)) :
              (a : F.obj (Opposite.unop X) ⟶ Y) → Opposite.unop X ⟶ G.obj Y)
            ((AddEquiv.ulift : (a : ULift.{max v₁ v₂, v₂} (F.obj (Opposite.unop X) ⟶ Y)) → F.obj (Opposite.unop X) ⟶ Y)
              a) } :
      ULift.{max v₁ v₂, v₁} (Opposite.unop X ⟶ G.obj Y))

Tactic:
rfl

Premises used: rfl
-- 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 : G.IsRightAdjoint
A : C
⊢ ∃ (ι : Type w) (B : ι → D) (f : (i : ι) → A ⟶ G.obj (B i)),
    ∀ (X : D) (h : A ⟶ G.obj X), ∃ (i : ι) (g : B i ⟶ X), f i ≫ G.map g = h

Tactic:
⟨PUnit, fun _ => G.leftAdjoint.obj A, fun _ => (Adjunction.ofIsRightAdjoint G).unit.app A, ?_⟩

Premises used: CategoryTheory.Adjunction.unit, PUnit, CategoryTheory.Functor.leftAdjoint, Exists.intro, CategoryTheory.Adjunction.ofIsRightAdjoint, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- 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 : G.IsRightAdjoint
A : C
fun :
  ∀ (X : D) (h : A ⟶ G.obj X),
    ∃ (i : PUnit.{w + 1}) (g : (fun (x : PUnit.{w + 1}) ↦ G.leftAdjoint.obj A) i ⟶ X),
      (fun (x : PUnit.{w + 1}) ↦
              (NatTrans.app (Adjunction.unit (Adjunction.ofIsRightAdjoint G)) A :
                Functor.obj.{v, v, u, u} (𝟭 C) A ⟶ (G.leftAdjoint ⋙ G).obj A))
            i ≫
          G.map g =
        h
⊢ ∃ (ι : Type w) (B : ι → D) (f : (i : ι) → A ⟶ G.obj (B i)),
    ∀ (X : D) (h : A ⟶ G.obj X), ∃ (i : ι) (g : B i ⟶ X), f i ≫ G.map g = h

Tactic:
refine
    ⟨PUnit, fun _ => G.leftAdjoint.obj A, fun _ => (Adjunction.ofIsRightAdjoint G).unit.app A, ?_⟩
-- 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 : G.IsRightAdjoint
A : C
B : D
h : A ⟶ G.obj B
⊢ ∃ (i : PUnit.{w + 1}) (g : (fun (x : PUnit.{w + 1}) ↦ G.leftAdjoint.obj A) i ⟶ B),
    (fun (x : PUnit.{w + 1}) ↦
            (NatTrans.app (Adjunction.unit (Adjunction.ofIsRightAdjoint G)) A :
              Functor.obj.{v, v, u, u} (𝟭 C) A ⟶ (G.leftAdjoint ⋙ G).obj A))
          i ≫
        G.map g =
      h

Tactic:
⟨PUnit.unit, ((Adjunction.ofIsRightAdjoint G).homEquiv _ _).symm h, ?_⟩

Premises used: Exists.intro, PUnit.unit, CategoryTheory.Adjunction.homEquiv, Equiv.symm, DFunLike.coe, CategoryTheory.Adjunction.ofIsRightAdjoint
-- 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 : G.IsRightAdjoint
A : C
B : D
h : A ⟶ G.obj B
refine :
  CategoryStruct.comp (Y := G.obj ((fun (x : PUnit.{w + 1}) ↦ G.leftAdjoint.obj A) PUnit.unit))
      ((fun (x : PUnit.{w + 1}) ↦
          (NatTrans.app (Adjunction.unit (Adjunction.ofIsRightAdjoint G)) A :
            Functor.obj.{v, v, u, u} (𝟭 C) A ⟶ (G.leftAdjoint ⋙ G).obj A))
        PUnit.unit)
      (G.map
        (((Equiv.symm (Adjunction.homEquiv (Adjunction.ofIsRightAdjoint G) A B) :
              Equiv.{v + 1, v₁ + 1} (A ⟶ G.obj B) (G.leftAdjoint.obj A ⟶ B)) :
            (a : A ⟶ G.obj B) → G.leftAdjoint.obj A ⟶ B)
          h)) =
    h
⊢ ∃ (i : PUnit.{w + 1}) (g : (fun (x : PUnit.{w + 1}) ↦ G.leftAdjoint.obj A) i ⟶ B),
    (fun (x : PUnit.{w + 1}) ↦
            (NatTrans.app (Adjunction.unit (Adjunction.ofIsRightAdjoint G)) A :
              Functor.obj.{v, v, u, u} (𝟭 C) A ⟶ (G.leftAdjoint ⋙ G).obj A))
          i ≫
        G.map g =
      h

Tactic:
refine ⟨PUnit.unit, ((Adjunction.ofIsRightAdjoint G).homEquiv _ _).symm h, ?_⟩
-- 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 : G.IsRightAdjoint
A : C
B : D
h : A ⟶ G.obj B
rw :
  ((Adjunction.homEquiv (Adjunction.ofIsRightAdjoint G) A B :
          Equiv.{v₁ + 1, v + 1} (G.leftAdjoint.obj A ⟶ B) (A ⟶ G.obj B)) :
        (a : G.leftAdjoint.obj A ⟶ B) → A ⟶ G.obj B)
      (((Equiv.symm (Adjunction.homEquiv (Adjunction.ofIsRightAdjoint G) A B) :
            Equiv.{v + 1, v₁ + 1} (A ⟶ G.obj B) (G.leftAdjoint.obj A ⟶ B)) :
          (a : A ⟶ G.obj B) → G.leftAdjoint.obj A ⟶ B)
        h) =
    h
rw₁ rw₂ : h = h
⊢ CategoryStruct.comp (Y := G.obj ((fun (x : PUnit.{w + 1}) ↦ G.leftAdjoint.obj A) PUnit.unit))
      ((fun (x : PUnit.{w + 1}) ↦
          (NatTrans.app (Adjunction.unit (Adjunction.ofIsRightAdjoint G)) A :
            Functor.obj.{v, v, u, u} (𝟭 C) A ⟶ (G.leftAdjoint ⋙ G).obj A))
        PUnit.unit)
      (G.map
        (((Equiv.symm (Adjunction.homEquiv (Adjunction.ofIsRightAdjoint G) A B) :
              Equiv.{v + 1, v₁ + 1} (A ⟶ G.obj B) (G.leftAdjoint.obj A ⟶ B)) :
            (a : A ⟶ G.obj B) → G.leftAdjoint.obj A ⟶ B)
          h)) =
    h

Tactic:
rw [← Adjunction.homEquiv_unit, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, CategoryTheory.Adjunction.homEquiv_unit
-- 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
hG : SolutionSetCondition G
⊢ G.IsRightAdjoint

Tactic:
@isRightAdjointOfStructuredArrowInitials _ _ _ _ G ?_

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
G : Functor.{v₁, v, u₁, u} D C
inst_2 : HasLimits.{v₁, u₁} D
inst_3 : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
hG : SolutionSetCondition G
refine : ∀ (A : C), HasInitial (StructuredArrow A G)
⊢ G.IsRightAdjoint

Tactic:
refine @isRightAdjointOfStructuredArrowInitials _ _ _ _ G ?_

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
G : Functor.{v₁, v, u₁, u} D C
inst_2 : HasLimits.{v₁, u₁} D
inst_3 : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
hG : SolutionSetCondition G
A : C
⊢ ∃ (ι : Type v₁) (B : ι → D) (f : (i : ι) → A ⟶ G.obj (B i)),
    ∀ (X : D) (h : A ⟶ G.obj X), ∃ (i : ι) (g : B i ⟶ X), f i ≫ G.map g = h

Tactic:
specialize hG A
-- 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
hG :
  ∃ (ι : Type v₁) (B : ι → D) (f : (i : ι) → A ⟶ G.obj (B i)),
    ∀ (X : D) (h : A ⟶ G.obj X), ∃ (i : ι) (g : B i ⟶ X), f i ≫ G.map g = h
choose :
  ∀ (ι : 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), HasInitial (StructuredArrow A G)
⊢ HasInitial (StructuredArrow A G)

Tactic:
choose ι B f g using hG
-- 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)
A' : StructuredArrow A G
obtain : ∀ (i : ι) (w : B i ⟶ A'.right) (t : f i ≫ G.map w = A'.hom), ∃ (i : ι), Nonempty.{v₁ + 1} (B' i ⟶ A')
⊢ ∃ (i : ι), Nonempty.{v₁ + 1} (B' i ⟶ A')

Tactic:
obtain ⟨i, _, t⟩ := g _ A'.hom

Premises used: CategoryTheory.StructuredArrow.hom
-- 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)
A' : StructuredArrow A G
i : ι
w : B i ⟶ A'.right
t : f i ≫ G.map w = A'.hom
⊢ ∃ (i : ι), Nonempty.{v₁ + 1} (B' i ⟶ A')

Tactic:
⟨i, ⟨StructuredArrow.homMk _ t⟩⟩

Premises used: CategoryTheory.StructuredArrow.homMk, Nonempty.intro, Exists.intro
-- 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)
A' : StructuredArrow A G
i : ι
w : B i ⟶ A'.right
t : f i ≫ G.map w = A'.hom
⊢ ∃ (i : ι), Nonempty.{v₁ + 1} (B' i ⟶ A')

Tactic:
exact ⟨i, ⟨StructuredArrow.homMk _ t⟩⟩
-- 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)
⊢ ∀ (A' : StructuredArrow A G), ∃ (i : ι), Nonempty.{v₁ + 1} (B' i ⟶ A')

Tactic:
have hB' : ∀ A' : StructuredArrow A G, ∃ i, Nonempty (B' i ⟶ A') := by
    intro A'
    obtain ⟨i, _, t⟩ := g _ A'.hom
    exact ⟨i, ⟨StructuredArrow.homMk _ t⟩⟩
-- 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')
obtain :
  ∀ (T : StructuredArrow A G) (hT : ∀ (X : StructuredArrow A G), Nonempty.{v₁ + 1} (T ⟶ X)),
    HasInitial (StructuredArrow A G)
⊢ HasInitial (StructuredArrow A G)

Tactic:
obtain ⟨T, hT⟩ := has_weakly_initial_of_weakly_initial_set_and_hasProducts hB'

Premises used: CategoryTheory.has_weakly_initial_of_weakly_initial_set_and_hasProducts