awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
y y' : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))
hy :
  Eq (α := (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
    ((hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        y :
      (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
    ((hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        y' :
      (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
ky : (i : α) → I i
yk₀ : (pointwiseProduct (I := I) F).obj ky
hyk₀ :
  (hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) ky) :
        (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj ky)) →
          (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
      yk₀ =
    y
⊢ y = y'
have refine_1 : ∀ (ky' : (i : α) → I i) (yk₀' : (pointwiseProduct (I := I) F).obj ky')
  (hyk₀' :
    (hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) ky') :
          (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj ky')) →
            (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
        yk₀' =
      y'),
  y = y'
Tactic: obtain ⟨ky', yk₀', hyk₀'⟩ := Types.jointly_surjective' y'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (hypothesis)
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
x : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))
⊢ ∃ (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))),
    (hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        a =
      x
have hch : ∀ (s : α),
  ∃ (i : I s) (xi : (F s).obj i),
    Eq (α := (fun (X : Type u) ↦ X) (colimit (F s)))
      ((hom (FC := TypeCat.Fun) (colimit.ι (F s) i) :
            (a : (fun (X : Type u) ↦ X) ((F s).obj i)) → (fun (X : Type u) ↦ X) (colimit (F s)))
          xi :
        (fun (X : Type u) ↦ X) (colimit (F s)))
      ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ colimit (F s)) s) :
            (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
          x :
        (fun (X : Type u) ↦ X) (colimit (F s)))
Tactic: have hch : ∀ (s : α), ∃ (i : I s) (xi : (F s).obj i), colimit.ι (F s) i xi =
        Pi.π (fun s => colimit (F s)) s x := fun s => Types.jointly_surjective' _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
x : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))
hch :
  ∀ (s : α),
    ∃ (i : I s) (xi : (F s).obj i),
      Eq (α := (fun (X : Type u) ↦ X) (colimit (F s)))
        ((hom (FC := TypeCat.Fun) (colimit.ι (F s) i) :
              (a : (fun (X : Type u) ↦ X) ((F s).obj i)) → (fun (X : Type u) ↦ X) (colimit (F s)))
            xi :
          (fun (X : Type u) ↦ X) (colimit (F s)))
        ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ colimit (F s)) s) :
              (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
            x :
          (fun (X : Type u) ↦ X) (colimit (F s)))
⊢ ∃ (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))),
    (hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        a =
      x
have refine_2 : ∀ (k : (s : α) → I s) (p : (s : α) → (F s).obj (k s))
  (hk :
    ∀ (s : α),
      Eq (α := (fun (X : Type u) ↦ X) (colimit (F s)))
        ((hom (FC := TypeCat.Fun) (colimit.ι (F s) (k s)) :
              (a : (fun (X : Type u) ↦ X) ((F s).obj (k s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
            (p s) :
          (fun (X : Type u) ↦ X) (colimit (F s)))
        ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ colimit (F s)) s) :
              (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
            x :
          (fun (X : Type u) ↦ X) (colimit (F s)))),
  ∃ (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))),
    (hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        a =
      x
Tactic: choose k p hk using hch
Cleared hypotheses: hch
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
x : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))
k : (s : α) → I s
p : (s : α) → (F s).obj (k s)
hk :
  ∀ (s : α),
    Eq (α := (fun (X : Type u) ↦ X) (colimit (F s)))
      ((hom (FC := TypeCat.Fun) (colimit.ι (F s) (k s)) :
            (a : (fun (X : Type u) ↦ X) ((F s).obj (k s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
          (p s) :
        (fun (X : Type u) ↦ X) (colimit (F s)))
      ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ colimit (F s)) s) :
            (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
          x :
        (fun (X : Type u) ↦ X) (colimit (F s)))
⊢ ∃ (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))),
    (hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        a =
      x
have refine_2 : (hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
      (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
        (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
    ((hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) k) :
          (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj k)) →
            (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
        ((hom (FC := TypeCat.Fun) (productIso ((Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k)).inv :
              (a : (fun (X : Type u) ↦ X) ((j : α) → (Functor.pi F).obj k j)) →
                (fun (X : Type u) ↦ X) (∏ᶜ (Functor.pi F).obj k))
            p :
          (fun (X : Type u) ↦ X) (∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k)) :
      (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))) =
  x
Tactic: refine ⟨colimit.ι (pointwiseProduct F) k ((Types.productIso _).inv p), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
inst_1 : HasProductsOfShape.{u_1, u, v} ι C
inst_2 : IsIPCOfShape.{w, u_1, v, u} ι C
inst_3 : HasFilteredColimitsOfSize.{w, w, v, u} C
D : Type u₁
inst_4 : Category.{v₁, u₁} D
J : ι → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → J i ⥤ Functor.{v₁, v, u₁, u} D C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
⊢ Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))
have refine : (X : D) →
  IsColimit (F := pointwiseProduct (I := J) F ⋙ Functor.obj (evaluation D C) X)
    (Functor.mapCocone (Functor.obj (evaluation D C) X) (coconePointwiseProduct (I := J) c))
Tactic: refine ⟨evaluationJointlyReflectsColimits _ fun X ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Connected (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
inst_1 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
⊢ IsConnected.{v, u} C ↔ F.Final
have rw : IsConnected (StructuredArrow { as := default } F) ↔ F.Final
Tactic: rw [← isConnected_iff_of_equivalence
    (Discrete.structuredArrowEquivalenceOfUnique F default)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Connected (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
inst_1 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
⊢ IsConnected (StructuredArrow { as := default } F) ↔ F.Final
have refine : IsConnected (StructuredArrow { as := default } F) → ∀ (d : Discrete T), IsConnected (StructuredArrow d F)
Tactic: refine ⟨fun _ ↦ ⟨?_⟩, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Connected (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
inst_1 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
⊢ IsConnected.{v, u} C ↔ F.Initial
have rw : IsConnected (CostructuredArrow F { as := default }) ↔ F.Initial
Tactic: rw [← isConnected_iff_of_equivalence
    (Discrete.costructuredArrowEquivalenceOfUnique F default)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.Connected (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
inst_1 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
⊢ IsConnected (CostructuredArrow F { as := default }) ↔ F.Initial
have refine : IsConnected (CostructuredArrow F { as := default }) → ∀ (d : Discrete T), IsConnected (CostructuredArrow F d)
Tactic: refine ⟨fun _ ↦ ⟨?_⟩, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.ParallelPair (hypothesis)
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
⊢ IsConnected.{0, v_1} (CostructuredArrow (parallelPair f g) Z)
have this : Nonempty.{max 1 (v_1 + 1)} (CostructuredArrow (parallelPair f g) Z)
Tactic: have : Nonempty (CostructuredArrow (parallelPair f g) Z) :=
      ⟨mk (Y := zero) (h₁ Z).some⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.ParallelPair (goal)
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)
have one : Zigzag
  { left := one, right := { as := as : Discrete PUnit.{1} }, hom := φ : Comma (parallelPair f g) (Functor.fromPUnit Z) }
  (mk (Y := zero) (f ≫ φ))
Tactic: refine Zigzag.trans ?_ (h₂ (f ≫ φ) _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.ParallelPair (hypothesis)
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)
⊢ IsConnected.{0, v_1} (CostructuredArrow (parallelPair f g) Z)
have this₁ : ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x (mk (Y := zero) sorry.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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final.ParallelPair (goal)
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
⊢ Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) i) (mk (Y := zero) j)
have obtain : ∀ (a : Y ⟶ Z),
  Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) (f ≫ a)) (mk (Y := zero) (g ≫ a))
Tactic: obtain ⟨a, rfl, rfl⟩ := h₂ i j
Cleared hypotheses: i, j
-- 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
⊢ Function.Bijective (α := (↑P.sections : Type (max u₂ w))) F.sectionsPrecomp
have refine_1 : ∀ (s₁ s₂ : (↑P.sections : Type (max u₂ w))) (h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂), s₁ = s₂
Tactic: refine ⟨fun s₁ s₂ h ↦ ?_, fun t ↦ ?_⟩
-- 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
refine_1 : ∀ (s₁ s₂ : (↑P.sections : Type (max u₂ w))) (h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂), s₁ = s₂
⊢ Function.Bijective (α := (↑P.sections : Type (max u₂ w))) F.sectionsPrecomp
have refine_2 : ∀ (t : (↑(F ⋙ P).sections : Type (max u₁ w))), ∃ (a : (↑P.sections : Type (max u₂ w))), F.sectionsPrecomp a = t
Tactic: refine ⟨fun s₁ s₂ h ↦ ?_, fun t ↦ ?_⟩
-- 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
s₁ s₂ : (↑P.sections : Type (max u₂ w))
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
⊢ s₁ = s₂
have refine_1 : ∀ (Y : D), (↑s₁ : (j : D) → P.obj j) Y = (↑s₂ : (j : D) → P.obj j) Y
Tactic: ext Y
-- 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
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)
⊢ (↑s₁ : (j : D) → P.obj j) Y = (↑s₂ : (j : D) → P.obj j) Y
have this : (↑(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
-- 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
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
⊢ (↑s₁ : (j : D) → P.obj j) Y = (↑s₂ : (j : D) → P.obj j) Y
have 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
Tactic: have h₁ := s₁.property X.hom
-- 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
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
⊢ (↑s₁ : (j : D) → P.obj j) Y = (↑s₂ : (j : D) → P.obj j) Y
have 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
Tactic: have h₂ := s₂.property X.hom
-- 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
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
⊢ (↑s₁ : (j : D) → P.obj j) Y = (↑s₂ : (j : D) → P.obj j) Y
have 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
Tactic: rw [← h₁, this, 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
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
⊢ (↑s₁ : (j : D) → P.obj j) Y = (↑s₂ : (j : D) → P.obj j) Y
have refine_1₂ : (↑s₂ : (j : D) → P.obj j) Y = (↑s₂ : (j : D) → P.obj j) Y
Tactic: rw [← h₁, this, 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))
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
have 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))
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.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)
        ((↑t : (j : C) → P.obj (F.obj j)) 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)
      ((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: rw [← t.property φ.left]
-- 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) ((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)
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)
      ((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: dsimp