awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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
s : PullbackCone f g
m : s.pt ⟶ (pullbackCone f g pb).pt
h₁ : m ≫ (pullbackCone f g pb).fst = s.fst
h₂ : m ≫ (pullbackCone f g pb).snd = s.snd
h :
  (s.fst, s.snd) =
    (↑((homPullbackEquiv f g pb hpb s.pt :
              (s.pt ⟶ (pullbackCone f g pb).pt) ≃ { p : (s.pt ⟶ X) × (s.pt ⟶ Y) // p.1 ≫ f = p.2 ≫ g }).1
          m) :
      (s.pt ⟶ X) × (s.pt ⟶ Y))
⊢ m =
    (fun (s : PullbackCone f g) ↦
        Equiv.invFun (homPullbackEquiv f g pb hpb s.pt)
          (Subtype.mk (p := fun (p : (s.pt ⟶ X) × (s.pt ⟶ Y)) ↦ p.1 ≫ f = p.2 ≫ g) (s.fst, s.snd) ⋯))
      s

Tactic:
convert! ((homPullbackEquiv f g pb hpb s.pt).left_inv m).symm using 3

Premises used: CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv, CategoryTheory.Limits.Cone.pt, Eq.symm, Equiv.left_inv
-- 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 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
s : PullbackCone f g
m : s.pt ⟶ (pullbackCone f g pb).pt
h₁ : m ≫ (pullbackCone f g pb).fst = s.fst
h₂ : m ≫ (pullbackCone f g pb).snd = s.snd
h :
  (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd) =
    (↑((homPullbackEquiv f g pb hpb s.pt :
              (s.pt ⟶ (pullbackCone f g pb).pt) ≃ { p : (s.pt ⟶ X) × (s.pt ⟶ Y) // p.1 ≫ f = p.2 ≫ g }).1
          m) :
      (s.pt ⟶ X) × (s.pt ⟶ Y))
⊢ (s.fst, s.snd) =
    (↑((homPullbackEquiv f g pb hpb s.pt :
              (s.pt ⟶ (pullbackCone f g pb).pt) ≃ { p : (s.pt ⟶ X) × (s.pt ⟶ Y) // p.1 ≫ f = p.2 ≫ g }).1
          m) :
      (s.pt ⟶ X) × (s.pt ⟶ Y))

Tactic:
rw [← h₁, ← 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 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
s : PullbackCone f g
m : s.pt ⟶ (pullbackCone f g pb).pt
h₁ : m ≫ (pullbackCone f g pb).fst = s.fst
h₂ : m ≫ (pullbackCone f g pb).snd = s.snd
⊢ (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd) =
    (↑((homPullbackEquiv f g pb hpb s.pt :
              (s.pt ⟶ (pullbackCone f g pb).pt) ≃ { p : (s.pt ⟶ X) × (s.pt ⟶ Y) // p.1 ≫ f = p.2 ≫ g }).1
          m) :
      (s.pt ⟶ X) × (s.pt ⟶ Y))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
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)
⊢ HasPullback f g

Tactic:
⟨⟨⟨_, isLimitPullbackCone f g pb hpb⟩⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.FormalCoproduct.isLimitPullbackCone, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
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)
⊢ IsPullback (pullbackCone f g pb).fst (pullbackCone f g pb).snd f g

Tactic:
⟨⟨pullbackCone_condition f g pb⟩, ⟨isLimitPullbackCone f g pb hpb⟩⟩

Premises used: CategoryTheory.IsPullback.mk, CategoryTheory.CommSq.mk, Nonempty.intro, CategoryTheory.Limits.FormalCoproduct.isLimitPullbackCone, CategoryTheory.Limits.FormalCoproduct.pullbackCone_condition
-- 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 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
inst_2 : HasPullbacks.{v, u} C
⊢ HasPullback f g

Tactic:
hasPullback_of_pullbackCone f g (fun _ ↦ pullback.cone _ _) (fun _ ↦ pullback.isLimit _ _)

Premises used: CategoryTheory.Limits.FormalCoproduct.hasPullback_of_pullbackCone, CategoryTheory.eqToHom, CategoryTheory.Limits.pullback.isLimit, Prod.fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.FormalCoproduct.Hom.φ, _private.0._proof_1, Subtype.val, Prod.snd, CategoryTheory.Limits.pullback.cone
-- 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 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
inst_2 : HasPullbacks.{v, u} C
⊢ HasPullbacks (FormalCoproduct.{w, u} C)

Tactic:
hasPullbacks_of_hasLimit_cospan _

Premises used: CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
inst_2 : HasCoproducts.{w, v₁, u₁} A
J : Type w
f : J → FormalCoproduct.{w, u} C
F_1 F : Functor.{v, v₁, u, u₁} C A
X Y Z : FormalCoproduct.{w, u} C
x : X ⟶ Y
x_1 : Y ⟶ Z
x_2 : X.I
⊢ Eq.{v₁ + 1} (α := F.obj (X.obj x_2) ⟶ sigmaObj.{w, v₁, u₁} fun (i : Z.I) ↦ F.obj (Z.obj i))
    (CategoryStruct.comp (Y := sigmaObj.{w, v₁, u₁} fun (i : X.I) ↦ F.obj (X.obj i))
        (Sigma.ι.{w, v₁, u₁} (C := A) (fun (i : X.I) ↦ F.obj (X.obj i)) x_2)
        (Sigma.desc fun (i : X.I) ↦ F.map ((x ≫ x_1).φ i) ≫ Sigma.ι (F.obj ∘ Z.obj) ((x ≫ x_1).f i)) :
      F.obj (X.obj x_2) ⟶ sigmaObj.{w, v₁, u₁} fun (i : Z.I) ↦ F.obj (Z.obj i))
    (CategoryStruct.comp (Y := sigmaObj.{w, v₁, u₁} fun (i : X.I) ↦ F.obj (X.obj i))
        (Sigma.ι.{w, v₁, u₁} (C := A) (fun (i : X.I) ↦ F.obj (X.obj i)) x_2)
        (CategoryStruct.comp (Y := sigmaObj.{w, v₁, u₁} fun (i : Y.I) ↦ F.obj (Y.obj i))
          (Sigma.desc fun (i : X.I) ↦ F.map (x.φ i) ≫ Sigma.ι (F.obj ∘ Y.obj) (x.f i))
          (Sigma.desc fun (i : Y.I) ↦ F.map (x_1.φ i) ≫ Sigma.ι (F.obj ∘ Z.obj) (x_1.f i))) :
      F.obj (X.obj x_2) ⟶ sigmaObj.{w, v₁, u₁} fun (i : Z.I) ↦ F.obj (Z.obj i))

Tactic:
simp [Sigma.ι_desc]

Premises used: CategoryTheory.Limits.Sigma.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
inst_2 : HasCoproducts.{w, v₁, u₁} A
J : Type w
f : J → FormalCoproduct.{w, u} C
F_1 F : Functor.{v, v₁, u, u₁} C A
x : C
⊢ (Sigma.desc fun (x_1 : (Functor.obj (incl C) x).I) ↦ 𝟙 (F.obj ((Functor.obj (incl C) x).obj x_1))) ≫
      Sigma.ι.{w, v₁, u₁} (C := A) (fun (x_1 : PUnit.{w + 1}) ↦ F.obj x) PUnit.unit =
    𝟙 ((Functor.obj (eval C A ⋙ Functor.obj (whiskeringLeft C (FormalCoproduct.{w, u} C) A) (incl C)) F).obj 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
inst_2 : HasCoproducts.{w, v₁, u₁} A
J : Type w
f : J → FormalCoproduct.{w, u} C
F_1 F : Functor.{v, v₁, u, u₁} C A
x : C
⊢ Eq.{v₁ + 1} (α :=
    (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} C A)) F).obj x ⟶ (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} C A)) F).obj x)
    (CategoryStruct.comp (Y :=
        (Functor.obj (eval C A ⋙ Functor.obj (whiskeringLeft C (FormalCoproduct.{w, u} C) A) (incl C)) F).obj x)
        (Sigma.ι.{w, v₁, u₁} (C := A) (fun (x_1 : PUnit.{w + 1}) ↦ F.obj x) PUnit.unit)
        (Sigma.desc fun (x_1 : (Functor.obj (incl C) x).I) ↦ 𝟙 (F.obj ((Functor.obj (incl C) x).obj x_1))) :
      (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} C A)) F).obj x ⟶ (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} C A)) F).obj x)
    (𝟙 ((Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} C A)) F).obj x) :
      (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} C A)) F).obj x ⟶ (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} C A)) F).obj x)

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
inst_2 : HasCoproducts.{w, v₁, u₁} A
J : Type w
f_1 : J → FormalCoproduct.{w, u} C
F_1 F : Functor.{v, v₁, u, u₁} C A
X Y : C
f : X ⟶ Y
⊢ ∀ (b : (Functor.obj (incl C) X).I),
    Eq (α := F.obj ((Functor.obj (incl C) X).obj b) ⟶ (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} C A)) F).obj Y)
      (Sigma.ι.{w, v₁, u₁} (C := A) (fun (i : (Functor.obj (incl C) X).I) ↦ F.obj ((Functor.obj (incl C) X).obj i)) b ≫
        (Functor.obj (eval C A ⋙ Functor.obj (whiskeringLeft C (FormalCoproduct.{w, u} C) A) (incl C)) F).map f ≫
          Iso.hom
            ((fun (x : C) ↦
                ({
                    hom :=
                      Sigma.desc fun (x_1 : (Functor.obj (incl C) x).I) ↦ 𝟙 (F.obj ((Functor.obj (incl C) x).obj x_1)),
                    inv := Sigma.ι.{w, v₁, u₁} (C := A) (fun (x_1 : PUnit.{w + 1}) ↦ F.obj x) PUnit.unit,
                    hom_inv_id := ⋯, inv_hom_id := ⋯ } :
                  (Functor.obj (eval C A ⋙ Functor.obj (whiskeringLeft C (FormalCoproduct.{w, u} C) A) (incl C)) F).obj
                      x ≅
                    (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} C A)) F).obj x))
              Y))
      (CategoryStruct.comp (Y :=
        sigmaObj.{w, v₁, u₁} fun (i : (Functor.obj (incl C) X).I) ↦ F.obj ((Functor.obj (incl C) X).obj i))
        (Sigma.ι.{w, v₁, u₁} (C := A) (fun (i : (Functor.obj (incl C) X).I) ↦ F.obj ((Functor.obj (incl C) X).obj i)) b)
        (Iso.hom
            ((fun (x : C) ↦
                ({
                    hom :=
                      Sigma.desc fun (x_1 : (Functor.obj (incl C) x).I) ↦ 𝟙 (F.obj ((Functor.obj (incl C) x).obj x_1)),
                    inv := Sigma.ι.{w, v₁, u₁} (C := A) (fun (x_1 : PUnit.{w + 1}) ↦ F.obj x) PUnit.unit,
                    hom_inv_id := ⋯, inv_hom_id := ⋯ } :
                  (Functor.obj (eval C A ⋙ Functor.obj (whiskeringLeft C (FormalCoproduct.{w, u} C) A) (incl C)) F).obj
                      x ≅
                    (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} C A)) F).obj x))
              X) ≫
          (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} C A)) F).map f))

Tactic:
simp [Sigma.ι_desc]

Premises used: CategoryTheory.Limits.Sigma.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
inst_2 : HasCoproducts.{w, v₁, u₁} A
J : Type w
f : J → FormalCoproduct.{w, u} C
F : Functor.{v, v₁, u, u₁} C A
s : Cocone (Discrete.functor f ⋙ Functor.obj (eval C A) F)
i_1 : Discrete J
i : (Functor.obj (Discrete.functor f) i_1).I
⊢ (Sigma.ι.{w, v₁, u₁} (C := A)
        (fun (i : (Functor.obj (Discrete.functor f) i_1).I) ↦ F.obj ((Functor.obj (Discrete.functor f) i_1).obj i)) i ≫
      ((Functor.obj (eval C A) F).mapCocone (cofan J f)).ι.app i_1 ≫
        Sigma.desc fun (i : (Cocone.pt (cofan J f)).I) ↦
          CategoryStruct.comp (Y := sigmaObj.{w, v₁, u₁} (F.obj ∘ (f (i.fst (β := fun (i : J) ↦ (f i).I))).obj))
            (Sigma.ι (F.obj ∘ (f (i.fst (β := fun (i : J) ↦ (f i).I))).obj) (i.snd (β := fun (i : J) ↦ (f i).I)))
            (s.ι.app { as := i.fst (β := fun (i : J) ↦ (f i).I) : Discrete J })) =
    Sigma.ι.{w, v₁, u₁} (C := A)
        (fun (i : (Functor.obj (Discrete.functor f) i_1).I) ↦ F.obj ((Functor.obj (Discrete.functor f) i_1).obj i)) i ≫
      s.ι.app i_1

Tactic:
simp [cofan, Function.comp_def]

Premises used: Function.comp_def, CategoryTheory.Limits.FormalCoproduct.cofan
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
inst_2 : HasCoproducts.{w, v₁, u₁} A
J : Type w
f : J → FormalCoproduct.{w, u} C
F : Functor.{v, v₁, u, u₁} C A
s : Cocone (Discrete.functor f ⋙ Functor.obj (eval C A) F)
m : ((Functor.obj (eval C A) F).mapCocone (cofan J f)).pt ⟶ s.pt
h : ∀ (j : Discrete J), ((Functor.obj (eval C A) F).mapCocone (cofan J f)).ι.app j ≫ m = s.ι.app j
x : (Cocone.pt (cofan J f)).I
i₁ : J
i₂ : (f i₁).I
⊢ Eq (α := F.obj (obj.{w, u} (Cocone.pt (cofan J f)) (Sigma.mk (β := fun (i : J) ↦ (f i).I) i₁ i₂)) ⟶ s.pt)
    (Sigma.ι.{w, v₁, u₁} (C := A) (fun (i : (Cocone.pt (cofan J f)).I) ↦ F.obj ((Cocone.pt (cofan J f)).obj i))
        (Sigma.mk (β := fun (i : J) ↦ (f i).I) i₁ i₂) ≫
      m)
    (CategoryStruct.comp (Y :=
      sigmaObj.{w, v₁, u₁} fun (i : (Cocone.pt (cofan J f)).I) ↦ F.obj ((Cocone.pt (cofan J f)).obj i))
      (Sigma.ι.{w, v₁, u₁} (C := A) (fun (i : (Cocone.pt (cofan J f)).I) ↦ F.obj ((Cocone.pt (cofan J f)).obj i))
        (Sigma.mk (β := fun (i : J) ↦ (f i).I) i₁ i₂))
      (Sigma.desc fun (i : (Cocone.pt (cofan J f)).I) ↦
        CategoryStruct.comp (Y := sigmaObj.{w, v₁, u₁} (F.obj ∘ (f (i.fst (β := fun (i : J) ↦ (f i).I))).obj))
          (Sigma.ι (F.obj ∘ (f (i.fst (β := fun (i : J) ↦ (f i).I))).obj) (i.snd (β := fun (i : J) ↦ (f i).I)))
          (s.ι.app { as := i.fst (β := fun (i : J) ↦ (f i).I) })))

Tactic:
simp [← h, cofan, Function.comp_def]

Premises used: Function.comp_def, CategoryTheory.Limits.FormalCoproduct.cofan
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
inst_2 : HasCoproducts.{w, v₁, u₁} A
J : Type w
f : J → FormalCoproduct.{w, u} C
F : Functor.{v, v₁, u, u₁} C A
⊢ PreservesColimit (Discrete.functor f) (Functor.obj (eval C A) F)

Tactic:
⟨fun hc ↦ ⟨IsColimit.ofIsoColimit (isColimitEvalMapCoconeCofan J f F)
    ((Cocone.functoriality _ _).mapIso ((isColimitCofan J f).uniqueUpToIso hc))⟩⟩

Premises used: CategoryTheory.Limits.FormalCoproduct.eval, CategoryTheory.Limits.FormalCoproduct.isColimitCofan, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Discrete.functor, CategoryTheory.Limits.IsColimit.uniqueUpToIso, Nonempty.intro, CategoryTheory.Limits.Cocone.functoriality, CategoryTheory.Limits.PreservesColimit.mk, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj, CategoryTheory.Limits.FormalCoproduct.isColimitEvalMapCoconeCofan
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
inst_2 : HasCoproducts.{w, v₁, u₁} A
J : Type w
f : J → FormalCoproduct.{w, u} C
F : Functor.{v, v₁, u, u₁} C A
⊢ PreservesColimitsOfShape (Discrete J) (Functor.obj (eval C A) F)

Tactic:
preservesColimitsOfShape_of_discrete _

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_discrete
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
inst_2 : HasProducts.{w, v₁, u₁} A
J : Type w
f : J → FormalCoproduct.{w, u} C
F_1 F : Functor.{v, v₁, u, u₁} Cᵒᵖ A
x : Cᵒᵖ
⊢ (Pi.π
        (fun (i : (unop (Functor.obj (Functor.op (incl C)) x)).I) ↦
          F.obj (op ((unop (Functor.obj (Functor.op (incl C)) x)).obj i)))
        PUnit.unit ≫
      Pi.lift fun (x_1 : (unop (Functor.obj (Functor.op (incl C)) x)).I) ↦
        𝟙 ((Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} Cᵒᵖ A)) F).obj x)) =
    𝟙
      ((Functor.obj (evalOp C A ⋙ Functor.obj (whiskeringLeft Cᵒᵖ (FormalCoproduct.{w, u} C)ᵒᵖ A) (Functor.op (incl C)))
            F).obj
        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
inst_2 : HasProducts.{w, v₁, u₁} A
J : Type w
f : J → FormalCoproduct.{w, u} C
F_1 F : Functor.{v, v₁, u, u₁} Cᵒᵖ A
x : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} Cᵒᵖ A)) F).obj x ⟶ (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} Cᵒᵖ A)) F).obj x)
    (CategoryStruct.comp (Y :=
        (Functor.obj
              (evalOp C A ⋙ Functor.obj (whiskeringLeft Cᵒᵖ (FormalCoproduct.{w, u} C)ᵒᵖ A) (Functor.op (incl C)))
              F).obj
          x)
        (Pi.lift fun (x_1 : (unop (Functor.obj (Functor.op (incl C)) x)).I) ↦
          𝟙 ((Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} Cᵒᵖ A)) F).obj x))
        (Pi.π
          (fun (i : (unop (Functor.obj (Functor.op (incl C)) x)).I) ↦
            F.obj (op ((unop (Functor.obj (Functor.op (incl C)) x)).obj i)))
          PUnit.unit) :
      (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} Cᵒᵖ A)) F).obj x ⟶
        (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} Cᵒᵖ A)) F).obj x)
    (𝟙 ((Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} Cᵒᵖ A)) F).obj x) :
      (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} Cᵒᵖ A)) F).obj x ⟶
        (Functor.obj (𝟭 (Functor.{v, v₁, u, u₁} Cᵒᵖ A)) F).obj x)

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
inst_2 : HasProducts.{w, v₁, u₁} A
J : Type w
f : J → FormalCoproduct.{w, u} C
F : Functor.{v, v₁, u, u₁} Cᵒᵖ A
s : Cone.{w, v₁, w, u₁} (J := Discrete J) ((Discrete.functor fun (x : J) ↦ op (f x)) ⋙ Functor.obj (evalOp C A) F)
i_1 : Discrete J
i : I.{w, u} (C := C) (unop (Functor.obj (Discrete.functor fun (x : J) ↦ op (f x)) i_1))
⊢ ((Pi.lift fun (i : (unop (Cone.pt (Cofan.op (cofan J f)))).I) ↦
          CategoryStruct.comp (Y :=
            Functor.obj ((Discrete.functor fun (x : J) ↦ op (f x)) ⋙ Functor.obj (evalOp C A) F)
              { as := i.fst (β := fun (i : J) ↦ (f i).I) : Discrete J })
            (s.π.app { as := i.fst (β := fun (i : J) ↦ (f i).I) : Discrete J })
            (Pi.π
              (fun
                  (i_2 :
                    I.{w, u} (C := C)
                      (unop
                        (Functor.obj (Discrete.functor fun (x : J) ↦ op (f x))
                          { as := i.fst (β := fun (i : J) ↦ (f i).I) : Discrete J }))) ↦
                F.obj
                  (op
                    (obj
                      (unop
                        (Functor.obj (Discrete.functor fun (x : J) ↦ op (f x))
                          { as := i.fst (β := fun (i : J) ↦ (f i).I) : Discrete J }))
                      i_2)))
              (i.snd (β := fun (i : J) ↦ (f i).I)))) ≫
        ((Functor.obj (evalOp C A) F).mapCone (Cofan.op (cofan J f))).π.app i_1) ≫
      Pi.π
        (fun (i : I.{w, u} (C := C) (unop (Functor.obj (Discrete.functor fun (x : J) ↦ op (f x)) i_1))) ↦
          F.obj (op (obj (unop (Functor.obj (Discrete.functor fun (x : J) ↦ op (f x)) i_1)) i)))
        i =
    s.π.app i_1 ≫
      Pi.π
        (fun (i : I.{w, u} (C := C) (unop (Functor.obj (Discrete.functor fun (x : J) ↦ op (f x)) i_1))) ↦
          F.obj (op (obj (unop (Functor.obj (Discrete.functor fun (x : J) ↦ op (f x)) i_1)) i)))
        i

Tactic:
simp [cofan]

Premises used: CategoryTheory.Limits.FormalCoproduct.cofan
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
inst_2 : HasProducts.{w, v₁, u₁} A
J : Type w
f : J → FormalCoproduct.{w, u} C
F : Functor.{v, v₁, u, u₁} Cᵒᵖ A
s : Cone.{w, v₁, w, u₁} (J := Discrete J) ((Discrete.functor fun (x : J) ↦ op (f x)) ⋙ Functor.obj (evalOp C A) F)
m : s.pt ⟶ ((Functor.obj (evalOp C A) F).mapCone (Cofan.op (cofan J f))).pt
h : ∀ (j : Discrete J), m ≫ ((Functor.obj (evalOp C A) F).mapCone (Cofan.op (cofan J f))).π.app j = s.π.app j
x : (unop (Cone.pt (Cofan.op (cofan J f)))).I
i₁ : J
i₂ : (f i₁).I
⊢ Eq (α :=
    s.pt ⟶
      F.obj (op (obj.{w, u} (unop (Cone.pt (Cofan.op (cofan J f)))) (Sigma.mk (β := fun (i : J) ↦ (f i).I) i₁ i₂))))
    (m ≫
      Pi.π
        (fun (i : (unop (Cone.pt (Cofan.op (cofan J f)))).I) ↦
          F.obj (op ((unop (Cone.pt (Cofan.op (cofan J f)))).obj i)))
        (Sigma.mk (β := fun (i : J) ↦ (f i).I) i₁ i₂))
    (CategoryStruct.comp (Y :=
      piObj.{w, v₁, u₁} fun (i : (unop (Cone.pt (Cofan.op (cofan J f)))).I) ↦
        F.obj (op ((unop (Cone.pt (Cofan.op (cofan J f)))).obj i)))
      (Pi.lift fun (i : (unop (Cone.pt (Cofan.op (cofan J f)))).I) ↦
        CategoryStruct.comp (Y :=
          Functor.obj ((Discrete.functor fun (x : J) ↦ op (f x)) ⋙ Functor.obj (evalOp C A) F)
            { as := i.fst (β := fun (i : J) ↦ (f i).I) : Discrete J })
          (s.π.app { as := i.fst (β := fun (i : J) ↦ (f i).I) })
          (Pi.π
            (fun
                (i_1 :
                  I.{w, u} (C := C)
                    (unop
                      (Functor.obj (Discrete.functor fun (x : J) ↦ op (f x))
                        { as := i.fst (β := fun (i : J) ↦ (f i).I) : Discrete J }))) ↦
              F.obj
                (op
                  (obj
                    (unop
                      (Functor.obj (Discrete.functor fun (x : J) ↦ op (f x))
                        { as := i.fst (β := fun (i : J) ↦ (f i).I) : Discrete J }))
                    i_1)))
            (i.snd (β := fun (i : J) ↦ (f i).I))))
      (Pi.π
        (fun (i : (unop (Cone.pt (Cofan.op (cofan J f)))).I) ↦
          F.obj (op ((unop (Cone.pt (Cofan.op (cofan J f)))).obj i)))
        (Sigma.mk (β := fun (i : J) ↦ (f i).I) i₁ i₂)))

Tactic:
simp [← h, cofan]

Premises used: CategoryTheory.Limits.FormalCoproduct.cofan
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
inst_2 : HasProducts.{w, v₁, u₁} A
J : Type w
f : J → FormalCoproduct.{w, u} C
F : Functor.{v, v₁, u, u₁} Cᵒᵖ A
⊢ PreservesLimit (Discrete.functor (op ∘ f)) (Functor.obj (evalOp C A) F)

Tactic:
⟨fun hc ↦ ⟨IsLimit.ofIsoLimit (isLimitEvalMapConeCofanOp J f F) ((Cone.functoriality _ _).mapIso
    ((Cofan.IsColimit.op (isColimitCofan J f)).uniqueUpToIso hc))⟩⟩

Premises used: CategoryTheory.Limits.FormalCoproduct.isColimitCofan, CategoryTheory.Limits.FormalCoproduct.isLimitEvalMapConeCofanOp, CategoryTheory.Limits.IsLimit.uniqueUpToIso, CategoryTheory.Discrete.functor, CategoryTheory.Limits.FormalCoproduct.evalOp, Nonempty.intro, CategoryTheory.Limits.Cofan.IsColimit.op, CategoryTheory.Limits.PreservesLimit.mk, Opposite.op, CategoryTheory.Limits.Cone.functoriality, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj