awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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))
Y : D
Z₁ Z₂ : CostructuredArrow F Y
φ : Z₁ ⟶ Z₂
⊢ Eq (α := P.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom) : (a : P.obj (F.obj Z₁.left)) → P.obj Y)
        ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
      P.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₂.hom) : (a : P.obj (F.obj Z₂.left)) → P.obj Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (F.map φ.left)) :
              (a : P.obj (F.obj Z₁.left)) → P.obj (F.obj Z₂.left))
            ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
          P.obj (F.obj Z₂.left)) :
      P.obj Y)
have h : Eq (α := P.obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom) : (a : P.obj (F.obj Z₁.left)) → P.obj Y)
      ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
    P.obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (F.map φ.left) ≫ P.map Z₂.hom) :
        (a : P.obj (F.obj Z₁.left)) → P.obj Y)
      ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
    P.obj Y)
Tactic: rw [← comp_apply, ← Functor.map_comp, CostructuredArrow.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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))
Y : D
Z₁ Z₂ : CostructuredArrow F Y
φ : Z₁ ⟶ Z₂
h :
  Eq (α := P.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom) : (a : P.obj (F.obj Z₁.left)) → P.obj Y)
        ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
      P.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (F.map φ.left) ≫ P.map Z₂.hom) :
          (a : P.obj (F.obj Z₁.left)) → P.obj Y)
        ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
      P.obj Y)
⊢ Eq (α := P.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom) : (a : P.obj (F.obj Z₁.left)) → P.obj Y)
        ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
      P.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₂.hom) : (a : P.obj (F.obj Z₂.left)) → P.obj Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (F.map φ.left)) :
              (a : P.obj (F.obj Z₁.left)) → P.obj (F.obj Z₂.left))
            ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
          P.obj (F.obj Z₂.left)) :
      P.obj Y)
have h₁ : Eq (α := P.obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom) : (a : P.obj (F.obj Z₁.left)) → P.obj Y)
      ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
    P.obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (F.map φ.left ≫ Z₂.hom)) : (a : P.obj (F.obj Z₁.left)) → P.obj Y)
      ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
    P.obj Y)
Tactic: rw [← comp_apply, ← Functor.map_comp, CostructuredArrow.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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))
Y : D
Z₁ Z₂ : CostructuredArrow F Y
φ : Z₁ ⟶ Z₂
h :
  Eq (α := P.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom) : (a : P.obj (F.obj Z₁.left)) → P.obj Y)
        ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
      P.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (F.map φ.left) ≫ P.map Z₂.hom) :
          (a : P.obj (F.obj Z₁.left)) → P.obj Y)
        ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
      P.obj Y)
h₁ :
  Eq (α := P.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom) : (a : P.obj (F.obj Z₁.left)) → P.obj Y)
        ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
      P.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (F.map φ.left ≫ Z₂.hom)) : (a : P.obj (F.obj Z₁.left)) → P.obj Y)
        ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
      P.obj Y)
⊢ Eq (α := P.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom) : (a : P.obj (F.obj Z₁.left)) → P.obj Y)
        ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
      P.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₂.hom) : (a : P.obj (F.obj Z₂.left)) → P.obj Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (F.map φ.left)) :
              (a : P.obj (F.obj Z₁.left)) → P.obj (F.obj Z₂.left))
            ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
          P.obj (F.obj Z₂.left)) :
      P.obj Y)
have h₂ : Eq (α := P.obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom) : (a : P.obj (F.obj Z₁.left)) → P.obj Y)
      ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
    P.obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₁.hom) : (a : P.obj (F.obj Z₁.left)) → P.obj Y)
      ((↑t : (j : C) → P.obj (F.obj j)) Z₁.left) :
    P.obj Y)
Tactic: rw [← comp_apply, ← Functor.map_comp, CostructuredArrow.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (hypothesis)
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))
⊢ ∃ (a : (↑P.sections : Type (max u₂ w))), F.sectionsPrecomp a = t
have h : ∀ (Y : D),
  ∃ (a : P.obj Y),
    ∀ (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) =
        a
Tactic: have h (Y : D) : ∃ (a : P.obj Y),
        ∀ (j : CostructuredArrow F Y), P.map j.hom (t.val j.left) = a := by
      apply constant_of_preserves_morphisms'
      intro Z₁ Z₂ φ
      dsimp
      rw [← t.property φ.left]
      dsimp
      rw [← comp_apply, ← Functor.map_comp, CostructuredArrow.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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))
h :
  ∀ (Y : D),
    ∃ (a : P.obj Y),
      ∀ (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) =
          a
⊢ ∃ (a : (↑P.sections : Type (max u₂ w))), F.sectionsPrecomp a = t
have refine_2 : ∀ (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),
  ∃ (a : (↑P.sections : Type (max u₂ w))), F.sectionsPrecomp a = t
Tactic: choose val hval using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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
⊢ ∃ (a : (↑P.sections : Type (max u₂ w))), F.sectionsPrecomp a = t
have 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₂
Tactic: refine ⟨⟨val, fun {Y₁ Y₂} f ↦ ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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₂
⊢ ∃ (a : (↑P.sections : Type (max u₂ w))), F.sectionsPrecomp a = t
have refine_2₁ : F.sectionsPrecomp (Subtype.mk (p := fun (x : (j : D) → P.obj j) ↦ x ∈ P.sections) val sorry) = t
Tactic: refine ⟨⟨val, fun {Y₁ Y₂} f ↦ ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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
⊢ F.sectionsPrecomp (Subtype.mk (p := fun (x : (j : D) → P.obj j) ↦ x ∈ P.sections) val ⋯) = t
have refine_2 : ∀ (X : C),
  (↑(F.sectionsPrecomp (Subtype.mk (p := fun (x : (j : D) → P.obj j) ↦ x ∈ P.sections) val sorry)) :
        (j : C) → (F ⋙ P).obj j)
      X =
    (↑t : (j : C) → (F ⋙ P).obj j) X
Tactic: ext X : 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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)
have refine_1 : Function.Injective (F.colimitTypePrecomp P)
Tactic: refine ⟨?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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)
⊢ Function.Bijective (F.colimitTypePrecomp P)
have refine_2 : ∀ (x : P.ColimitType), ∃ (a : (F ⋙ P).ColimitType), F.colimitTypePrecomp P a = x
Tactic: refine ⟨?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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
have 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))))
Tactic: apply constant_of_preserves_morphisms'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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₂
⊢ 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))))
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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 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)
have 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)
Tactic: rw [← (F ⋙ P).ιColimitType_map f.right, comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (hypothesis)
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.Injective (F.colimitTypePrecomp P)
have 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
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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
⊢ Function.Injective (F.colimitTypePrecomp P)
have 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)
Tactic: choose φ hφ using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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₂
⊢ φ 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₁
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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₁)
⊢ (φ 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
have 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
Tactic: have X : StructuredArrow Y₂ F := Classical.arbitrary _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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
⊢ (φ 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
have 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
Tactic: rw [← hφ Y₂ X, ← hφ Y₁ ((StructuredArrow.map f).obj X)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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)
have refine_1 : ∀ (x : (F ⋙ P).ColimitType), P.descColimitType c (F.colimitTypePrecomp P x) = x
Tactic: refine Function.RightInverse.injective (g := (P.descColimitType c)) (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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
⊢ P.descColimitType c (F.colimitTypePrecomp P x) = x
have 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
Tactic: obtain ⟨X, x, rfl⟩ := (F ⋙ P).ιColimitType_jointly_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Type (goal)
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
⊢ ∃ (a : (F ⋙ P).ColimitType), F.colimitTypePrecomp P a = x
have refine_2 : ∀ (X : D) (x : P.obj X), ∃ (a : (F ⋙ P).ColimitType), F.colimitTypePrecomp P a = P.ιColimitType X x
Tactic: obtain ⟨X, x, rfl⟩ := P.ιColimitType_jointly_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
d : D
Z : (X : C) → (d ⟶ F.obj X) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : d ⟶ F.obj X₁) → (k₂ : d ⟶ F.obj X₂) → (f : X₁ ⟶ X₂) → k₁ ≫ F.map f = k₂ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : d ⟶ F.obj X₁) → (k₂ : d ⟶ F.obj X₂) → (f : X₁ ⟶ X₂) → k₁ ≫ F.map f = k₂ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : d ⟶ F.obj X₀
z : Z X₀ k₀
⊢ Z (lift F d) (homToLift F d)
have h : Nonempty.{u_1} (Z (lift F d) (homToLift F d))
Tactic: apply Nonempty.some