awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v, v, u} C
X : C
x : Type v
a :
  Eq (α :=
    Opposite.unop (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x) ⟶
      Opposite.unop (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x))
    (Quiver.Hom.unop
      (CategoryStruct.comp (Y :=
        Functor.obj (Functor.rightOp (Functor.obj piConst X))
          (Functor.obj (Functor.obj yoneda X) (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x)))
        (Functor.map (Functor.rightOp (Functor.obj piConst X))
          (NatTrans.app
            { app := fun (n : Type v) ↦ ↾fun (i : Functor.obj (𝟭 (Type v)) n) ↦ Pi.π (fun (x : n) ↦ X) i,
              naturality := ⋯ }
            x))
        (NatTrans.app { app := fun (Y : Cᵒᵖ) ↦ Quiver.Hom.op (Pi.lift id), naturality := ⋯ }
          (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x))))
    (Quiver.Hom.unop (𝟙 (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x)))
⊢ CategoryStruct.comp (Y :=
      Functor.obj (Functor.rightOp (Functor.obj piConst X))
        (Functor.obj (Functor.obj yoneda X) (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x)))
      (Functor.map (Functor.rightOp (Functor.obj piConst X))
        (NatTrans.app
          { app := fun (n : Type v) ↦ ↾fun (i : Functor.obj (𝟭 (Type v)) n) ↦ Pi.π (fun (x : n) ↦ X) i,
            naturality := ⋯ }
          x))
      (NatTrans.app { app := fun (Y : Cᵒᵖ) ↦ Quiver.Hom.op (Pi.lift id), naturality := ⋯ }
        (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x)) =
    𝟙 (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x)

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
x : Discrete β
j : β
dsimp : f default = f j
⊢ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) { as := j : Discrete β } =
    Functor.obj.{w, v, w, u} (Discrete.functor f) { as := j : Discrete β }

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
x : Discrete β
j : β
e_a : default = j
⊢ f default = f j

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
x : Discrete β
j : β
⊢ default = j

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
s : Cone.{w, v, w, u} (Discrete.functor f)
j : Discrete β
obtain :
  Eq (α := s.pt ⟶ Functor.obj.{w, v, w, u} (Discrete.functor f) default)
    (CategoryStruct.comp (Y :=
      Cone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
        { pt := f default,
          π :=
            Discrete.natTrans fun (x : Discrete β) ↦
              match (motive :=
                (x : Discrete β) →
                  Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                    Functor.obj.{w, v, w, u} (Discrete.functor f) x)
                x with
              | { as := j } => eqToHom ⋯ })
      (s.π.app default)
      (NatTrans.app
        (Cone.π
          { pt := f default,
            π :=
              Discrete.natTrans fun (x : Discrete β) ↦
                match (motive :=
                  (x : Discrete β) →
                    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                      Functor.obj.{w, v, w, u} (Discrete.functor f) x)
                  x with
                | { as := j } => eqToHom ⋯ })
        default))
    (s.π.app default)
⊢ CategoryStruct.comp (Y :=
      Cone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
        { pt := f default,
          π :=
            Discrete.natTrans fun (x : Discrete β) ↦
              match (motive :=
                (x : Discrete β) →
                  Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                    Functor.obj.{w, v, w, u} (Discrete.functor f) x)
                x with
              | { as := j } => eqToHom ⋯ })
      (s.π.app default)
      (NatTrans.app
        (Cone.π
          { pt := f default,
            π :=
              Discrete.natTrans fun (x : Discrete β) ↦
                match (motive :=
                  (x : Discrete β) →
                    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                      Functor.obj.{w, v, w, u} (Discrete.functor f) x)
                  x with
                | { as := j } => eqToHom ⋯ })
        j) =
    s.π.app j

Tactic:
obtain rfl := Subsingleton.elim j default

Premises used: Inhabited.default, Subsingleton.elim, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
s : Cone.{w, v, w, u} (Discrete.functor f)
⊢ Eq (α := s.pt ⟶ Functor.obj.{w, v, w, u} (Discrete.functor f) default)
    (CategoryStruct.comp (Y :=
      Cone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
        { pt := f default,
          π :=
            Discrete.natTrans fun (x : Discrete β) ↦
              match (motive :=
                (x : Discrete β) →
                  Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                    Functor.obj.{w, v, w, u} (Discrete.functor f) x)
                x with
              | { as := j } => eqToHom ⋯ })
      (s.π.app default)
      (NatTrans.app
        (Cone.π
          { pt := f default,
            π :=
              Discrete.natTrans fun (x : Discrete β) ↦
                match (motive :=
                  (x : Discrete β) →
                    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                      Functor.obj.{w, v, w, u} (Discrete.functor f) x)
                  x with
                | { as := j } => eqToHom ⋯ })
        default))
    (s.π.app default)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
s : Cone.{w, v, w, u} (Discrete.functor f)
m :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
      { pt := f default,
        π :=
          Discrete.natTrans fun (x : Discrete β) ↦
            match (motive :=
              (x : Discrete β) →
                Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                  Functor.obj.{w, v, w, u} (Discrete.functor f) x)
              x with
            | { as := j } => eqToHom ⋯ }
w :
  ∀ (j : Discrete β),
    m ≫
        NatTrans.app
          (Cone.π
            { pt := f default,
              π :=
                Discrete.natTrans fun (x : Discrete β) ↦
                  match (motive :=
                    (x : Discrete β) →
                      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                        Functor.obj.{w, v, w, u} (Discrete.functor f) x)
                    x with
                  | { as := j } => eqToHom ⋯ })
          j =
      s.π.app j
⊢ Eq (α := s.pt ⟶ Functor.obj.{w, v, w, u} (Discrete.functor f) default)
    (m ≫
      NatTrans.app
        (Cone.π
          { pt := f default,
            π :=
              Discrete.natTrans fun (x : Discrete β) ↦
                match (motive :=
                  (x : Discrete β) →
                    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                      Functor.obj.{w, v, w, u} (Discrete.functor f) x)
                  x with
                | { as := j } => eqToHom ⋯ })
        default)
    (s.π.app default)

Tactic:
specialize w default

Premises used: Inhabited.default
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
s : Cone.{w, v, w, u} (Discrete.functor f)
m :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
      { pt := f default,
        π :=
          Discrete.natTrans fun (x : Discrete β) ↦
            match (motive :=
              (x : Discrete β) →
                Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                  Functor.obj.{w, v, w, u} (Discrete.functor f) x)
              x with
            | { as := j } => eqToHom ⋯ }
w :
  Eq (α := s.pt ⟶ Functor.obj.{w, v, w, u} (Discrete.functor f) default)
    (m ≫
      NatTrans.app
        (Cone.π
          { pt := f default,
            π :=
              Discrete.natTrans fun (x : Discrete β) ↦
                match (motive :=
                  (x : Discrete β) →
                    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                      Functor.obj.{w, v, w, u} (Discrete.functor f) x)
                  x with
                | { as := j } => eqToHom ⋯ })
        default)
    (s.π.app default)
⊢ m = s.π.app default

Tactic:
simpa using w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Nonempty β
inst_2 : Subsingleton β
f : β → C
⊢ HasProduct.{w, v, u} f

Tactic:
let ⟨_⟩ := nonempty_unique β; HasLimit.mk (limitConeOfUnique f)

Premises used: CategoryTheory.Limits.HasProduct, _private.0.CategoryTheory.Limits.hasProduct_unique.match_1, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.limitConeOfUnique, nonempty_unique
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst_1 : Unique J
refine_1 :
  ∀ (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y) (j : J),
    CategoryStruct.comp (Y :=
        Cone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ Y) (mk X fun (x : J) ↦ e.hom))
        ((fun (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y) ↦ s.proj default ≫ e.inv) s)
        (proj (mk X fun (x : J) ↦ e.hom) j) =
      s.proj j
refine_2 :
  ∀ (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y)
    (m :
      s.pt ⟶
        Cone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ Y) (mk X fun (x : J) ↦ e.hom))
    (hm : ∀ (j : J), m ≫ proj (mk X fun (x : J) ↦ e.hom) j = s.proj j),
    m = (fun (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y) ↦ s.proj default ≫ e.inv) s
⊢ IsLimit.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ Y) (mk X fun (x : J) ↦ e.hom)

Tactic:
refine Fan.IsLimit.mk _ (fun s ↦ s.proj default ≫ e.inv) (fun s j ↦ ?_) fun s m hm ↦ ?_

Premises used: Inhabited.default, CategoryTheory.Limits.Fan.proj, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Fan.IsLimit.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst_1 : Unique J
s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y
j : J
⊢ j = default

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst_1 : Unique J
s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y
j : J
refine_1 :
  CategoryStruct.comp (Y :=
      Cone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ Y) (mk X fun (x : J) ↦ e.hom))
      ((fun (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y) ↦ s.proj default ≫ e.inv) s)
      (proj (mk X fun (x : J) ↦ e.hom) default) =
    s.proj default
⊢ CategoryStruct.comp (Y :=
      Cone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ Y) (mk X fun (x : J) ↦ e.hom))
      ((fun (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y) ↦ s.proj default ≫ e.inv) s)
      (proj (mk X fun (x : J) ↦ e.hom) j) =
    s.proj j

Tactic:
obtain rfl : j = default := Subsingleton.elim _ _

Premises used: Inhabited.default, Subsingleton.elim, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst_1 : Unique J
s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y
⊢ CategoryStruct.comp (Y :=
      Cone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ Y) (mk X fun (x : J) ↦ e.hom))
      ((fun (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y) ↦ s.proj default ≫ e.inv) s)
      (proj (mk X fun (x : J) ↦ e.hom) default) =
    s.proj default

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst_1 : Unique J
s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y
m : s.pt ⟶ Cone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ Y) (mk X fun (x : J) ↦ e.hom)
hm : ∀ (j : J), m ≫ proj (mk X fun (x : J) ↦ e.hom) j = s.proj j
⊢ m = (fun (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y) ↦ s.proj default ≫ e.inv) s

Tactic:
simpa [← cancel_mono e.hom] using hm default

Premises used: Inhabited.default, CategoryTheory.cancel_mono, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
x : Discrete β
j : β
dsimp : f j = f default
⊢ Functor.obj.{w, v, w, u} (Discrete.functor f) { as := j : Discrete β } =
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) { as := j : Discrete β }

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
x : Discrete β
j : β
e_a : j = default
⊢ f j = f default

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
x : Discrete β
j : β
⊢ j = default

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
s : Cocone.{w, v, w, u} (Discrete.functor f)
j : Discrete β
obtain :
  Eq (α := Functor.obj.{w, v, w, u} (Discrete.functor f) default ⟶ s.pt)
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u} (C := Discrete β)
        (Functor.obj (Functor.const (Discrete β))
          (Cocone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
            { pt := f default,
              ι :=
                Discrete.natTrans fun (x : Discrete β) ↦
                  match (motive :=
                    (x : Discrete β) →
                      Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                    x with
                  | { as := j } => eqToHom ⋯ :
              Cocone.{w, v, w, u} (Discrete.functor f) }))
        default)
      (NatTrans.app
        (Cocone.ι
          { pt := f default,
            ι :=
              Discrete.natTrans fun (x : Discrete β) ↦
                match (motive :=
                  (x : Discrete β) →
                    Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                  x with
                | { as := j } => eqToHom ⋯ })
        default)
      (s.ι.app default))
    (s.ι.app default)
⊢ CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u}
        (Functor.obj (Functor.const (Discrete β))
          (Cocone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
            { pt := f default,
              ι :=
                Discrete.natTrans fun (x : Discrete β) ↦
                  match (motive :=
                    (x : Discrete β) →
                      Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                    x with
                  | { as := j } => eqToHom ⋯ :
              Cocone.{w, v, w, u} (Discrete.functor f) }))
        j)
      (NatTrans.app
        (Cocone.ι
          { pt := f default,
            ι :=
              Discrete.natTrans fun (x : Discrete β) ↦
                match (motive :=
                  (x : Discrete β) →
                    Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                  x with
                | { as := j } => eqToHom ⋯ })
        j)
      (s.ι.app default) =
    s.ι.app j

Tactic:
obtain rfl := Subsingleton.elim j default

Premises used: Inhabited.default, Subsingleton.elim, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
s : Cocone.{w, v, w, u} (Discrete.functor f)
⊢ Eq (α := Functor.obj.{w, v, w, u} (Discrete.functor f) default ⟶ s.pt)
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u} (C := Discrete β)
        (Functor.obj (Functor.const (Discrete β))
          (Cocone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
            { pt := f default,
              ι :=
                Discrete.natTrans fun (x : Discrete β) ↦
                  match (motive :=
                    (x : Discrete β) →
                      Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                    x with
                  | { as := j } => eqToHom ⋯ :
              Cocone.{w, v, w, u} (Discrete.functor f) }))
        default)
      (NatTrans.app
        (Cocone.ι
          { pt := f default,
            ι :=
              Discrete.natTrans fun (x : Discrete β) ↦
                match (motive :=
                  (x : Discrete β) →
                    Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                  x with
                | { as := j } => eqToHom ⋯ })
        default)
      (s.ι.app default))
    (s.ι.app default)

Tactic:
apply Category.id_comp

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
s : Cocone.{w, v, w, u} (Discrete.functor f)
m :
  Cocone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
      { pt := f default,
        ι :=
          Discrete.natTrans fun (x : Discrete β) ↦
            match (motive :=
              (x : Discrete β) →
                Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                  Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
              x with
            | { as := j } => eqToHom ⋯ :
        Cocone.{w, v, w, u} (Discrete.functor f) } ⟶
    s.pt
w :
  ∀ (j : Discrete β),
    NatTrans.app
          (Cocone.ι
            { pt := f default,
              ι :=
                Discrete.natTrans fun (x : Discrete β) ↦
                  match (motive :=
                    (x : Discrete β) →
                      Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                    x with
                  | { as := j } => eqToHom ⋯ })
          j ≫
        m =
      s.ι.app j
⊢ Eq (α := Functor.obj.{w, v, w, u} (Discrete.functor f) default ⟶ s.pt)
    (NatTrans.app
        (Cocone.ι
          { pt := f default,
            ι :=
              Discrete.natTrans fun (x : Discrete β) ↦
                match (motive :=
                  (x : Discrete β) →
                    Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                  x with
                | { as := j } => eqToHom ⋯ })
        default ≫
      m)
    (s.ι.app default)

Tactic:
specialize w default

Premises used: Inhabited.default
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
s : Cocone.{w, v, w, u} (Discrete.functor f)
m :
  Cocone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
      { pt := f default,
        ι :=
          Discrete.natTrans fun (x : Discrete β) ↦
            match (motive :=
              (x : Discrete β) →
                Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                  Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
              x with
            | { as := j } => eqToHom ⋯ :
        Cocone.{w, v, w, u} (Discrete.functor f) } ⟶
    s.pt
w :
  Eq (α := Functor.obj.{w, v, w, u} (Discrete.functor f) default ⟶ s.pt)
    (NatTrans.app
        (Cocone.ι
          { pt := f default,
            ι :=
              Discrete.natTrans fun (x : Discrete β) ↦
                match (motive :=
                  (x : Discrete β) →
                    Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                  x with
                | { as := j } => eqToHom ⋯ })
        default ≫
      m)
    (s.ι.app default)
⊢ m = s.ι.app default

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Nonempty β
inst_2 : Subsingleton β
f : β → C
⊢ HasCoproduct.{w, v, u} f

Tactic:
let ⟨_⟩ := nonempty_unique β; HasColimit.mk (colimitCoconeOfUnique f)

Premises used: CategoryTheory.Limits.colimitCoconeOfUnique, _private.0.CategoryTheory.Limits.hasProduct_unique.match_1, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.HasCoproduct, nonempty_unique
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst_1 : Unique J
refine_1 :
  ∀ (s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X) (j : J),
    CategoryStruct.comp (Y :=
        Cocone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom))
        (inj.{u_1, v, u} (f := fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom) j)
        ((fun (s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X) ↦ e.inv ≫ s.inj default) s) =
      s.inj j
refine_2 :
  ∀ (s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X)
    (m :
      Cocone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom) ⟶
        s.pt)
    (hm : ∀ (j : J), inj.{u_1, v, u} (f := fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom) j ≫ m = s.inj j),
    m = (fun (s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X) ↦ e.inv ≫ s.inj default) s
⊢ IsColimit.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom)

Tactic:
refine Cofan.IsColimit.mk _ (fun s ↦ e.inv ≫ s.inj default) (fun s j ↦ ?_) fun s m hm ↦ ?_

Premises used: Inhabited.default, CategoryTheory.Limits.Cofan.IsColimit.mk, CategoryTheory.Limits.Cofan.inj, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst_1 : Unique J
s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X
j : J
⊢ j = default

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim