awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty.{v_1 + 1} (X ⟶ Z)
h₂ :
  ∀ ⦃Z : C⦄ (i j : X ⟶ Z),
    Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) i) (mk (Y := zero) j)
Z : C
this : Nonempty.{max 1 (v_1 + 1)} (CostructuredArrow (parallelPair f g) Z)
as : PUnit.{1}
φ : (parallelPair f g).obj zero ⟶ Functor.obj.{0, v_1, 0, u_1} (Functor.fromPUnit Z) { as := as : Discrete PUnit.{1} }
⊢ Zigzag
    { left := zero, right := { as := as : Discrete PUnit.{1} }, hom := φ :
      Comma (parallelPair f g) (Functor.fromPUnit Z) }
    (mk (Y := zero) ⋯.some)

Tactic:
apply h₂
-- Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty.{v_1 + 1} (X ⟶ Z)
h₂ :
  ∀ ⦃Z : C⦄ (i j : X ⟶ Z),
    Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) i) (mk (Y := zero) j)
Z : C
this : Nonempty.{max 1 (v_1 + 1)} (CostructuredArrow (parallelPair f g) Z)
as : PUnit.{1}
φ : (parallelPair f g).obj one ⟶ Functor.obj.{0, v_1, 0, u_1} (Functor.fromPUnit Z) { as := as : Discrete PUnit.{1} }
⊢ Zigzag
    { left := one, right := { as := as : Discrete PUnit.{1} }, hom := φ :
      Comma (parallelPair f g) (Functor.fromPUnit Z) }
    (mk (Y := zero) ⋯.some)

Tactic:
Zigzag.trans ?_ (h₂ (f ≫ φ) _)

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Zigzag.trans
-- Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty.{v_1 + 1} (X ⟶ Z)
h₂ :
  ∀ ⦃Z : C⦄ (i j : X ⟶ Z),
    Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) i) (mk (Y := zero) j)
Z : C
this : Nonempty.{max 1 (v_1 + 1)} (CostructuredArrow (parallelPair f g) Z)
as : PUnit.{1}
φ :
  (parallelPair f g).obj WalkingParallelPair.one ⟶
    Functor.obj.{0, v_1, 0, u_1} (Functor.fromPUnit Z) { as := as : Discrete PUnit.{1} }
one :
  Zigzag
    { left := WalkingParallelPair.one, right := { as := as : Discrete PUnit.{1} }, hom := φ :
      Comma (parallelPair f g) (Functor.fromPUnit Z) }
    (mk (Y := zero) (f ≫ φ))
⊢ Zigzag
    { left := WalkingParallelPair.one, right := { as := as : Discrete PUnit.{1} }, hom := φ :
      Comma (parallelPair f g) (Functor.fromPUnit Z) }
    (mk (Y := zero) ⋯.some)

Tactic:
refine Zigzag.trans ?_ (h₂ (f ≫ φ) _)

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Zigzag.trans
-- Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty.{v_1 + 1} (X ⟶ Z)
h₂ :
  ∀ ⦃Z : C⦄ (i j : X ⟶ Z),
    Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) i) (mk (Y := zero) j)
Z : C
this : Nonempty.{max 1 (v_1 + 1)} (CostructuredArrow (parallelPair f g) Z)
as : PUnit.{1}
φ : (parallelPair f g).obj one ⟶ Functor.obj.{0, v_1, 0, u_1} (Functor.fromPUnit Z) { as := as : Discrete PUnit.{1} }
⊢ Zigzag
    { left := one, right := { as := as : Discrete PUnit.{1} }, hom := φ :
      Comma (parallelPair f g) (Functor.fromPUnit Z) }
    (mk (Y := zero) (f ≫ φ))

Tactic:
Zigzag.of_inv (homMk left)

Premises used: CategoryTheory.CostructuredArrow.homMk, CategoryTheory.Limits.WalkingParallelPairHom.left, CategoryTheory.Zigzag.of_inv
-- Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty.{v_1 + 1} (X ⟶ Z)
h₂ :
  ∀ ⦃Z : C⦄ (i j : X ⟶ Z),
    Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) i) (mk (Y := zero) j)
Z : C
this : Nonempty.{max 1 (v_1 + 1)} (CostructuredArrow (parallelPair f g) Z)
as : PUnit.{1}
φ : (parallelPair f g).obj one ⟶ Functor.obj.{0, v_1, 0, u_1} (Functor.fromPUnit Z) { as := as : Discrete PUnit.{1} }
⊢ Zigzag
    { left := one, right := { as := as : Discrete PUnit.{1} }, hom := φ :
      Comma (parallelPair f g) (Functor.fromPUnit Z) }
    (mk (Y := zero) (f ≫ φ))

Tactic:
exact Zigzag.of_inv (homMk left)
-- Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty.{v_1 + 1} (X ⟶ Z)
h₂ :
  ∀ ⦃Z : C⦄ (i j : X ⟶ Z),
    Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) i) (mk (Y := zero) j)
Z : C
this : Nonempty.{max 1 (v_1 + 1)} (CostructuredArrow (parallelPair f g) Z)
⊢ ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x (mk (Y := zero) ⋯.some)

Tactic:
have : ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x
      (mk (Y := zero) (h₁ Z).some) := by
        rintro ⟨(_ | _), ⟨⟩, φ⟩
        · apply h₂
        · refine Zigzag.trans ?_ (h₂ (f ≫ φ) _)
          exact Zigzag.of_inv (homMk left)
-- Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty.{v_1 + 1} (X ⟶ Z)
h₂ :
  ∀ ⦃Z : C⦄ (i j : X ⟶ Z),
    Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) i) (mk (Y := zero) j)
Z : C
this_1 : Nonempty.{max 1 (v_1 + 1)} (CostructuredArrow (parallelPair f g) Z)
this : ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x (mk (Y := zero) ⋯.some)
⊢ IsConnected.{0, v_1} (CostructuredArrow (parallelPair f g) Z)

Tactic:
zigzag_isConnected (fun x y => (this x).trans (this y).symm)

Premises used: CategoryTheory.zigzag_isConnected, CategoryTheory.Zigzag.trans, CategoryTheory.Zigzag.symm
-- Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty.{v_1 + 1} (X ⟶ Z)
h₂ :
  ∀ ⦃Z : C⦄ (i j : X ⟶ Z),
    Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) i) (mk (Y := zero) j)
Z : C
this_1 : Nonempty.{max 1 (v_1 + 1)} (CostructuredArrow (parallelPair f g) Z)
this : ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x (mk (Y := zero) ⋯.some)
⊢ IsConnected.{0, v_1} (CostructuredArrow (parallelPair f g) Z)

Tactic:
exact zigzag_isConnected (fun x y => (this x).trans (this y).symm)

Premises used: CategoryTheory.zigzag_isConnected, CategoryTheory.Zigzag.trans, CategoryTheory.Zigzag.symm
-- Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty.{v_1 + 1} (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ (a : Y ⟶ Z), i = f ≫ a ∧ j = g ≫ a
Z : C
i j : X ⟶ Z
obtain :
  ∀ (a : Y ⟶ Z),
    Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) (f ≫ a)) (mk (Y := zero) (g ≫ a))
⊢ Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) i) (mk (Y := zero) j)

Tactic:
obtain ⟨a, rfl, rfl⟩ := h₂ i j

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty.{v_1 + 1} (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ (a : Y ⟶ Z), i = f ≫ a ∧ j = g ≫ a
Z : C
a : Y ⟶ Z
f₁ : mk (f ≫ a) ⟶ mk (Y := one) a := homMk WalkingParallelPairHom.left ⋯
f₂ : mk (g ≫ a) ⟶ mk (Y := one) a := homMk right ⋯
⊢ Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) (f ≫ a)) (mk (Y := zero) (g ≫ a))

Tactic:
Zigzag.of_hom_inv f₁ f₂

Premises used: CategoryTheory.Zigzag.of_hom_inv
-- Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty.{v_1 + 1} (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ (a : Y ⟶ Z), i = f ≫ a ∧ j = g ≫ a
Z : C
a : Y ⟶ Z
f₁ : mk (f ≫ a) ⟶ mk (Y := one) a := homMk WalkingParallelPairHom.left ⋯
f₂ : mk (g ≫ a) ⟶ mk (Y := one) a := homMk right ⋯
⊢ Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) (f ≫ a)) (mk (Y := zero) (g ≫ a))

Tactic:
exact Zigzag.of_hom_inv f₁ f₂

Premises used: CategoryTheory.Zigzag.of_hom_inv
-- 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
⊢ Function.Bijective (α := (↑P.sections : Type (max u₂ w))) F.sectionsPrecomp

Tactic:
⟨fun s₁ s₂ h ↦ ?_, fun t ↦ ?_⟩

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.Initial
refine_1 : ∀ (s₁ s₂ : (↑P.sections : Type (max u₂ w))) (h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂), s₁ = s₂
refine_2 :
  ∀ (t : (↑(F ⋙ P).sections : Type (max u₁ w))), ∃ (a : (↑P.sections : Type (max u₂ w))), F.sectionsPrecomp a = t
⊢ Function.Bijective (α := (↑P.sections : Type (max u₂ w))) F.sectionsPrecomp

Tactic:
refine ⟨fun s₁ s₂ h ↦ ?_, fun t ↦ ?_⟩
-- 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
s₁ s₂ : (↑P.sections : Type (max u₂ w))
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
refine_1 : ∀ (Y : D), (↑s₁ : (j : D) → P.obj j) Y = (↑s₂ : (j : D) → P.obj j) Y
⊢ s₁ = s₂

Tactic:
ext Y
-- 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
s₁ s₂ : (↑P.sections : Type (max u₂ w))
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
Y : D
X : CostructuredArrow F Y := Classical.arbitrary (CostructuredArrow F Y)
⊢ (↑(F.sectionsPrecomp s₁) : (x : C) → (F ⋙ P).obj x) X.left =
    (↑(F.sectionsPrecomp s₂) : (x : C) → (F ⋙ P).obj x) X.left

Tactic:
have := congr_fun (congr_arg Subtype.val h) X.left
-- 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
s₁ s₂ : (↑P.sections : Type (max u₂ w))
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
Y : D
X : CostructuredArrow F Y := Classical.arbitrary (CostructuredArrow F Y)
this :
  (↑(F.sectionsPrecomp s₁) : (x : C) → (F ⋙ P).obj x) X.left =
    (↑(F.sectionsPrecomp s₂) : (x : C) → (F ⋙ P).obj x) X.left
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map X.hom) :
        (a : (fun (X : Type w) ↦ X) (P.obj (F.obj X.left))) → (fun (X : Type w) ↦ X) (P.obj Y))
      ((↑s₁ : (j : D) → P.obj j) (F.obj X.left)) =
    (↑s₁ : (j : D) → P.obj j) Y

Tactic:
have h₁ := s₁.property X.hom
-- 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
s₁ s₂ : (↑P.sections : Type (max u₂ w))
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
Y : D
X : CostructuredArrow F Y := Classical.arbitrary (CostructuredArrow F Y)
this :
  (↑(F.sectionsPrecomp s₁) : (x : C) → (F ⋙ P).obj x) X.left =
    (↑(F.sectionsPrecomp s₂) : (x : C) → (F ⋙ P).obj x) X.left
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map X.hom) :
        (a : (fun (X : Type w) ↦ X) (P.obj (F.obj X.left))) → (fun (X : Type w) ↦ X) (P.obj Y))
      ((↑s₁ : (j : D) → P.obj j) (F.obj X.left)) =
    (↑s₁ : (j : D) → P.obj j) Y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map X.hom) :
        (a : (fun (X : Type w) ↦ X) (P.obj (F.obj X.left))) → (fun (X : Type w) ↦ X) (P.obj Y))
      ((↑s₂ : (j : D) → P.obj j) (F.obj X.left)) =
    (↑s₂ : (j : D) → P.obj j) Y

Tactic:
have h₂ := s₂.property X.hom
-- 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
s₁ s₂ : (↑P.sections : Type (max u₂ w))
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
Y : D
X : CostructuredArrow F Y := Classical.arbitrary (CostructuredArrow F Y)
this : (↑s₁ : (j : D) → P.obj j) (F.obj X.left) = (↑s₂ : (j : D) → P.obj j) (F.obj X.left)
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map X.hom) : (a : P.obj (F.obj X.left)) → P.obj Y)
      ((↑s₁ : (j : D) → P.obj j) (F.obj X.left)) =
    (↑s₁ : (j : D) → P.obj j) Y
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map X.hom) : (a : P.obj (F.obj X.left)) → P.obj Y)
      ((↑s₂ : (j : D) → P.obj j) (F.obj X.left)) =
    (↑s₂ : (j : D) → P.obj j) Y
refine_1 :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map X.hom) : (a : P.obj (F.obj X.left)) → P.obj Y)
      ((↑s₁ : (j : D) → P.obj j) (F.obj X.left)) =
    (↑s₂ : (j : D) → P.obj j) Y
refine_1₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map X.hom) : (a : P.obj (F.obj X.left)) → P.obj Y)
      ((↑s₂ : (j : D) → P.obj j) (F.obj X.left)) =
    (↑s₂ : (j : D) → P.obj j) Y
refine_1₂ refine_1₃ : (↑s₂ : (j : D) → P.obj j) Y = (↑s₂ : (j : D) → P.obj j) Y
⊢ (↑s₁ : (j : D) → P.obj j) Y = (↑s₂ : (j : D) → P.obj j) Y

Tactic:
rw [← h₁, this, 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.Initial
t : (↑(F ⋙ P).sections : Type (max u₁ w))
Y : D
h :
  ∀ (j₁ j₂ : CostructuredArrow F Y) (x : j₁ ⟶ j₂),
    Eq (α := P.obj 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) :
        (fun (X : Type w) ↦ X) (P.obj 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) :
        (fun (X : Type w) ↦ X) (P.obj Y))
⊢ ∃ (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:
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.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 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 : (fun (X : Type w) ↦ X) (P.obj (F.obj Z₁.left))) → (fun (X : Type w) ↦ X) (P.obj Y))
        ((↑t : (j : C) → (F ⋙ P).obj j) Z₁.left) :
      (fun (X : Type w) ↦ X) (P.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map Z₂.hom) :
          (a : (fun (X : Type w) ↦ X) (P.obj (F.obj Z₂.left))) → (fun (X : Type w) ↦ X) (P.obj Y))
        ((↑t : (j : C) → (F ⋙ P).obj j) Z₂.left) :
      (fun (X : Type w) ↦ X) (P.obj Y))

Tactic:
dsimp
-- 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))
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 Z₂.hom) : (a : P.obj (F.obj Z₂.left)) → P.obj Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ P).map φ.left) :
              (a : (fun (X : Type w) ↦ X) ((F ⋙ P).obj Z₁.left)) → (fun (X : Type w) ↦ X) ((F ⋙ P).obj Z₂.left))
            ((↑t : (j : C) → (F ⋙ P).obj j) Z₁.left) :
          (fun (X : Type w) ↦ X) ((F ⋙ P).obj 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)
        ((↑t : (j : C) → P.obj (F.obj j)) Z₂.left) :
      P.obj Y)

Tactic:
rw [← t.property φ.left]

Premises used: CategoryTheory.CommaMorphism.left, Subtype.property
-- 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))
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 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)
⊢ 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) ((F ⋙ P).map φ.left) :
              (a : (fun (X : Type w) ↦ X) ((F ⋙ P).obj Z₁.left)) → (fun (X : Type w) ↦ X) ((F ⋙ P).obj Z₂.left))
            ((↑t : (j : C) → (F ⋙ P).obj j) Z₁.left) :
          (fun (X : Type w) ↦ X) ((F ⋙ P).obj Z₂.left)) :
      P.obj Y)

Tactic:
dsimp
-- 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))
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)
h₂ 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)
⊢ 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)

Tactic:
rw [← comp_apply, ← Functor.map_comp, CostructuredArrow.w]

Premises used: CategoryTheory.CostructuredArrow.w, 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.Initial
t : (↑(F ⋙ P).sections : Type (max u₁ w))
⊢ ∀ (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]
-- 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))
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
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
⊢ ∃ (a : (↑P.sections : Type (max u₂ w))), F.sectionsPrecomp a = t

Tactic:
choose val hval 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.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

Tactic:
⟨⟨val, fun {Y₁ Y₂} f ↦ ?_⟩, ?_⟩

Premises used: Subtype.mk, Exists.intro