awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FinallySmall (goal)
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : InitiallySmall.{w, v, u} J
⊢ ∃ (s : Set J) (_ : Small.{w, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
have refine : ∀ (i : J),
  ∃ j ∈ Set.range.{u, w + 1} (ι := InitialModel.{w, v, u} J) (obj (fromInitialModel J)), Nonempty.{v + 1} (j ⟶ i)
Tactic: refine ⟨Set.range (fromInitialModel J).obj, inferInstance, fun i => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FinallySmall (goal)
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : InitiallySmall.{w, v, u} J
i : J
⊢ ∃ j ∈ Set.range.{u, w + 1} (ι := InitialModel.{w, v, u} J) (obj (fromInitialModel J)), Nonempty.{v + 1} (j ⟶ i)
have obtain : ∀ (f : CostructuredArrow.{w, v, w, u} (C := InitialModel.{w, v, u} J) (fromInitialModel J) i),
  ∃ j ∈ Set.range.{u, w + 1} (ι := InitialModel.{w, v, u} J) (obj (fromInitialModel J)), Nonempty.{v + 1} (j ⟶ i)
Tactic: obtain ⟨f⟩ : Nonempty (CostructuredArrow (fromInitialModel J) i) := IsConnected.is_nonempty
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FinallySmall (goal)
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
⊢ InitiallySmall.{v, v, u} J
have suffices : Initial.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s)
  (ObjectProperty.ι fun (x : J) ↦ x ∈ s)
Tactic: suffices Functor.Initial (ObjectProperty.ι (· ∈ s)) from
    initiallySmall_of_initial_of_essentiallySmall (ObjectProperty.ι (· ∈ s))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FinallySmall (goal)
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
⊢ Initial.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s)
    (ObjectProperty.ι fun (x : J) ↦ x ∈ s)
have refine : ∀ (i : J),
  ∃ (c : ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s),
    Nonempty.{v + 1} (obj (ObjectProperty.ι fun (x : J) ↦ x ∈ s) c ⟶ i)
Tactic: refine Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful _ (fun i => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FinallySmall (goal)
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
i : J
⊢ ∃ (c : ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s),
    Nonempty.{v + 1} (obj (ObjectProperty.ι fun (x : J) ↦ x ∈ s) c ⟶ i)
have obtain : ∀ (j : J) (hj₁ : j ∈ s) (hj₂ : Nonempty.{v + 1} (j ⟶ i)),
  ∃ (c : ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s),
    Nonempty.{v + 1} (obj (ObjectProperty.ι fun (x : J) ↦ x ∈ s) c ⟶ i)
Tactic: obtain ⟨j, hj₁, hj₂⟩ := hs i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FinallySmall (goal)
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
⊢ InitiallySmall.{v, v, u} J ↔
    ∃ (s : Set J) (_ : Small.{v, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
have refine : ∀ (h : ∃ (s : Set J) (_ : Small.{v, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)),
  InitiallySmall.{v, v, u} J
Tactic: refine ⟨fun _ => InitiallySmall.exists_small_weakly_initial_set _, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FinallySmall (goal)
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
h : ∃ (s : Set J) (_ : Small.{v, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
⊢ InitiallySmall.{v, v, u} J
have rcases : ∀ (s : Set J) (hs : Small.{v, u} (↑s : Type u)) (hs' : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)),
  InitiallySmall.{v, v, u} J
Tactic: rcases h with ⟨s, hs, hs'⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FintypeCat (goal)
Goal:
J : Type
inst : SmallCategory J
K : J ⥤ FintypeCat
j : J
⊢ Finite.{u + 1} ((K ⋙ FintypeCat.incl).obj j)
have simp : Finite.{u + 1} (K.obj j).obj
Tactic: simp only [comp_obj, FintypeCat.incl_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FintypeCat (goal)
Goal:
J : Type
inst : SmallCategory J
inst_1 : FinCategory J
K : J ⥤ Type u_1
inst_2 : ∀ (j : J), Finite.{u_1 + 1} (K.obj j)
⊢ Fintype (limit K)
have have : (this : Fintype (↑K.sections : Type u_1)) → Fintype (limit K)
Tactic: have : Fintype (sections K) := Fintype.ofFinite (sections K)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FintypeCat (goal)
Goal:
ι : Type u_1
inst : Finite ι
X : ι → FintypeCat
x : (i : ι) → (X i).obj
i : ι
⊢ (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (Pi.π X i : ∏ᶜ X ⟶ X i) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (∏ᶜ X)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (X i))
      (((Equiv.symm (productEquiv X) : ((i : ι) → (X i).obj) ≃ (∏ᶜ X).obj) : (a : (i : ι) → (X i).obj) → (∏ᶜ X).obj) x :
        (∏ᶜ X).obj) =
    x i
have rw : ((productEquiv X : (∏ᶜ X).obj ≃ ((i : ι) → (X i).obj)) : (a : (∏ᶜ X).obj) → (i : ι) → (X i).obj)
    (((Equiv.symm (productEquiv X) : ((i : ι) → (X i).obj) ≃ (∏ᶜ X).obj) : (a : (i : ι) → (X i).obj) → (∏ᶜ X).obj) x :
      (∏ᶜ X).obj)
    i =
  x i
Tactic: rw [← productEquiv_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FintypeCat (goal)
Goal:
ι : Type u_1
inst : Finite ι
X : ι → FintypeCat
x : (i : ι) → (X i).obj
i : ι
rw :
  ((productEquiv X : (∏ᶜ X).obj ≃ ((i : ι) → (X i).obj)) : (a : (∏ᶜ X).obj) → (i : ι) → (X i).obj)
      (((Equiv.symm (productEquiv X) : ((i : ι) → (X i).obj) ≃ (∏ᶜ X).obj) : (a : (i : ι) → (X i).obj) → (∏ᶜ X).obj) x :
        (∏ᶜ X).obj)
      i =
    x i
⊢ (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (Pi.π X i : ∏ᶜ X ⟶ X i) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (∏ᶜ X)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (X i))
      (((Equiv.symm (productEquiv X) : ((i : ι) → (X i).obj) ≃ (∏ᶜ X).obj) : (a : (i : ι) → (X i).obj) → (∏ᶜ X).obj) x :
        (∏ᶜ X).obj) =
    x i
have rw₁ : x i = x i
Tactic: rw [← productEquiv_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FintypeCat (hypothesis)
Goal:
J : Type
inst : SmallCategory J
inst_1 : FinCategory J
K : J ⥤ Type u_1
inst_2 : ∀ (j : J), Finite.{u_1 + 1} (K.obj j)
⊢ Fintype (colimit K)
have this : Finite.{u_1 + 1} (colimit K)
Tactic: have : Finite (colimit K) := finite_of_isColimit (colimit.isColimit K)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
X Y : FormalCoproduct.{w, u} C
f g : X ⟶ Y
h₁ : f.f = g.f
i : X.I
⊢ Y.obj (f.f i) = Y.obj (g.f i)
have rw : Y.obj (g.f i) = Y.obj (g.f i)
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : FormalCoproduct.{w, u} C
f g : X ⟶ Y
h₁ : f.f = g.f
h₂ : ∀ (i : X.I), f.φ i ≫ eqToHom ⋯ = g.φ i
⊢ f = g
have obtain : ∀ (f : X.I → Y.I) (F : (i : X.I) → X.obj i ⟶ Y.obj (f i)) (h₁ : { f := f, φ := F : Hom.{w, v, u} X Y }.f = g.f)
  (h₂ : ∀ (i : X.I), { f := f, φ := F : Hom.{w, v, u} X Y }.φ i ≫ eqToHom sorry = g.φ i),
  { f := f, φ := F : Hom.{w, v, u} X Y } = g
Tactic: obtain ⟨f, F⟩ := f
Cleared hypotheses: f, h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : FormalCoproduct.{w, u} C
g : X ⟶ Y
f : X.I → Y.I
F : (i : X.I) → X.obj i ⟶ Y.obj (f i)
h₁ : { f := f, φ := F : Hom.{w, v, u} X Y }.f = g.f
h₂ : ∀ (i : X.I), { f := f, φ := F : Hom.{w, v, u} X Y }.φ i ≫ eqToHom ⋯ = g.φ i
⊢ { f := f, φ := F : Hom.{w, v, u} X Y } = g
have obtain : ∀ (g : X.I → Y.I) (G : (i : X.I) → X.obj i ⟶ Y.obj (g i))
  (h₁ : { f := f, φ := F : Hom.{w, v, u} X Y }.f = { f := g, φ := G : Hom.{w, v, u} X Y }.f)
  (h₂ : ∀ (i : X.I), { f := f, φ := F : Hom.{w, v, u} X Y }.φ i ≫ eqToHom sorry = { f := g, φ := G }.φ i),
  { f := f, φ := F : Hom.{w, v, u} X Y } = { f := g, φ := G }
Tactic: obtain ⟨g, G⟩ := g
Cleared hypotheses: g, h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : FormalCoproduct.{w, u} C
f : X.I → Y.I
F : (i : X.I) → X.obj i ⟶ Y.obj (f i)
g : X.I → Y.I
G : (i : X.I) → X.obj i ⟶ Y.obj (g i)
h₁ : { f := f, φ := F : Hom.{w, v, u} X Y }.f = { f := g, φ := G : Hom.{w, v, u} X Y }.f
h₂ : ∀ (i : X.I), { f := f, φ := F : Hom.{w, v, u} X Y }.φ i ≫ eqToHom ⋯ = { f := g, φ := G }.φ i
⊢ { f := f, φ := F : Hom.{w, v, u} X Y } = { f := g, φ := G }
have obtain : ∀ (G : (i : X.I) → X.obj i ⟶ Y.obj (f i))
  (h₂ :
    ∀ (i : X.I), { f := f, φ := F : Hom.{w, v, u} X Y }.φ i ≫ eqToHom sorry = { f := f, φ := G : Hom.{w, v, u} X Y }.φ i),
  { f := f, φ := F : Hom.{w, v, u} X Y } = { f := f, φ := G }
Tactic: obtain rfl : f = g := h₁
Cleared hypotheses: g, G, h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : FormalCoproduct.{w, u} C
f : X.I → Y.I
F G : (i : X.I) → X.obj i ⟶ Y.obj (f i)
h₂ : ∀ (i : X.I), { f := f, φ := F : Hom.{w, v, u} X Y }.φ i ≫ eqToHom ⋯ = { f := f, φ := G : Hom.{w, v, u} X Y }.φ i
⊢ F = G
have h : ∀ (i : X.I), F i = G i
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : FormalCoproduct.{w, u} C
f : X.I → Y.I
F G : (i : X.I) → X.obj i ⟶ Y.obj (f i)
h₂ : ∀ (i : X.I), { f := f, φ := F : Hom.{w, v, u} X Y }.φ i ≫ eqToHom ⋯ = { f := f, φ := G : Hom.{w, v, u} X Y }.φ i
⊢ { f := f, φ := F : Hom.{w, v, u} X Y } = { f := f, φ := G }
have obtain : ∀
  (h₂ :
    ∀ (i : X.I), { f := f, φ := F : Hom.{w, v, u} X Y }.φ i ≫ eqToHom sorry = { f := f, φ := F : Hom.{w, v, u} X Y }.φ i),
  { f := f, φ := F : Hom.{w, v, u} X Y } = { f := f, φ := F }
Tactic: obtain rfl : F = G := by ext i; simpa using h₂ i
Cleared hypotheses: G, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
X Y : FormalCoproduct.{w, u} C
f g : X ⟶ Y
i : X.I
h₁ : f.f i = g.f i
⊢ Y.obj (f.f i) = Y.obj (g.f i)
have rw : Y.obj (g.f i) = Y.obj (g.f i)
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
X Y : FormalCoproduct.{w, u} C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj ((e : (a : X.I) → Y.I) i)
⊢ Eq (α := X ⟶ X)
    (CategoryStruct.comp (Y := Y) { f := (⇑e : (a : X.I) → Y.I), φ := fun (i : X.I) ↦ (h i).hom }
      { f := (⇑e.symm : (a : Y.I) → X.I), φ := fun (i : Y.I) ↦ eqToHom ⋯ ≫ Iso.inv (h ((e.symm : (a : Y.I) → X.I) i)) })
    (𝟙 X)
have h₁ : ∀ (x : X.I),
  Eq (α := X.I)
    (Hom.f.{w, v, u}
      (CategoryStruct.comp (Y := Y) { f := (⇑e : (a : X.I) → Y.I), φ := fun (i : X.I) ↦ (h i).hom }
        { f := (⇑e.symm : (a : Y.I) → X.I),
          φ := fun (i : Y.I) ↦ eqToHom sorry ≫ Iso.inv (h ((e.symm : (a : Y.I) → X.I) i)) })
      x)
    (Hom.f.{w, v, u} (𝟙 X) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
X Y : FormalCoproduct.{w, u} C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj ((e : (a : X.I) → Y.I) i)
h₁ :
  ∀ (x : X.I),
    Eq (α := X.I)
      (Hom.f.{w, v, u}
        (CategoryStruct.comp (Y := Y) { f := (⇑e : (a : X.I) → Y.I), φ := fun (i : X.I) ↦ (h i).hom }
          { f := (⇑e.symm : (a : Y.I) → X.I),
            φ := fun (i : Y.I) ↦ eqToHom ⋯ ≫ Iso.inv (h ((e.symm : (a : Y.I) → X.I) i)) })
        x)
      (Hom.f.{w, v, u} (𝟙 X) x)
⊢ Eq (α := X ⟶ X)
    (CategoryStruct.comp (Y := Y) { f := (⇑e : (a : X.I) → Y.I), φ := fun (i : X.I) ↦ (h i).hom }
      { f := (⇑e.symm : (a : Y.I) → X.I), φ := fun (i : Y.I) ↦ eqToHom ⋯ ≫ Iso.inv (h ((e.symm : (a : Y.I) → X.I) i)) })
    (𝟙 X)
have h₂ : ∀ (i : X.I),
  Eq.{v + 1} (α := X.obj i ⟶ X.obj (Hom.f.{w, v, u} (𝟙 X) i))
    (CategoryStruct.comp (Y :=
      X.obj
        (Hom.f.{w, v, u}
          (CategoryStruct.comp (Y := Y) { f := (⇑e : (a : X.I) → Y.I), φ := fun (i : X.I) ↦ (h i).hom }
            { f := (⇑e.symm : (a : Y.I) → X.I),
              φ := fun (i : Y.I) ↦ eqToHom sorry ≫ Iso.inv (h ((e.symm : (a : Y.I) → X.I) i)) })
          i))
      (Hom.φ
        (CategoryStruct.comp (Y := Y) { f := (⇑e : (a : X.I) → Y.I), φ := fun (i : X.I) ↦ (h i).hom }
          { f := (⇑e.symm : (a : Y.I) → X.I),
            φ := fun (i : Y.I) ↦ eqToHom sorry ≫ Iso.inv (h ((e.symm : (a : Y.I) → X.I) i)) })
        i)
      (eqToHom sorry))
    (Hom.φ (𝟙 X) i)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
X Y : FormalCoproduct.{w, u} C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj ((e : (a : X.I) → Y.I) i)
⊢ Eq (α := Y ⟶ Y)
    (CategoryStruct.comp (Y := X)
      { f := (⇑e.symm : (a : Y.I) → X.I), φ := fun (i : Y.I) ↦ eqToHom ⋯ ≫ Iso.inv (h ((e.symm : (a : Y.I) → X.I) i)) }
      { f := (⇑e : (a : X.I) → Y.I), φ := fun (i : X.I) ↦ (h i).hom })
    (𝟙 Y)
have h₁ : ∀ (x : Y.I),
  Eq (α := Y.I)
    (Hom.f.{w, v, u}
      (CategoryStruct.comp (Y := X)
        { f := (⇑e.symm : (a : Y.I) → X.I),
          φ := fun (i : Y.I) ↦ eqToHom sorry ≫ Iso.inv (h ((e.symm : (a : Y.I) → X.I) i)) }
        { f := (⇑e : (a : X.I) → Y.I), φ := fun (i : X.I) ↦ (h i).hom })
      x)
    (Hom.f.{w, v, u} (𝟙 Y) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
X Y : FormalCoproduct.{w, u} C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj ((e : (a : X.I) → Y.I) i)
h₁ :
  ∀ (x : Y.I),
    Eq (α := Y.I)
      (Hom.f.{w, v, u}
        (CategoryStruct.comp (Y := X)
          { f := (⇑e.symm : (a : Y.I) → X.I),
            φ := fun (i : Y.I) ↦ eqToHom ⋯ ≫ Iso.inv (h ((e.symm : (a : Y.I) → X.I) i)) }
          { f := (⇑e : (a : X.I) → Y.I), φ := fun (i : X.I) ↦ (h i).hom })
        x)
      (Hom.f.{w, v, u} (𝟙 Y) x)
⊢ Eq (α := Y ⟶ Y)
    (CategoryStruct.comp (Y := X)
      { f := (⇑e.symm : (a : Y.I) → X.I), φ := fun (i : Y.I) ↦ eqToHom ⋯ ≫ Iso.inv (h ((e.symm : (a : Y.I) → X.I) i)) }
      { f := (⇑e : (a : X.I) → Y.I), φ := fun (i : X.I) ↦ (h i).hom })
    (𝟙 Y)
have h₂ : ∀ (i : Y.I),
  Eq.{v + 1} (α := Y.obj i ⟶ Y.obj (Hom.f.{w, v, u} (𝟙 Y) i))
    (CategoryStruct.comp (Y :=
      Y.obj
        (Hom.f.{w, v, u}
          (CategoryStruct.comp (Y := X)
            { f := (⇑e.symm : (a : Y.I) → X.I),
              φ := fun (i : Y.I) ↦ eqToHom sorry ≫ Iso.inv (h ((e.symm : (a : Y.I) → X.I) i)) }
            { f := (⇑e : (a : X.I) → Y.I), φ := fun (i : X.I) ↦ (h i).hom })
          i))
      (Hom.φ
        (CategoryStruct.comp (Y := X)
          { f := (⇑e.symm : (a : Y.I) → X.I),
            φ := fun (i : Y.I) ↦ eqToHom sorry ≫ Iso.inv (h ((e.symm : (a : Y.I) → X.I) i)) }
          { f := (⇑e : (a : X.I) → Y.I), φ := fun (i : X.I) ↦ (h i).hom })
        i)
      (eqToHom sorry))
    (Hom.φ (𝟙 Y) i)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : FormalCoproduct.{w, u} C
f : Functor.obj (incl C) X ⟶ Y
⊢ fromIncl ((asSigma f).fst (β := fun (i : Y.I) ↦ X ⟶ Y.obj i)) ((asSigma f).snd (β := fun (i : Y.I) ↦ X ⟶ Y.obj i)) = f
have h₁ : ∀ (x : (Functor.obj (incl C) X).I),
  (fromIncl ((asSigma f).fst (β := fun (i : Y.I) ↦ X ⟶ Y.obj i)) ((asSigma f).snd (β := fun (i : Y.I) ↦ X ⟶ Y.obj i))).f
      x =
    f.f x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : FormalCoproduct.{w, u} C
f : Functor.obj (incl C) X ⟶ Y
h₁ :
  ∀ (x : (Functor.obj (incl C) X).I),
    (fromIncl ((asSigma f).fst (β := fun (i : Y.I) ↦ X ⟶ Y.obj i))
            ((asSigma f).snd (β := fun (i : Y.I) ↦ X ⟶ Y.obj i))).f
        x =
      f.f x
⊢ fromIncl ((asSigma f).fst (β := fun (i : Y.I) ↦ X ⟶ Y.obj i)) ((asSigma f).snd (β := fun (i : Y.I) ↦ X ⟶ Y.obj i)) = f
have h₂ : ∀ (i : (Functor.obj (incl C) X).I),
  (fromIncl ((asSigma f).fst (β := fun (i : Y.I) ↦ X ⟶ Y.obj i)) ((asSigma f).snd (β := fun (i : Y.I) ↦ X ⟶ Y.obj i))).φ
        i ≫
      eqToHom sorry =
    f.φ i
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
𝒜 : Type w
f : 𝒜 → FormalCoproduct.{w, u} C
t X : FormalCoproduct.{w, u} C
p : (i : 𝒜) → f i ⟶ t
⊢ (fun (m : Cocone.pt (cofan 𝒜 f) ⟶ t) (i : 𝒜) ↦ Cofan.inj (cofan 𝒜 f) i ≫ m)
      ((fun (s : (i : 𝒜) → f i ⟶ t) ↦
          ({
              f := fun (p : (Cocone.pt (cofan 𝒜 f)).I) ↦
                Hom.f (s (p.fst (β := fun (i : 𝒜) ↦ (f i).I))) (p.snd (β := fun (i : 𝒜) ↦ (f i).I)),
              φ := fun (p : (Cocone.pt (cofan 𝒜 f)).I) ↦
                Hom.φ (s (p.fst (β := fun (i : 𝒜) ↦ (f i).I))) (p.snd (β := fun (i : 𝒜) ↦ (f i).I)) } :
            Hom.{w, v, u} (Cocone.pt (cofan 𝒜 f)) t))
        p) =
    p
have h : ∀ (x : 𝒜) (x_1 : (f x).I),
  Hom.f.{w, v, u}
      ((fun (m : Cocone.pt (cofan 𝒜 f) ⟶ t) (i : 𝒜) ↦ Cofan.inj (cofan 𝒜 f) i ≫ m)
        ((fun (s : (i : 𝒜) → f i ⟶ t) ↦
            ({
                f := fun (p : (Cocone.pt (cofan 𝒜 f)).I) ↦
                  Hom.f (s (p.fst (β := fun (i : 𝒜) ↦ (f i).I))) (p.snd (β := fun (i : 𝒜) ↦ (f i).I)),
                φ := fun (p : (Cocone.pt (cofan 𝒜 f)).I) ↦
                  Hom.φ (s (p.fst (β := fun (i : 𝒜) ↦ (f i).I))) (p.snd (β := fun (i : 𝒜) ↦ (f i).I)) } :
              Hom.{w, v, u} (Cocone.pt (cofan 𝒜 f)) t))
          p)
        x)
      x_1 =
    (p x).f x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
𝒜 : Type w
f : 𝒜 → FormalCoproduct.{w, u} C
t X : FormalCoproduct.{w, u} C
p : (i : 𝒜) → f i ⟶ t
h :
  ∀ (x : 𝒜) (x_1 : (f x).I),
    Hom.f.{w, v, u}
        ((fun (m : Cocone.pt (cofan 𝒜 f) ⟶ t) (i : 𝒜) ↦ Cofan.inj (cofan 𝒜 f) i ≫ m)
          ((fun (s : (i : 𝒜) → f i ⟶ t) ↦
              ({
                  f := fun (p : (Cocone.pt (cofan 𝒜 f)).I) ↦
                    Hom.f (s (p.fst (β := fun (i : 𝒜) ↦ (f i).I))) (p.snd (β := fun (i : 𝒜) ↦ (f i).I)),
                  φ := fun (p : (Cocone.pt (cofan 𝒜 f)).I) ↦
                    Hom.φ (s (p.fst (β := fun (i : 𝒜) ↦ (f i).I))) (p.snd (β := fun (i : 𝒜) ↦ (f i).I)) } :
                Hom.{w, v, u} (Cocone.pt (cofan 𝒜 f)) t))
            p)
          x)
        x_1 =
      (p x).f x_1
⊢ (fun (m : Cocone.pt (cofan 𝒜 f) ⟶ t) (i : 𝒜) ↦ Cofan.inj (cofan 𝒜 f) i ≫ m)
      ((fun (s : (i : 𝒜) → f i ⟶ t) ↦
          ({
              f := fun (p : (Cocone.pt (cofan 𝒜 f)).I) ↦
                Hom.f (s (p.fst (β := fun (i : 𝒜) ↦ (f i).I))) (p.snd (β := fun (i : 𝒜) ↦ (f i).I)),
              φ := fun (p : (Cocone.pt (cofan 𝒜 f)).I) ↦
                Hom.φ (s (p.fst (β := fun (i : 𝒜) ↦ (f i).I))) (p.snd (β := fun (i : 𝒜) ↦ (f i).I)) } :
            Hom.{w, v, u} (Cocone.pt (cofan 𝒜 f)) t))
        p) =
    p
have h₁ : ∀ (x : 𝒜) (i : (f x).I),
  CategoryStruct.comp (Y :=
      t.obj
        (Hom.f.{w, v, u}
          ((fun (m : Cocone.pt (cofan 𝒜 f) ⟶ t) (i : 𝒜) ↦ Cofan.inj (cofan 𝒜 f) i ≫ m)
            ((fun (s : (i : 𝒜) → f i ⟶ t) ↦
                ({
                    f := fun (p : (Cocone.pt (cofan 𝒜 f)).I) ↦
                      Hom.f (s (p.fst (β := fun (i : 𝒜) ↦ (f i).I))) (p.snd (β := fun (i : 𝒜) ↦ (f i).I)),
                    φ := fun (p : (Cocone.pt (cofan 𝒜 f)).I) ↦
                      Hom.φ (s (p.fst (β := fun (i : 𝒜) ↦ (f i).I))) (p.snd (β := fun (i : 𝒜) ↦ (f i).I)) } :
                  Hom.{w, v, u} (Cocone.pt (cofan 𝒜 f)) t))
              p)
            x)
          i))
      (Hom.φ
        ((fun (m : Cocone.pt (cofan 𝒜 f) ⟶ t) (i : 𝒜) ↦ Cofan.inj (cofan 𝒜 f) i ≫ m)
          ((fun (s : (i : 𝒜) → f i ⟶ t) ↦
              ({
                  f := fun (p : (Cocone.pt (cofan 𝒜 f)).I) ↦
                    Hom.f (s (p.fst (β := fun (i : 𝒜) ↦ (f i).I))) (p.snd (β := fun (i : 𝒜) ↦ (f i).I)),
                  φ := fun (p : (Cocone.pt (cofan 𝒜 f)).I) ↦
                    Hom.φ (s (p.fst (β := fun (i : 𝒜) ↦ (f i).I))) (p.snd (β := fun (i : 𝒜) ↦ (f i).I)) } :
                Hom.{w, v, u} (Cocone.pt (cofan 𝒜 f)) t))
            p)
          x)
        i)
      (eqToHom sorry) =
    (p x).φ i
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
X Y Z : FormalCoproduct.{w, u} C
f : X ⟶ Z
g : Y ⟶ Z
i : Function.Pullback f.f g.f
⊢ Z.obj (f.f (↑i : X.I × Y.I).1) = Z.obj (g.f (↑i : X.I × Y.I).2)
have rw : Z.obj (g.f (↑i : X.I × Y.I).2) = Z.obj (g.f (↑i : X.I × Y.I).2)
Tactic: rw [i.2]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
X Y Z : FormalCoproduct.{w, u} C
f : X ⟶ Z
g : Y ⟶ Z
pb : (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i : X.I × Y.I).1 ≫ eqToHom ⋯) (g.φ (↑i : X.I × Y.I).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct.{w, u} C
m : T ⟶ (pullbackCone f g pb).pt
i : T.I
⊢ Hom.φ
        ((fun (s : { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }) ↦
            ({
                f := fun (i : T.I) ↦
                  Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                    ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) ⋯,
                φ := fun (i : T.I) ↦
                  IsLimit.lift
                    (hpb
                      ((fun (i : T.I) ↦
                          (Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                              ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) ⋯ :
                            { p : X.I × Y.I // f.f p.1 = g.f p.2 }))
                        i))
                    (PullbackCone.mk ((↑s : (T ⟶ X) × (T ⟶ Y)).1.φ i) ((↑s : (T ⟶ X) × (T ⟶ Y)).2.φ i) ⋯) } :
              Hom.{w, v, u} T (pullbackCone f g pb).pt))
          ((fun (m : T ⟶ (pullbackCone f g pb).pt) ↦
              (Subtype.mk (p := fun (p : (T ⟶ X) × (T ⟶ Y)) ↦ p.1 ≫ f = p.2 ≫ g)
                  (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd) ⋯ :
                { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }))
            m))
        i ≫
      eqToHom ⋯ =
    m.φ i
have simp : IsLimit.lift
    (hpb
      (Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
        ((pullbackCone f g pb).fst.f (m.f i), (pullbackCone f g pb).snd.f (m.f i)) sorry))
    (PullbackCone.mk (m.φ i ≫ (pullbackCone f g pb).fst.φ (m.f i)) (m.φ i ≫ (pullbackCone f g pb).snd.φ (m.f i)) sorry) =
  m.φ i
Tactic: simp only [category_comp_f, category_comp_φ, eqToHom_refl, Category.comp_id]