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
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (C := Discrete PUnit.{w + 1}) (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁) :=
  coconeOfDiagramInitial h (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
c₂ : Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₂) :=
  coconeOfDiagramInitial h (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
rw :
  Eq (α :=
    Functor.obj.{w, v, w, u} (C := Discrete PUnit.{w + 1}) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
        (⊥_ Discrete PUnit.{w + 1}) ⟶
      Cocone.pt (F := Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
        { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι :
          Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁) })
    (NatTrans.app (Cocone.ι { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι })
        (⊥_ Discrete PUnit.{w + 1}) :
      Functor.obj.{w, v, w, u} (C := Discrete PUnit.{w + 1}) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
          (⊥_ Discrete PUnit.{w + 1}) ⟶
        Functor.obj.{w, v, w, u} (C := Discrete PUnit.{w + 1})
          (Functor.obj (Functor.const (Discrete PUnit.{w + 1}))
            (Cocone.pt (F := Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
              { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι :
                Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C)
                  (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁) }))
          (⊥_ Discrete PUnit.{w + 1}))
    (c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ f)
⊢ Eq (α :=
    Functor.obj.{w, v, w, u} (C := Discrete PUnit.{w + 1}) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
        (⊥_ Discrete PUnit.{w + 1}) ⟶
      Cocone.pt (F := Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
        { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι :
          Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁) })
    (c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫
      hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι })
    (c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ f)

Tactic:
rw [IsColimit.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (C := Discrete PUnit.{w + 1}) (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁) :=
  coconeOfDiagramInitial h (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
c₂ : Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₂) :=
  coconeOfDiagramInitial h (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Eq (α :=
    Functor.obj.{w, v, w, u} (C := Discrete PUnit.{w + 1}) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
        (⊥_ Discrete PUnit.{w + 1}) ⟶
      Cocone.pt (F := Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
        { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι :
          Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁) })
    (NatTrans.app (Cocone.ι { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι })
        (⊥_ Discrete PUnit.{w + 1}) :
      Functor.obj.{w, v, w, u} (C := Discrete PUnit.{w + 1}) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
          (⊥_ Discrete PUnit.{w + 1}) ⟶
        Functor.obj.{w, v, w, u} (C := Discrete PUnit.{w + 1})
          (Functor.obj (Functor.const (Discrete PUnit.{w + 1}))
            (Cocone.pt (F := Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
              { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι :
                Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C)
                  (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁) }))
          (⊥_ Discrete PUnit.{w + 1}))
    (c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ f)

Tactic:
simp [c₁, c₂]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (C := Discrete PUnit.{w + 1}) (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁) :=
  coconeOfDiagramInitial h (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
c₂ : Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₂) :=
  coconeOfDiagramInitial h (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι } = f

Tactic:
have : hc₁.desc (Cocone.mk _ (Discrete.natTrans (fun _ ↦ by exact f) ≫ c₂.ι)) = f :=
    hc₁.hom_ext (fun x ↦ by
      obtain rfl : x = ⊥_ _ := by ext
      rw [IsColimit.fac]
      simp [c₁, c₂])
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (C := Discrete PUnit.{w + 1}) (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁) :=
  coconeOfDiagramInitial h (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
c₂ : Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₂) :=
  coconeOfDiagramInitial h (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
this : hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι } = f
rw :
  colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) (Y := X₂)
    (hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι } :
      c₁.pt ⟶
        Cocone.pt (F := Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
          { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι })
⊢ colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) f

Tactic:
rw [← this]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (C := Discrete PUnit.{w + 1}) (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁) :=
  coconeOfDiagramInitial h (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
c₂ : Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₂) :=
  coconeOfDiagramInitial h (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
this : hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι } = f
⊢ colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) (Y := X₂)
    (hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι } :
      c₁.pt ⟶
        Cocone.pt (F := Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
          { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι })

Tactic:
⟨_, _, _, _, _, hc₂, _, fun _ ↦ hf⟩

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (C := Discrete PUnit.{w + 1}) (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁) :=
  coconeOfDiagramInitial h (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
c₂ : Cocone.{w, v, w, u} (J := Discrete PUnit.{w + 1}) (C := C) (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₂) :=
  coconeOfDiagramInitial h (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
this : hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι } = f
⊢ colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) (Y := X₂)
    (hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι } :
      c₁.pt ⟶
        Cocone.pt (F := Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁)
          { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι })

Tactic:
exact ⟨_, _, _, _, _, hc₂, _, fun _ ↦ hf⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
⊢ W ≤ coproducts.{w, v, u} W

Tactic:
(le_colimitsOfShape_punit.{w} W).trans
    (colimitsOfShape_le_coproducts W PUnit.{w + 1})

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape_le_coproducts, PUnit, LE.le.trans, CategoryTheory.MorphismProperty.le_colimitsOfShape_punit
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
h : W₁ ≤ 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₁ W₂ : MorphismProperty.{v, u} C
h : W₁ ≤ 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), coproducts.{w, v, u} W₂ f
⊢ coproducts.{w, v, u} W₂ f

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

Tactic:
W₂.colimitsOfShape_le_coproducts J _
    (colimitsOfShape_monotone h _ _ hf)

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape_le_coproducts, CategoryTheory.MorphismProperty.colimitsOfShape_monotone
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
J : Type w
hf : colimitsOfShape.{v, u, w, w} W₁ (Discrete J) f
⊢ coproducts.{w, v, u} W₂ f

Tactic:
exact W₂.colimitsOfShape_le_coproducts J _
    (colimitsOfShape_monotone h _ _ hf)

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape_le_coproducts, CategoryTheory.MorphismProperty.colimitsOfShape_monotone
-- 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
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 : 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 }
⊢ HasLimit X₁

Tactic:
have : HasLimit 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 : 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 : HasLimit X₁
⊢ HasLimit X₂

Tactic:
have : HasLimit 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 : 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 : HasLimit X₂
⊢ HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₁.obj { as := j }

Tactic:
have : HasProduct fun j ↦ X₁.obj (Discrete.mk j) :=
      hasLimit_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 : 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 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₁.obj { as := j }
⊢ HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ X₂.obj { as := j }

Tactic:
have : HasProduct fun j ↦ X₂.obj (Discrete.mk j) :=
      hasLimit_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 : 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 }
⊢ 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 φ)

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 : 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 φ)
⊢ W α

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

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- 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 φ)
refine :
  Arrow.mk α ≅
    Arrow.mk (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 φ)
⊢ W α

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

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- 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 φ)
refine :
  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 =
    (Arrow.mk α).hom ≫
      Iso.hom
        (Iso.trans (Y := (limit.cone X₂).pt) (hc₂.conePointUniqueUpToIso (limit.isLimit X₂))
          (Iso.symm (Pi.isoLimit X₂)))
⊢ Arrow.mk α ≅
    Arrow.mk (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 φ)

Tactic:
refine Arrow.isoMk
      (IsLimit.conePointUniqueUpToIso hc₁ (limit.isLimit X₁) ≪≫ (Pi.isoLimit X₁).symm)
      (IsLimit.conePointUniqueUpToIso hc₂ (limit.isLimit X₂) ≪≫ (Pi.isoLimit _).symm) ?_

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 : 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 φ)
w :
  ∀ (j : Discrete 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 }) 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 }) 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 =
    (Arrow.mk α).hom ≫
      Iso.hom
        (Iso.trans (Y := (limit.cone X₂).pt) (hc₂.conePointUniqueUpToIso (limit.isLimit X₂))
          (Iso.symm (Pi.isoLimit X₂)))

Tactic:
apply limit.hom_ext

Premises used: CategoryTheory.Limits.limit.hom_ext