awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
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
rw₃ rw₄ :
  HasColimit.{0, 0, v₁, u₁} (C := Cᵒᵖ) (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

Tactic:
rw [HasPullback, hasLimit_iff_of_iso (cospanUnop f g), hasLimit_inverse_equivalence_comp_iff,
    hasLimit_leftOp_iff_hasColimit]

Premises used: CategoryTheory.Limits.hasLimit_iff_of_iso, CategoryTheory.Limits.cospanUnop, CategoryTheory.Limits.HasPullback, CategoryTheory.Limits.hasLimit_leftOp_iff_hasColimit, CategoryTheory.Limits.hasLimit_inverse_equivalence_comp_iff
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
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
inst_2 rwa rwa₁ rwa₂ rwa₃ : HasPushout f g
⊢ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op Z) (Z := op X) f.op g.op

Tactic:
rwa [hasPullback_op_iff_hasPushout]

Premises used: CategoryTheory.Limits.hasPullback_op_iff_hasPushout
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
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
inst_2 rwa rwa₁ rwa₂ rwa₃ : HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ HasPullback f.unop g.unop

Tactic:
rwa [hasPullback_unop_iff_hasPushout]

Premises used: CategoryTheory.Limits.hasPullback_unop_iff_hasPushout
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst_1 : HasPushout f g
⊢ Eq.{v₁ + 1} (α :=
    (span f g).obj WalkingSpan.left ⟶
      Cocone.pt.{0, v₁, 0, u₁} (F := span f g) (PullbackCone.unop (limit.cone (cospan f.op g.op))))
    (NatTrans.app (Cocone.ι (PullbackCone.unop (limit.cone (cospan f.op g.op)))) WalkingSpan.left :
      (span f g).obj WalkingSpan.left ⟶
        obj.{0, v₁, 0, u₁}
          (obj (const WalkingSpan)
            (Cocone.pt.{0, v₁, 0, u₁} (F := span f g) (PullbackCone.unop (limit.cone (cospan f.op g.op)))))
          WalkingSpan.left)
    (Quiver.Hom.unop (pullback.fst f.op g.op))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst_1 : HasPushout f g
⊢ Eq.{v₁ + 1} (α :=
    (span f g).obj WalkingSpan.right ⟶
      Cocone.pt.{0, v₁, 0, u₁} (F := span f g) (PullbackCone.unop (limit.cone (cospan f.op g.op))))
    (NatTrans.app (Cocone.ι (PullbackCone.unop (limit.cone (cospan f.op g.op)))) WalkingSpan.right :
      (span f g).obj WalkingSpan.right ⟶
        obj.{0, v₁, 0, u₁}
          (obj (const WalkingSpan)
            (Cocone.pt.{0, v₁, 0, u₁} (F := span f g) (PullbackCone.unop (limit.cone (cospan f.op g.op)))))
          WalkingSpan.right)
    (Quiver.Hom.unop (pullback.snd f.op g.op))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst_1 : HasPushout f g
⊢ Eq (α := unop (op Z) ⟶ unop (op (pushout f g)))
    (Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f g)) ≫ pullback.fst f.op g.op))
    (Quiver.Hom.unop (Quiver.Hom.op (pushout.inl f g)))

Tactic:
simp [← pushoutIsoUnopPullback_inl_hom]

Premises used: CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst_1 : HasPushout f g
⊢ Eq (α := unop (op Y) ⟶ unop (op (pushout f g)))
    (Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f g)) ≫ pullback.snd f.op g.op))
    (Quiver.Hom.unop (Quiver.Hom.op (pushout.inr f g)))

Tactic:
simp [← pushoutIsoUnopPullback_inr_hom]

Premises used: CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : X ⟶ Y
inst_1 : HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Z) (Z := Y) f g
⊢ (PullbackCone.op (limit.cone (cospan f.unop g.unop))).ι.app WalkingSpan.left =
    Quiver.Hom.op (pullback.fst f.unop g.unop)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : X ⟶ Y
inst_1 : HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Z) (Z := Y) f g
⊢ (PullbackCone.op (limit.cone (cospan f.unop g.unop))).ι.app WalkingSpan.right =
    Quiver.Hom.op (pullback.snd f.unop g.unop)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : X ⟶ Y
inst_1 : HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Z) (Z := Y) f g
⊢ Eq (α := op (unop Z) ⟶ op (unop (pushout.{v₁, u₁} (X := X) (Y := Z) (Z := Y) f g)))
    (Quiver.Hom.op (Quiver.Hom.unop (Iso.inv (pushoutIsoOpPullback f g)) ≫ pullback.fst f.unop g.unop))
    (Quiver.Hom.op (Quiver.Hom.unop (pushout.inl f g)))

Tactic:
simp [← pushoutIsoOpPullback_inl_hom]

Premises used: CategoryTheory.Limits.pushoutIsoOpPullback_inl_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : X ⟶ Y
inst_1 : HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Z) (Z := Y) f g
⊢ Eq (α := op (unop Y) ⟶ op (unop (pushout.{v₁, u₁} (X := X) (Y := Z) (Z := Y) f g)))
    (Quiver.Hom.op (Quiver.Hom.unop (Iso.inv (pushoutIsoOpPullback f g)) ≫ pullback.snd f.unop g.unop))
    (Quiver.Hom.op (Quiver.Hom.unop (pushout.inr f g)))

Tactic:
simp [← pushoutIsoOpPullback_inr_hom]

Premises used: CategoryTheory.Limits.pushoutIsoOpPullback_inr_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_2 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_3 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Eq.{v₁ + 1} (α := op T ⟶ op W) (g₁.op ≫ i₁.op) (i₃.op ≫ f₁.op)

Tactic:
simp [eq₁, ← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_2 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_3 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Eq.{v₁ + 1} (α := op T ⟶ op X) (g₂.op ≫ i₂.op) (i₃.op ≫ f₂.op)

Tactic:
simp [eq₂, ← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
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₂
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 ⋯ ⋯) (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))
⊢ 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))

Tactic:
rw [Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
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₂))
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 ⋯ ⋯) (Iso.hom (pushoutIsoOpPullback f₁.op f₂.op))) :
      op Z ⟶ 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))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
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 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₂))

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
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 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 ⋯ ⋯) (Iso.hom (pushoutIsoOpPullback f₁.op f₂.op))) :
      op Z ⟶ op (pullback f₁ f₂))

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_2 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_3 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ Eq.{v₁ + 1} (α := op Y ⟶ op S) (g₁.op ≫ i₃.op) (i₁.op ≫ f₁.op)

Tactic:
simp [eq₁, ← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_2 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_3 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ Eq.{v₁ + 1} (α := op Z ⟶ op S) (g₂.op ≫ i₃.op) (i₂.op ≫ f₂.op)

Tactic:
simp [eq₂, ← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
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₂
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 ⋯ ⋯) :
      op (pushout g₁.op.unop g₂.op.unop) ⟶ pullback.{v₁, u₁} (X := op W) (Y := op X) (Z := op S) f₁.op f₂.op)
⊢ 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))

Tactic:
rw [← Category.assoc, ← Iso.comp_inv_eq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
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)
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 ⋯ ⋯))
        (pullback.snd f₁.op f₂.op) :
      op (pushout g₁ g₂) ⟶ op X)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
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 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)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
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 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 ⋯ ⋯))
        (pullback.snd f₁.op f₂.op) :
      op (pushout g₁ g₂) ⟶ op X)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ p.cone.op.inl ≫ Iso.hom (Iso.refl p.cone.op.pt) = ⋯.cocone.inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ p.cone.op.inr ≫ Iso.hom (Iso.refl p.cone.op.pt) = ⋯.cocone.inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ p.cocone.op.fst = Iso.hom (Iso.refl p.cocone.op.pt) ≫ ⋯.cone.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ p.cocone.op.snd = Iso.hom (Iso.refl p.cocone.op.pt) ≫ ⋯.cone.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq.{v_1, u_1} (C := Cᵒᵖ) (W := W) (X := X) (Y := Y) (Z := Z) f g h i
⊢ p.cone.unop.inl ≫ Iso.hom (Iso.refl p.cone.unop.pt) = ⋯.cocone.inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq.{v_1, u_1} (C := Cᵒᵖ) (W := W) (X := X) (Y := Y) (Z := Z) f g h i
⊢ p.cone.unop.inr ≫ Iso.hom (Iso.refl p.cone.unop.pt) = ⋯.cocone.inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq.{v_1, u_1} (C := Cᵒᵖ) (W := W) (X := X) (Y := Y) (Z := Z) f g h i
⊢ p.cocone.unop.fst = Iso.hom (Iso.refl p.cocone.unop.pt) ≫ ⋯.cone.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq.{v_1, u_1} (C := Cᵒᵖ) (W := W) (X := X) (Y := Y) (Z := Z) f g h i
⊢ p.cocone.unop.snd = Iso.hom (Iso.refl p.cocone.unop.pt) ≫ ⋯.cone.snd

Tactic:
simp