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 g : α → C
inst_1 : HasProduct.{w₂, v, u} f
inst_2 : HasProduct.{w₂, v, u} g
p : (b : α) → f b ⟶ g b
⊢ Eq (α := piObj.{w₂, v, u} f ⟶ piObj.{w₂, v, u} g) (map' id p) (map p)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.NatTrans.vcomp, CategoryTheory.Limits.Fan.mk, CategoryTheory.Limits.Pi.map', CategoryTheory.Discrete.natTrans, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.map, CategoryTheory.Limits.limMap, CategoryTheory.Limits.limit.lift, rfl, CategoryTheory.Limits.Pi.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst_1 : HasProduct.{w₂, v, u} f
inst_2 : HasProduct.{w, v, u} g
inst_3 : HasProduct.{w₃, v, u} h
p : β → α
p' : γ → β
q : (b : β) → f (p b) ⟶ g b
q' : (c : γ) → g (p' c) ⟶ h c
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' p q) (map' p' q')) (π h b))
      (CategoryStruct.comp (Y := piObj.{w₃, v, u} h) (map' (p ∘ p') fun (c : γ) ↦ q (p' c) ≫ q' c) (π h b))
⊢ Eq (α := piObj.{w₂, v, u} f ⟶ piObj.{w₃, v, u} h)
    (CategoryStruct.comp (Y := piObj.{w, v, u} g) (map' p q) (map' p' q')) (map' (p ∘ p') fun (c : γ) ↦ q (p' c) ≫ q' c)

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
g : β → C
h : γ → C
inst_1 : HasProduct.{w₂, v, u} f
inst_2 : HasProduct.{w, v, u} g
inst_3 : HasProduct.{w₃, v, u} h
p : β → α
p' : γ → β
q : (b : β) → f (p b) ⟶ g b
q' : (c : γ) → g (p' c) ⟶ h c
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' p q) (map' p' q')) (π h b))
    (CategoryStruct.comp (Y := piObj.{w₃, v, u} h) (map' (p ∘ p') fun (c : γ) ↦ q (p' c) ≫ q' c) (π h b))

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

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

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

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

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
f g : β → C
inst_1 : HasProductsOfShape.{w, u, v} β C
p : (b : β) → f b ≅ g b
b : β
⊢ Eq (α := piObj.{w, v, u} f ⟶ g b)
    (CategoryStruct.comp (Y := piObj.{w, v, u} g) (Iso.hom (mapIso p) : piObj.{w, v, u} f ⟶ piObj.{w, v, u} g)
        (π g b : piObj.{w, v, u} g ⟶ g b) :
      piObj.{w, v, u} f ⟶ g b)
    (π f b ≫ (p b).hom : piObj.{w, v, u} f ⟶ g b)

Tactic:
limMap_π _ _

Premises used: CategoryTheory.Limits.limMap_π, CategoryTheory.Limits.IsLimit.map, CategoryTheory.Limits.limMap
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
f g : β → C
inst_1 : HasProductsOfShape.{w, u, v} β C
p : (b : β) → f b ≅ g b
b : β
⊢ Eq (α := piObj.{w, v, u} g ⟶ f b)
    (CategoryStruct.comp (Y := piObj.{w, v, u} f) (Iso.inv (mapIso p) : piObj.{w, v, u} g ⟶ piObj.{w, v, u} f)
        (π f b : piObj.{w, v, u} f ⟶ f b) :
      piObj.{w, v, u} g ⟶ f b)
    (π g b ≫ (p b).inv : piObj.{w, v, u} g ⟶ f b)

Tactic:
limMap_π _ _

Premises used: CategoryTheory.Limits.limMap_π, CategoryTheory.Limits.IsLimit.map, CategoryTheory.Limits.limMap
-- 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 : HasProductsOfShape.{w, u, v} β C
p : (b : β) → f b ⟶ g b
inst_2 : ∀ (b : β), IsIso (p b)
⊢ IsIso (X := piObj.{w, v, u} f) (Y := piObj.{w, v, u} g) (map p)

Tactic:
inferInstanceAs (IsIso (Pi.mapIso (fun b ↦ asIso (p b))).hom)

Premises used: _private.0.CategoryTheory.Limits.Pi.map_isIso._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasProduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
s : Cone X
⊢ ∀ (j : Discrete α), (Pi.lift fun (j : α) ↦ s.π.app { as := j }) ≫ (Pi.cone X).π.app j = s.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasProduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
s : Cone X
m : s.pt ⟶ (Pi.cone X).pt
hm : ∀ (j : Discrete α), m ≫ (Pi.cone X).π.app j = s.π.app j
dsimp : m = Pi.lift fun (j : α) ↦ s.π.app { as := j }
⊢ m = Pi.lift fun (j : α) ↦ s.π.app { 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
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasProduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
s : Cone X
m : s.pt ⟶ (Pi.cone X).pt
hm : ∀ (j : Discrete α), m ≫ (Pi.cone X).π.app j = s.π.app j
h :
  ∀ (b : α),
    m ≫ Pi.π (fun (j : α) ↦ X.obj { as := j : Discrete α }) b =
      CategoryStruct.comp (Y := piObj.{w₂, v, u} fun (j : α) ↦ X.obj { as := j })
        (Pi.lift fun (j : α) ↦ s.π.app { as := j }) (Pi.π (fun (j : α) ↦ X.obj { as := j }) b)
⊢ m = Pi.lift fun (j : α) ↦ s.π.app { as := j }

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasProduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
s : Cone X
m : s.pt ⟶ (Pi.cone X).pt
hm : ∀ (j : Discrete α), m ≫ (Pi.cone X).π.app j = s.π.app j
b : α
h : m ≫ Pi.π (fun (j : α) ↦ X.obj { as := j : Discrete α }) b = s.π.app { as := b }
⊢ m ≫ Pi.π (fun (j : α) ↦ X.obj { as := j : Discrete α }) b =
    CategoryStruct.comp (Y := piObj.{w₂, v, u} fun (j : α) ↦ X.obj { as := j })
      (Pi.lift fun (j : α) ↦ s.π.app { as := j }) (Pi.π (fun (j : α) ↦ X.obj { as := j }) b)

Tactic:
simp only [limit.lift_π, Fan.mk_pt, Fan.mk_π_app]

Premises used: CategoryTheory.Limits.Fan.mk_pt, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasProduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
s : Cone X
m : s.pt ⟶ (Pi.cone X).pt
hm : ∀ (j : Discrete α), m ≫ (Pi.cone X).π.app j = s.π.app j
b : α
⊢ m ≫ Pi.π (fun (j : α) ↦ X.obj { as := j : Discrete α }) b = s.π.app { as := b }

Tactic:
apply hm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasProduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
inst_2 : HasLimit X
j : α
⊢ Eq (α := limit X ⟶ X.obj { as := j })
    (CategoryStruct.comp (Y := piObj.{w₂, v, u} fun (j : α) ↦ X.obj { as := j }) (Iso.inv (isoLimit X))
      (π (fun (j : α) ↦ X.obj { as := j }) j))
    (limit.π X { as := j })

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ _

Premises used: CategoryTheory.Limits.limit.π, Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.Discrete.functor, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasProduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
inst_2 : HasLimit X
j : α
⊢ Eq (α := (piObj.{w₂, v, u} fun (j : α) ↦ X.obj { as := j }) ⟶ X.obj { as := j : Discrete α })
    (CategoryStruct.comp (Y := limit X) (Iso.hom (isoLimit X)) (limit.π X { as := j }))
    (π (fun (j : α) ↦ X.obj { as := j }) j)

Tactic:
IsLimit.conePointUniqueUpToIso_hom_comp _ _ _

Premises used: CategoryTheory.Limits.limit.π, Eq.mpr, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.eqToHom, CategoryTheory.Discrete.functor, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
f g : β → C
inst_1 : HasCoproduct.{w, v, u} f
inst_2 : HasCoproduct.{w, v, u} g
p : (b : β) → f b ⟶ g b
b : β
⊢ Eq (α := f b ⟶ sigmaObj.{w, v, u} g) (CategoryStruct.comp (Y := sigmaObj.{w, v, u} f) (ι f b) (map p)) (p b ≫ ι g b)

Tactic:
simp [Sigma.map]

Premises used: CategoryTheory.Limits.Sigma.map
-- 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
h :
  ∀ (b : α),
    CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b) (map fun (a : α) ↦ 𝟙 (f a)) =
      ι f b ≫ 𝟙 (sigmaObj.{w₂, v, u} f)
⊢ (map fun (a : α) ↦ 𝟙 (f a)) = 𝟙 (sigmaObj.{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 : HasCoproduct.{w₂, v, u} f
b : α
⊢ CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b) (map fun (a : α) ↦ 𝟙 (f a)) =
    ι 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 g h : α → C
inst_1 : HasCoproduct.{w₂, v, u} f
inst_2 : HasCoproduct.{w₂, v, u} g
inst_3 : HasCoproduct.{w₂, v, u} h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
h₁ :
  ∀ (b : α),
    Eq (α := f b ⟶ sigmaObj.{w₂, v, u} h)
      (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b)
        (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} g) (map q) (map q')))
      (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b) (map fun (a : α) ↦ q a ≫ q' a))
⊢ Eq (α := sigmaObj.{w₂, v, u} f ⟶ sigmaObj.{w₂, v, u} h)
    (CategoryStruct.comp (Y := sigmaObj.{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 : HasCoproduct.{w₂, v, u} f
inst_2 : HasCoproduct.{w₂, v, u} g
inst_3 : HasCoproduct.{w₂, v, u} h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
b : α
⊢ Eq (α := f b ⟶ sigmaObj.{w₂, v, u} h)
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b)
      (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} g) (map q) (map q')))
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b) (map fun (a : α) ↦ q a ≫ q' a))

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 : HasCoproduct.{w, v, u} f
inst_2 : HasCoproduct.{w, v, u} g
p : (b : β) → f b ⟶ g b
inst_3 : ∀ (i : β), Epi (p i)
dsimp : ∀ (j : Discrete β), Epi (X := f j.as) (p j.as)
⊢ ∀ (j : Discrete β),
    Epi.{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 : HasCoproduct.{w, v, u} f
inst_2 : HasCoproduct.{w, v, u} g
p : (b : β) → f b ⟶ g b
inst_3 : ∀ (i : β), Epi (p i)
⊢ ∀ (j : Discrete β), Epi (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 : HasCoproduct.{w₂, v, u} f
inst_2 : HasCoproduct.{w, v, u} g
p : α → β
q : (a : α) → f a ⟶ g (p a)
a : α
⊢ Eq (α := f a ⟶ sigmaObj.{w, v, u} g) (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f a) (map' p q))
    (q a ≫ ι g (p a))

Tactic:
colimit.ι_desc _ _

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.Sigma.map'
-- 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
h :
  ∀ (b : α),
    CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b) (map' id fun (a : α) ↦ 𝟙 (f a)) =
      ι f b ≫ 𝟙 (sigmaObj.{w₂, v, u} f)
⊢ (map' id fun (a : α) ↦ 𝟙 (f a)) = 𝟙 (sigmaObj.{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 : HasCoproduct.{w₂, v, u} f
b : α
⊢ CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b) (map' id fun (a : α) ↦ 𝟙 (f a)) =
    ι 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 g : α → C
inst_1 : HasCoproduct.{w₂, v, u} f
inst_2 : HasCoproduct.{w₂, v, u} g
p : (b : α) → f b ⟶ g b
⊢ Eq (α := sigmaObj.{w₂, v, u} f ⟶ sigmaObj.{w₂, v, u} g) (map' id p) (map p)

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.natTrans, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.colimMap, CategoryTheory.Limits.Sigma.map', CategoryTheory.Limits.Sigma.map, CategoryTheory.Limits.Cofan.mk, CategoryTheory.Limits.IsColimit.map, rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst_1 : HasCoproduct.{w₂, v, u} f
inst_2 : HasCoproduct.{w, v, u} g
inst_3 : HasCoproduct.{w₃, v, u} h
p : α → β
p' : β → γ
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h (p' b)
h₁ :
  ∀ (b : α),
    Eq (α := f b ⟶ sigmaObj.{w₃, v, u} h)
      (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b)
        (CategoryStruct.comp (Y := sigmaObj.{w, v, u} g) (map' p q) (map' p' q')))
      (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b) (map' (p' ∘ p) fun (a : α) ↦ q a ≫ q' (p a)))
⊢ Eq (α := sigmaObj.{w₂, v, u} f ⟶ sigmaObj.{w₃, v, u} h)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} g) (map' p q) (map' p' q'))
    (map' (p' ∘ p) fun (a : α) ↦ q a ≫ q' (p a))

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
g : β → C
h : γ → C
inst_1 : HasCoproduct.{w₂, v, u} f
inst_2 : HasCoproduct.{w, v, u} g
inst_3 : HasCoproduct.{w₃, v, u} h
p : α → β
p' : β → γ
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h (p' b)
b : α
⊢ Eq (α := f b ⟶ sigmaObj.{w₃, v, u} h)
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b)
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} g) (map' p q) (map' p' q')))
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b) (map' (p' ∘ p) fun (a : α) ↦ q a ≫ q' (p a)))

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

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

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

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

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
f g : β → C
inst_1 : HasCoproductsOfShape.{w, u, v} β C
p : (b : β) → f b ≅ g b
b : β
⊢ Eq (α := f b ⟶ sigmaObj.{w, v, u} g)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} f) (ι f b : f b ⟶ sigmaObj.{w, v, u} f)
        (Iso.hom (mapIso p) : sigmaObj.{w, v, u} f ⟶ sigmaObj.{w, v, u} g) :
      f b ⟶ sigmaObj.{w, v, u} g)
    ((p b).hom ≫ ι g b : f b ⟶ sigmaObj.{w, v, u} g)

Tactic:
ι_colimMap _ _

Premises used: CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.colimMap, CategoryTheory.Limits.IsColimit.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
f g : β → C
inst_1 : HasCoproductsOfShape.{w, u, v} β C
p : (b : β) → f b ≅ g b
b : β
⊢ Eq (α := g b ⟶ sigmaObj.{w, v, u} f)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} g) (ι g b : g b ⟶ sigmaObj.{w, v, u} g)
        (Iso.inv (mapIso p) : sigmaObj.{w, v, u} g ⟶ sigmaObj.{w, v, u} f) :
      g b ⟶ sigmaObj.{w, v, u} f)
    ((p b).inv ≫ ι f b : g b ⟶ sigmaObj.{w, v, u} f)

Tactic:
ι_colimMap _ _

Premises used: CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.colimMap, CategoryTheory.Limits.IsColimit.map
-- 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 : HasCoproductsOfShape.{w, u, v} β C
p : (b : β) → f b ⟶ g b
inst_2 : ∀ (b : β), IsIso (p b)
⊢ IsIso (X := sigmaObj.{w, v, u} f) (Y := sigmaObj.{w, v, u} g) (map p)

Tactic:
inferInstanceAs (IsIso (Sigma.mapIso (fun b ↦ asIso (p b))).hom)

Premises used: _private.0.CategoryTheory.Limits.Sigma.map_isIso._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasCoproduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
s : Cocone X
⊢ ∀ (j : Discrete α), ((Sigma.cocone X).ι.app j ≫ Sigma.desc fun (j : α) ↦ s.ι.app { as := j }) = s.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasCoproduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
s : Cocone X
m : (Sigma.cocone X).pt ⟶ s.pt
hm : ∀ (j : Discrete α), (Sigma.cocone X).ι.app j ≫ m = s.ι.app j
dsimp : m = Sigma.desc fun (j : α) ↦ s.ι.app { as := j }
⊢ m = Sigma.desc fun (j : α) ↦ s.ι.app { 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
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasCoproduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
s : Cocone X
m : (Sigma.cocone X).pt ⟶ s.pt
hm : ∀ (j : Discrete α), (Sigma.cocone X).ι.app j ≫ m = s.ι.app j
h :
  ∀ (b : α),
    Sigma.ι.{w₂, v, u} (C := C) (fun (j : α) ↦ X.obj { as := j : Discrete α }) b ≫ m =
      CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} fun (j : α) ↦ X.obj { as := j })
        (Sigma.ι.{w₂, v, u} (C := C) (fun (j : α) ↦ X.obj { as := j }) b) (Sigma.desc fun (j : α) ↦ s.ι.app { as := j })
⊢ m = Sigma.desc fun (j : α) ↦ s.ι.app { as := j }

Tactic:
ext