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
𝒜 : 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
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 ⋯) =
      (p x).φ i
⊢ (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

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
𝒜 : Type w
f : 𝒜 → FormalCoproduct.{w, u} C
t X : FormalCoproduct.{w, u} C
p : (i : 𝒜) → f i ⟶ t
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:
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
𝒜 : Type w
f : 𝒜 → FormalCoproduct.{w, u} C
t X : FormalCoproduct.{w, u} C
p : (i : 𝒜) → f i ⟶ t
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 ⋯) =
    (p 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
𝒜 : Type w
f : 𝒜 → FormalCoproduct.{w, u} C
t X : FormalCoproduct.{w, u} C
⊢ HasCoproducts (FormalCoproduct.{w, u} C)

Tactic:
hasCoproducts_of_colimit_cofans _ (isColimitCofan _)

Premises used: CategoryTheory.Limits.hasCoproducts_of_colimit_cofans, CategoryTheory.Limits.FormalCoproduct.isColimitCofan
-- 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)) (Sigma.ι f i ≫ Iso.hom (coproductIsoCofanPt 𝒜 f)) (Cofan.inj (cofan 𝒜 f) i)

Tactic:
colimit.isoColimitCocone_ι_hom _ _

Premises used: CategoryTheory.Limits.Cofan.inj, CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : FormalCoproduct.{w, u} C
i_1 : X.I
i : (toFun.{w, v, u} X i_1).I
⊢ (Cofan.inj (cofan X.I (toFun.{w, v, u} X)) i_1 ≫ Iso.hom X.cofanPtIsoSelf).φ i ≫ eqToHom ⋯ =
    Hom.φ (Hom.fromIncl i_1 (𝟙 (X.obj i_1))) i

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : FormalCoproduct.{w, u} C
i : X.I
⊢ Hom.fromIncl i (𝟙 (X.obj i)) ≫ Iso.inv X.cofanPtIsoSelf = Cofan.inj (cofan X.I (toFun.{w, v, u} X)) i

Tactic:
(Iso.comp_inv_eq _).2 (inj_comp_cofanPtIsoSelf_hom _ _).symm

Premises used: Iff.mpr, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Limits.FormalCoproduct.inj_comp_cofanPtIsoSelf_hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : FormalCoproduct.{w, u} C
i : X.I
⊢ Sigma.ι (toFun.{w, v, u} X) i ≫ Iso.hom X.coproductIsoSelf = Hom.fromIncl i (𝟙 (X.obj i))

Tactic:
simp [coproductIsoSelf]

Premises used: CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : FormalCoproduct.{w, u} C
i : X.I
⊢ Hom.fromIncl i (𝟙 (X.obj i)) ≫ Iso.inv X.coproductIsoSelf = Sigma.ι (toFun.{w, v, u} X) i

Tactic:
(Iso.comp_inv_eq _).2 (ι_comp_coproductIsoSelf_hom _ _).symm

Premises used: Iff.mpr, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Limits.FormalCoproduct.ι_comp_coproductIsoSelf_hom, Eq.symm
-- 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 : HasTerminal.{v, u} C
⊢ HasTerminal (FormalCoproduct.{w, u} C)

Tactic:
(isTerminalIncl (⊤_ C) terminalIsTerminal).hasTerminal

Premises used: CategoryTheory.Limits.FormalCoproduct.isTerminalIncl, CategoryTheory.Limits.terminal, CategoryTheory.Limits.IsTerminal.hasTerminal, CategoryTheory.Limits.terminalIsTerminal
-- 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
i : Function.Pullback f.f g.f
rw rw₁ : Z.obj (g.f (↑i : X.I × Y.I).2) = Z.obj (g.f (↑i : X.I × Y.I).2)
⊢ Z.obj (f.f (↑i : X.I × Y.I).1) = Z.obj (g.f (↑i : X.I × Y.I).2)

Tactic:
rw [i.2]

Premises used: Subtype.property
-- 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)
i : (pullbackCone f g pb).pt.I
⊢ (pullbackCone f g pb).fst.f i = (↑i : X.I × Y.I).1

Tactic:
rfl

Premises used: 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)
i : (pullbackCone f g pb).pt.I
⊢ (pullbackCone f g pb).fst.φ i = (pb i).fst

Tactic:
rfl

Premises used: 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)
i : (pullbackCone f g pb).pt.I
⊢ (pullbackCone f g pb).snd.f i = (↑i : X.I × Y.I).2

Tactic:
rfl

Premises used: 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)
i : (pullbackCone f g pb).pt.I
⊢ (pullbackCone f g pb).snd.φ i = (pb i).snd

Tactic:
rfl

Premises used: 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)
⊢ (pullbackCone f g pb).fst ≫ f = (pullbackCone f g pb).snd ≫ g

Tactic:
PullbackCone.condition _

Premises used: CategoryTheory.Limits.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
m : T ⟶ (pullbackCone f g pb).pt
⊢ (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd).1 ≫ f =
    (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd).2 ≫ g

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 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 : { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }
i : T.I
⊢ (↑s : (T ⟶ X) × (T ⟶ Y)).1.φ i ≫
      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) ⋯ :
                      { p : X.I × Y.I // f.f p.1 = g.f p.2 }))
                  i) :
              X.I × Y.I).1 ≫
        eqToHom ⋯ =
    (↑s : (T ⟶ X) × (T ⟶ Y)).2.φ i ≫
      g.φ
        (↑((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) :
            X.I × Y.I).2

Tactic:
simpa using ((hom_ext_iff _ _).1 s.2).2 i

Premises used: CategoryTheory.Limits.FormalCoproduct.hom_ext_iff, Iff.mp, Subtype.property
-- 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
m : T ⟶ (pullbackCone f g pb).pt
i : T.I
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)) ⋯))
      (PullbackCone.mk (m.φ i ≫ (pullbackCone f g pb).fst.φ (m.f i)) (m.φ i ≫ (pullbackCone f g pb).snd.φ (m.f i)) ⋯) =
    m.φ 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

Tactic:
simp only [category_comp_f, category_comp_φ, eqToHom_refl, Category.comp_id]

Premises used: CategoryTheory.Limits.FormalCoproduct.category_comp_f, CategoryTheory.eqToHom_refl, CategoryTheory.Limits.FormalCoproduct.category_comp_φ, CategoryTheory.Category.comp_id
-- 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
m : T ⟶ (pullbackCone f g pb).pt
i : T.I
⊢ 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)) ⋯))
        (PullbackCone.mk (m.φ i ≫ (pullbackCone f g pb).fst.φ (m.f i)) (m.φ i ≫ (pullbackCone f g pb).snd.φ (m.f i))
          ⋯) ≫
      PullbackCone.fst
        (pb
          (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)) ⋯)) =
    m.φ i ≫
      PullbackCone.fst
        (pb
          (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)) ⋯))

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 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
⊢ 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)) ⋯))
        (PullbackCone.mk (m.φ i ≫ (pullbackCone f g pb).fst.φ (m.f i)) (m.φ i ≫ (pullbackCone f g pb).snd.φ (m.f i))
          ⋯) ≫
      PullbackCone.snd
        (pb
          (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)) ⋯)) =
    m.φ i ≫
      PullbackCone.snd
        (pb
          (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)) ⋯))

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 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
⊢ 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)) ⋯))
      (PullbackCone.mk (m.φ i ≫ (pullbackCone f g pb).fst.φ (m.f i)) (m.φ i ≫ (pullbackCone f g pb).snd.φ (m.f i)) ⋯) =
    m.φ i

Tactic:
exact (hpb _).hom_ext ((pb _).equalizer_ext (by aesop) (by aesop))

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.PullbackCone.equalizer_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 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 : { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }
x : T.I
⊢ Hom.f.{w, v, u}
      (↑((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 }))
              ((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))
                s)) :
          (T ⟶ X) × (T ⟶ Y)).1
      x =
    (↑s : (T ⟶ X) × (T ⟶ Y)).1.f 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
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 : { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }
x : T.I
⊢ Hom.f.{w, v, u}
      (↑((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 }))
              ((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))
                s)) :
          (T ⟶ X) × (T ⟶ Y)).2
      x =
    (↑s : (T ⟶ X) × (T ⟶ Y)).2.f 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
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
refine :
  ∀ (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 =
      (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
⊢ IsLimit (pullbackCone f g pb)

Tactic:
refine PullbackCone.IsLimit.mk
    (fst := (pullbackCone f g pb).fst) (snd := (pullbackCone f g pb).snd) _
    (fun s ↦ (homPullbackEquiv f g pb hpb s.pt).2 ⟨(s.fst, s.snd), s.condition⟩)
    (fun s ↦ congrArg (·.1.fst)
      ((homPullbackEquiv f g pb hpb s.pt).right_inv ⟨(s.fst, s.snd), s.condition⟩))
    (fun s ↦ congrArg (·.1.snd)
      ((homPullbackEquiv f g pb hpb s.pt).right_inv ⟨(s.fst, s.snd), s.condition⟩))
    (fun s m h₁ h₂ ↦ ?_)

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.PullbackCone.IsLimit.mk, Prod.mk, CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv, CategoryTheory.Limits.Cone.pt, Subtype.mk, CategoryTheory.Limits.PullbackCone.snd, Equiv.invFun
-- 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 = Equiv.invFun (homPullbackEquiv f g pb hpb s.pt) (Equiv.toFun (homPullbackEquiv f g pb hpb s.pt) m)

Tactic:
((homPullbackEquiv f g pb hpb s.pt).left_inv m).symm

Premises used: CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv, CategoryTheory.Limits.Cone.pt, Eq.symm, Equiv.left_inv