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
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₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
    { 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, ι := f ≫ c₂.ι } } ≅
  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, ι := f ≫ c₂.ι } } ≅
  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 : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ Functor.map (Functor.const J) e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ Functor.map (Functor.const J) e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
hg : h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } = g
rw :
  colimitsOfShape.{v, u, v_1, u_1} W J (X :=
    Arrow.left.{v, u}
      { left := Y₁, right := Y₂,
        hom := (h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } : c₁'.pt ⟶ { pt := c₂'.pt, ι := f ≫ c₂'.ι : Cocone X₁ }.pt) })
    (Arrow.hom
      { left := Y₁, right := Y₂,
        hom := (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
    (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₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
    { 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, ι := f ≫ c₂.ι } } ≅
  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, ι := f ≫ c₂.ι } } ≅
  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 : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ Functor.map (Functor.const J) e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ Functor.map (Functor.const J) e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
hg : h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } = g
⊢ colimitsOfShape.{v, u, v_1, u_1} W J (X :=
    Arrow.left.{v, u}
      { left := Y₁, right := Y₂,
        hom := (h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } : c₁'.pt ⟶ { pt := c₂'.pt, ι := f ≫ c₂'.ι : Cocone X₁ }.pt) })
    (Arrow.hom
      { left := Y₁, right := Y₂,
        hom := (h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } : c₁'.pt ⟶ { pt := c₂'.pt, ι := f ≫ c₂'.ι : Cocone X₁ }.pt) })

Tactic:
⟨_, _, _, _, _, h₂', _, 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
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₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
    { 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, ι := f ≫ c₂.ι } } ≅
  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, ι := f ≫ c₂.ι } } ≅
  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 : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ Functor.map (Functor.const J) e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ Functor.map (Functor.const J) e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
hg : h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } = g
⊢ colimitsOfShape.{v, u, v_1, u_1} W J (X :=
    Arrow.left.{v, u}
      { left := Y₁, right := Y₂,
        hom := (h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } : c₁'.pt ⟶ { pt := c₂'.pt, ι := f ≫ c₂'.ι : Cocone X₁ }.pt) })
    (Arrow.hom
      { left := Y₁, right := Y₂,
        hom := (h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } : c₁'.pt ⟶ { pt := c₂'.pt, ι := f ≫ c₂'.ι : Cocone X₁ }.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 : HasColimit X
inst_3 : HasColimit Y
hf : W.functorCategory J f
⊢ colimitsOfShape.{v, u, v_1, u_1} W J (X := colimit X) (Y := colimit Y) (colimMap f)

Tactic:
⟨_, _, _, _, _, colimit.isColimit Y, _, hf⟩

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimMap, CategoryTheory.MorphismProperty.colimitsOfShape.mk, CategoryTheory.Limits.IsColimit.map
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_2
inst_1 : Preorder J
inst_2 : OrderBot J
F : Functor.{u_2, v, u_2, u} J C
c : Cocone F
hc : IsColimit c
h : ∀ (j : J), W (X := F.obj ⊥) (Y := F.obj j) (F.map (homOfLE ⋯))
x x_1 : J
x_2 : x ⟶ x_1
dsimp : 𝟙 (F.obj ⊥) ≫ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ F.map x_2
⊢ Eq.{v + 1} (α := Functor.obj.{u_2, v, u_2, u} (Functor.obj (Functor.const J) (F.obj ⊥)) x ⟶ F.obj x_1)
    (Functor.map (Functor.obj (Functor.const J) (F.obj ⊥)) x_2 ≫ F.map (homOfLE ⋯)) (F.map (homOfLE ⋯) ≫ F.map x_2)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_2
inst_1 : Preorder J
inst_2 : OrderBot J
F : Functor.{u_2, v, u_2, u} J C
c : Cocone F
hc : IsColimit c
h : ∀ (j : J), W (X := F.obj ⊥) (Y := F.obj j) (F.map (homOfLE ⋯))
x x_1 : J
x_2 : x ⟶ x_1
rw : Eq (α := F.obj ⊥ ⟶ F.obj x_1) (F.map (homOfLE ⋯)) (F.map (homOfLE ⋯ ≫ x_2))
⊢ 𝟙 (F.obj ⊥) ≫ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ F.map x_2

Tactic:
rw [Category.id_comp, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_2
inst_1 : Preorder J
inst_2 : OrderBot J
F : Functor.{u_2, v, u_2, u} J C
c : Cocone F
hc : IsColimit c
h : ∀ (j : J), W (X := F.obj ⊥) (Y := F.obj j) (F.map (homOfLE ⋯))
x x_1 : J
x_2 : x ⟶ x_1
⊢ Eq (α := F.obj ⊥ ⟶ F.obj x_1) (F.map (homOfLE ⋯)) (F.map (homOfLE ⋯ ≫ x_2))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_2
inst_1 : Preorder J
inst_2 : OrderBot J
F : Functor.{u_2, v, u_2, u} J C
c : Cocone F
hc : IsColimit c
h : ∀ (j : J), W (X := F.obj ⊥) (Y := F.obj j) (F.map (homOfLE ⋯))
⊢ ∀ (j : J),
    CategoryStruct.comp (Y :=
        Functor.obj.{u_2, v, u_2, u}
          (Functor.obj (Functor.const J) (Cocone.pt.{u_2, v, u_2, u} (constCocone J (F.obj ⊥)))) j)
        (NatTrans.app (Cocone.ι (constCocone J (F.obj ⊥))) j) (c.ι.app ⊥) =
      NatTrans.app
          { app := fun (k : J) ↦ F.map (homOfLE ⋯), naturality := ⋯ :
            NatTrans (Functor.obj (Functor.const J) (F.obj ⊥)) F }
          j ≫
        c.ι.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
mp : IsStableUnderColimitsOfShape.{v, u, v_1, u_1} W J → colimitsOfShape.{v, u, v_1, u_1} W J ≤ W
mpr : colimitsOfShape.{v, u, v_1, u_1} W J ≤ W → IsStableUnderColimitsOfShape.{v, u, v_1, u_1} W J
⊢ IsStableUnderColimitsOfShape.{v, u, v_1, u_1} W J ↔ colimitsOfShape.{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 : IsStableUnderColimitsOfShape.{v, u, v_1, u_1} W J
X Y : C
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
⊢ ∀ (j : J), c₁.ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = f.app j ≫ c₂.ι.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 : IsStableUnderColimitsOfShape.{v, u, v_1, u_1} W J
X Y : C
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
⊢ W (Y := { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt) (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

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

Premises used: CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.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 : colimitsOfShape.{v, u, v_1, u_1} W J ≤ W
mpr :
  ∀ (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₂),
    W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt) (hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j), W φ
⊢ IsStableUnderColimitsOfShape.{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 : colimitsOfShape.{v, u, v_1, u_1} W J ≤ W
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
⊢ W φ

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

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
J : Type u_1
inst_1 : Category.{v_1, u_1} J
h : colimitsOfShape.{v, u, v_1, u_1} W J ≤ W
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
⊢ W φ

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

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
J : Type u_1
inst_1 : Category.{v_1, u_1} J
inst_2 rwa rwa₁ rwa₂ rwa₃ : IsStableUnderColimitsOfShape.{v, u, v_1, u_1} W J
⊢ colimitsOfShape.{v, u, v_1, u_1} W J ≤ W

Tactic:
rwa [← isStableUnderColimitsOfShape_iff_colimitsOfShape_le]

Premises used: CategoryTheory.MorphismProperty.isStableUnderColimitsOfShape_iff_colimitsOfShape_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 : IsStableUnderColimitsOfShape.{v, u, v_1, u_1} W J
X Y : Functor.{v_1, v, u_1, u} J C
f : X ⟶ Y
inst_3 : HasColimit X
inst_4 : HasColimit Y
hf : W.functorCategory J f
⊢ W (X := colimit X) (Y := colimit Y) (colimMap f)

Tactic:
colimitsOfShape_le _ (colimitsOfShape_colimMap _ hf)

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape_le, CategoryTheory.MorphismProperty.colimitsOfShape_colimMap
-- 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
F₁ F₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
h : ∀ (j : J), IsIso (f.app j)
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
⊢ IsIso f

Tactic:
have := NatIso.isIso_of_isIso_app f
-- 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
F₁ F₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
h : ∀ (j : J), IsIso (f.app j)
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
this : IsIso f
j : J
⊢ c₁.ι.app j ≫ φ ≫ h₂.desc { pt := c₁.pt, ι := inv f ≫ c₁.ι } = c₁.ι.app j ≫ 𝟙 c₁.pt

Tactic:
simp [reassoc_of% (hφ 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
F₁ F₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
h : ∀ (j : J), IsIso (f.app j)
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
this : IsIso f
⊢ ∀ (j : J), c₂.ι.app j ≫ h₂.desc { pt := c₁.pt, ι := inv f ≫ c₁.ι } ≫ φ = c₂.ι.app j ≫ 𝟙 c₂.pt

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
F₁ F₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
h : ∀ (j : J), IsIso (f.app j)
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
this : IsIso f
⊢ MorphismProperty.isomorphisms C φ

Tactic:
exact ⟨h₂.desc (Cocone.mk _ (inv f ≫ c₁.ι)),
      h₁.hom_ext (fun j ↦ by simp [reassoc_of% (hφ j)]),
      h₂.hom_ext (by simp [hφ])⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
⊢ colimitsOfShape.{v, u, w, w} W (Discrete J) ≤ coproducts.{w, v, u} W

Tactic:
le_iSup (f := fun (J : Type w) ↦ W.colimitsOfShape (Discrete J)) J

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

Tactic:
simp only [coproducts, iSup_iff]

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

Tactic:
rw [coproducts_iff]

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
X Y : C
f : X ⟶ Y
J : Type w'
hf : colimitsOfShape.{v, u, w', w'} W (Discrete J) f
inst_1 : Small.{w, w'} J
⊢ ∃ (J : Type w), colimitsOfShape.{v, u, w, w} W (Discrete J) f

Tactic:
⟨Shrink J, ?_⟩

Premises used: Exists.intro, Shrink
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
J : Type w'
hf : colimitsOfShape.{v, u, w', w'} W (Discrete J) f
inst_1 : Small.{w, w'} J
refine : colimitsOfShape.{v, u, w, w} W (Discrete (Shrink.{w, w'} J)) f
⊢ ∃ (J : Type w), colimitsOfShape.{v, u, w, w} W (Discrete J) f

Tactic:
refine ⟨Shrink J, ?_⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
J : Type w'
hf : colimitsOfShape.{v, u, w', w'} W (Discrete J) f
inst_1 : Small.{w, w'} J
rwa rwa₁ rwa₂ rwa₃ : colimitsOfShape.{v, u, w', w'} W (Discrete J) f
⊢ colimitsOfShape.{v, u, w, w} W (Discrete (Shrink.{w, w'} J)) f

Tactic:
rwa [← W.colimitsOfShape_eq_of_equivalence (Discrete.equivalence (equivShrink.{w} J))]
-- 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
have :
  ∀ (h : IsInitial (C := Discrete PUnit.{w + 1}) (⊥_ Discrete PUnit.{w + 1})),
    colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) f
⊢ colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) f

Tactic:
have h := initialIsInitial (C := Discrete (PUnit.{w + 1}))
-- 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₂)
have : ∀ (hc₁ : IsColimit c₁), colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) f
⊢ colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) f

Tactic:
have hc₁ : IsColimit c₁ := colimitOfDiagramInitial h _
-- 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₁
have : ∀ (hc₂ : IsColimit c₂), colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) f
⊢ colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) f

Tactic:
have hc₂ : IsColimit c₂ := colimitOfDiagramInitial h _
-- 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₂
x : Discrete PUnit.{w + 1}
⊢ Quiver.Hom.{v, u} (V := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₁) x)
    (Functor.obj.{w, v, w, u} (Discrete.functor fun (x : PUnit.{w + 1}) ↦ X₂) x)

Tactic:
exact f
-- 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₂
x : Discrete PUnit.{w + 1}
⊢ x = ⊥_ Discrete PUnit.{w + 1}

Tactic:
ext
-- 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₂
x : Discrete PUnit.{w + 1}
obtain :
  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)
⊢ c₁.ι.app x ≫ hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι } =
    c₁.ι.app x ≫ f

Tactic:
obtain rfl : x = ⊥_ _ := by ext

Premises used: rfl