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
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
⊢ g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (Iso.inv (asIso (pushout.inl (f ≫ g) f)))
have rw : g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (inv (pushout.inl (f ≫ g) f))
Tactic: rw [asIso_inv, IsIso.eq_comp_inv, ← cancel_epi f, ← pushout.condition, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
rw : g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (inv (pushout.inl (f ≫ g) f))
⊢ g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (Iso.inv (asIso (pushout.inl (f ≫ g) f)))
have rw₁ : Eq (α := Y ⟶ pushout (f ≫ g) f) (g ≫ pushout.inl (f ≫ g) f) (pushout.inr (f ≫ g) f)
Tactic: rw [asIso_inv, IsIso.eq_comp_inv, ← cancel_epi f, ← pushout.condition, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
rw : g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (inv (pushout.inl (f ≫ g) f))
rw₁ : Eq (α := Y ⟶ pushout (f ≫ g) f) (g ≫ pushout.inl (f ≫ g) f) (pushout.inr (f ≫ g) f)
⊢ g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (Iso.inv (asIso (pushout.inl (f ≫ g) f)))
have rw₂ : Eq (α := X ⟶ pushout (f ≫ g) f) (f ≫ g ≫ pushout.inl (f ≫ g) f) (f ≫ pushout.inr (f ≫ g) f)
Tactic: rw [asIso_inv, IsIso.eq_comp_inv, ← cancel_epi f, ← pushout.condition, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
rw : g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (inv (pushout.inl (f ≫ g) f))
rw₁ : Eq (α := Y ⟶ pushout (f ≫ g) f) (g ≫ pushout.inl (f ≫ g) f) (pushout.inr (f ≫ g) f)
rw₂ : Eq (α := X ⟶ pushout (f ≫ g) f) (f ≫ g ≫ pushout.inl (f ≫ g) f) (f ≫ pushout.inr (f ≫ g) f)
⊢ g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (Iso.inv (asIso (pushout.inl (f ≫ g) f)))
have rw₃ : Eq (α := X ⟶ pushout (f ≫ g) f) (f ≫ g ≫ pushout.inl (f ≫ g) f) ((f ≫ g) ≫ pushout.inl (f ≫ g) f)
Tactic: rw [asIso_inv, IsIso.eq_comp_inv, ← cancel_epi f, ← pushout.condition, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
rw : g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (inv (pushout.inl (f ≫ g) f))
rw₁ : Eq (α := Y ⟶ pushout (f ≫ g) f) (g ≫ pushout.inl (f ≫ g) f) (pushout.inr (f ≫ g) f)
rw₂ : Eq (α := X ⟶ pushout (f ≫ g) f) (f ≫ g ≫ pushout.inl (f ≫ g) f) (f ≫ pushout.inr (f ≫ g) f)
rw₃ : Eq (α := X ⟶ pushout (f ≫ g) f) (f ≫ g ≫ pushout.inl (f ≫ g) f) ((f ≫ g) ≫ pushout.inl (f ≫ g) f)
⊢ g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (Iso.inv (asIso (pushout.inl (f ≫ g) f)))
have rw₄ : Eq (α := X ⟶ pushout (f ≫ g) f) (f ≫ g ≫ pushout.inl (f ≫ g) f) (f ≫ g ≫ pushout.inl (f ≫ g) f)
Tactic: rw [asIso_inv, IsIso.eq_comp_inv, ← cancel_epi f, ← pushout.condition, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
⊢ P g
have have : ∀
  (this :
    g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (Iso.inv (asIso (pushout.inl (f ≫ g) f)))),
  P g
Tactic: have : g = pushout.inr (f ≫ g) f ≫ (asIso (pushout.inl (f ≫ g) f)).inv := by
      rw [asIso_inv, IsIso.eq_comp_inv, ← cancel_epi f, ← pushout.condition, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
this :
  g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (Iso.inv (asIso (pushout.inl (f ≫ g) f)))
⊢ P g
have rw : P (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f)
Tactic: rw [this, cancel_right_of_respectsIso (P := P)]
-- 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
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
⊢ limitsOfShape.{v, u, v_1, u_1} W J φ
have obtain : ∀ (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: obtain rfl : φ = h₂.lift (Cone.mk _ (c₁.π ≫ f)) := h₂.hom_ext (fun j ↦ by simp [hφ])
Cleared hypotheses: φ, hφ
-- 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₁ : 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
⊢ 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) })
have fac : 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
-- 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₁ : 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₂.π }
⊢ 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) })
have 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) })
Tactic: have h₁' : IsLimit c₁' := IsLimit.ofIsoLimit h₁ (Cone.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₁ : 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₁'
⊢ 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) })
have 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) })
Tactic: have h₂' : IsLimit c₂' := IsLimit.ofIsoLimit h₂ (Cone.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₁ : 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
⊢ h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } ≫ c₂'.π.app j = g ≫ c₂'.π.app j
have rw : { pt := c₁'.pt, π := c₁'.π ≫ f : Cone X₂ }.π.app j = g ≫ c₂'.π.app j
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₁ : 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₂'
⊢ 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) })
have hg : 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₂'])
-- 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₁ : 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
    (Arrow.hom { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) })
have 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) })
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_1
inst_1 : Category.{v_1, u_1} J
⊢ IsStableUnderLimitsOfShape.{v, u, v_1, u_1} W J ↔ limitsOfShape.{v, u, v_1, u_1} W J ≤ W
have mp : IsStableUnderLimitsOfShape.{v, u, v_1, u_1} W J → limitsOfShape.{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 : IsStableUnderLimitsOfShape.{v, u, v_1, u_1} W J → limitsOfShape.{v, u, v_1, u_1} W J ≤ W
⊢ IsStableUnderLimitsOfShape.{v, u, v_1, u_1} W J ↔ limitsOfShape.{v, u, v_1, u_1} W J ≤ W
have mpr : limitsOfShape.{v, u, v_1, u_1} W J ≤ W → IsStableUnderLimitsOfShape.{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 : limitsOfShape.{v, u, v_1, u_1} W J ≤ W
⊢ IsStableUnderLimitsOfShape.{v, u, v_1, u_1} W J
have 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 φ
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
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
⊢ colimitsOfShape.{v, u, v_1, u_1} W J φ
have 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)
Tactic: obtain rfl : φ = h₁.desc (Cocone.mk _ (f ≫ c₂.ι)) := h₁.hom_ext (fun j ↦ by simp [hφ])
Cleared hypotheses: φ, 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
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 : X ⟶ Y
⊢ colimitsOfShape.{v, u, v_2, u_2} W J' f → colimitsOfShape.{v, u, v_1, u_1} W J f
have this : ∀ (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),
  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₂.ι })
Tactic: ⟨X₁, X₂, c₁, c₂, h₁, h₂, f, 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 : 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
⊢ 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 have : ∀ (h₁' : IsColimit (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₂.ι })
Tactic: have h₁' : IsColimit (c₁.whisker F) := (Functor.Final.isColimitWhiskerEquiv F c₁).symm 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
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₁)
⊢ 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 have : ∀ (h₂' : IsColimit (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₂.ι })
Tactic: have h₂' : IsColimit (c₂.whisker F) := (Functor.Final.isColimitWhiskerEquiv F c₂).symm h₂
-- 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
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₂)
j : J
⊢ Eq (α := (F ⋙ X₁).obj j ⟶ { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
    ((Cocone.whisker F c₁).ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })
    ((Cocone.whisker F c₁).ι.app j ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι })
have this : (Cocone.whisker F c₁).ι.app j ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι } =
  { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι : Cocone (F ⋙ X₁) }.ι.app j
Tactic: have := h₁'.fac (Cocone.mk c₂.pt (Functor.whiskerLeft F f ≫ Functor.whiskerLeft F c₂.ι)) 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 : 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₂)
j : J
this :
  (Cocone.whisker F c₁).ι.app j ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι } =
    { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι : Cocone (F ⋙ X₁) }.ι.app j
⊢ Eq (α := (F ⋙ X₁).obj j ⟶ { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
    ((Cocone.whisker F c₁).ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })
    ((Cocone.whisker F c₁).ι.app j ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι })
have dsimp : Eq (α := X₁.obj (F.obj j) ⟶ c₂.pt)
  (c₁.ι.app (F.obj j) ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } : X₁.obj (F.obj j) ⟶ c₂.pt)
  (c₁.ι.app (F.obj j) ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι } : X₁.obj (F.obj j) ⟶ c₂.pt)
Tactic: dsimp at 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
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₂)
⊢ 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 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₂).ι })
Tactic: have : h₁.desc (Cocone.mk c₂.pt (f ≫ c₂.ι)) =
      h₁'.desc (Cocone.mk c₂.pt (Functor.whiskerLeft _ f ≫ (c₂.whisker F).ι)) :=
    h₁'.hom_ext (fun j ↦ by
      have := h₁'.fac (Cocone.mk c₂.pt (Functor.whiskerLeft F f ≫ Functor.whiskerLeft F c₂.ι)) j
      dsimp at this ⊢
      simp [this])