awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (hypothesis)
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
⊢ coproducts.{w, v, u} W₂ f
have hf₁ : ∃ (J : Type w), colimitsOfShape.{v, u, w, w} W₁ (Discrete J) f
Tactic: rw [coproducts_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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
⊢ coproducts.{w, v, u} W₂ f
have obtain : ∀ (J : Type w) (hf : colimitsOfShape.{v, u, w, w} W₁ (Discrete J) f), coproducts.{w, v, u} W₂ f
Tactic: obtain ⟨J, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (hypothesis)
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 }
⊢ W α
have this : HasLimit X₁
Tactic: have : HasLimit X₁ := ⟨c₁, hc₁⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (hypothesis)
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₁
⊢ W α
have this₁ : HasLimit X₂
Tactic: have : HasLimit X₂ := ⟨c₂, hc₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (hypothesis)
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₂
⊢ W α
have this₁ : 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)))
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (hypothesis)
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 }
⊢ W α
have this₁ : 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)))
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (hypothesis)
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 α
have 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 φ)
Tactic: have hf' := hW _ _ φ (fun j => hf (Discrete.mk j))
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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 α
have 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 φ)
Tactic: refine (W.arrow_mk_iso_iff ?_).2 hf'
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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 φ)
⊢ 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 φ)
have 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₂)))
Tactic: refine Arrow.isoMk
      (IsLimit.conePointUniqueUpToIso hc₁ (limit.isLimit X₁) ≪≫ (Pi.isoLimit X₁).symm)
      (IsLimit.conePointUniqueUpToIso hc₂ (limit.isLimit X₂) ≪≫ (Pi.isoLimit _).symm) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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 φ)
⊢ 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₂)))
have 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)
Tactic: apply limit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (hypothesis)
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 }
⊢ W α
have this : HasColimit X₁
Tactic: have : HasColimit X₁ := ⟨c₁, hc₁⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (hypothesis)
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₁
⊢ W α
have this₁ : HasColimit X₂
Tactic: have : HasColimit X₂ := ⟨c₂, hc₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (hypothesis)
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₂
⊢ W α
have this₁ : 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)))
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (hypothesis)
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 }
⊢ W α
have this₁ : 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)))
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (hypothesis)
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 α
have 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 φ)
Tactic: have hf' := hW _ _ φ (fun j => hf (Discrete.mk j))
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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 α
have 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 α
Tactic: refine (W.arrow_mk_iso_iff ?_).1 hf'
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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 φ)
⊢ 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 α
have 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₂))
Tactic: refine Arrow.isoMk
      ((Sigma.isoColimit _) ≪≫ IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₁) hc₁)
      ((Sigma.isoColimit _) ≪≫ IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₂) hc₂) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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 φ)
⊢ 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₂))
have 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₂))
Tactic: apply colimit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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.{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 })
have dsimp : Mono (f j)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (hypothesis)
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
⊢ W f
have hf₁ : ∃ (J : Type w), colimitsOfShape.{v, u, w, w} W (Discrete J) f
Tactic: rw [coproducts_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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
⊢ W f
have obtain : ∀ (J : Type w) (hf : colimitsOfShape.{v, u, w, w} W (Discrete J) f), W f
Tactic: obtain ⟨J, hf⟩ := hf
Cleared hypotheses: hf