awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
inst_3 : F.Full
A B : Under.{v₁, u₁} X
f : Functor.obj (post F) A ⟶ Functor.obj (post F) B
a : A.right ⟶ B.right
ha : F.map a = Hom.right f
⊢ F.map (A.hom ≫ a) = F.map B.hom

Tactic:
simp [ha, dsimp% f.w]

Premises used: CategoryTheory.Under.Hom.w
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
inst_3 : F.Full
A B : Under.{v₁, u₁} X
f : Functor.obj (post F) A ⟶ Functor.obj (post F) B
a : A.right ⟶ B.right
ha : F.map a = Hom.right f
h : Hom.right (Functor.map (post F) (homMk a ⋯)) = Hom.right f
⊢ Functor.map (post F) (homMk a ⋯) = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
inst_3 : F.Full
A B : Under.{v₁, u₁} X
f : Functor.obj (post F) A ⟶ Functor.obj (post F) B
a : A.right ⟶ B.right
ha : F.map a = Hom.right f
⊢ Hom.right (Functor.map (post F) (homMk a ⋯)) = Hom.right f

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
inst_3 : F.Full
A B : Under.{v₁, u₁} X
f : Functor.obj (post F) A ⟶ Functor.obj (post F) B
a : A.right ⟶ B.right
ha : F.map a = Hom.right f
⊢ ∃ (a : A ⟶ B), Functor.map (post F) a = f

Tactic:
exact ⟨Under.homMk a (F.map_injective (by simp [ha, dsimp% f.w])), by ext; simpa⟩
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f g : Under.{v₁, u₁} X
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Full
inst_3 : F.EssSurj
B : Under.{v₂, u₂} (F.obj X)
obtain : ∀ (B' : T) (e : F.obj B' ≅ B.right), Functor.essImage (post F) B
⊢ Functor.essImage (post F) B

Tactic:
obtain ⟨B', ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := F) B.right

Premises used: CategoryTheory.Under.right, CategoryTheory.Functor.EssSurj.mem_essImage
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f g : Under.{v₁, u₁} X
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Full
inst_3 : F.EssSurj
B : Under.{v₂, u₂} (F.obj X)
B' : T
e : F.obj B' ≅ B.right
obtain : ∀ (f : X ⟶ B') (hf : F.map f = B.hom ≫ e.inv), Functor.essImage (post F) B
⊢ Functor.essImage (post F) B

Tactic:
obtain ⟨f, hf⟩ := F.map_surjective (B.hom ≫ e.inv)

Premises used: CategoryTheory.Under.hom, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Full
inst_3 : F.EssSurj
B : Under.{v₂, u₂} (F.obj X)
B' : T
e : F.obj B' ≅ B.right
f : X ⟶ B'
hf : F.map f = B.hom ≫ e.inv
⊢ Functor.essImage (post F) B

Tactic:
⟨Under.mk f, ⟨Under.isoMk e⟩⟩

Premises used: CategoryTheory.Under.mk, CategoryTheory.Under.isoMk, CategoryTheory.Functor.essImage, Nonempty.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Full
inst_3 : F.EssSurj
B : Under.{v₂, u₂} (F.obj X)
B' : T
e : F.obj B' ≅ B.right
f : X ⟶ B'
hf : F.map f = B.hom ≫ e.inv
⊢ Functor.essImage (post F) B

Tactic:
exact ⟨Under.mk f, ⟨Under.isoMk e⟩⟩
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
h : F.FullyFaithful
A B : Under.{v₁, u₁} X
f : Functor.obj (post F) A ⟶ Functor.obj (post F) B
⊢ F.map (A.hom ≫ h.preimage (Hom.right f)) = F.map B.hom

Tactic:
simpa using Under.w f

Premises used: CategoryTheory.Under.w
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 : T
f_1 g : Under.{v₁, u₁} X_1
φ : f_1 ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
x x_1 : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)
f : x ⟶ x_1
h :
  Eq (α :=
    (Functor.obj (𝟭 (Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) x).right ⟶
      ((post F ⋙ post G ⋙ map (a.unit.app X)).obj x_1).right)
    (Hom.right
      (Functor.map (𝟭 (Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) f ≫ homMk (a.unit.app x_1.right) ⋯))
    (Hom.right (homMk (a.unit.app x.right) ⋯ ≫ (post F ⋙ post G ⋙ map (a.unit.app X)).map f))
⊢ Eq (α :=
    Functor.obj (𝟭 (Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) x ⟶
      (post F ⋙ post G ⋙ map (a.unit.app X)).obj x_1)
    (Functor.map (𝟭 (Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) f ≫ homMk (a.unit.app x_1.right) ⋯)
    (homMk (a.unit.app x.right) ⋯ ≫ (post F ⋙ post G ⋙ map (a.unit.app X)).map f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 : T
f_1 g : Under.{v₁, u₁} X_1
φ : f_1 ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
x x_1 : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)
f : x ⟶ x_1
⊢ Eq (α :=
    (Functor.obj (𝟭 (Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) x).right ⟶
      ((post F ⋙ post G ⋙ map (a.unit.app X)).obj x_1).right)
    (Hom.right
      (Functor.map (𝟭 (Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) f ≫ homMk (a.unit.app x_1.right) ⋯))
    (Hom.right (homMk (a.unit.app x.right) ⋯ ≫ (post F ⋙ post G ⋙ map (a.unit.app X)).map f))

Tactic:
(a.unit_naturality f.right).symm

Premises used: CategoryTheory.Adjunction.unit_naturality, CategoryTheory.Under.Hom.right, Eq.symm
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 : T
f_1 g : Under.{v₁, u₁} X_1
φ : f_1 ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
x x_1 : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)
f : x ⟶ x_1
⊢ Eq (α :=
    (Functor.obj (𝟭 (Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) x).right ⟶
      ((post F ⋙ post G ⋙ map (a.unit.app X)).obj x_1).right)
    (Hom.right
      (Functor.map (𝟭 (Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) f ≫ homMk (a.unit.app x_1.right) ⋯))
    (Hom.right (homMk (a.unit.app x.right) ⋯ ≫ (post F ⋙ post G ⋙ map (a.unit.app X)).map f))

Tactic:
exact (a.unit_naturality f.right).symm

Premises used: CategoryTheory.Adjunction.unit_naturality, CategoryTheory.Under.Hom.right, Eq.symm
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 : T
f_1 g : Under.{v₁, u₁} X_1
φ : f_1 ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
x x_1 : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))
f : x ⟶ x_1
h :
  Hom.right (((post G ⋙ map (a.unit.app X)) ⋙ post F).map f ≫ homMk (a.counit.app x_1.right) ⋯) =
    Hom.right
      (homMk (a.counit.app x.right) ⋯ ≫
        Functor.map (𝟭 (Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)))) f)
⊢ ((post G ⋙ map (a.unit.app X)) ⋙ post F).map f ≫ homMk (a.counit.app x_1.right) ⋯ =
    homMk (a.counit.app x.right) ⋯ ≫ Functor.map (𝟭 (Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)))) f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 : T
f_1 g : Under.{v₁, u₁} X_1
φ : f_1 ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
x x_1 : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))
f : x ⟶ x_1
⊢ Hom.right (((post G ⋙ map (a.unit.app X)) ⋙ post F).map f ≫ homMk (a.counit.app x_1.right) ⋯) =
    Hom.right
      (homMk (a.counit.app x.right) ⋯ ≫
        Functor.map (𝟭 (Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)))) f)

Tactic:
(a.counit_naturality f.right)

Premises used: CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Under.Hom.right
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 : T
f_1 g : Under.{v₁, u₁} X_1
φ : f_1 ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
x x_1 : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))
f : x ⟶ x_1
⊢ Hom.right (((post G ⋙ map (a.unit.app X)) ⋙ post F).map f ≫ homMk (a.counit.app x_1.right) ⋯) =
    Hom.right
      (homMk (a.counit.app x.right) ⋯ ≫
        Functor.map (𝟭 (Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)))) f)

Tactic:
exact (a.counit_naturality f.right)

Premises used: CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Under.Hom.right
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 : T
f g : Under.{v₁, u₁} X_1
φ : f ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
A : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)
h :
  Hom.right
      (CategoryStruct.comp (Y := Functor.obj (post F) ((post G ⋙ map (a.unit.app X)).obj (Functor.obj (post F) A)))
        (Functor.map (post F)
          (NatTrans.app
            { app := fun (A : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)) ↦ homMk (a.unit.app A.right) ⋯,
              naturality := ⋯ }
            A))
        (NatTrans.app
          {
            app := fun (A : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) ↦
              homMk (a.counit.app A.right) ⋯,
            naturality := ⋯ }
          (Functor.obj (post F) A))) =
    Hom.right (𝟙 (Functor.obj (post F) A))
⊢ Eq (α := Functor.obj (post F) A ⟶ Functor.obj (post F) A)
    (CategoryStruct.comp (Y := Functor.obj (post F) ((post G ⋙ map (a.unit.app X)).obj (Functor.obj (post F) A)))
        (Functor.map (post F)
          (NatTrans.app
            { app := fun (A : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)) ↦ homMk (a.unit.app A.right) ⋯,
              naturality := ⋯ }
            A))
        (NatTrans.app
          {
            app := fun (A : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) ↦
              homMk (a.counit.app A.right) ⋯,
            naturality := ⋯ }
          (Functor.obj (post F) A)) :
      Functor.obj (post F) A ⟶ Functor.obj (post F) A)
    (𝟙 (Functor.obj (post F) A) : Functor.obj (post F) A ⟶ Functor.obj (post F) A)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 : T
f g : Under.{v₁, u₁} X_1
φ : f ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
A : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)
⊢ Hom.right
      (CategoryStruct.comp (Y := Functor.obj (post F) ((post G ⋙ map (a.unit.app X)).obj (Functor.obj (post F) A)))
        (Functor.map (post F)
          (NatTrans.app
            { app := fun (A : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)) ↦ homMk (a.unit.app A.right) ⋯,
              naturality := ⋯ }
            A))
        (NatTrans.app
          {
            app := fun (A : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) ↦
              homMk (a.counit.app A.right) ⋯,
            naturality := ⋯ }
          (Functor.obj (post F) A))) =
    Hom.right (𝟙 (Functor.obj (post F) A))

Tactic:
simp [-Functor.id_obj]

Premises used: CategoryTheory.Functor.id_obj
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 : T
f g : Under.{v₁, u₁} X_1
φ : f ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
A : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))
h :
  Hom.right
      (CategoryStruct.comp (Y :=
        (post G ⋙ map (a.unit.app X)).obj (Functor.obj (post F) ((post G ⋙ map (a.unit.app X)).obj A)))
        (NatTrans.app
          { app := fun (A : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)) ↦ homMk (a.unit.app A.right) ⋯,
            naturality := ⋯ }
          ((post G ⋙ map (a.unit.app X)).obj A))
        ((post G ⋙ map (a.unit.app X)).map
          (NatTrans.app
            {
              app := fun (A : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) ↦
                homMk (a.counit.app A.right) ⋯,
              naturality := ⋯ }
            A))) =
    Hom.right (𝟙 ((post G ⋙ map (a.unit.app X)).obj A))
⊢ Eq.{v₁ + 1} (α := (post G ⋙ map (a.unit.app X)).obj A ⟶ (post G ⋙ map (a.unit.app X)).obj A)
    (CategoryStruct.comp (Y :=
        (post G ⋙ map (a.unit.app X)).obj (Functor.obj (post F) ((post G ⋙ map (a.unit.app X)).obj A)))
        (NatTrans.app
          { app := fun (A : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)) ↦ homMk (a.unit.app A.right) ⋯,
            naturality := ⋯ }
          ((post G ⋙ map (a.unit.app X)).obj A))
        ((post G ⋙ map (a.unit.app X)).map
          (NatTrans.app
            {
              app := fun (A : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) ↦
                homMk (a.counit.app A.right) ⋯,
              naturality := ⋯ }
            A)) :
      (post G ⋙ map (a.unit.app X)).obj A ⟶ (post G ⋙ map (a.unit.app X)).obj A)
    (𝟙 ((post G ⋙ map (a.unit.app X)).obj A) :
      (post G ⋙ map (a.unit.app X)).obj A ⟶ (post G ⋙ map (a.unit.app X)).obj A)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 : T
f g : Under.{v₁, u₁} X_1
φ : f ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
A : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))
⊢ Hom.right
      (CategoryStruct.comp (Y :=
        (post G ⋙ map (a.unit.app X)).obj (Functor.obj (post F) ((post G ⋙ map (a.unit.app X)).obj A)))
        (NatTrans.app
          { app := fun (A : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)) ↦ homMk (a.unit.app A.right) ⋯,
            naturality := ⋯ }
          ((post G ⋙ map (a.unit.app X)).obj A))
        ((post G ⋙ map (a.unit.app X)).map
          (NatTrans.app
            {
              app := fun (A : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) ↦
                homMk (a.counit.app A.right) ⋯,
              naturality := ⋯ }
            A))) =
    Hom.right (𝟙 ((post G ⋙ map (a.unit.app X)).obj A))

Tactic:
simp [-Functor.id_obj]

Premises used: CategoryTheory.Functor.id_obj
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f g : Under.{v₁, u₁} X
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.IsLeftAdjoint
⊢ Functor.IsLeftAdjoint (C := Under.{v₁, u₁} X) (post F)

Tactic:
let ⟨G, ⟨a⟩⟩ := ‹F.IsLeftAdjoint›; ⟨_, ⟨postAdjunctionLeft a⟩⟩

Premises used: CategoryTheory.Under.postAdjunctionLeft, _private.0.CategoryTheory.Under.isLeftAdjoint_post.match_1, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.unit, Nonempty.intro, CategoryTheory.Functor.IsLeftAdjoint, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, CategoryTheory.Under.post, CategoryTheory.Under.map, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f_1 g : Under.{v₁, u₁} X_1
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : Functor.obj (Functor.const J) X ⟶ D
X_2 Y : J
f : X_2 ⟶ Y
⊢ (mk (s.app X_2)).hom ≫ D.map f = (mk (s.app Y)).hom

Tactic:
simpa using (s.naturality f).symm

Premises used: CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f g : Under.{v₁, u₁} X_1
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : Nonempty J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : Functor.obj (Functor.const J) X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
j : J := Classical.arbitrary J
⊢ (liftCocone D s c p hp).pt.hom ≫ hc.desc (Functor.mapCocone (forget X) t) = t.pt.hom

Tactic:
simp [← dsimp% (t.ι.app j).w, ← dsimp% (hp j), dsimp% hc.fac ((forget X).mapCocone t)]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Under.Hom.w, CategoryTheory.Functor.mapCocone, CategoryTheory.Under.forget, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f g : Under.{v₁, u₁} X_1
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : Nonempty J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : Functor.obj (Functor.const J) X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
j : J
h :
  Hom.right ((liftCocone D s c p hp).ι.app j ≫ homMk (hc.desc (Functor.mapCocone (forget X) t)) ⋯) =
    Hom.right (t.ι.app j)
⊢ (liftCocone D s c p hp).ι.app j ≫ homMk (hc.desc (Functor.mapCocone (forget X) t)) ⋯ = t.ι.app j

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f g : Under.{v₁, u₁} X_1
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : Nonempty J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : Functor.obj (Functor.const J) X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
j : J
⊢ Hom.right ((liftCocone D s c p hp).ι.app j ≫ homMk (hc.desc (Functor.mapCocone (forget X) t)) ⋯) =
    Hom.right (t.ι.app j)

Tactic:
simp [dsimp% hc.fac ((forget X).mapCocone t) j]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.mapCocone, CategoryTheory.Under.forget
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f g : Under.{v₁, u₁} X_1
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : Nonempty J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : Functor.obj (Functor.const J) X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
x : (liftCocone D s c p hp).pt ⟶ t.pt
hm : ∀ (j : J), (liftCocone D s c p hp).ι.app j ≫ x = t.ι.app j
h : Hom.right x = Hom.right (homMk (hc.desc (Functor.mapCocone (forget X) t)) ⋯)
⊢ x = homMk (hc.desc (Functor.mapCocone (forget X) t)) ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f g : Under.{v₁, u₁} X_1
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : Nonempty J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : Functor.obj (Functor.const J) X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
x : (liftCocone D s c p hp).pt ⟶ t.pt
hm : ∀ (j : J), (liftCocone D s c p hp).ι.app j ≫ x = t.ι.app j
⊢ Hom.right x = Hom.right (homMk (hc.desc (Functor.mapCocone (forget X) t)) ⋯)

Tactic:
hc.hom_ext (fun j ↦ ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f g : Under.{v₁, u₁} X_1
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : Nonempty J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : Functor.obj (Functor.const J) X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
x : (liftCocone D s c p hp).pt ⟶ t.pt
hm : ∀ (j : J), (liftCocone D s c p hp).ι.app j ≫ x = t.ι.app j
h : ∀ (j : J), c.ι.app j ≫ Hom.right x = c.ι.app j ≫ Hom.right (homMk (hc.desc (Functor.mapCocone (forget X) t)) ⋯)
⊢ Hom.right x = Hom.right (homMk (hc.desc (Functor.mapCocone (forget X) t)) ⋯)

Tactic:
refine hc.hom_ext (fun j ↦ ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f g : Under.{v₁, u₁} X_1
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : Nonempty J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : Functor.obj (Functor.const J) X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
x : (liftCocone D s c p hp).pt ⟶ t.pt
hm : ∀ (j : J), (liftCocone D s c p hp).ι.app j ≫ x = t.ι.app j
j : J
⊢ c.ι.app j ≫ Hom.right x = c.ι.app j ≫ Hom.right (homMk (hc.desc (Functor.mapCocone (forget X) t)) ⋯)

Tactic:
simp [dsimp% hc.fac ((forget X).mapCocone t) j, ← hm]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.mapCocone, CategoryTheory.Under.forget
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
D : Type u₂
inst_2 : Category.{v₂, u₂} D
X : T
F : Functor.{v₂, v₁, u₂, u₁} D T
inst_3 : F.Faithful
⊢ (toUnder X F).Faithful

Tactic:
show (StructuredArrow.pre _ _ _).Faithful from inferInstance

Premises used: CategoryTheory.StructuredArrow.Hom, CategoryTheory.Functor.comp, inferInstance, CategoryTheory.Under, CategoryTheory.Under.Hom, CategoryTheory.StructuredArrow.toUnder
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
D : Type u₂
inst_2 : Category.{v₂, u₂} D
X : T
F : Functor.{v₂, v₁, u₂, u₁} D T
inst_3 : F.Full
⊢ (toUnder X F).Full

Tactic:
show (StructuredArrow.pre _ _ _).Full from inferInstance

Premises used: CategoryTheory.StructuredArrow.Hom, CategoryTheory.Functor.comp, inferInstance, CategoryTheory.Under, CategoryTheory.Under.Hom, CategoryTheory.StructuredArrow.toUnder
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
D : Type u₂
inst_2 : Category.{v₂, u₂} D
X : T
F : Functor.{v₂, v₁, u₂, u₁} D T
inst_3 : F.EssSurj
⊢ (toUnder X F).EssSurj

Tactic:
show (StructuredArrow.pre _ _ _).EssSurj from inferInstance

Premises used: CategoryTheory.StructuredArrow.Hom, CategoryTheory.Functor.comp, inferInstance, CategoryTheory.Under, CategoryTheory.Under.Hom, CategoryTheory.StructuredArrow.toUnder