awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.FintypeCat
Goal:
⊢ PreservesFiniteLimits
    (forget FintypeCat (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
      fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))

Tactic:
FintypeCat.inclusion_preservesFiniteLimits

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.inducedFunctor, CategoryTheory.Limits.FintypeCat.inclusion_preservesFiniteLimits, CategoryTheory.InducedCategory
-- Module: Mathlib.CategoryTheory.Limits.FintypeCat
Goal:
ι : Type u_1
inst : Finite ι
X : ι → FintypeCat
x : (∏ᶜ X).obj
i : ι
⊢ Eq.{u + 1} (α := (X i).obj)
    (((productEquiv X : (∏ᶜ X).obj ≃ ((i : ι) → (X i).obj)) : (a : (∏ᶜ X).obj) → (i : ι) → (X i).obj) x i : (X i).obj)
    ((@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))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (X i))

Tactic:
simpa [productEquiv, equivEquivIso, equivIsoIso, Iso.toEquiv] using
    piComparison_comp_π_apply FintypeCat.incl X i x

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Limits.piComparison_comp_π_apply, FintypeCat.incl, equivEquivIso, equivIsoIso, CategoryTheory.Limits.FintypeCat.productEquiv
-- Module: Mathlib.CategoryTheory.Limits.FintypeCat
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
rw₁ rw₂ : x 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

Tactic:
rw [← productEquiv_apply, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, CategoryTheory.Limits.FintypeCat.productEquiv_apply
-- Module: Mathlib.CategoryTheory.Limits.FintypeCat
Goal:
ι : Type u_1
inst : Finite ι
X : ι → FintypeCat
inst_1 : ∀ (i : ι), Nonempty.{u + 1} (X i).obj
⊢ Nonempty.{u + 1} (∏ᶜ X).obj

Tactic:
(Equiv.nonempty_congr <| productEquiv X).mpr inferInstance

Premises used: Iff.mpr, inferInstance, Equiv.nonempty_congr, CategoryTheory.Limits.FintypeCat.productEquiv
-- Module: Mathlib.CategoryTheory.Limits.FintypeCat
Goal:
J : Type u_1
inst : SmallCategory J
inst_1 : FinCategory J
K : J ⥤ Type u
inst_2 : ∀ (j : J), Finite.{u + 1} (K.obj j)
⊢ Finite K.ColimitType

Tactic:
Quot.finite _

Premises used: Quot.finite, CategoryTheory.Functor.ColimitType
-- Module: Mathlib.CategoryTheory.Limits.FintypeCat
Goal:
J : Type u_1
inst : SmallCategory J
inst_1 : FinCategory J
K : J ⥤ Type u
inst_2 : ∀ (j : J), Finite.{u + 1} (K.obj j)
c : Cocone K
hc : IsColimit c
⊢ Finite.{u + 1} c.pt

Tactic:
Finite.of_equiv _ ((Types.isColimit_iff_coconeTypesIsColimit c).1 ⟨hc⟩).equiv

Premises used: Finite.of_equiv, CategoryTheory.Limits.Types.isColimit_iff_coconeTypesIsColimit, Nonempty.intro, CategoryTheory.Functor.CoconeTypes.IsColimit.equiv, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.FintypeCat
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)
⊢ Finite.{u_1 + 1} (colimit K)

Tactic:
have : Finite (colimit K) := finite_of_isColimit (colimit.isColimit K)
-- Module: Mathlib.CategoryTheory.Limits.FintypeCat
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)
this : Finite.{u_1 + 1} (colimit K)
⊢ Fintype (colimit K)

Tactic:
apply Fintype.ofFinite

Premises used: Fintype.ofFinite
-- Module: Mathlib.CategoryTheory.Limits.FintypeCat
Goal:
⊢ PreservesFiniteColimits
    (forget FintypeCat (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
      fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))

Tactic:
FintypeCat.inclusion_preservesFiniteColimits

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.inducedFunctor, CategoryTheory.InducedCategory, CategoryTheory.Limits.FintypeCat.inclusion_preservesFiniteColimits
-- Module: Mathlib.CategoryTheory.Limits.FintypeCat
Goal:
J : Type u_1
inst : SmallCategory J
inst_1 : FinCategory J
F : J ⥤ FintypeCat
t : Cocone F
h : IsColimit t
x : t.pt.obj
⊢ ∃ (j : J) (y : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj j)),
    (@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))
            _ _ _ (t.ι.app j) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj j)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (((const J).obj t.pt).obj j))
        y =
      x

Tactic:
let hs := isColimitOfPreserves FintypeCat.incl.{u} h
  Types.jointly_surjective (F ⋙ FintypeCat.incl) hs x

Premises used: CategoryTheory.Functor.comp, FintypeCat.incl, CategoryTheory.Limits.Types.jointly_surjective, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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
rw rw₁ : Y.obj (g.f i) = Y.obj (g.f i)
⊢ Y.obj (f.f i) = Y.obj (g.f i)

Tactic:
rw [h₁]
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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
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 ⋯ = g.φ i),
    { f := f, φ := F : Hom.{w, v, u} X Y } = g
⊢ f = g

Tactic:
obtain ⟨f, F⟩ := f
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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
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 ⋯ = { f := g, φ := G }.φ i),
    { f := f, φ := F : Hom.{w, v, u} X Y } = { f := g, φ := G }
⊢ { f := f, φ := F : Hom.{w, v, u} X Y } = g

Tactic:
obtain ⟨g, G⟩ := g
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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 = g

Tactic:
h₁
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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
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 ⋯ = { f := f, φ := G : Hom.{w, v, u} X Y }.φ i),
    { f := f, φ := F : Hom.{w, v, u} X Y } = { f := f, φ := G }
⊢ { f := f, φ := F : Hom.{w, v, u} X Y } = { f := g, φ := G }

Tactic:
obtain rfl : f = g := h₁

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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
h : ∀ (i : X.I), F i = G i
⊢ F = G

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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
i : X.I
⊢ F i = G i

Tactic:
simpa using h₂ i
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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
obtain :
  ∀
    (h₂ :
      ∀ (i : X.I), { f := f, φ := F : Hom.{w, v, u} X Y }.φ i ≫ eqToHom ⋯ = { f := f, φ := F : Hom.{w, v, u} X Y }.φ i),
    { f := f, φ := F : Hom.{w, v, u} X Y } = { f := f, φ := F }
⊢ { f := f, φ := F : Hom.{w, v, u} X Y } = { f := f, φ := G }

Tactic:
obtain rfl : F = G := by ext i; simpa using h₂ i

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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)
h₂ : ∀ (i : X.I), { f := f, φ := F : Hom.{w, v, u} X Y }.φ i ≫ eqToHom ⋯ = { f := f, φ := F : Hom.{w, v, u} X Y }.φ i
⊢ { f := f, φ := F : Hom.{w, v, u} X Y } = { f := f, φ := F }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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
rw rw₁ : Y.obj (g.f i) = Y.obj (g.f i)
⊢ Y.obj (f.f i) = Y.obj (g.f i)

Tactic:
rw [h₁]
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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)
i : Y.I
⊢ Y.obj i = Y.obj ((e : (a : X.I) → Y.I) ((e.symm : (a : Y.I) → X.I) i : X.I))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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)
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 ⋯ ≫ 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 ⋯ ≫ Iso.inv (h ((e.symm : (a : Y.I) → X.I) i)) })
          i)
        (eqToHom ⋯))
      (Hom.φ (𝟙 X) 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)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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)
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)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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)
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 ⋯ ≫ 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 ⋯ ≫ Iso.inv (h ((e.symm : (a : Y.I) → X.I) i)) })
        i)
      (eqToHom ⋯))
    (Hom.φ (𝟙 X) i)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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)
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 ⋯ ≫ 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 ⋯ ≫ 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 ⋯))
      (Hom.φ (𝟙 Y) 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)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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)
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)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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)
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 ⋯ ≫ 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 ⋯ ≫ 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 ⋯))
    (Hom.φ (𝟙 Y) i)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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
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 ⋯ =
      f.φ 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

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : FormalCoproduct.{w, u} C
f : Functor.obj (incl C) X ⟶ Y
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:
aesop
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : FormalCoproduct.{w, u} C
f : Functor.obj (incl C) X ⟶ Y
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 ⋯ =
    f.φ i

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
⊢ Full (incl C)

Tactic:
fullyFaithfulIncl.full

Premises used: CategoryTheory.Limits.FormalCoproduct.fullyFaithfulIncl, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
⊢ Faithful (incl C)

Tactic:
fullyFaithfulIncl.faithful

Premises used: CategoryTheory.Limits.FormalCoproduct.fullyFaithfulIncl, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
𝒜 : Type w
f : 𝒜 → FormalCoproduct.{w, u} C
i : 𝒜
⊢ Eq (α := f i ⟶ Cocone.pt (cofan 𝒜 f)) (Cofan.inj (cofan 𝒜 f) i)
    { f := fun (x : (f i).I) ↦ Sigma.mk (β := fun (i : 𝒜) ↦ (f i).I) i x, φ := fun (x : (f i).I) ↦ 𝟙 ((f i).obj x) }

Tactic:
rfl

Premises used: CategoryTheory.Limits.Cofan.inj, rfl
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
𝒜 : Type w
f : 𝒜 → FormalCoproduct.{w, u} C
i : 𝒜
x : (f i).I
⊢ Sigma.fst (β := fun (i : 𝒜) ↦ (f i).I) (Hom.f (Cofan.inj (cofan 𝒜 f) i) x) = i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
𝒜 : Type w
f : 𝒜 → FormalCoproduct.{w, u} C
i : 𝒜
x : (f i).I
⊢ Sigma.snd (β := fun (i : 𝒜) ↦ (f i).I) (Hom.f (Cofan.inj (cofan 𝒜 f) i) x) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
𝒜 : Type w
f : 𝒜 → FormalCoproduct.{w, u} C
i : 𝒜
x : (f i).I
⊢ Eq.{v + 1} (α := (f i).obj x ⟶ (Cocone.pt (cofan 𝒜 f)).obj (Hom.f (Cofan.inj (cofan 𝒜 f) i) x))
    (Hom.φ (Cofan.inj (cofan 𝒜 f) i) x) (𝟙 ((f i).obj x))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
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
m : Cocone.pt (cofan 𝒜 f) ⟶ t
x_1 : (Cocone.pt (cofan 𝒜 f)).I
i : 𝒜
x : (f i).I
⊢ Eq (α :=
    obj.{w, u} (Cocone.pt (cofan 𝒜 f)) (Sigma.mk (β := fun (i : 𝒜) ↦ (f i).I) i x) ⟶
      t.obj (m.f (Sigma.mk (β := fun (i : 𝒜) ↦ (f i).I) i x)))
    (Hom.φ
        ((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))
          ((fun (m : Cocone.pt (cofan 𝒜 f) ⟶ t) (i : 𝒜) ↦ Cofan.inj (cofan 𝒜 f) i ≫ m) m))
        (Sigma.mk (β := fun (i : 𝒜) ↦ (f i).I) i x) ≫
      eqToHom ⋯)
    (m.φ (Sigma.mk (β := fun (i : 𝒜) ↦ (f i).I) i x))

Tactic:
simp [cofan_inj]

Premises used: CategoryTheory.Limits.FormalCoproduct.cofan_inj