awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Category.{v_1, u_1} J
J' : Type u_2
inst_2 : Category.{v_2, u_2} J'
F : Functor.{v_1, v_2, u_1, u_2} J J'
inst_3 : F.Final
X Y : C
f_1 : X ⟶ Y
X₁ X₂ : Functor.{v_2, v, u_2, u} J' C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
this :
  Eq (α := c₁.pt ⟶ { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt) (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })
    (h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι })
⊢ colimitsOfShape.{v, u, v_1, u_1} W J (Y := { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
    (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })
have rw : colimitsOfShape.{v, u, v_1, u_1} W J (Y := { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
  (h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι } :
    (Cocone.whisker F c₁).pt ⟶ { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι : Cocone (F ⋙ X₁) }.pt)
Tactic: rw [this]
-- 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 : 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
⊢ 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) })
have fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
Tactic: have fac : e₁.hom ≫ g = h₁.desc (Cocone.mk _ (f ≫ c₂.ι)) ≫ e₂.hom := e.hom.w
-- 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 : 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 }
⊢ 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) })
have have : ∀ (h₁' : IsColimit c₁'),
  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: have h₁' : IsColimit c₁' := IsColimit.ofIsoColimit h₁ (Cocone.ext e₁)
-- 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 : 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₁'
⊢ 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) })
have have : ∀ (h₂' : IsColimit c₂'),
  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: have h₂' : IsColimit c₂' := IsColimit.ofIsoColimit h₂ (Cocone.ext e₂)
-- 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 : 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₂'
j : J
⊢ c₁'.ι.app j ≫ h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } = c₁'.ι.app j ≫ g
have rw : { pt := c₂'.pt, ι := f ≫ c₂'.ι : Cocone X₁ }.ι.app j = c₁'.ι.app j ≫ g
Tactic: rw [h₁'.fac]
-- 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 : 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₂'
⊢ 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) })
have hg : h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } = g
Tactic: obtain hg : h₁'.desc (Cocone.mk _ (f ≫ c₂'.ι)) = g :=
      h₁'.hom_ext (fun j ↦ by
        rw [h₁'.fac]
        simp [fac, c₁', c₂'])
-- 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 : 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
    (Arrow.hom { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) })
have 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) })
Tactic: rw [← hg]
-- 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_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.{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)
have dsimp : 𝟙 (F.obj ⊥) ≫ F.map (homOfLE sorry) = F.map (homOfLE sorry) ≫ F.map x_2
Tactic: dsimp
-- 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_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
⊢ 𝟙 (F.obj ⊥) ≫ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ F.map x_2
have rw : Eq (α := F.obj ⊥ ⟶ F.obj x_1) (F.map (homOfLE sorry)) (F.map (homOfLE sorry ≫ x_2))
Tactic: rw [Category.id_comp, ← Functor.map_comp]
-- 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 : Category.{v_1, u_1} J
⊢ IsStableUnderColimitsOfShape.{v, u, v_1, u_1} W J ↔ colimitsOfShape.{v, u, v_1, u_1} W J ≤ W
have mp : IsStableUnderColimitsOfShape.{v, u, v_1, u_1} W J → colimitsOfShape.{v, u, v_1, u_1} W J ≤ W
Tactic: constructor
-- 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 : 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
⊢ IsStableUnderColimitsOfShape.{v, u, v_1, u_1} W J ↔ colimitsOfShape.{v, u, v_1, u_1} W J ≤ W
have mpr : colimitsOfShape.{v, u, v_1, u_1} W J ≤ W → IsStableUnderColimitsOfShape.{v, u, v_1, u_1} W J
Tactic: constructor
-- 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 : Category.{v_1, u_1} J
h : colimitsOfShape.{v, u, v_1, u_1} W J ≤ W
⊢ IsStableUnderColimitsOfShape.{v, u, v_1, u_1} W J
have 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 φ
Tactic: constructor
-- 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 : 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
⊢ MorphismProperty.isomorphisms C φ
have this : IsIso f
Tactic: have := NatIso.isIso_of_isIso_app f
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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
⊢ coproducts.{w, v, u} W f
have rw : ∃ (J : Type w), colimitsOfShape.{v, u, w, w} W (Discrete J) f
Tactic: rw [coproducts_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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
have refine : colimitsOfShape.{v, u, w, w} W (Discrete (Shrink.{w, w'} J)) f
Tactic: refine ⟨Shrink 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
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
⊢ colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) f
have have : ∀ (h : IsInitial (C := Discrete PUnit.{w + 1}) (⊥_ Discrete PUnit.{w + 1})),
  colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) f
Tactic: have h := initialIsInitial (C := Discrete (PUnit.{w + 1}))
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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₂)
⊢ colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) f
have have : ∀ (hc₁ : IsColimit c₁), colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) f
Tactic: have hc₁ : IsColimit c₁ := colimitOfDiagramInitial h _
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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₁
⊢ colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) f
have have : ∀ (hc₂ : IsColimit c₂), colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) f
Tactic: have hc₂ : IsColimit c₂ := colimitOfDiagramInitial h _
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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}
⊢ c₁.ι.app x ≫ hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun (x : Discrete PUnit.{w + 1}) ↦ f) ≫ c₂.ι } =
    c₁.ι.app x ≫ f
have 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)
Tactic: obtain rfl : x = ⊥_ _ := by ext
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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₁) })
    (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)
have 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)
Tactic: rw [IsColimit.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (hypothesis)
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₂
⊢ colimitsOfShape.{v, u, w, w} W (Discrete PUnit.{w + 1}) f
have this : 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₂])
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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}) f
have 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₂.ι })
Tactic: rw [← this]