awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
f : β → C
inst_1 : HasProduct.{w, v, u} f
c : Fan.{w, v, u} f
⊢ Nonempty (IsLimit c) ↔ IsIso (Y := piObj.{w, v, u} f) (Pi.lift c.proj)

Tactic:
(limit.isLimit (Discrete.functor f)).nonempty_isLimit_iff_isIso_lift

Premises used: CategoryTheory.Limits.Fan.proj, CategoryTheory.Limits.Fan.mk, CategoryTheory.Limits.IsLimit.nonempty_isLimit_iff_isIso_lift, CategoryTheory.Discrete.functor, CategoryTheory.Discrete.natTrans, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
β : Type w
f : β → C
inst_1 : HasCoproduct.{w, v, u} f
P : C
p : (b : β) → f b ⟶ P
b : β
⊢ CategoryStruct.comp (Y := sigmaObj.{w, v, u} f) (ι f b) (desc p) = p b

Tactic:
simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]

Premises used: CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
f : β → C
inst_1 : HasCoproduct.{w, v, u} f
⊢ IsIso.{v, u} (𝟙 (sigmaObj.{w, v, u} f))

Tactic:
IsIso.id _

Premises used: CategoryTheory.IsIso.id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
f : β → C
inst_1 : HasCoproduct.{w, v, u} f
h : (Sigma.desc fun (a : β) ↦ Sigma.ι f a) = 𝟙 (sigmaObj.{w, v, u} f)
⊢ IsIso.{v, u} (C := C) (X := sigmaObj.{w, v, u} f) (Y := sigmaObj.{w, v, u} f) (Sigma.desc fun (a : β) ↦ Sigma.ι f a)

Tactic:
convert! IsIso.id _

Premises used: CategoryTheory.IsIso.id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
f : β → C
inst_1 : HasCoproduct.{w, v, u} f
h :
  ∀ (b : β),
    CategoryStruct.comp (Y := sigmaObj.{w, v, u} f) (Sigma.ι f b) (Sigma.desc fun (a : β) ↦ Sigma.ι f a) =
      Sigma.ι f b ≫ 𝟙 (sigmaObj.{w, v, u} f)
⊢ (Sigma.desc fun (a : β) ↦ Sigma.ι f a) = 𝟙 (sigmaObj.{w, v, u} f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
f : β → C
inst_1 : HasCoproduct.{w, v, u} f
b : β
⊢ CategoryStruct.comp (Y := sigmaObj.{w, v, u} f) (Sigma.ι f b) (Sigma.desc fun (a : β) ↦ Sigma.ι f a) =
    Sigma.ι f b ≫ 𝟙 (sigmaObj.{w, v, u} f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
f : β → C
inst_1 : HasCoproduct.{w, v, u} f
c : Cofan.{w, v, u} f
⊢ Nonempty (IsColimit c) ↔ IsIso (X := sigmaObj.{w, v, u} f) (Sigma.desc c.inj)

Tactic:
(colimit.isColimit (Discrete.functor f)).nonempty_isColimit_iff_isIso_desc

Premises used: CategoryTheory.Limits.IsColimit.nonempty_isColimit_iff_isIso_desc, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Discrete.functor, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.natTrans, CategoryTheory.Limits.Cofan.inj, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.Cofan.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ (t :
      Cofan (C := C) fun (x : (a : α) × β a) ↦
        match (motive := (a : α) × β a → C) x with
        | ⟨a, b⟩ => Y a b) →
    Cocone.pt (J := Discrete ((a : α) × β a)) (F :=
        Discrete.functor fun (x : (a : α) × β a) ↦
          match (motive := (a : α) × β a → C) x with
          | ⟨a, b⟩ => Y a b)
        (mk c.pt fun (x : (a : α) × β a) ↦
          match (motive :=
            (x : (a : α) × β a) →
              (fun (x : (a : α) × β a) ↦
                    (match (motive := (a : α) × β a → C) x with
                      | ⟨a, b⟩ => Y a b :
                      C))
                  x ⟶
                c.pt)
            x with
          | ⟨a, b⟩ => π a b ≫ c.inj a) ⟶
      t.pt

Tactic:
exact fun t ↦ hc.desc (Cofan.mk _ fun a ↦ (hs a).desc (Cofan.mk t.pt (fun b ↦ t.inj ⟨a, b⟩)))

Premises used: CategoryTheory.Limits.IsColimit.desc, CategoryTheory.Limits.Cofan.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan (C := C) fun (x : (a : α) × β a) ↦
    match (motive := (a : α) × β a → C) x with
    | ⟨a, b⟩ => Y a b
a : α
b : β a
refine_2 :
  Eq (α := Y a b ⟶ t.pt)
    (π a b ≫
        c.inj a ≫
          hc.desc
            (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b))) :
      Y a b ⟶ t.pt)
    (t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b) :
      Y ((Sigma.mk (β := fun (a : α) ↦ β a) a b).fst (β := fun (a : α) ↦ β a))
          ((Sigma.mk (β := fun (a : α) ↦ β a) a b).snd (β := fun (a : α) ↦ β a)) ⟶
        t.pt)
⊢ Eq.{v + 1} (α :=
    (match (motive := (a : α) × β a → C) Sigma.mk (β := fun (a : α) ↦ β a) a b with
      | ⟨a, b⟩ => Y a b) ⟶
      t.pt)
    (CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete ((a : α) × β a)) (F :=
          Discrete.functor fun (x : (a : α) × β a) ↦
            match (motive := (a : α) × β a → C) x with
            | ⟨a, b⟩ => Y a b)
          (mk c.pt fun (x : (a : α) × β a) ↦
            match (motive :=
              (x : (a : α) × β a) →
                (fun (x : (a : α) × β a) ↦
                      (match (motive := (a : α) × β a → C) x with
                        | ⟨a, b⟩ => Y a b :
                        C))
                    x ⟶
                  c.pt)
              x with
            | ⟨a, b⟩ => π a b ≫ c.inj a))
        (inj (f := fun (x : (a : α) × β a) ↦
          match (motive := (a : α) × β a → C) x with
          | ⟨a, b⟩ => Y a b)
          (mk c.pt fun (x : (a : α) × β a) ↦
            match (motive :=
              (x : (a : α) × β a) →
                (fun (x : (a : α) × β a) ↦
                      (match (motive := (a : α) × β a → C) x with
                        | ⟨a, b⟩ => Y a b :
                        C))
                    x ⟶
                  c.pt)
              x with
            | ⟨a, b⟩ => π a b ≫ c.inj a)
          (Sigma.mk (β := fun (a : α) ↦ β a) a b))
        (hc.desc
          (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b)))) :
      (match (motive := (a : α) × β a → C) Sigma.mk (β := fun (a : α) ↦ β a) a b with
        | ⟨a, b⟩ => Y a b) ⟶
        t.pt)
    (t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b) :
      (match (motive := (a : α) × β a → C) Sigma.mk (β := fun (a : α) ↦ β a) a b with
        | ⟨a, b⟩ => Y a b) ⟶
        t.pt)

Tactic:
simp only [mk_pt, cofan_mk_inj, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Limits.cofan_mk_inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan (C := C) fun (x : (a : α) × β a) ↦
    match (motive := (a : α) × β a → C) x with
    | ⟨a, b⟩ => Y a b
a : α
b : β a
refine_2 :
  Eq.{v + 1} (α := Y a b ⟶ t.pt)
    (NatTrans.app
        (Cocone.ι (mk t.pt fun (b : β { as := a }.as) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) { as := a }.as b)))
        { as := b } :
      Functor.obj.{u_1, v, u_1, u} (Discrete.functor (Y a)) { as := b : Discrete (β a) } ⟶
        Functor.obj.{u_1, v, u_1, u}
          (Functor.obj (Functor.const (Discrete (β a)))
            (Cocone.pt.{u_1, v, u_1, u} (J := Discrete (β a)) (F := Discrete.functor (Y a))
              (mk t.pt fun (b : β { as := a : Discrete α }.as) ↦
                t.inj (Sigma.mk (β := fun (a : α) ↦ β a) { as := a : Discrete α }.as b))))
          { as := b : Discrete (β a) })
    (t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b))
⊢ Eq (α := Y a b ⟶ t.pt)
    (π a b ≫
        c.inj a ≫
          hc.desc
            (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b))) :
      Y a b ⟶ t.pt)
    (t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b) :
      Y ((Sigma.mk (β := fun (a : α) ↦ β a) a b).fst (β := fun (a : α) ↦ β a))
          ((Sigma.mk (β := fun (a : α) ↦ β a) a b).snd (β := fun (a : α) ↦ β a)) ⟶
        t.pt)

Tactic:
erw [hc.fac, (hs a).fac]

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan (C := C) fun (x : (a : α) × β a) ↦
    match (motive := (a : α) × β a → C) x with
    | ⟨a, b⟩ => Y a b
a : α
b : β a
⊢ Eq.{v + 1} (α := Y a b ⟶ t.pt)
    (NatTrans.app
        (Cocone.ι (mk t.pt fun (b : β { as := a }.as) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) { as := a }.as b)))
        { as := b } :
      Functor.obj.{u_1, v, u_1, u} (Discrete.functor (Y a)) { as := b : Discrete (β a) } ⟶
        Functor.obj.{u_1, v, u_1, u}
          (Functor.obj (Functor.const (Discrete (β a)))
            (Cocone.pt.{u_1, v, u_1, u} (J := Discrete (β a)) (F := Discrete.functor (Y a))
              (mk t.pt fun (b : β { as := a : Discrete α }.as) ↦
                t.inj (Sigma.mk (β := fun (a : α) ↦ β a) { as := a : Discrete α }.as b))))
          { as := b : Discrete (β a) })
    (t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan (C := C) fun (x : (a : α) × β a) ↦
    match (motive := (a : α) × β a → C) x with
    | ⟨a, b⟩ => Y a b
m :
  Cocone.pt (J := Discrete ((a : α) × β a)) (F :=
      Discrete.functor fun (x : (a : α) × β a) ↦
        match (motive := (a : α) × β a → C) x with
        | ⟨a, b⟩ => Y a b)
      (mk c.pt fun (x : (a : α) × β a) ↦
        match (motive :=
          (x : (a : α) × β a) →
            (fun (x : (a : α) × β a) ↦
                  (match (motive := (a : α) × β a → C) x with
                    | ⟨a, b⟩ => Y a b :
                    C))
                x ⟶
              c.pt)
          x with
        | ⟨a, b⟩ => π a b ≫ c.inj a) ⟶
    t.pt
h :
  ∀ (j : (a : α) × β a),
    inj (f := fun (x : (a : α) × β a) ↦
          match (motive := (a : α) × β a → C) x with
          | ⟨a, b⟩ => Y a b)
          (mk c.pt fun (x : (a : α) × β a) ↦
            match (motive :=
              (x : (a : α) × β a) →
                (fun (x : (a : α) × β a) ↦
                      (match (motive := (a : α) × β a → C) x with
                        | ⟨a, b⟩ => Y a b :
                        C))
                    x ⟶
                  c.pt)
              x with
            | ⟨a, b⟩ => π a b ≫ c.inj a)
          j ≫
        m =
      t.inj j
⊢ m = hc.desc (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b)))

Tactic:
hc.hom_ext fun ⟨a⟩ ↦ (hs a).hom_ext fun ⟨b⟩ ↦ ?_

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.Fan.ext.match_1, CategoryTheory.Discrete.functor, CategoryTheory.Limits.Cofan.isColimitTrans.match_3, CategoryTheory.Discrete.mk, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.Cofan.inj, CategoryTheory.Limits.IsColimit.desc, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Cofan.mk, Sigma.mk, Eq, CategoryTheory.NatTrans.app, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan (C := C) fun (x : (a : α) × β a) ↦
    match (motive := (a : α) × β a → C) x with
    | ⟨a, b⟩ => Y a b
m :
  Cocone.pt (J := Discrete ((a : α) × β a)) (F :=
      Discrete.functor fun (x : (a : α) × β a) ↦
        match (motive := (a : α) × β a → C) x with
        | ⟨a, b⟩ => Y a b)
      (mk c.pt fun (x : (a : α) × β a) ↦
        match (motive :=
          (x : (a : α) × β a) →
            (fun (x : (a : α) × β a) ↦
                  (match (motive := (a : α) × β a → C) x with
                    | ⟨a, b⟩ => Y a b :
                    C))
                x ⟶
              c.pt)
          x with
        | ⟨a, b⟩ => π a b ≫ c.inj a) ⟶
    t.pt
h :
  ∀ (j : (a : α) × β a),
    inj (f := fun (x : (a : α) × β a) ↦
          match (motive := (a : α) × β a → C) x with
          | ⟨a, b⟩ => Y a b)
          (mk c.pt fun (x : (a : α) × β a) ↦
            match (motive :=
              (x : (a : α) × β a) →
                (fun (x : (a : α) × β a) ↦
                      (match (motive := (a : α) × β a → C) x with
                        | ⟨a, b⟩ => Y a b :
                        C))
                    x ⟶
                  c.pt)
              x with
            | ⟨a, b⟩ => π a b ≫ c.inj a)
          j ≫
        m =
      t.inj j
refine_3 :
  ∀ (x : Discrete α) (a : α) (x : Discrete (β a)) (b : β a),
    Eq (α := Functor.obj.{u_1, v, u_1, u} (Discrete.functor (Y a)) { as := b : Discrete (β a) } ⟶ t.pt)
      ((mk (X a) (π a)).ι.app { as := b : Discrete (β a) } ≫ c.ι.app { as := a } ≫ m)
      ((mk (X a) (π a)).ι.app { as := b : Discrete (β a) } ≫
        c.ι.app { as := a : Discrete α } ≫
          hc.desc
            (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b))))
⊢ m = hc.desc (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b)))

Tactic:
refine hc.hom_ext fun ⟨a⟩ ↦ (hs a).hom_ext fun ⟨b⟩ ↦ ?_

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.Cofan.isColimitTrans.match_3, CategoryTheory.Discrete.mk, CategoryTheory.Limits.Cocone.ι, CategoryTheory.CategoryStruct.comp, _private.0.CategoryTheory.Limits.Fan.IsLimit.hom_ext.match_1, CategoryTheory.Limits.Cofan.mk, Eq, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan (C := C) fun (x : (a : α) × β a) ↦
    match (motive := (a : α) × β a → C) x with
    | ⟨a, b⟩ => Y a b
m :
  Cocone.pt (J := Discrete ((a : α) × β a)) (F :=
      Discrete.functor fun (x : (a : α) × β a) ↦
        match (motive := (a : α) × β a → C) x with
        | ⟨a, b⟩ => Y a b)
      (mk c.pt fun (x : (a : α) × β a) ↦
        match (motive :=
          (x : (a : α) × β a) →
            (fun (x : (a : α) × β a) ↦
                  (match (motive := (a : α) × β a → C) x with
                    | ⟨a, b⟩ => Y a b :
                    C))
                x ⟶
              c.pt)
          x with
        | ⟨a, b⟩ => π a b ≫ c.inj a) ⟶
    t.pt
h :
  ∀ (j : (a : α) × β a),
    inj (f := fun (x : (a : α) × β a) ↦
          match (motive := (a : α) × β a → C) x with
          | ⟨a, b⟩ => Y a b)
          (mk c.pt fun (x : (a : α) × β a) ↦
            match (motive :=
              (x : (a : α) × β a) →
                (fun (x : (a : α) × β a) ↦
                      (match (motive := (a : α) × β a → C) x with
                        | ⟨a, b⟩ => Y a b :
                        C))
                    x ⟶
                  c.pt)
              x with
            | ⟨a, b⟩ => π a b ≫ c.inj a)
          j ≫
        m =
      t.inj j
x : Discrete α
a : α
x_1 : Discrete (β a)
b : β a
refine_3 :
  Eq (α := Functor.obj.{u_1, v, u_1, u} (Discrete.functor (Y a)) { as := b : Discrete (β a) } ⟶ t.pt)
    ((mk (X a) (π a)).ι.app { as := b : Discrete (β a) } ≫ c.ι.app { as := a } ≫ m)
    (NatTrans.app
      (Cocone.ι (mk t.pt fun (b : β { as := a }.as) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) { as := a }.as b)))
      { as := b })
⊢ Eq (α := Functor.obj.{u_1, v, u_1, u} (Discrete.functor (Y a)) { as := b : Discrete (β a) } ⟶ t.pt)
    ((mk (X a) (π a)).ι.app { as := b : Discrete (β a) } ≫ c.ι.app { as := a } ≫ m)
    ((mk (X a) (π a)).ι.app { as := b : Discrete (β a) } ≫
      c.ι.app { as := a : Discrete α } ≫
        hc.desc
          (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b))))

Tactic:
erw [hc.fac, (hs a).fac]

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan (C := C) fun (x : (a : α) × β a) ↦
    match (motive := (a : α) × β a → C) x with
    | ⟨a, b⟩ => Y a b
m :
  Cocone.pt (J := Discrete ((a : α) × β a)) (F :=
      Discrete.functor fun (x : (a : α) × β a) ↦
        match (motive := (a : α) × β a → C) x with
        | ⟨a, b⟩ => Y a b)
      (mk c.pt fun (x : (a : α) × β a) ↦
        match (motive :=
          (x : (a : α) × β a) →
            (fun (x : (a : α) × β a) ↦
                  (match (motive := (a : α) × β a → C) x with
                    | ⟨a, b⟩ => Y a b :
                    C))
                x ⟶
              c.pt)
          x with
        | ⟨a, b⟩ => π a b ≫ c.inj a) ⟶
    t.pt
h :
  ∀ (j : (a : α) × β a),
    inj (f := fun (x : (a : α) × β a) ↦
          match (motive := (a : α) × β a → C) x with
          | ⟨a, b⟩ => Y a b)
          (mk c.pt fun (x : (a : α) × β a) ↦
            match (motive :=
              (x : (a : α) × β a) →
                (fun (x : (a : α) × β a) ↦
                      (match (motive := (a : α) × β a → C) x with
                        | ⟨a, b⟩ => Y a b :
                        C))
                    x ⟶
                  c.pt)
              x with
            | ⟨a, b⟩ => π a b ≫ c.inj a)
          j ≫
        m =
      t.inj j
x : Discrete α
a : α
x_1 : Discrete (β a)
b : β a
⊢ Eq (α := Functor.obj.{u_1, v, u_1, u} (Discrete.functor (Y a)) { as := b : Discrete (β a) } ⟶ t.pt)
    ((mk (X a) (π a)).ι.app { as := b : Discrete (β a) } ≫ c.ι.app { as := a } ≫ m)
    (NatTrans.app
      (Cocone.ι (mk t.pt fun (b : β { as := a }.as) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) { as := a }.as b)))
      { as := b })

Tactic:
simpa using h ⟨a, b⟩

Premises used: Sigma.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
f g : β → C
inst_1 : HasProduct.{w, v, u} f
inst_2 : HasProduct.{w, v, u} g
p : (b : β) → f b ⟶ g b
b : β
⊢ Eq (α := piObj.{w, v, u} f ⟶ g b) (CategoryStruct.comp (Y := piObj.{w, v, u} g) (map p) (π g b)) (π f b ≫ p b)

Tactic:
simp [Pi.map]

Premises used: CategoryTheory.Limits.Pi.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
inst_1 : HasProduct.{w₂, v, u} f
h :
  ∀ (b : α),
    CategoryStruct.comp (Y := piObj.{w₂, v, u} f) (map fun (a : α) ↦ 𝟙 (f a)) (π f b) = 𝟙 (piObj.{w₂, v, u} f) ≫ π f b
⊢ (map fun (a : α) ↦ 𝟙 (f a)) = 𝟙 (piObj.{w₂, v, u} f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
inst_1 : HasProduct.{w₂, v, u} f
b : α
⊢ CategoryStruct.comp (Y := piObj.{w₂, v, u} f) (map fun (a : α) ↦ 𝟙 (f a)) (π f b) = 𝟙 (piObj.{w₂, v, u} f) ≫ π f b

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
f g h : α → C
inst_1 : HasProduct.{w₂, v, u} f
inst_2 : HasProduct.{w₂, v, u} g
inst_3 : HasProduct.{w₂, v, u} h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
h₁ :
  ∀ (b : α),
    Eq (α := piObj.{w₂, v, u} f ⟶ h b)
      (CategoryStruct.comp (Y := piObj.{w₂, v, u} h) (CategoryStruct.comp (Y := piObj.{w₂, v, u} g) (map q) (map q'))
        (π h b))
      (CategoryStruct.comp (Y := piObj.{w₂, v, u} h) (map fun (a : α) ↦ q a ≫ q' a) (π h b))
⊢ Eq (α := piObj.{w₂, v, u} f ⟶ piObj.{w₂, v, u} h) (CategoryStruct.comp (Y := piObj.{w₂, v, u} g) (map q) (map q'))
    (map fun (a : α) ↦ q a ≫ q' a)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
f g h : α → C
inst_1 : HasProduct.{w₂, v, u} f
inst_2 : HasProduct.{w₂, v, u} g
inst_3 : HasProduct.{w₂, v, u} h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
b : α
⊢ Eq (α := piObj.{w₂, v, u} f ⟶ h b)
    (CategoryStruct.comp (Y := piObj.{w₂, v, u} h) (CategoryStruct.comp (Y := piObj.{w₂, v, u} g) (map q) (map q'))
      (π h b))
    (CategoryStruct.comp (Y := piObj.{w₂, v, u} h) (map fun (a : α) ↦ q a ≫ q' a) (π h b))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
f g : β → C
inst_1 : HasProduct.{w, v, u} f
inst_2 : HasProduct.{w, v, u} g
p : (b : β) → f b ⟶ g b
inst_3 : ∀ (i : β), Mono (p i)
dsimp : ∀ (j : Discrete β), Mono (X := f j.as) (p j.as)
⊢ ∀ (j : Discrete β),
    Mono.{v, u} (C := C) (X := Functor.obj.{w, v, w, u} (Discrete.functor f) j) (Y :=
      Functor.obj.{w, v, w, u} (Discrete.functor g) j)
      (NatTrans.app (Discrete.natTrans fun (X : Discrete β) ↦ p X.as) j)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
f g : β → C
inst_1 : HasProduct.{w, v, u} f
inst_2 : HasProduct.{w, v, u} g
p : (b : β) → f b ⟶ g b
inst_3 : ∀ (i : β), Mono (p i)
⊢ ∀ (j : Discrete β), Mono (X := f j.as) (p j.as)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
g : β → C
inst_1 : HasProduct.{w₂, v, u} f
inst_2 : HasProduct.{w, v, u} g
p : β → α
q : (b : β) → f (p b) ⟶ g b
b : β
⊢ Eq (α := piObj.{w₂, v, u} f ⟶ g b) (CategoryStruct.comp (Y := piObj.{w, v, u} g) (map' p q) (π g b)) (π f (p b) ≫ q b)

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.Pi.map', CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
inst_1 : HasProduct.{w₂, v, u} f
h :
  ∀ (b : α),
    CategoryStruct.comp (Y := piObj.{w₂, v, u} f) (map' id fun (a : α) ↦ 𝟙 (f a)) (π f b) =
      𝟙 (piObj.{w₂, v, u} f) ≫ π f b
⊢ (map' id fun (a : α) ↦ 𝟙 (f a)) = 𝟙 (piObj.{w₂, v, u} f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
inst_1 : HasProduct.{w₂, v, u} f
b : α
⊢ CategoryStruct.comp (Y := piObj.{w₂, v, u} f) (map' id fun (a : α) ↦ 𝟙 (f a)) (π f b) = 𝟙 (piObj.{w₂, v, u} f) ≫ π f b

Tactic:
simp