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 : Category.{v_1, u_1} J
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
hφ : ∀ (j : J), h₂.lift { pt := c₁.pt, π := c₁.π ≫ f } ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
⊢ limitsOfShape.{v, u, v_1, u_1} W J (X := c₁.pt)
    (h₂.lift { pt := c₁.pt, π := c₁.π ≫ f } : { pt := c₁.pt, π := c₁.π ≫ f : Cone X₂ }.pt ⟶ c₂.pt)

Tactic:
⟨_, _, _, _, h₁, _, _, hf⟩

Premises used: CategoryTheory.MorphismProperty.limitsOfShape.mk
-- 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 : Category.{v_1, u_1} J
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
hφ : ∀ (j : J), h₂.lift { pt := c₁.pt, π := c₁.π ≫ f } ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
⊢ limitsOfShape.{v, u, v_1, u_1} W J (X := c₁.pt)
    (h₂.lift { pt := c₁.pt, π := c₁.π ≫ f } : { pt := c₁.pt, π := c₁.π ≫ f : Cone X₂ }.pt ⟶ c₂.pt)

Tactic:
exact ⟨_, _, _, _, h₁, _, _, hf⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
h : W₁ ≤ W₂
J : Type u_2
inst_1 : Category.{v_2, u_2} J
X Y : C
X₁ X₂ : Functor.{v_2, v, u_2, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W₁.functorCategory J f
⊢ limitsOfShape.{v, u, v_2, u_2} W₂ J (X := { pt := c₁.pt, π := c₁.π ≫ f : Cone X₂ }.pt)
    (h₂.lift { pt := c₁.pt, π := c₁.π ≫ f })

Tactic:
⟨_, _, _, _, h₁, _, f, fun j ↦ h _ (hf j)⟩

Premises used: CategoryTheory.MorphismProperty.limitsOfShape.mk, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
h : W₁ ≤ W₂
J : Type u_2
inst_1 : Category.{v_2, u_2} J
X Y : C
X₁ X₂ : Functor.{v_2, v, u_2, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W₁.functorCategory J f
⊢ limitsOfShape.{v, u, v_2, u_2} W₂ J (X := { pt := c₁.pt, π := c₁.π ≫ f : Cone X₂ }.pt)
    (h₂.lift { pt := c₁.pt, π := c₁.π ≫ f })

Tactic:
exact ⟨_, _, _, _, h₁, _, f, fun j ↦ h _ (hf 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 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
⊢ g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }

Tactic:
have fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift (Cone.mk _ (c₁.π ≫ f)) :=
      e.inv.w.symm
-- 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 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := Functor.map (Functor.const J) e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := Functor.map (Functor.const J) e₂.inv ≫ c₂.π }
have :
  ∀ (h₁' : IsLimit c₁'),
    limitsOfShape.{v, u, v_1, u_1} W J
      (Arrow.hom { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) })
⊢ limitsOfShape.{v, u, v_1, u_1} W J
    (Arrow.hom { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) })

Tactic:
have h₁' : IsLimit c₁' := IsLimit.ofIsoLimit h₁ (Cone.ext e₁)
-- 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 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := Functor.map (Functor.const J) e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := Functor.map (Functor.const J) e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
have :
  ∀ (h₂' : IsLimit c₂'),
    limitsOfShape.{v, u, v_1, u_1} W J
      (Arrow.hom { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) })
⊢ limitsOfShape.{v, u, v_1, u_1} W J
    (Arrow.hom { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) })

Tactic:
have h₂' : IsLimit c₂' := IsLimit.ofIsoLimit h₂ (Cone.ext e₂)
-- 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 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := Functor.map (Functor.const J) e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := Functor.map (Functor.const J) e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
h₂' : IsLimit c₂'
j : J
rw : { pt := c₁'.pt, π := c₁'.π ≫ f : Cone X₂ }.π.app j = g ≫ c₂'.π.app j
⊢ h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } ≫ c₂'.π.app j = g ≫ c₂'.π.app j

Tactic:
rw [h₂'.fac]

Premises used: CategoryTheory.Limits.IsLimit.fac
-- 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 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := Functor.map (Functor.const J) e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := Functor.map (Functor.const J) e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
h₂' : IsLimit c₂'
j : J
⊢ { pt := c₁'.pt, π := c₁'.π ≫ f : Cone X₂ }.π.app j = g ≫ c₂'.π.app j

Tactic:
simp [reassoc_of% fac, c₁', c₂']
-- 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 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := Functor.map (Functor.const J) e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := Functor.map (Functor.const J) e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
h₂' : IsLimit c₂'
⊢ h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } = g

Tactic:
obtain hg : h₂'.lift (Cone.mk _ (c₁'.π ≫ f)) = g :=
      h₂'.hom_ext (fun j ↦ by
        rw [h₂'.fac]
        simp [reassoc_of% fac, c₁', c₂'])

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Cone.mk, CategoryTheory.Limits.IsLimit.lift
-- 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 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := Functor.map (Functor.const J) e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := Functor.map (Functor.const J) e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
h₂' : IsLimit c₂'
hg : h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } = g
rw :
  limitsOfShape.{v, u, v_1, u_1} W J (X :=
    Arrow.left.{v, u}
      { left := Y₁, right := Y₂,
        hom := (h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } : { pt := c₁'.pt, π := c₁'.π ≫ f : Cone X₂ }.pt ⟶ c₂'.pt) })
    (Arrow.hom
      { left := Y₁, right := Y₂,
        hom := (h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } : { pt := c₁'.pt, π := c₁'.π ≫ f : Cone X₂ }.pt ⟶ c₂'.pt) })
⊢ limitsOfShape.{v, u, v_1, u_1} W J
    (Arrow.hom { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) })

Tactic:
rw [← hg]
-- 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 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := Functor.map (Functor.const J) e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := Functor.map (Functor.const J) e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
h₂' : IsLimit c₂'
hg : h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } = g
⊢ limitsOfShape.{v, u, v_1, u_1} W J (X :=
    Arrow.left.{v, u}
      { left := Y₁, right := Y₂,
        hom := (h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } : { pt := c₁'.pt, π := c₁'.π ≫ f : Cone X₂ }.pt ⟶ c₂'.pt) })
    (Arrow.hom
      { left := Y₁, right := Y₂,
        hom := (h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } : { pt := c₁'.pt, π := c₁'.π ≫ f : Cone X₂ }.pt ⟶ c₂'.pt) })

Tactic:
⟨_, _, _, _, h₁', _, _, hf⟩

Premises used: CategoryTheory.MorphismProperty.limitsOfShape.mk
-- 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 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := Functor.map (Functor.const J) e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := Functor.map (Functor.const J) e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
h₂' : IsLimit c₂'
hg : h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } = g
⊢ limitsOfShape.{v, u, v_1, u_1} W J (X :=
    Arrow.left.{v, u}
      { left := Y₁, right := Y₂,
        hom := (h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } : { pt := c₁'.pt, π := c₁'.π ≫ f : Cone X₂ }.pt ⟶ c₂'.pt) })
    (Arrow.hom
      { left := Y₁, right := Y₂,
        hom := (h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } : { pt := c₁'.pt, π := c₁'.π ≫ f : Cone X₂ }.pt ⟶ c₂'.pt) })

Tactic:
exact ⟨_, _, _, _, h₁', _, _, hf⟩
-- 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 : Category.{v_1, u_1} J
X Y : Functor.{v_1, v, u_1, u} J C
f : X ⟶ Y
inst_2 : HasLimit X
inst_3 : HasLimit Y
hf : W.functorCategory J f
⊢ limitsOfShape.{v, u, v_1, u_1} W J (X := limit X) (Y := limit Y) (limMap f)

Tactic:
⟨_, _, _, _, limit.isLimit X, _, _, hf⟩

Premises used: CategoryTheory.MorphismProperty.limitsOfShape.mk, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.map, CategoryTheory.Limits.limMap
-- 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 : Category.{v_1, u_1} J
mp : IsStableUnderLimitsOfShape.{v, u, v_1, u_1} W J → limitsOfShape.{v, u, v_1, u_1} W J ≤ W
mpr : limitsOfShape.{v, u, v_1, u_1} W J ≤ W → IsStableUnderLimitsOfShape.{v, u, v_1, u_1} W J
⊢ IsStableUnderLimitsOfShape.{v, u, v_1, u_1} W J ↔ limitsOfShape.{v, u, v_1, u_1} W J ≤ W

Tactic:
constructor
-- 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 : Category.{v_1, u_1} J
h : IsStableUnderLimitsOfShape.{v, u, v_1, u_1} W J
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
⊢ ∀ (j : J), h₂.lift { pt := c₁.pt, π := c₁.π ≫ f } ≫ c₂.π.app j = c₁.π.app j ≫ f.app j

Tactic:
simp
-- 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 : Category.{v_1, u_1} J
h : IsStableUnderLimitsOfShape.{v, u, v_1, u_1} W J
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
⊢ W (X := { pt := c₁.pt, π := c₁.π ≫ f : Cone X₂ }.pt) (h₂.lift { pt := c₁.pt, π := c₁.π ≫ f })

Tactic:
exact h.condition _ _ _ _ h₁ h₂ f hf _ (by simp)

Premises used: CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.condition
-- 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 : Category.{v_1, u_1} J
h : limitsOfShape.{v, u, v_1, u_1} W J ≤ W
mpr :
  ∀ (X₁ X₂ : Functor.{v_1, v, u_1, u} J C) (c₁ : Cone X₁) (c₂ : Cone X₂) (x : IsLimit c₁) (h₂ : IsLimit c₂)
    (f : X₁ ⟶ X₂),
    W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt) (hφ : ∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j), W φ
⊢ IsStableUnderLimitsOfShape.{v, u, v_1, u_1} W J

Tactic:
constructor
-- 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 : Category.{v_1, u_1} J
h : limitsOfShape.{v, u, v_1, u_1} W J ≤ W
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
⊢ W φ

Tactic:
h _ (limitsOfShape.mk' X₁ X₂ c₁ c₂ h₁ h₂ f hf φ hφ)

Premises used: CategoryTheory.MorphismProperty.limitsOfShape.mk'
-- 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 : Category.{v_1, u_1} J
h : limitsOfShape.{v, u, v_1, u_1} W J ≤ W
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
⊢ W φ

Tactic:
exact h _ (limitsOfShape.mk' X₁ X₂ c₁ c₂ h₁ h₂ f hf φ hφ)

Premises used: CategoryTheory.MorphismProperty.limitsOfShape.mk'
-- 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 : Category.{v_1, u_1} J
inst_2 rwa rwa₁ rwa₂ rwa₃ : IsStableUnderLimitsOfShape.{v, u, v_1, u_1} W J
⊢ limitsOfShape.{v, u, v_1, u_1} W J ≤ W

Tactic:
rwa [← isStableUnderLimitsOfShape_iff_limitsOfShape_le]

Premises used: CategoryTheory.MorphismProperty.isStableUnderLimitsOfShape_iff_limitsOfShape_le
-- 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 : Category.{v_1, u_1} J
inst_2 : IsStableUnderLimitsOfShape.{v, u, v_1, u_1} W J
X Y : Functor.{v_1, v, u_1, u} J C
f : X ⟶ Y
inst_3 : HasLimit X
inst_4 : HasLimit Y
hf : W.functorCategory J f
⊢ W (X := limit X) (Y := limit Y) (limMap f)

Tactic:
limitsOfShape_le _ (limitsOfShape_limMap _ hf)

Premises used: CategoryTheory.MorphismProperty.limitsOfShape_le, CategoryTheory.MorphismProperty.limitsOfShape_limMap
-- 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 : Category.{v_1, u_1} J
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
j : J
⊢ c₁.ι.app j ≫ φ = c₁.ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι }

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 : Category.{v_1, u_1} J
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
obtain :
  ∀ (hφ : ∀ (j : J), c₁.ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = f.app j ≫ c₂.ι.app j),
    colimitsOfShape.{v, u, v_1, u_1} W J (Y := c₂.pt)
      (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } : c₁.pt ⟶ { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
⊢ colimitsOfShape.{v, u, v_1, u_1} W J φ

Tactic:
obtain rfl : φ = h₁.desc (Cocone.mk _ (f ≫ c₂.ι)) := h₁.hom_ext (fun j ↦ by simp [hφ])

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.Cocone.mk, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.IsColimit.desc, CategoryTheory.CategoryStruct.comp, rfl