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
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
refine_1 :
  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} (β := J) (f := fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom) default)
      ((fun (s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X) ↦ e.inv ≫ s.inj default) s) =
    s.inj default
⊢ 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

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 : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X
⊢ 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} (β := J) (f := fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom) default)
      ((fun (s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X) ↦ e.inv ≫ s.inj default) s) =
    s.inj 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 : 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

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

Premises used: Inhabited.default, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasProduct.{w', v, u} f
inst_2 : HasProduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
dsimp :
  Eq.{v + 1} (α := piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)) ⟶ f ((ε : (a : β) → γ) b))
    (CategoryStruct.comp (Y := piObj.{w', v, u} f)
      (Iso.hom
        (HasLimit.isoOfEquivalence (Discrete.equivalence ε)
          (Discrete.natIso fun (x : Discrete β) ↦ Iso.refl (f ((ε : (a : β) → γ) x.as)))))
      (π f ((ε : (a : β) → γ) b)))
    (π (f ∘ (⇑ε : (a : β) → γ)) b)
⊢ Eq.{v + 1} (α := piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)) ⟶ f ((ε : (a : β) → γ) b))
    (CategoryStruct.comp (Y := piObj.{w', v, u} f) (Iso.hom (reindex ε f)) (π f ((ε : (a : β) → γ) b)))
    (π (f ∘ (⇑ε : (a : β) → γ)) b)

Tactic:
dsimp [Pi.reindex]

Premises used: CategoryTheory.Limits.Pi.reindex
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasProduct.{w', v, u} f
inst_2 : HasProduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
simp :
  Eq.{v + 1} (α := piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)) ⟶ f ((ε : (a : β) → γ) b))
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)))
        (limit.π (Discrete.functor (f ∘ (⇑ε : (a : β) → γ))) { as := (ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) })
        (Functor.map (Discrete.functor f) ((Discrete.equivalence ε).counit.app { as := (ε : (a : β) → γ) b })) :
      limit.{w, w, v, u} (J := Discrete β) (Discrete.functor (f ∘ (⇑ε : (a : β) → γ))) ⟶ f ((ε : (a : β) → γ) b))
    (π (f ∘ (⇑ε : (a : β) → γ)) b : piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)) ⟶ (f ∘ (⇑ε : (a : β) → γ)) b)
⊢ Eq.{v + 1} (α := piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)) ⟶ f ((ε : (a : β) → γ) b))
    (CategoryStruct.comp (Y := piObj.{w', v, u} f)
      (Iso.hom
        (HasLimit.isoOfEquivalence (Discrete.equivalence ε)
          (Discrete.natIso fun (x : Discrete β) ↦ Iso.refl (f ((ε : (a : β) → γ) x.as)))))
      (π f ((ε : (a : β) → γ) b)))
    (π (f ∘ (⇑ε : (a : β) → γ)) b)

Tactic:
simp only [HasLimit.isoOfEquivalence_hom_π, Discrete.equivalence_inverse, Discrete.functor_obj,
    Function.comp_apply, Functor.id_obj, Discrete.equivalence_functor, Functor.comp_obj,
    Discrete.natIso_inv_app, Iso.refl_inv, Category.id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Discrete.functor_obj, CategoryTheory.Limits.HasLimit.isoOfEquivalence_hom_π, CategoryTheory.Discrete.equivalence_functor, CategoryTheory.Iso.refl_inv, CategoryTheory.Functor.id_obj, Function.comp_apply, CategoryTheory.Discrete.equivalence_inverse, CategoryTheory.Discrete.natIso_inv_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasProduct.{w', v, u} f
inst_2 : HasProduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
⊢ Eq.{v + 1} (α := piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)) ⟶ f ((ε : (a : β) → γ) b))
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)))
        (limit.π (Discrete.functor (f ∘ (⇑ε : (a : β) → γ))) { as := (ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) })
        (Functor.map (Discrete.functor f) ((Discrete.equivalence ε).counit.app { as := (ε : (a : β) → γ) b })) :
      limit.{w, w, v, u} (J := Discrete β) (Discrete.functor (f ∘ (⇑ε : (a : β) → γ))) ⟶ f ((ε : (a : β) → γ) b))
    (π (f ∘ (⇑ε : (a : β) → γ)) b : piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)) ⟶ (f ∘ (⇑ε : (a : β) → γ)) b)

Tactic:
limit.w (Discrete.functor (f ∘ ε)) (Discrete.eqToHom' (ε.symm_apply_apply b))

Premises used: Equiv.symm_apply_apply, CategoryTheory.Discrete.functor, Function.comp, CategoryTheory.Discrete.eqToHom', DFunLike.coe, CategoryTheory.Limits.limit.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasProduct.{w', v, u} f
inst_2 : HasProduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
⊢ Eq.{v + 1} (α := piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)) ⟶ f ((ε : (a : β) → γ) b))
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)))
        (limit.π (Discrete.functor (f ∘ (⇑ε : (a : β) → γ))) { as := (ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) })
        (Functor.map (Discrete.functor f) ((Discrete.equivalence ε).counit.app { as := (ε : (a : β) → γ) b })) :
      limit.{w, w, v, u} (J := Discrete β) (Discrete.functor (f ∘ (⇑ε : (a : β) → γ))) ⟶ f ((ε : (a : β) → γ) b))
    (π (f ∘ (⇑ε : (a : β) → γ)) b : piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)) ⟶ (f ∘ (⇑ε : (a : β) → γ)) b)

Tactic:
exact limit.w (Discrete.functor (f ∘ ε)) (Discrete.eqToHom' (ε.symm_apply_apply b))

Premises used: Equiv.symm_apply_apply, CategoryTheory.Discrete.functor, Function.comp, CategoryTheory.Discrete.eqToHom', DFunLike.coe, CategoryTheory.Limits.limit.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasProduct.{w', v, u} f
inst_2 : HasProduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
⊢ Eq.{v + 1} (α := piObj.{w', v, u} f ⟶ (f ∘ (⇑ε : (a : β) → γ)) b)
    (CategoryStruct.comp (Y := piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))) (Iso.inv (reindex ε f))
      (π (f ∘ (⇑ε : (a : β) → γ)) b))
    (π f ((ε : (a : β) → γ) b))

Tactic:
simp [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasCoproduct.{w', v, u} f
inst_2 : HasCoproduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
dsimp :
  Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))) (ι (f ∘ (⇑ε : (a : β) → γ)) b)
        (Iso.hom
          (HasColimit.isoOfEquivalence (Discrete.equivalence ε)
            (Discrete.natIso fun (x : Discrete β) ↦ Iso.refl (f ((ε : (a : β) → γ) x.as))))) :
      f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
⊢ Eq.{v + 1} (α := (f ∘ (⇑ε : (a : β) → γ)) b ⟶ sigmaObj.{w', v, u} f)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))) (ι (f ∘ (⇑ε : (a : β) → γ)) b)
      (Iso.hom (reindex ε f)))
    (ι f ((ε : (a : β) → γ) b))

Tactic:
dsimp [Sigma.reindex]

Premises used: CategoryTheory.Limits.Sigma.reindex
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasCoproduct.{w', v, u} f
inst_2 : HasCoproduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
simp :
  Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)))
        (Functor.map (Discrete.functor (f ∘ (⇑ε : (a : β) → γ))) ((Discrete.equivalence ε).unit.app { as := b }))
        (colimit.ι (Discrete.functor f)
          { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) }) :
      f ((ε : (a : β) → γ) b) ⟶ colimit.{w', w', v, u} (Discrete.functor f))
    (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
⊢ Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))) (ι (f ∘ (⇑ε : (a : β) → γ)) b)
        (Iso.hom
          (HasColimit.isoOfEquivalence (Discrete.equivalence ε)
            (Discrete.natIso fun (x : Discrete β) ↦ Iso.refl (f ((ε : (a : β) → γ) x.as))))) :
      f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)

Tactic:
simp only [HasColimit.ι_isoOfEquivalence_hom, Functor.id_obj, Discrete.functor_obj,
    Function.comp_apply, Discrete.equivalence_functor, Discrete.equivalence_inverse,
    Functor.comp_obj, Discrete.natIso_inv_app, Iso.refl_inv, Category.id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Discrete.functor_obj, CategoryTheory.Discrete.equivalence_functor, CategoryTheory.Iso.refl_inv, CategoryTheory.Functor.id_obj, CategoryTheory.Limits.HasColimit.ι_isoOfEquivalence_hom, Function.comp_apply, CategoryTheory.Discrete.equivalence_inverse, CategoryTheory.Discrete.natIso_inv_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasCoproduct.{w', v, u} f
inst_2 : HasCoproduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w', v, w', u} (Discrete.functor f)
        { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) : Discrete γ } ⟶
      colimit.{w', w', v, u} (Discrete.functor f))
    (Functor.map (Discrete.functor f) (Discrete.eqToHom' ⋯) ≫
      colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) b })
    (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) })

Tactic:
have h := colimit.w (Discrete.functor f) (Discrete.eqToHom' (ε.apply_symm_apply (ε b)))
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasCoproduct.{w', v, u} f
inst_2 : HasCoproduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
h :
  Eq.{v + 1} (α :=
    f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)) ⟶
      colimit.{w', w', v, u} (Discrete.functor f))
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) b)) (Functor.map (Discrete.functor f) (Discrete.eqToHom' ⋯))
        (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) b }) :
      f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)) ⟶
        colimit.{w', w', v, u} (Discrete.functor f))
    (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) } :
      Functor.obj.{w', v, w', u} (Discrete.functor f)
          { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) : Discrete γ } ⟶
        colimit.{w', w', v, u} (Discrete.functor f))
erw :
  Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) b)) (eqToHom ⋯)
        (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) b }) :
      f ((ε : (a : β) → γ) b) ⟶ colimit.{w', w', v, u} (Discrete.functor f))
    (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
p : { as := b : Discrete β } = { as := (ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) }
⊢ Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)))
        (Functor.map (Discrete.functor (f ∘ (⇑ε : (a : β) → γ))) ((Discrete.equivalence ε).unit.app { as := b }))
        (colimit.ι (Discrete.functor f)
          { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) }) :
      f ((ε : (a : β) → γ) b) ⟶ colimit.{w', w', v, u} (Discrete.functor f))
    (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)

Tactic:
erw [← h, eqToHom_map, eqToHom_map, eqToHom_trans_assoc]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.eqToHom_trans_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasCoproduct.{w', v, u} f
inst_2 : HasCoproduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
h :
  Eq.{v + 1} (α :=
    f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)) ⟶
      colimit.{w', w', v, u} (Discrete.functor f))
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) b)) (Functor.map (Discrete.functor f) (Discrete.eqToHom' ⋯))
        (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) b }) :
      f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)) ⟶
        colimit.{w', w', v, u} (Discrete.functor f))
    (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) } :
      Functor.obj.{w', v, w', u} (Discrete.functor f)
          { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) : Discrete γ } ⟶
        colimit.{w', w', v, u} (Discrete.functor f))
⊢ Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) b)) (eqToHom ⋯)
        (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) b }) :
      f ((ε : (a : β) → γ) b) ⟶ colimit.{w', w', v, u} (Discrete.functor f))
    (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) 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
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasCoproduct.{w', v, u} f
inst_2 : HasCoproduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
h :
  Eq.{v + 1} (α :=
    f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)) ⟶
      colimit.{w', w', v, u} (Discrete.functor f))
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) b)) (Functor.map (Discrete.functor f) (Discrete.eqToHom' ⋯))
        (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) b }) :
      f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)) ⟶
        colimit.{w', w', v, u} (Discrete.functor f))
    (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) } :
      Functor.obj.{w', v, w', u} (Discrete.functor f)
          { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) : Discrete γ } ⟶
        colimit.{w', w', v, u} (Discrete.functor f))
⊢ Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) b)) (eqToHom ⋯)
        (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) b }) :
      f ((ε : (a : β) → γ) b) ⟶ colimit.{w', w', v, u} (Discrete.functor f))
    (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) 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
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasCoproduct.{w', v, u} f
inst_2 : HasCoproduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
h :
  Eq.{v + 1} (α :=
    f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)) ⟶
      colimit.{w', w', v, u} (Discrete.functor f))
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) b)) (Functor.map (Discrete.functor f) (Discrete.eqToHom' ⋯))
        (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) b }) :
      f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)) ⟶
        colimit.{w', w', v, u} (Discrete.functor f))
    (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) } :
      Functor.obj.{w', v, w', u} (Discrete.functor f)
          { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) : Discrete γ } ⟶
        colimit.{w', w', v, u} (Discrete.functor f))
⊢ { as := b : Discrete β } = { as := (ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) }

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasCoproduct.{w', v, u} f
inst_2 : HasCoproduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
h :
  Eq.{v + 1} (α :=
    f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)) ⟶
      colimit.{w', w', v, u} (Discrete.functor f))
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) b)) (Functor.map (Discrete.functor f) (Discrete.eqToHom' ⋯))
        (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) b }) :
      f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)) ⟶
        colimit.{w', w', v, u} (Discrete.functor f))
    (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) } :
      Functor.obj.{w', v, w', u} (Discrete.functor f)
          { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) : Discrete γ } ⟶
        colimit.{w', w', v, u} (Discrete.functor f))
⊢ { as := b : Discrete β } = { as := (ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) }

Tactic:
{ simp }
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasCoproduct.{w', v, u} f
inst_2 : HasCoproduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
⊢ Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)))
    (CategoryStruct.comp (Y := sigmaObj.{w', v, u} f) (ι f ((ε : (a : β) → γ) b)) (Iso.inv (reindex ε f)))
    (ι (f ∘ (⇑ε : (a : β) → γ)) b)

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v, u₂, u} J C
inst_2 : HasLimit F
inst_3 : HasProduct.{u₂, v, u} F.obj
Z : C
x x_1 : Z ⟶ limit F
h : Eq (α := Z ⟶ piObj.{u₂, v, u} F.obj) (x ≫ Pi.lift (limit.π F)) (x_1 ≫ Pi.lift (limit.π F))
⊢ x = x_1

Tactic:
limit.hom_ext fun j => ?_

Premises used: CategoryTheory.Limits.limit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v, u₂, u} J C
inst_2 : HasLimit F
inst_3 : HasProduct.{u₂, v, u} F.obj
Z : C
x x_1 : Z ⟶ limit F
h : Eq (α := Z ⟶ piObj.{u₂, v, u} F.obj) (x ≫ Pi.lift (limit.π F)) (x_1 ≫ Pi.lift (limit.π F))
refine : ∀ (j : J), x ≫ limit.π F j = x_1 ≫ limit.π F j
⊢ x = x_1

Tactic:
refine limit.hom_ext fun j => ?_

Premises used: CategoryTheory.Limits.limit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v, u₂, u} J C
inst_2 : HasLimit F
inst_3 : HasProduct.{u₂, v, u} F.obj
Z : C
x x_1 : Z ⟶ limit F
h : Eq (α := Z ⟶ piObj.{u₂, v, u} F.obj) (x ≫ Pi.lift (limit.π F)) (x_1 ≫ Pi.lift (limit.π F))
j : J
⊢ x ≫ limit.π F j = x_1 ≫ limit.π F j

Tactic:
simpa using h =≫ Pi.π _ j

Premises used: CategoryTheory.Limits.Pi.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v, u₂, u} J C
inst_2 : HasColimit F
inst_3 : HasCoproduct.{u₂, v, u} F.obj
Z : C
x x_1 : colimit F ⟶ Z
h : Eq (α := sigmaObj.{u₂, v, u} F.obj ⟶ Z) (Sigma.desc (colimit.ι F) ≫ x) (Sigma.desc (colimit.ι F) ≫ x_1)
⊢ x = x_1

Tactic:
colimit.hom_ext fun j => ?_

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v, u₂, u} J C
inst_2 : HasColimit F
inst_3 : HasCoproduct.{u₂, v, u} F.obj
Z : C
x x_1 : colimit F ⟶ Z
h : Eq (α := sigmaObj.{u₂, v, u} F.obj ⟶ Z) (Sigma.desc (colimit.ι F) ≫ x) (Sigma.desc (colimit.ι F) ≫ x_1)
refine : ∀ (j : J), colimit.ι F j ≫ x = colimit.ι F j ≫ x_1
⊢ x = x_1

Tactic:
refine colimit.hom_ext fun j => ?_

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v, u₂, u} J C
inst_2 : HasColimit F
inst_3 : HasCoproduct.{u₂, v, u} F.obj
Z : C
x x_1 : colimit F ⟶ Z
h : Eq (α := sigmaObj.{u₂, v, u} F.obj ⟶ Z) (Sigma.desc (colimit.ι F) ≫ x) (Sigma.desc (colimit.ι F) ≫ x_1)
j : J
⊢ colimit.ι F j ≫ x = colimit.ι F j ≫ x_1

Tactic:
simpa using Sigma.ι _ j ≫= h

Premises used: CategoryTheory.Limits.Sigma.ι