awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst_2 : HasProduct.{u_1, v, u} X₁] [inst_3 : HasProduct.{u_1, v, u} X₂]
    (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (X := piObj.{u_1, v, u} X₁) (Y := piObj.{u_1, v, u} X₂) (Limits.Pi.map f)
X₁ X₂ : Functor.{u_1, v, u_1, u} (Discrete J) C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), α ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
φ : (j : J) → X₁.obj { as := j : Discrete J } ⟶ X₂.obj { as := j } := fun (j : J) ↦ f.app { as := j }
this_1 : HasLimit X₁
this_2 : HasLimit X₂
this_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₁.obj { as := j }
this : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₂.obj { as := j }
hf' :
  W (X := piObj.{u_1, v, u} fun (j : J) ↦ X₁.obj { as := j }) (Y := piObj.{u_1, v, u} fun (j : J) ↦ X₂.obj { as := j })
    (Limits.Pi.map φ)
j : J
⊢ (Iso.hom
          (Iso.trans (Y := (limit.cone X₁).pt) (hc₁.conePointUniqueUpToIso (limit.isLimit X₁))
            (Iso.symm (Pi.isoLimit X₁))) ≫
        (Arrow.mk (X := piObj.{u_1, v, u} fun (j : J) ↦ X₁.obj { as := j : Discrete J }) (Y :=
            piObj.{u_1, v, u} fun (j : J) ↦ X₂.obj { as := j : Discrete J }) (Limits.Pi.map φ)).hom) ≫
      limit.π (Discrete.functor fun (j : J) ↦ X₂.obj { as := j : Discrete J }) { as := j : Discrete J } =
    CategoryStruct.comp (Y :=
      limit.{u_1, u_1, v, u} (J := Discrete J) (Discrete.functor fun (j : J) ↦ X₂.obj { as := j }))
      ((Arrow.mk α).hom ≫
        Iso.hom
          (Iso.trans (Y := (limit.cone X₂).pt) (hc₂.conePointUniqueUpToIso (limit.isLimit X₂))
            (Iso.symm (Pi.isoLimit X₂))))
      (limit.π (Discrete.functor fun (j : J) ↦ X₂.obj { as := j }) { as := j })

Tactic:
simp [φ, hα]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst_2 : HasCoproduct.{u_1, v, u} X₁] [inst_3 : HasCoproduct.{u_1, v, u} X₂]
    (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (X := sigmaObj.{u_1, v, u} X₁) (Y := sigmaObj.{u_1, v, u} X₂) (Limits.Sigma.map f)
X₁ X₂ : Functor.{u_1, v, u_1, u} (Discrete J) C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
let : W α
⊢ W α

Tactic:
let φ := fun j => f.app (Discrete.mk j)
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst_2 : HasCoproduct.{u_1, v, u} X₁] [inst_3 : HasCoproduct.{u_1, v, u} X₂]
    (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (X := sigmaObj.{u_1, v, u} X₁) (Y := sigmaObj.{u_1, v, u} X₂) (Limits.Sigma.map f)
X₁ X₂ : Functor.{u_1, v, u_1, u} (Discrete J) C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j : Discrete J } ⟶ X₂.obj { as := j } := fun (j : J) ↦ f.app { as := j }
⊢ HasColimit X₁

Tactic:
have : HasColimit X₁ := ⟨c₁, hc₁⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst_2 : HasCoproduct.{u_1, v, u} X₁] [inst_3 : HasCoproduct.{u_1, v, u} X₂]
    (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (X := sigmaObj.{u_1, v, u} X₁) (Y := sigmaObj.{u_1, v, u} X₂) (Limits.Sigma.map f)
X₁ X₂ : Functor.{u_1, v, u_1, u} (Discrete J) C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j : Discrete J } ⟶ X₂.obj { as := j } := fun (j : J) ↦ f.app { as := j }
this : HasColimit X₁
⊢ HasColimit X₂

Tactic:
have : HasColimit X₂ := ⟨c₂, hc₂⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst_2 : HasCoproduct.{u_1, v, u} X₁] [inst_3 : HasCoproduct.{u_1, v, u} X₂]
    (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (X := sigmaObj.{u_1, v, u} X₁) (Y := sigmaObj.{u_1, v, u} X₂) (Limits.Sigma.map f)
X₁ X₂ : Functor.{u_1, v, u_1, u} (Discrete J) C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j : Discrete J } ⟶ X₂.obj { as := j } := fun (j : J) ↦ f.app { as := j }
this_1 : HasColimit X₁
this : HasColimit X₂
⊢ HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₁.obj { as := j }

Tactic:
have : HasCoproduct fun j ↦ X₁.obj (Discrete.mk j) :=
      hasColimit_of_iso (Discrete.natIso (fun j ↦ Iso.refl (X₁.obj j)))
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst_2 : HasCoproduct.{u_1, v, u} X₁] [inst_3 : HasCoproduct.{u_1, v, u} X₂]
    (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (X := sigmaObj.{u_1, v, u} X₁) (Y := sigmaObj.{u_1, v, u} X₂) (Limits.Sigma.map f)
X₁ X₂ : Functor.{u_1, v, u_1, u} (Discrete J) C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j : Discrete J } ⟶ X₂.obj { as := j } := fun (j : J) ↦ f.app { as := j }
this_1 : HasColimit X₁
this_2 : HasColimit X₂
this : HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₁.obj { as := j }
⊢ HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₂.obj { as := j }

Tactic:
have : HasCoproduct fun j ↦ X₂.obj (Discrete.mk j) :=
      hasColimit_of_iso (Discrete.natIso (fun j ↦ Iso.refl (X₂.obj j)))
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst_2 : HasCoproduct.{u_1, v, u} X₁] [inst_3 : HasCoproduct.{u_1, v, u} X₂]
    (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (X := sigmaObj.{u_1, v, u} X₁) (Y := sigmaObj.{u_1, v, u} X₂) (Limits.Sigma.map f)
X₁ X₂ : Functor.{u_1, v, u_1, u} (Discrete J) C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j : Discrete J } ⟶ X₂.obj { as := j } := fun (j : J) ↦ f.app { as := j }
this_1 : HasColimit X₁
this_2 : HasColimit X₂
this_3 : HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₁.obj { as := j }
this : HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₂.obj { as := j }
⊢ W (X := sigmaObj.{u_1, v, u} fun (j : J) ↦ X₁.obj { as := j }) (Y :=
    sigmaObj.{u_1, v, u} fun (j : J) ↦ X₂.obj { as := j }) (Limits.Sigma.map φ)

Tactic:
have hf' := hW _ _ φ (fun j => hf (Discrete.mk j))
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst_2 : HasCoproduct.{u_1, v, u} X₁] [inst_3 : HasCoproduct.{u_1, v, u} X₂]
    (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (X := sigmaObj.{u_1, v, u} X₁) (Y := sigmaObj.{u_1, v, u} X₂) (Limits.Sigma.map f)
X₁ X₂ : Functor.{u_1, v, u_1, u} (Discrete J) C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j : Discrete J } ⟶ X₂.obj { as := j } := fun (j : J) ↦ f.app { as := j }
this_1 : HasColimit X₁
this_2 : HasColimit X₂
this_3 : HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₁.obj { as := j }
this : HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₂.obj { as := j }
hf' :
  W (X := sigmaObj.{u_1, v, u} fun (j : J) ↦ X₁.obj { as := j }) (Y :=
    sigmaObj.{u_1, v, u} fun (j : J) ↦ X₂.obj { as := j }) (Limits.Sigma.map φ)
⊢ W α

Tactic:
(W.arrow_mk_iso_iff ?_).1 hf'

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst_2 : HasCoproduct.{u_1, v, u} X₁] [inst_3 : HasCoproduct.{u_1, v, u} X₂]
    (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (X := sigmaObj.{u_1, v, u} X₁) (Y := sigmaObj.{u_1, v, u} X₂) (Limits.Sigma.map f)
X₁ X₂ : Functor.{u_1, v, u_1, u} (Discrete J) C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j : Discrete J } ⟶ X₂.obj { as := j } := fun (j : J) ↦ f.app { as := j }
this_1 : HasColimit X₁
this_2 : HasColimit X₂
this_3 : HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₁.obj { as := j }
this : HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₂.obj { as := j }
hf' :
  W (X := sigmaObj.{u_1, v, u} fun (j : J) ↦ X₁.obj { as := j }) (Y :=
    sigmaObj.{u_1, v, u} fun (j : J) ↦ X₂.obj { as := j }) (Limits.Sigma.map φ)
refine :
  Arrow.mk (X := sigmaObj.{u_1, v, u} fun (j : J) ↦ X₁.obj { as := j : Discrete J }) (Y :=
      sigmaObj.{u_1, v, u} fun (j : J) ↦ X₂.obj { as := j : Discrete J }) (Limits.Sigma.map φ) ≅
    Arrow.mk α
⊢ W α

Tactic:
refine (W.arrow_mk_iso_iff ?_).1 hf'

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst_2 : HasCoproduct.{u_1, v, u} X₁] [inst_3 : HasCoproduct.{u_1, v, u} X₂]
    (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (X := sigmaObj.{u_1, v, u} X₁) (Y := sigmaObj.{u_1, v, u} X₂) (Limits.Sigma.map f)
X₁ X₂ : Functor.{u_1, v, u_1, u} (Discrete J) C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j : Discrete J } ⟶ X₂.obj { as := j } := fun (j : J) ↦ f.app { as := j }
this_1 : HasColimit X₁
this_2 : HasColimit X₂
this_3 : HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₁.obj { as := j }
this : HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₂.obj { as := j }
hf' :
  W (X := sigmaObj.{u_1, v, u} fun (j : J) ↦ X₁.obj { as := j }) (Y :=
    sigmaObj.{u_1, v, u} fun (j : J) ↦ X₂.obj { as := j }) (Limits.Sigma.map φ)
refine :
  Iso.hom
        (Iso.trans (Y := colimit X₁) (Sigma.isoColimit X₁)
          (IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₁) hc₁)) ≫
      (Arrow.mk α).hom =
    (Arrow.mk (X := sigmaObj.{u_1, v, u} fun (j : J) ↦ X₁.obj { as := j : Discrete J }) (Y :=
          sigmaObj.{u_1, v, u} fun (j : J) ↦ X₂.obj { as := j : Discrete J }) (Limits.Sigma.map φ)).hom ≫
      Iso.hom
        (Iso.trans (Y := colimit X₂) (Sigma.isoColimit X₂)
          (IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₂) hc₂))
⊢ Arrow.mk (X := sigmaObj.{u_1, v, u} fun (j : J) ↦ X₁.obj { as := j : Discrete J }) (Y :=
      sigmaObj.{u_1, v, u} fun (j : J) ↦ X₂.obj { as := j : Discrete J }) (Limits.Sigma.map φ) ≅
    Arrow.mk α

Tactic:
refine Arrow.isoMk
      ((Sigma.isoColimit _) ≪≫ IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₁) hc₁)
      ((Sigma.isoColimit _) ≪≫ IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₂) hc₂) ?_

Premises used: CategoryTheory.Iso.trans, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst_2 : HasCoproduct.{u_1, v, u} X₁] [inst_3 : HasCoproduct.{u_1, v, u} X₂]
    (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (X := sigmaObj.{u_1, v, u} X₁) (Y := sigmaObj.{u_1, v, u} X₂) (Limits.Sigma.map f)
X₁ X₂ : Functor.{u_1, v, u_1, u} (Discrete J) C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j : Discrete J } ⟶ X₂.obj { as := j } := fun (j : J) ↦ f.app { as := j }
this_1 : HasColimit X₁
this_2 : HasColimit X₂
this_3 : HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₁.obj { as := j }
this : HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₂.obj { as := j }
hf' :
  W (X := sigmaObj.{u_1, v, u} fun (j : J) ↦ X₁.obj { as := j }) (Y :=
    sigmaObj.{u_1, v, u} fun (j : J) ↦ X₂.obj { as := j }) (Limits.Sigma.map φ)
w :
  ∀ (j : Discrete J),
    CategoryStruct.comp (Y :=
        colimit.{u_1, u_1, v, u} (J := Discrete J) (Discrete.functor fun (j : J) ↦ X₁.obj { as := j : Discrete J }))
        (colimit.ι (Discrete.functor fun (j : J) ↦ X₁.obj { as := j : Discrete J }) j)
        (Iso.hom
            (Iso.trans (Y := colimit X₁) (Sigma.isoColimit X₁)
              (IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₁) hc₁)) ≫
          (Arrow.mk α).hom) =
      colimit.ι (Discrete.functor fun (j : J) ↦ X₁.obj { as := j }) j ≫
        (Arrow.mk (X := sigmaObj.{u_1, v, u} fun (j : J) ↦ X₁.obj { as := j : Discrete J }) (Y :=
              sigmaObj.{u_1, v, u} fun (j : J) ↦ X₂.obj { as := j : Discrete J }) (Limits.Sigma.map φ)).hom ≫
          Iso.hom
            (Iso.trans (Y := colimit X₂) (Sigma.isoColimit X₂)
              (IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₂) hc₂))
⊢ Iso.hom
        (Iso.trans (Y := colimit X₁) (Sigma.isoColimit X₁)
          (IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₁) hc₁)) ≫
      (Arrow.mk α).hom =
    (Arrow.mk (X := sigmaObj.{u_1, v, u} fun (j : J) ↦ X₁.obj { as := j : Discrete J }) (Y :=
          sigmaObj.{u_1, v, u} fun (j : J) ↦ X₂.obj { as := j : Discrete J }) (Limits.Sigma.map φ)).hom ≫
      Iso.hom
        (Iso.trans (Y := colimit X₂) (Sigma.isoColimit X₂)
          (IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₂) hc₂))

Tactic:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst_2 : HasCoproduct.{u_1, v, u} X₁] [inst_3 : HasCoproduct.{u_1, v, u} X₂]
    (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (X := sigmaObj.{u_1, v, u} X₁) (Y := sigmaObj.{u_1, v, u} X₂) (Limits.Sigma.map f)
X₁ X₂ : Functor.{u_1, v, u_1, u} (Discrete J) C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j : Discrete J } ⟶ X₂.obj { as := j } := fun (j : J) ↦ f.app { as := j }
this_1 : HasColimit X₁
this_2 : HasColimit X₂
this_3 : HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₁.obj { as := j }
this : HasCoproduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₂.obj { as := j }
hf' :
  W (X := sigmaObj.{u_1, v, u} fun (j : J) ↦ X₁.obj { as := j }) (Y :=
    sigmaObj.{u_1, v, u} fun (j : J) ↦ X₂.obj { as := j }) (Limits.Sigma.map φ)
j : J
⊢ CategoryStruct.comp (Y :=
      colimit.{u_1, u_1, v, u} (J := Discrete J) (Discrete.functor fun (j : J) ↦ X₁.obj { as := j : Discrete J }))
      (colimit.ι (Discrete.functor fun (j : J) ↦ X₁.obj { as := j : Discrete J }) { as := j : Discrete J })
      (Iso.hom
          (Iso.trans (Y := colimit X₁) (Sigma.isoColimit X₁)
            (IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₁) hc₁)) ≫
        (Arrow.mk α).hom) =
    colimit.ι (Discrete.functor fun (j : J) ↦ X₁.obj { as := j }) { as := j } ≫
      (Arrow.mk (X := sigmaObj.{u_1, v, u} fun (j : J) ↦ X₁.obj { as := j : Discrete J }) (Y :=
            sigmaObj.{u_1, v, u} fun (j : J) ↦ X₂.obj { as := j : Discrete J }) (Limits.Sigma.map φ)).hom ≫
        Iso.hom
          (Iso.trans (Y := colimit X₂) (Sigma.isoColimit X₂)
            (IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₂) hc₂))

Tactic:
simp [φ, hα]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : IsStableUnderCoproductsOfShape.{v, u, u_1} (monomorphisms C) J
X₁ X₂ : J → C
f : (j : J) → X₁ j ⟶ X₂ j
inst_2 : HasCoproduct.{u_1, v, u} X₁
inst_3 : HasCoproduct.{u_1, v, u} X₂
inst_4 : ∀ (j : J), Mono (f j)
x : Discrete J
j : J
dsimp : Mono (f j)
⊢ Mono.{v, u} (C := C) (X := Functor.obj.{u_1, v, u_1, u} (Discrete.functor X₁) { as := j : Discrete J }) (Y :=
    Functor.obj.{u_1, v, u_1, u} (Discrete.functor X₂) { as := j : Discrete J })
    (NatTrans.app (Discrete.natTrans fun (X : Discrete J) ↦ f X.as) { as := j })

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : IsStableUnderCoproductsOfShape.{v, u, u_1} (monomorphisms C) J
X₁ X₂ : J → C
f : (j : J) → X₁ j ⟶ X₂ j
inst_2 : HasCoproduct.{u_1, v, u} X₁
inst_3 : HasCoproduct.{u_1, v, u} X₂
inst_4 : ∀ (j : J), Mono (f j)
x : Discrete J
j : J
⊢ Mono (f j)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
hf : coproducts.{w, v, u} W f
⊢ ∃ (J : Type w), colimitsOfShape.{v, u, w, w} W (Discrete J) f

Tactic:
rw [coproducts_iff] at hf

Premises used: CategoryTheory.MorphismProperty.coproducts_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
hf : ∃ (J : Type w), colimitsOfShape.{v, u, w, w} W (Discrete J) f
obtain : ∀ (J : Type w) (hf : colimitsOfShape.{v, u, w, w} W (Discrete J) f), W f
⊢ W f

Tactic:
obtain ⟨J, hf⟩ := hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
J : Type w
hf : colimitsOfShape.{v, u, w, w} W (Discrete J) f
⊢ W f

Tactic:
colimitsOfShape_le _ hf

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape_le
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
J : Type w
hf : colimitsOfShape.{v, u, w, w} W (Discrete J) f
⊢ W f

Tactic:
exact colimitsOfShape_le _ hf

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape_le
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : IsStableUnderCoproducts.{w, v, u} W
⊢ coproducts.{w, v, u} W = W

Tactic:
le_antisymm W.coproducts_le W.le_coproducts

Premises used: CategoryTheory.MorphismProperty.le_coproducts, CategoryTheory.MorphismProperty.coproducts_le, le_antisymm
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : IsStableUnderCoproducts.{w, v, u} Q
mp : coproducts.{w, v, u} P ≤ Q → P ≤ Q
mpr : P ≤ Q → coproducts.{w, v, u} P ≤ Q
⊢ coproducts.{w, v, u} P ≤ Q ↔ P ≤ Q

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : IsStableUnderCoproducts.{w, v, u} Q
⊢ coproducts.{w, v, u} P ≤ Q → P ≤ Q

Tactic:
le_trans P.le_coproducts

Premises used: CategoryTheory.MorphismProperty.le_coproducts, le_trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : IsStableUnderCoproducts.{w, v, u} Q
⊢ coproducts.{w, v, u} P ≤ Q → P ≤ Q

Tactic:
exact le_trans P.le_coproducts

Premises used: CategoryTheory.MorphismProperty.le_coproducts, le_trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : IsStableUnderCoproducts.{w, v, u} Q
h : P ≤ Q
⊢ coproducts.{w, v, u} P ≤ Q

Tactic:
le_trans (coproducts_monotone h) Q.coproducts_le

Premises used: CategoryTheory.MorphismProperty.coproducts_monotone, CategoryTheory.MorphismProperty.coproducts_le, le_trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : IsStableUnderCoproducts.{w, v, u} Q
h : P ≤ Q
⊢ coproducts.{w, v, u} P ≤ Q

Tactic:
exact le_trans (coproducts_monotone h) Q.coproducts_le

Premises used: CategoryTheory.MorphismProperty.coproducts_monotone, CategoryTheory.MorphismProperty.coproducts_le, le_trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
⊢ P.diagonal f ↔ P (Y := pullback.diagonalObj f) (pullback.diagonal f)

Tactic:
Iff.rfl

Premises used: CategoryTheory.MorphismProperty.diagonal, Iff.rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.RespectsIso
hprecomp : ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P.diagonal f → P.diagonal (e.hom ≫ f)
hpostcomp : ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.diagonal f → P.diagonal (f ≫ e.hom)
⊢ P.diagonal.RespectsIso

Tactic:
apply RespectsIso.mk

Premises used: CategoryTheory.MorphismProperty.RespectsIso.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.RespectsIso
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : P.diagonal f
⊢ (e.hom ≫ f) ≫ 𝟙 Z = e.hom ≫ f

Tactic:
simp