awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Initial
t : (↑(F ⋙ P).sections : Type (max u₁ w))
val : (Y : D) → P.obj Y
hval :
  ∀ (Y : D) (j : CostructuredArrow F Y),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom) :
          (a : (fun (X : Type w) ↦ X) (P.obj (F.obj j.left))) → (fun (X : Type w) ↦ X) (P.obj Y))
        ((↑t : (j : C) → (F ⋙ P).obj j) j.left) =
      val Y
refine_2 :
  ∀ {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y₁)) → (fun (X : Type w) ↦ X) (P.obj Y₂))
        (val Y₁) =
      val Y₂
refine_2₁ : F.sectionsPrecomp (Subtype.mk (p := fun (x : (j : D) → P.obj j) ↦ x ∈ P.sections) val ⋯) = t
⊢ ∃ (a : (↑P.sections : Type (max u₂ w))), F.sectionsPrecomp a = t

Tactic:
refine ⟨⟨val, fun {Y₁ Y₂} f ↦ ?_⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Initial
t : (↑(F ⋙ P).sections : Type (max u₁ w))
val : (Y : D) → P.obj Y
hval :
  ∀ (Y : D) (j : CostructuredArrow F Y),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom) :
          (a : (fun (X : Type w) ↦ X) (P.obj (F.obj j.left))) → (fun (X : Type w) ↦ X) (P.obj Y))
        ((↑t : (j : C) → (F ⋙ P).obj j) j.left) =
      val Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
X : CostructuredArrow F Y₁ := Classical.arbitrary (CostructuredArrow F Y₁)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f) :
        (a : (fun (X : Type w) ↦ X) (P.obj Y₁)) → (fun (X : Type w) ↦ X) (P.obj Y₂))
      (val Y₁) =
    val Y₂

Tactic:
simp [← hval Y₁ X, ← hval Y₂ ((CostructuredArrow.map f).obj X)]

Premises used: CategoryTheory.CostructuredArrow.map, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Initial
t : (↑(F ⋙ P).sections : Type (max u₁ w))
val : (Y : D) → P.obj Y
hval :
  ∀ (Y : D) (j : CostructuredArrow F Y),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom) :
          (a : (fun (X : Type w) ↦ X) (P.obj (F.obj j.left))) → (fun (X : Type w) ↦ X) (P.obj Y))
        ((↑t : (j : C) → (F ⋙ P).obj j) j.left) =
      val Y
refine_2 :
  ∀ (X : C),
    (↑(F.sectionsPrecomp (Subtype.mk (p := fun (x : (j : D) → P.obj j) ↦ x ∈ P.sections) val ⋯)) :
          (j : C) → (F ⋙ P).obj j)
        X =
      (↑t : (j : C) → (F ⋙ P).obj j) X
⊢ F.sectionsPrecomp (Subtype.mk (p := fun (x : (j : D) → P.obj j) ↦ x ∈ P.sections) val ⋯) = t

Tactic:
ext X : 2
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Initial
t : (↑(F ⋙ P).sections : Type (max u₁ w))
val : (Y : D) → P.obj Y
hval :
  ∀ (Y : D) (j : CostructuredArrow F Y),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom) :
          (a : (fun (X : Type w) ↦ X) (P.obj (F.obj j.left))) → (fun (X : Type w) ↦ X) (P.obj Y))
        ((↑t : (j : C) → (F ⋙ P).obj j) j.left) =
      val Y
X : C
⊢ (↑(F.sectionsPrecomp (Subtype.mk (p := fun (x : (j : D) → P.obj j) ↦ x ∈ P.sections) val ⋯)) :
        (j : C) → (F ⋙ P).obj j)
      X =
    (↑t : (j : C) → (F ⋙ P).obj j) X

Tactic:
simpa using (hval (F.obj X) (CostructuredArrow.mk (𝟙 _))).symm

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.CostructuredArrow.mk, Eq.symm, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
i : C
x : P.obj (F.obj i)
⊢ F.colimitTypePrecomp P ((F ⋙ P).ιColimitType i x) = P.ιColimitType (F.obj i) x

Tactic:
rfl

Premises used: CategoryTheory.Functor.colimitTypePrecomp, CategoryTheory.Functor.ιColimitType, rfl
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
⊢ Function.Bijective (F.colimitTypePrecomp P)

Tactic:
⟨?_, fun x ↦ ?_⟩

Premises used: And.intro, Function.Bijective
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
refine_1 : Function.Injective (F.colimitTypePrecomp P)
refine_2 : ∀ (x : P.ColimitType), ∃ (a : (F ⋙ P).ColimitType), F.colimitTypePrecomp P a = x
⊢ Function.Bijective (F.colimitTypePrecomp P)

Tactic:
refine ⟨?_, fun x ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
Y : D
h :
  ∀ (j₁ j₂ : StructuredArrow Y F) (x : j₁ ⟶ j₂),
    Eq (α := P.obj Y → (F ⋙ P).ColimitType)
      (Function.comp (β := (F ⋙ P).obj j₁.right) ((F ⋙ P).ιColimitType j₁.right)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j₁.hom)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj j₁.right))))
      (Function.comp (β := (F ⋙ P).obj j₂.right) ((F ⋙ P).ιColimitType j₂.right)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j₂.hom)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj j₂.right))))
⊢ ∃ (a : P.obj Y → (F ⋙ P).ColimitType),
    ∀ (j : StructuredArrow Y F),
      Function.comp (β := (F ⋙ P).obj j.right) ((F ⋙ P).ιColimitType j.right)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom)) :
            (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj j.right))) =
        a

Tactic:
apply constant_of_preserves_morphisms'

Premises used: CategoryTheory.constant_of_preserves_morphisms'
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
Y : D
Z₁ Z₂ : StructuredArrow Y F
f : Z₁ ⟶ Z₂
h :
  ∀ (x : (fun (X : Type w) ↦ X) (P.obj Y)),
    Function.comp (β := (F ⋙ P).obj Z₁.right) ((F ⋙ P).ιColimitType Z₁.right)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj Z₁.right)))
        x =
      Function.comp (β := (F ⋙ P).obj Z₂.right) ((F ⋙ P).ιColimitType Z₂.right)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₂.hom)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj Z₂.right)))
        x
⊢ Eq (α := P.obj Y → (F ⋙ P).ColimitType)
    (Function.comp (β := (F ⋙ P).obj Z₁.right) ((F ⋙ P).ιColimitType Z₁.right)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom)) :
        (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj Z₁.right))))
    (Function.comp (β := (F ⋙ P).obj Z₂.right) ((F ⋙ P).ιColimitType Z₂.right)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₂.hom)) :
        (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj Z₂.right))))

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
Y : D
Z₁ Z₂ : StructuredArrow Y F
f : Z₁ ⟶ Z₂
x : (fun (X : Type w) ↦ X) (P.obj Y)
h :
  (F ⋙ P).ιColimitType Z₂.right
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (F.map (StructuredArrow.Hom.right f))) :
          (a : (fun (X : Type w) ↦ X) ((F ⋙ P).obj Z₁.right)) → (fun (X : Type w) ↦ X) ((F ⋙ P).obj Z₂.right))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom) : (a : P.obj Y) → P.obj (F.obj Z₁.right)) x :
          P.obj (F.obj Z₁.right))) =
    (F ⋙ P).ιColimitType Z₂.right
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₂.hom) : (a : P.obj Y) → P.obj (F.obj Z₂.right)) x)
⊢ (F ⋙ P).ιColimitType Z₁.right
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom) : (a : P.obj Y) → P.obj (F.obj Z₁.right)) x) =
    (F ⋙ P).ιColimitType Z₂.right
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₂.hom) : (a : P.obj Y) → P.obj (F.obj Z₂.right)) x)

Tactic:
rw [← (F ⋙ P).ιColimitType_map f.right, comp_map]

Premises used: CategoryTheory.Functor.ιColimitType_map, CategoryTheory.Functor.comp, CategoryTheory.Functor.comp_map, CategoryTheory.StructuredArrow.Hom.right
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
Y : D
Z₁ Z₂ : StructuredArrow Y F
f : Z₁ ⟶ Z₂
x : (fun (X : Type w) ↦ X) (P.obj Y)
⊢ (F ⋙ P).ιColimitType Z₂.right
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (F.map (StructuredArrow.Hom.right f))) :
          (a : (fun (X : Type w) ↦ X) ((F ⋙ P).obj Z₁.right)) → (fun (X : Type w) ↦ X) ((F ⋙ P).obj Z₂.right))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom) : (a : P.obj Y) → P.obj (F.obj Z₁.right)) x :
          P.obj (F.obj Z₁.right))) =
    (F ⋙ P).ιColimitType Z₂.right
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₂.hom) : (a : P.obj Y) → P.obj (F.obj Z₂.right)) x)

Tactic:
simp [← comp_apply, ← Functor.map_comp]

Premises used: CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
⊢ ∀ (Y : D),
    ∃ (a : P.obj Y → (F ⋙ P).ColimitType),
      ∀ (j : StructuredArrow Y F),
        Function.comp (β := (F ⋙ P).obj j.right) ((F ⋙ P).ιColimitType j.right)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom)) :
              (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj j.right))) =
          a

Tactic:
have h (Y : D) : ∃ (a : P.obj Y → (F ⋙ P).ColimitType), ∀ (j : StructuredArrow Y F),
        (F ⋙ P).ιColimitType j.right ∘ P.map j.hom = a := by
      apply constant_of_preserves_morphisms'
      intro Z₁ Z₂ f
      ext x
      dsimp
      rw [← (F ⋙ P).ιColimitType_map f.right, comp_map]
      simp [← comp_apply, ← Functor.map_comp]
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
h :
  ∀ (Y : D),
    ∃ (a : P.obj Y → (F ⋙ P).ColimitType),
      ∀ (j : StructuredArrow Y F),
        Function.comp (β := (F ⋙ P).obj j.right) ((F ⋙ P).ιColimitType j.right)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom)) :
              (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj j.right))) =
          a
refine_1 :
  ∀ (φ : (Y : D) → P.obj Y → (F ⋙ P).ColimitType)
    (hφ :
      ∀ (Y : D) (j : StructuredArrow Y F),
        Function.comp (β := (F ⋙ P).obj j.right) ((F ⋙ P).ιColimitType j.right)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom)) :
              (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj j.right))) =
          φ Y),
    Function.Injective (F.colimitTypePrecomp P)
⊢ Function.Injective (F.colimitTypePrecomp P)

Tactic:
choose φ hφ using h
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
φ : (Y : D) → P.obj Y → (F ⋙ P).ColimitType
hφ :
  ∀ (Y : D) (j : StructuredArrow Y F),
    Function.comp (β := (F ⋙ P).obj j.right) ((F ⋙ P).ιColimitType j.right)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj j.right))) =
      φ Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
h :
  ∀ (x : (fun (X : Type w) ↦ X) (P.obj Y₁)),
    (φ Y₂ ∘
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f)) :
            (a : (fun (X : Type w) ↦ X) (P.obj Y₁)) → (fun (X : Type w) ↦ X) (P.obj Y₂)))
        x =
      φ Y₁ x
⊢ φ Y₂ ∘
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f)) :
        (a : (fun (X : Type w) ↦ X) (P.obj Y₁)) → (fun (X : Type w) ↦ X) (P.obj Y₂)) =
    φ Y₁

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
φ : (Y : D) → P.obj Y → (F ⋙ P).ColimitType
hφ :
  ∀ (Y : D) (j : StructuredArrow Y F),
    Function.comp (β := (F ⋙ P).obj j.right) ((F ⋙ P).ιColimitType j.right)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj j.right))) =
      φ Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
x : (fun (X : Type w) ↦ X) (P.obj Y₁)
h :
  ∀ (X : StructuredArrow Y₂ F),
    (φ Y₂ ∘
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f)) :
            (a : (fun (X : Type w) ↦ X) (P.obj Y₁)) → (fun (X : Type w) ↦ X) (P.obj Y₂)))
        x =
      φ Y₁ x
⊢ (φ Y₂ ∘
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y₁)) → (fun (X : Type w) ↦ X) (P.obj Y₂)))
      x =
    φ Y₁ x

Tactic:
have X : StructuredArrow Y₂ F := Classical.arbitrary _
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
φ : (Y : D) → P.obj Y → (F ⋙ P).ColimitType
hφ :
  ∀ (Y : D) (j : StructuredArrow Y F),
    Function.comp (β := (F ⋙ P).obj j.right) ((F ⋙ P).ιColimitType j.right)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj j.right))) =
      φ Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
x : (fun (X : Type w) ↦ X) (P.obj Y₁)
X : StructuredArrow Y₂ F
h :
  Function.comp (β := P.obj Y₂)
      (Function.comp (β := (F ⋙ P).obj X.right) ((F ⋙ P).ιColimitType X.right)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map X.hom)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y₂)) → (fun (X : Type w) ↦ X) (P.obj (F.obj X.right))))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f)) :
        (a : (fun (X : Type w) ↦ X) (P.obj Y₁)) → (fun (X : Type w) ↦ X) (P.obj Y₂))
      x =
    Function.comp (β := (F ⋙ P).obj (obj (StructuredArrow.map f) X).right)
      ((F ⋙ P).ιColimitType (obj (StructuredArrow.map f) X).right)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (obj (StructuredArrow.map f) X).hom)) :
        (a : (fun (X : Type w) ↦ X) (P.obj Y₁)) →
          (fun (X : Type w) ↦ X) (P.obj (F.obj ((StructuredArrow.map f).obj X).right)))
      x
⊢ (φ Y₂ ∘
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y₁)) → (fun (X : Type w) ↦ X) (P.obj Y₂)))
      x =
    φ Y₁ x

Tactic:
rw [← hφ Y₂ X, ← hφ Y₁ ((StructuredArrow.map f).obj X)]

Premises used: CategoryTheory.StructuredArrow.map, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
φ : (Y : D) → P.obj Y → (F ⋙ P).ColimitType
hφ :
  ∀ (Y : D) (j : StructuredArrow Y F),
    Function.comp (β := (F ⋙ P).obj j.right) ((F ⋙ P).ιColimitType j.right)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj j.right))) =
      φ Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
x : (fun (X : Type w) ↦ X) (P.obj Y₁)
X : StructuredArrow Y₂ F
⊢ Function.comp (β := P.obj Y₂)
      (Function.comp (β := (F ⋙ P).obj X.right) ((F ⋙ P).ιColimitType X.right)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map X.hom)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y₂)) → (fun (X : Type w) ↦ X) (P.obj (F.obj X.right))))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f)) :
        (a : (fun (X : Type w) ↦ X) (P.obj Y₁)) → (fun (X : Type w) ↦ X) (P.obj Y₂))
      x =
    Function.comp (β := (F ⋙ P).obj (obj (StructuredArrow.map f) X).right)
      ((F ⋙ P).ιColimitType (obj (StructuredArrow.map f) X).right)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (obj (StructuredArrow.map f) X).hom)) :
        (a : (fun (X : Type w) ↦ X) (P.obj Y₁)) →
          (fun (X : Type w) ↦ X) (P.obj (F.obj ((StructuredArrow.map f).obj X).right)))
      x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
φ : (Y : D) → P.obj Y → (F ⋙ P).ColimitType
hφ :
  ∀ (Y : D) (j : StructuredArrow Y F),
    Function.comp (β := (F ⋙ P).obj j.right) ((F ⋙ P).ιColimitType j.right)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj j.right))) =
      φ Y
c : P.CoconeTypes := { pt := (F ⋙ P).ColimitType, ι := fun (Y : D) ↦ φ Y, ι_naturality := ⋯ }
⊢ Function.Injective (F.colimitTypePrecomp P)

Tactic:
Function.RightInverse.injective (g := (P.descColimitType c)) (fun x ↦ ?_)

Premises used: Function.RightInverse.injective
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
φ : (Y : D) → P.obj Y → (F ⋙ P).ColimitType
hφ :
  ∀ (Y : D) (j : StructuredArrow Y F),
    Function.comp (β := (F ⋙ P).obj j.right) ((F ⋙ P).ιColimitType j.right)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj j.right))) =
      φ Y
c : P.CoconeTypes := { pt := (F ⋙ P).ColimitType, ι := fun (Y : D) ↦ φ Y, ι_naturality := ⋯ }
refine_1 : ∀ (x : (F ⋙ P).ColimitType), P.descColimitType c (F.colimitTypePrecomp P x) = x
⊢ Function.Injective (F.colimitTypePrecomp P)

Tactic:
refine Function.RightInverse.injective (g := (P.descColimitType c)) (fun x ↦ ?_)

Premises used: Function.RightInverse.injective
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
φ : (Y : D) → P.obj Y → (F ⋙ P).ColimitType
hφ :
  ∀ (Y : D) (j : StructuredArrow Y F),
    Function.comp (β := (F ⋙ P).obj j.right) ((F ⋙ P).ιColimitType j.right)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj j.right))) =
      φ Y
c : P.CoconeTypes := { pt := (F ⋙ P).ColimitType, ι := fun (Y : D) ↦ φ Y, ι_naturality := ⋯ }
x : (F ⋙ P).ColimitType
refine_1 :
  ∀ (X : C) (x : (F ⋙ P).obj X),
    P.descColimitType c (F.colimitTypePrecomp P ((F ⋙ P).ιColimitType X x)) = (F ⋙ P).ιColimitType X x
⊢ P.descColimitType c (F.colimitTypePrecomp P x) = x

Tactic:
obtain ⟨X, x, rfl⟩ := (F ⋙ P).ιColimitType_jointly_surjective x

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
φ : (Y : D) → P.obj Y → (F ⋙ P).ColimitType
hφ :
  ∀ (Y : D) (j : StructuredArrow Y F),
    Function.comp (β := (F ⋙ P).obj j.right) ((F ⋙ P).ιColimitType j.right)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.hom)) :
          (a : (fun (X : Type w) ↦ X) (P.obj Y)) → (fun (X : Type w) ↦ X) (P.obj (F.obj j.right))) =
      φ Y
c : P.CoconeTypes := { pt := (F ⋙ P).ColimitType, ι := fun (Y : D) ↦ φ Y, ι_naturality := ⋯ }
X : C
x : (F ⋙ P).obj X
⊢ P.descColimitType c (F.colimitTypePrecomp P ((F ⋙ P).ιColimitType X x)) = (F ⋙ P).ιColimitType X x

Tactic:
simp [c, ← hφ (F.obj X) (StructuredArrow.mk (𝟙 _))]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.StructuredArrow.mk, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
x : P.ColimitType
refine_2 : ∀ (X : D) (x : P.obj X), ∃ (a : (F ⋙ P).ColimitType), F.colimitTypePrecomp P a = P.ιColimitType X x
⊢ ∃ (a : (F ⋙ P).ColimitType), F.colimitTypePrecomp P a = x

Tactic:
obtain ⟨X, x, rfl⟩ := P.ιColimitType_jointly_surjective x

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
X : D
x : P.obj X
Y : StructuredArrow X F := Classical.arbitrary (StructuredArrow X F)
⊢ F.colimitTypePrecomp P
      ((F ⋙ P).ιColimitType Y.right
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Y.hom) :
            (a : (fun (X : Type w) ↦ X) (P.obj X)) → (fun (X : Type w) ↦ X) (P.obj (F.obj Y.right)))
          x)) =
    P.ιColimitType X x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Final.Type
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : Functor.{v₂, w, u₂, w + 1} D (Type w)
inst_2 : F.Final
X : D
x : P.obj X
Y : StructuredArrow X F := Classical.arbitrary (StructuredArrow X F)
⊢ ∃ (a : (F ⋙ P).ColimitType), F.colimitTypePrecomp P a = P.ιColimitType X x

Tactic:
exact ⟨(F ⋙ P).ιColimitType Y.right (P.map Y.hom x), by simp⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_2 : F.op.Initial
⊢ F.Final

Tactic:
{
    out := fun d =>
      @isConnected_of_isConnected_op _ _
        (isConnected_of_equivalent (structuredArrowOpEquivalence F d).symm) }

Premises used: CategoryTheory.Functor.Final.mk, CategoryTheory.isConnected_of_isConnected_op
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_2 : F.op.Final
⊢ F.Initial

Tactic:
{
    out := fun d =>
      @isConnected_of_isConnected_op _ _
        (isConnected_of_equivalent (costructuredArrowOpEquivalence F d).symm) }

Premises used: CategoryTheory.Functor.Initial.mk, CategoryTheory.isConnected_of_isConnected_op
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
c : C
u : StructuredArrow c R := StructuredArrow.mk (adj.unit.app c)
f g : StructuredArrow c R
⊢ u.hom ≫
      R.map
        (((Equiv.symm (adj.homEquiv c f.right) : Equiv.{v₁ + 1, v₂ + 1} (c ⟶ R.obj f.right) (L.obj c ⟶ f.right)) :
            (a : c ⟶ R.obj f.right) → L.obj c ⟶ f.right)
          f.hom) =
    f.hom

Tactic:
simp [u]