awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ IsColimit c ≃ IsLimit c.unop
have f₁ : IsColimit c → IsLimit c.unop
Tactic: apply equivOfSubsingletonOfSubsingleton
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
f₁ : IsColimit c → IsLimit c.unop
⊢ IsColimit c ≃ IsLimit c.unop
have g₁ : IsLimit c.unop → IsColimit c
Tactic: apply equivOfSubsingletonOfSubsingleton
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := op Z) (Y := op X) (Z := op Y) f.op g.op ↔ HasPullback f g
have rw : HasColimit.{0, 0, v₁, u₁} (C := Cᵒᵖ) (span f.op g.op) ↔ HasPullback f g
Tactic: rw [HasPushout, hasColimit_iff_of_iso (spanOp f g), hasColimit_inverse_equivalence_comp_iff,
    hasColimit_op_iff_hasLimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
rw : HasColimit.{0, 0, v₁, u₁} (C := Cᵒᵖ) (span f.op g.op) ↔ HasPullback f g
⊢ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := op Z) (Y := op X) (Z := op Y) f.op g.op ↔ HasPullback f g
have rw₁ : HasColimit (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op) ↔ HasPullback f g
Tactic: rw [HasPushout, hasColimit_iff_of_iso (spanOp f g), hasColimit_inverse_equivalence_comp_iff,
    hasColimit_op_iff_hasLimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
rw : HasColimit.{0, 0, v₁, u₁} (C := Cᵒᵖ) (span f.op g.op) ↔ HasPullback f g
rw₁ : HasColimit (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op) ↔ HasPullback f g
⊢ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := op Z) (Y := op X) (Z := op Y) f.op g.op ↔ HasPullback f g
have rw₂ : HasColimit (cospan f g).op ↔ HasPullback f g
Tactic: rw [HasPushout, hasColimit_iff_of_iso (spanOp f g), hasColimit_inverse_equivalence_comp_iff,
    hasColimit_op_iff_hasLimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
rw : HasColimit.{0, 0, v₁, u₁} (C := Cᵒᵖ) (span f.op g.op) ↔ HasPullback f g
rw₁ : HasColimit (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op) ↔ HasPullback f g
rw₂ : HasColimit (cospan f g).op ↔ HasPullback f g
⊢ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := op Z) (Y := op X) (Z := op Y) f.op g.op ↔ HasPullback f g
have rw₃ : HasLimit (cospan f g) ↔ HasPullback f g
Tactic: rw [HasPushout, hasColimit_iff_of_iso (spanOp f g), hasColimit_inverse_equivalence_comp_iff,
    hasColimit_op_iff_hasLimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasPushout f.unop g.unop ↔ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
have rw : HasColimit (span f.unop g.unop) ↔ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
Tactic: rw [HasPushout, hasColimit_iff_of_iso (spanUnop f g), hasColimit_inverse_equivalence_comp_iff,
    hasColimit_leftOp_iff_hasLimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
rw : HasColimit (span f.unop g.unop) ↔ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ HasPushout f.unop g.unop ↔ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
have rw₁ : HasColimit.{0, 0, v₁, u₁} (C := C) (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f g)) ↔
  HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
Tactic: rw [HasPushout, hasColimit_iff_of_iso (spanUnop f g), hasColimit_inverse_equivalence_comp_iff,
    hasColimit_leftOp_iff_hasLimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
rw : HasColimit (span f.unop g.unop) ↔ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
rw₁ :
  HasColimit.{0, 0, v₁, u₁} (C := C) (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f g)) ↔
    HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ HasPushout f.unop g.unop ↔ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
have rw₂ : HasColimit.{0, 0, v₁, u₁} (C := C) (Functor.leftOp (cospan f g)) ↔
  HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
Tactic: rw [HasPushout, hasColimit_iff_of_iso (spanUnop f g), hasColimit_inverse_equivalence_comp_iff,
    hasColimit_leftOp_iff_hasLimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
rw : HasColimit (span f.unop g.unop) ↔ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
rw₁ :
  HasColimit.{0, 0, v₁, u₁} (C := C) (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f g)) ↔
    HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
rw₂ :
  HasColimit.{0, 0, v₁, u₁} (C := C) (Functor.leftOp (cospan f g)) ↔
    HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ HasPushout f.unop g.unop ↔ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
have rw₃ : HasLimit.{0, 0, v₁, u₁} (C := Cᵒᵖ) (cospan f g) ↔ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
Tactic: rw [HasPushout, hasColimit_iff_of_iso (spanUnop f g), hasColimit_inverse_equivalence_comp_iff,
    hasColimit_leftOp_iff_hasLimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op Z) (Z := op X) f.op g.op ↔ HasPushout f g
have rw : HasLimit.{0, 0, v₁, u₁} (C := Cᵒᵖ) (cospan f.op g.op) ↔ HasPushout f g
Tactic: rw [HasPullback, hasLimit_iff_of_iso (cospanOp f g), hasLimit_inverse_equivalence_comp_iff,
    hasLimit_op_iff_hasColimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
rw : HasLimit.{0, 0, v₁, u₁} (C := Cᵒᵖ) (cospan f.op g.op) ↔ HasPushout f g
⊢ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op Z) (Z := op X) f.op g.op ↔ HasPushout f g
have rw₁ : HasLimit (walkingSpanOpEquiv.inverse ⋙ (span f g).op) ↔ HasPushout f g
Tactic: rw [HasPullback, hasLimit_iff_of_iso (cospanOp f g), hasLimit_inverse_equivalence_comp_iff,
    hasLimit_op_iff_hasColimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
rw : HasLimit.{0, 0, v₁, u₁} (C := Cᵒᵖ) (cospan f.op g.op) ↔ HasPushout f g
rw₁ : HasLimit (walkingSpanOpEquiv.inverse ⋙ (span f g).op) ↔ HasPushout f g
⊢ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op Z) (Z := op X) f.op g.op ↔ HasPushout f g
have rw₂ : HasLimit (span f g).op ↔ HasPushout f g
Tactic: rw [HasPullback, hasLimit_iff_of_iso (cospanOp f g), hasLimit_inverse_equivalence_comp_iff,
    hasLimit_op_iff_hasColimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
rw : HasLimit.{0, 0, v₁, u₁} (C := Cᵒᵖ) (cospan f.op g.op) ↔ HasPushout f g
rw₁ : HasLimit (walkingSpanOpEquiv.inverse ⋙ (span f g).op) ↔ HasPushout f g
rw₂ : HasLimit (span f g).op ↔ HasPushout f g
⊢ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op Z) (Z := op X) f.op g.op ↔ HasPushout f g
have rw₃ : HasColimit (span f g) ↔ HasPushout f g
Tactic: rw [HasPullback, hasLimit_iff_of_iso (cospanOp f g), hasLimit_inverse_equivalence_comp_iff,
    hasLimit_op_iff_hasColimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
⊢ HasPullback f.unop g.unop ↔ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
have rw : HasLimit (cospan f.unop g.unop) ↔ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
Tactic: rw [HasPullback, hasLimit_iff_of_iso (cospanUnop f g), hasLimit_inverse_equivalence_comp_iff,
    hasLimit_leftOp_iff_hasColimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
rw : HasLimit (cospan f.unop g.unop) ↔ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ HasPullback f.unop g.unop ↔ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
have rw₁ : HasLimit.{0, 0, v₁, u₁} (C := C) (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) ↔
  HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
Tactic: rw [HasPullback, hasLimit_iff_of_iso (cospanUnop f g), hasLimit_inverse_equivalence_comp_iff,
    hasLimit_leftOp_iff_hasColimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
rw : HasLimit (cospan f.unop g.unop) ↔ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
rw₁ :
  HasLimit.{0, 0, v₁, u₁} (C := C) (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) ↔
    HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ HasPullback f.unop g.unop ↔ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
have rw₂ : HasLimit.{0, 0, v₁, u₁} (C := C) (Functor.leftOp (span f g)) ↔
  HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
Tactic: rw [HasPullback, hasLimit_iff_of_iso (cospanUnop f g), hasLimit_inverse_equivalence_comp_iff,
    hasLimit_leftOp_iff_hasColimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
rw : HasLimit (cospan f.unop g.unop) ↔ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
rw₁ :
  HasLimit.{0, 0, v₁, u₁} (C := C) (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) ↔
    HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
rw₂ :
  HasLimit.{0, 0, v₁, u₁} (C := C) (Functor.leftOp (span f g)) ↔
    HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ HasPullback f.unop g.unop ↔ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
have rw₃ : HasColimit.{0, 0, v₁, u₁} (C := Cᵒᵖ) (span f g) ↔ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
Tactic: rw [HasPullback, hasLimit_iff_of_iso (cospanUnop f g), hasLimit_inverse_equivalence_comp_iff,
    hasLimit_leftOp_iff_hasColimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Eq (α := op (pullback g₁ g₂) ⟶ op (pullback f₁ f₂))
    (Quiver.Hom.op (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) : op (pullback g₁ g₂) ⟶ op (pullback f₁ f₂))
    (CategoryStruct.comp (Y := pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op)
        (Iso.inv (pushoutIsoOpPullback g₁.op g₂.op))
        (CategoryStruct.comp (Y := pushout.{v₁, u₁} (X := op S) (Y := op W) (Z := op X) f₁.op f₂.op)
          (pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯) (Iso.hom (pushoutIsoOpPullback f₁.op f₂.op))) :
      op (pullback g₁.op.unop g₂.op.unop) ⟶ op (pullback f₁.op.unop f₂.op.unop))
have rw : Eq (α := pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op ⟶ op (pullback f₁ f₂))
  (Iso.hom (pushoutIsoOpPullback g₁.op g₂.op) ≫ Quiver.Hom.op (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) :
    pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op ⟶ op (pullback f₁ f₂))
  (CategoryStruct.comp (Y := pushout.{v₁, u₁} (X := op S) (Y := op W) (Z := op X) f₁.op f₂.op)
      (pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op sorry sorry) (Iso.hom (pushoutIsoOpPullback f₁.op f₂.op)) :
    pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op ⟶ op (pullback f₁.op.unop f₂.op.unop))
Tactic: rw [Iso.eq_inv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Eq (α := pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op ⟶ op (pullback f₁ f₂))
    (Iso.hom (pushoutIsoOpPullback g₁.op g₂.op) ≫ Quiver.Hom.op (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) :
      pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op ⟶ op (pullback f₁ f₂))
    (CategoryStruct.comp (Y := pushout.{v₁, u₁} (X := op S) (Y := op W) (Z := op X) f₁.op f₂.op)
        (pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯) (Iso.hom (pushoutIsoOpPullback f₁.op f₂.op)) :
      pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op ⟶ op (pullback f₁.op.unop f₂.op.unop))
have h₀ : Eq (α := op Y ⟶ op (pullback f₁ f₂))
  (CategoryStruct.comp (Y := pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op) (pushout.inl g₁.op g₂.op)
      (Iso.hom (pushoutIsoOpPullback g₁.op g₂.op) ≫ Quiver.Hom.op (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
    op Y ⟶ op (pullback f₁ f₂))
  (CategoryStruct.comp (Y := pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op) (pushout.inl g₁.op g₂.op)
      (CategoryStruct.comp (Y := pushout.{v₁, u₁} (X := op S) (Y := op W) (Z := op X) f₁.op f₂.op)
        (pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op sorry sorry) (Iso.hom (pushoutIsoOpPullback f₁.op f₂.op))) :
    op Y ⟶ op (pullback f₁ f₂))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
h₀ :
  Eq (α := op Y ⟶ op (pullback f₁ f₂))
    (CategoryStruct.comp (Y := pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op)
        (pushout.inl g₁.op g₂.op)
        (Iso.hom (pushoutIsoOpPullback g₁.op g₂.op) ≫ Quiver.Hom.op (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
      op Y ⟶ op (pullback f₁ f₂))
    (CategoryStruct.comp (Y := pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op)
        (pushout.inl g₁.op g₂.op)
        (CategoryStruct.comp (Y := pushout.{v₁, u₁} (X := op S) (Y := op W) (Z := op X) f₁.op f₂.op)
          (pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯) (Iso.hom (pushoutIsoOpPullback f₁.op f₂.op))) :
      op Y ⟶ op (pullback f₁ f₂))
⊢ Eq (α := pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op ⟶ op (pullback f₁ f₂))
    (Iso.hom (pushoutIsoOpPullback g₁.op g₂.op) ≫ Quiver.Hom.op (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) :
      pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op ⟶ op (pullback f₁ f₂))
    (CategoryStruct.comp (Y := pushout.{v₁, u₁} (X := op S) (Y := op W) (Z := op X) f₁.op f₂.op)
        (pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯) (Iso.hom (pushoutIsoOpPullback f₁.op f₂.op)) :
      pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op ⟶ op (pullback f₁.op.unop f₂.op.unop))
have h₁ : Eq (α := op Z ⟶ op (pullback f₁ f₂))
  (CategoryStruct.comp (Y := pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op) (pushout.inr g₁.op g₂.op)
      (Iso.hom (pushoutIsoOpPullback g₁.op g₂.op) ≫ Quiver.Hom.op (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
    op Z ⟶ op (pullback f₁ f₂))
  (CategoryStruct.comp (Y := pushout.{v₁, u₁} (X := op T) (Y := op Y) (Z := op Z) g₁.op g₂.op) (pushout.inr g₁.op g₂.op)
      (CategoryStruct.comp (Y := pushout.{v₁, u₁} (X := op S) (Y := op W) (Z := op X) f₁.op f₂.op)
        (pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op sorry sorry) (Iso.hom (pushoutIsoOpPullback f₁.op f₂.op))) :
    op Z ⟶ op (pullback f₁ f₂))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ Eq (α := op (pushout g₁ g₂) ⟶ op (pushout f₁ f₂))
    (Quiver.Hom.op (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) : op (pushout g₁ g₂) ⟶ op (pushout f₁ f₂))
    (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := op Y) (Y := op Z) (Z := op T) g₁.op g₂.op)
        (Iso.inv (pullbackIsoOpPushout g₁.op g₂.op))
        (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
          (pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯) (Iso.hom (pullbackIsoOpPushout f₁.op f₂.op))) :
      op (pushout g₁.op.unop g₂.op.unop) ⟶ op (pushout f₁.op.unop f₂.op.unop))
have rw : Eq (α := op (pushout g₁ g₂) ⟶ pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
  (Quiver.Hom.op (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) ≫ Iso.inv (pullbackIsoOpPushout f₁.op f₂.op) :
    op (pushout g₁ g₂) ⟶ pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
  (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := op Y) (Y := op Z) (Z := op T) g₁.op g₂.op)
      (Iso.inv (pullbackIsoOpPushout g₁.op g₂.op)) (pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op sorry sorry) :
    op (pushout g₁.op.unop g₂.op.unop) ⟶ pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
Tactic: rw [← Category.assoc, ← Iso.comp_inv_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ Eq (α := op (pushout g₁ g₂) ⟶ pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
    (Quiver.Hom.op (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) ≫ Iso.inv (pullbackIsoOpPushout f₁.op f₂.op) :
      op (pushout g₁ g₂) ⟶ pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
    (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := op Y) (Y := op Z) (Z := op T) g₁.op g₂.op)
        (Iso.inv (pullbackIsoOpPushout g₁.op g₂.op)) (pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯) :
      op (pushout g₁.op.unop g₂.op.unop) ⟶ pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
have h₀ : Eq (α := op (pushout g₁ g₂) ⟶ op W)
  (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
      (Quiver.Hom.op (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) ≫ Iso.inv (pullbackIsoOpPushout f₁.op f₂.op))
      (pullback.fst f₁.op f₂.op) :
    op (pushout g₁ g₂) ⟶ op W)
  (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
      (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := op Y) (Y := op Z) (Z := op T) g₁.op g₂.op)
        (Iso.inv (pullbackIsoOpPushout g₁.op g₂.op)) (pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op sorry sorry))
      (pullback.fst f₁.op f₂.op) :
    op (pushout g₁ g₂) ⟶ op W)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
h₀ :
  Eq (α := op (pushout g₁ g₂) ⟶ op W)
    (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
        (Quiver.Hom.op (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) ≫ Iso.inv (pullbackIsoOpPushout f₁.op f₂.op))
        (pullback.fst f₁.op f₂.op) :
      op (pushout g₁ g₂) ⟶ op W)
    (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
        (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := op Y) (Y := op Z) (Z := op T) g₁.op g₂.op)
          (Iso.inv (pullbackIsoOpPushout g₁.op g₂.op)) (pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯))
        (pullback.fst f₁.op f₂.op) :
      op (pushout g₁ g₂) ⟶ op W)
⊢ Eq (α := op (pushout g₁ g₂) ⟶ pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
    (Quiver.Hom.op (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) ≫ Iso.inv (pullbackIsoOpPushout f₁.op f₂.op) :
      op (pushout g₁ g₂) ⟶ pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
    (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := op Y) (Y := op Z) (Z := op T) g₁.op g₂.op)
        (Iso.inv (pullbackIsoOpPushout g₁.op g₂.op)) (pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯) :
      op (pushout g₁.op.unop g₂.op.unop) ⟶ pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
have h₁ : Eq (α := op (pushout g₁ g₂) ⟶ op X)
  (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
      (Quiver.Hom.op (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) ≫ Iso.inv (pullbackIsoOpPushout f₁.op f₂.op))
      (pullback.snd f₁.op f₂.op) :
    op (pushout g₁ g₂) ⟶ op X)
  (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
      (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := op Y) (Y := op Z) (Z := op T) g₁.op g₂.op)
        (Iso.inv (pullbackIsoOpPushout g₁.op g₂.op)) (pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op sorry sorry))
      (pullback.snd f₁.op f₂.op) :
    op (pushout g₁ g₂) ⟶ op X)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (hypothesis)
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasIterationOfShape.{w, v, u} J C
α : Type u_1
inst_3 : PartialOrder α
h : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
hα : Order.IsSuccLimit (h.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C
have this : HasColimitsOfShape.{w, w, v, u}
  (↑(Set.Iio (h.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))) : Type w) C
Tactic: have := hasColimitsOfShape_of_isSuccLimit C h.top hα
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (hypothesis)
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
K : Type u'
inst_2 : Category.{v', u'} K
inst_3 : HasIterationOfShape.{w, v, u} J C
j : J
hj : Order.IsSuccLimit j
⊢ HasColimitsOfShape (↑(Set.Iio j) : Type w) (Arrow.{v, u} C)
have this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio j) : Type w) C
Tactic: have := hasColimitsOfShape_of_isSuccLimit C j hj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (hypothesis)
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
K : Type u'
inst_2 : Category.{v', u'} K
inst_3 : HasIterationOfShape.{w, v, u} J C
j : J
hj : Order.IsSuccLimit j
⊢ HasColimitsOfShape (↑(Set.Iio j) : Type w) (Functor.{v', v, u', u} K C)
have this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio j) : Type w) C
Tactic: have := hasColimitsOfShape_of_isSuccLimit C j hj