awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
⊢ BicartesianSq (W := 0) 0 0 b.inl b.inr

Tactic:
of_isPullback_isPushout (IsPullback.of_is_bilimit' h) (IsPushout.of_isBilimit h)

Premises used: CategoryTheory.BicartesianSq.of_isPullback_isPushout, CategoryTheory.IsPushout.of_isBilimit, CategoryTheory.IsPullback.of_is_bilimit'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
inst_3 : HasBinaryBiproduct.{v₁, u₁} X Y
⊢ BicartesianSq.{v₁, u₁} (W := BinaryBicone.pt.{v₁, u₁} (BinaryBiproduct.bicone X Y)) (Z := 0)
    (BinaryBicone.fst (BinaryBiproduct.bicone X Y)) (BinaryBicone.snd (BinaryBiproduct.bicone X Y)) 0 0

Tactic:
of_is_biproduct₁ (BinaryBiproduct.isBilimit X Y)

Premises used: CategoryTheory.BicartesianSq.of_is_biproduct₁, CategoryTheory.Limits.BinaryBiproduct.isBilimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
inst_3 : HasBinaryBiproduct.{v₁, u₁} X Y
⊢ BicartesianSq.{v₁, u₁} (C := C) (W := biprod.{v₁, u₁} X Y) (Z := 0) biprod.fst biprod.snd 0 0

Tactic:
convert! of_is_biproduct₁ (BinaryBiproduct.isBilimit X Y)

Premises used: CategoryTheory.BicartesianSq.of_is_biproduct₁, CategoryTheory.Limits.BinaryBiproduct.isBilimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
inst_3 : HasBinaryBiproduct.{v₁, u₁} X Y
⊢ BicartesianSq.{v₁, u₁} (W := 0) (Z := BinaryBicone.pt.{v₁, u₁} (BinaryBiproduct.bicone X Y)) 0 0
    (BinaryBicone.inl (BinaryBiproduct.bicone X Y)) (BinaryBicone.inr (BinaryBiproduct.bicone X Y))

Tactic:
of_is_biproduct₂ (BinaryBiproduct.isBilimit X Y)

Premises used: CategoryTheory.BicartesianSq.of_is_biproduct₂, CategoryTheory.Limits.BinaryBiproduct.isBilimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
inst_3 : HasBinaryBiproduct.{v₁, u₁} X Y
⊢ BicartesianSq.{v₁, u₁} (C := C) (W := 0) (X := X) (Y := Y) (Z := biprod.{v₁, u₁} X Y) 0 0 biprod.inl biprod.inr

Tactic:
convert! of_is_biproduct₂ (BinaryBiproduct.isBilimit X Y)

Premises used: CategoryTheory.BicartesianSq.of_is_biproduct₂, CategoryTheory.Limits.BinaryBiproduct.isBilimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
⊢ h.cone.fst = fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
⊢ h.cone.snd = snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
hP : IsPullback fst snd f g
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ hP.lift h k w ≫ fst = h

Tactic:
PullbackCone.IsLimit.lift_fst hP.isLimit h k w

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst, CategoryTheory.IsPullback.lift, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
hP : IsPullback fst snd f g
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ hP.lift h k w ≫ snd = k

Tactic:
PullbackCone.IsLimit.lift_snd hP.isLimit h k w

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd, CategoryTheory.IsPullback.lift, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
hP : IsPullback fst snd f g
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ hP.lift h k w ≫ fst = h

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
hP : IsPullback fst snd f g
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ hP.lift h k w ≫ snd = k

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
hP : IsPullback fst snd f g
W : C
k l : W ⟶ P
h₀ : k ≫ fst = l ≫ fst
h₁ : k ≫ snd = l ≫ snd
⊢ k = l

Tactic:
PullbackCone.IsLimit.hom_ext hP.isLimit h₀ h₁

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
h : IsLimit c
⊢ c.fst = Iso.hom (Iso.refl c.pt) ≫ (PullbackCone.mk c.fst c.snd ⋯).fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
h : IsLimit c
⊢ c.snd = Iso.hom (Iso.refl c.pt) ≫ (PullbackCone.mk c.fst c.snd ⋯).snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
w : CommSq fst snd f g
h : IsLimit w.cone
⊢ IsPullback fst snd f g

Tactic:
of_isLimit h

Premises used: CategoryTheory.IsPullback.of_isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Functor.{0, v₁, 0, u₁} WalkingCospan C
c : Cone D
hc : IsLimit c
⊢ c.π.app WalkingCospan.left ≫ D.map WalkingCospan.Hom.inl = c.π.app WalkingCospan.right ≫ D.map WalkingCospan.Hom.inr

Tactic:
simp_rw [Cone.w]

Premises used: CategoryTheory.Limits.Cone.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ IsPullback (P := pullback f g) (pullback.fst f g) (pullback.snd f g) f g

Tactic:
of_isLimit (limit.isLimit (cospan f g))

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.IsPullback.of_isLimit, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.cospan
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
P' : C
fst' : P' ⟶ X
snd' : P' ⟶ Y
h : IsPullback fst snd f g
h' : IsPullback fst' snd' f g
⊢ (isoIsPullback X Y h h').hom ≫ fst' = fst

Tactic:
IsLimit.conePointUniqueUpToIso_hom_comp h.isLimit h'.isLimit WalkingCospan.left

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.WalkingCospan.left, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
P' : C
fst' : P' ⟶ X
snd' : P' ⟶ Y
h : IsPullback fst snd f g
h' : IsPullback fst' snd' f g
⊢ (isoIsPullback X Y h h').hom ≫ snd' = snd

Tactic:
IsLimit.conePointUniqueUpToIso_hom_comp h.isLimit h'.isLimit WalkingCospan.right

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
P' : C
fst' : P' ⟶ X
snd' : P' ⟶ Y
h : IsPullback fst snd f g
h' : IsPullback fst' snd' f g
⊢ (isoIsPullback X Y h h').inv ≫ fst = fst'

Tactic:
simp only [Iso.inv_comp_eq, isoIsPullback_hom_fst]

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.IsPullback.isoIsPullback_hom_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
P' : C
fst' : P' ⟶ X
snd' : P' ⟶ Y
h : IsPullback fst snd f g
h' : IsPullback fst' snd' f g
⊢ (isoIsPullback X Y h h').inv ≫ snd = snd'

Tactic:
simp only [Iso.inv_comp_eq, isoIsPullback_hom_snd]

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.IsPullback.isoIsPullback_hom_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : HasPullback f g
dsimp :
  CategoryStruct.comp (Y := pullback f g)
      (Iso.inv
        (limit.isoLimitCone { cone := PullbackCone.mk fst snd ⋯, isLimit := h.isLimit : LimitCone (cospan f g) }))
      (pullback.fst f g) =
    fst
⊢ CategoryStruct.comp (Y := pullback f g) (Iso.hom h.isoPullback) (pullback.fst f g) = fst

Tactic:
dsimp [isoPullback, cone, CommSq.cone]

Premises used: CategoryTheory.CommSq.cone, CategoryTheory.IsPullback.isoPullback, CategoryTheory.IsPullback.cone
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : HasPullback f g
⊢ CategoryStruct.comp (Y := pullback f g)
      (Iso.inv
        (limit.isoLimitCone { cone := PullbackCone.mk fst snd ⋯, isLimit := h.isLimit : LimitCone (cospan f g) }))
      (pullback.fst f g) =
    fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : HasPullback f g
dsimp :
  CategoryStruct.comp (Y := pullback f g)
      (Iso.inv
        (limit.isoLimitCone { cone := PullbackCone.mk fst snd ⋯, isLimit := h.isLimit : LimitCone (cospan f g) }))
      (pullback.snd f g) =
    snd
⊢ CategoryStruct.comp (Y := pullback f g) (Iso.hom h.isoPullback) (pullback.snd f g) = snd

Tactic:
dsimp [isoPullback, cone, CommSq.cone]

Premises used: CategoryTheory.CommSq.cone, CategoryTheory.IsPullback.isoPullback, CategoryTheory.IsPullback.cone
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : HasPullback f g
⊢ CategoryStruct.comp (Y := pullback f g)
      (Iso.inv
        (limit.isoLimitCone { cone := PullbackCone.mk fst snd ⋯, isLimit := h.isLimit : LimitCone (cospan f g) }))
      (pullback.snd f g) =
    snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : HasPullback f g
⊢ Eq (α := pullback f g ⟶ X) (Iso.inv h.isoPullback ≫ fst) (pullback.fst f g)

Tactic:
simp [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : HasPullback f g
⊢ Eq (α := pullback f g ⟶ Y) (Iso.inv h.isoPullback ≫ snd) (pullback.snd f g)

Tactic:
simp [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
⊢ h.cocone.inl = inl

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
⊢ h.cocone.inr = inr

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
⊢ inl ≫ hP.desc h k w = h

Tactic:
PushoutCocone.IsColimit.inl_desc hP.isColimit h k w

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc, CategoryTheory.IsPushout.isColimit, CategoryTheory.IsPushout.desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
⊢ inr ≫ hP.desc h k w = k

Tactic:
PushoutCocone.IsColimit.inr_desc hP.isColimit h k w

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc, CategoryTheory.IsPushout.isColimit, CategoryTheory.IsPushout.desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
⊢ inl ≫ hP.desc h k w = h

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
⊢ inr ≫ hP.desc h k w = k

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
k l : P ⟶ W
h₀ : inl ≫ k = inl ≫ l
h₁ : inr ≫ k = inr ≫ l
⊢ k = l

Tactic:
PushoutCocone.IsColimit.hom_ext hP.isColimit h₀ h₁

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y : C
f : Z ⟶ X
g : Z ⟶ Y
c : PushoutCocone f g
h : IsColimit c
⊢ c.inl ≫ Iso.hom (Iso.refl c.pt) = (PushoutCocone.mk c.inl c.inr ⋯).inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y : C
f : Z ⟶ X
g : Z ⟶ Y
c : PushoutCocone f g
h : IsColimit c
⊢ c.inr ≫ Iso.hom (Iso.refl c.pt) = (PushoutCocone.mk c.inl c.inr ⋯).inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
w : CommSq f g inl inr
h : IsColimit w.cocone
⊢ IsPushout f g inl inr

Tactic:
of_isColimit h

Premises used: CategoryTheory.IsPushout.of_isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Functor.{0, v₁, 0, u₁} WalkingSpan C
c : Cocone D
hc : IsColimit c
⊢ D.map WalkingSpan.Hom.fst ≫ c.ι.app WalkingSpan.left = D.map WalkingSpan.Hom.snd ≫ c.ι.app WalkingSpan.right

Tactic:
simp_rw [Cocone.w]

Premises used: CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y : C
f : Z ⟶ X
g : Z ⟶ Y
inst_1 : HasPushout f g
⊢ IsPushout (P := pushout f g) f g (pushout.inl f g) (pushout.inr f g)

Tactic:
of_isColimit (colimit.isColimit (span f g))

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.IsPushout.of_isColimit, CategoryTheory.Limits.span, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
P' : C
inl' : X ⟶ P'
inr' : Y ⟶ P'
h : IsPushout f g inl inr
h' : IsPushout f g inl' inr'
⊢ inl ≫ (isoIsPushout X Y h h').hom = inl'

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom h.isColimit h'.isColimit WalkingSpan.left

Premises used: CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
P' : C
inl' : X ⟶ P'
inr' : Y ⟶ P'
h : IsPushout f g inl inr
h' : IsPushout f g inl' inr'
⊢ inr ≫ (isoIsPushout X Y h h').hom = inr'

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom h.isColimit h'.isColimit WalkingSpan.right

Premises used: CategoryTheory.Limits.WalkingSpan.right, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
P' : C
inl' : X ⟶ P'
inr' : Y ⟶ P'
h : IsPushout f g inl inr
h' : IsPushout f g inl' inr'
⊢ inl' ≫ (isoIsPushout X Y h h').inv = inl

Tactic:
simp only [Iso.comp_inv_eq, inl_isoIsPushout_hom]

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.IsPushout.inl_isoIsPushout_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
P' : C
inl' : X ⟶ P'
inr' : Y ⟶ P'
h : IsPushout f g inl inr
h' : IsPushout f g inl' inr'
⊢ inr' ≫ (isoIsPushout X Y h h').inv = inr

Tactic:
simp only [Iso.comp_inv_eq, inr_isoIsPushout_hom]

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.IsPushout.inr_isoIsPushout_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst_1 : HasPushout f g
dsimp :
  CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
      (Iso.hom
        (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk inl inr ⋯, isColimit := h.isColimit : ColimitCocone (span f g) })) =
    inl
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (Iso.inv h.isoPushout) = inl

Tactic:
dsimp [isoPushout, cocone, CommSq.cocone]

Premises used: CategoryTheory.IsPushout.isoPushout, CategoryTheory.IsPushout.cocone, CategoryTheory.CommSq.cocone
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst_1 : HasPushout f g
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
      (Iso.hom
        (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk inl inr ⋯, isColimit := h.isColimit : ColimitCocone (span f g) })) =
    inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst_1 : HasPushout f g
dsimp :
  CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
      (Iso.hom
        (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk inl inr ⋯, isColimit := h.isColimit : ColimitCocone (span f g) })) =
    inr
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (Iso.inv h.isoPushout) = inr

Tactic:
dsimp [isoPushout, cocone, CommSq.cocone]

Premises used: CategoryTheory.IsPushout.isoPushout, CategoryTheory.IsPushout.cocone, CategoryTheory.CommSq.cocone
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst_1 : HasPushout f g
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
      (Iso.hom
        (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk inl inr ⋯, isColimit := h.isColimit : ColimitCocone (span f g) })) =
    inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst_1 : HasPushout f g
⊢ Eq (α := X ⟶ pushout f g) (inl ≫ Iso.hom h.isoPushout) (pushout.inl f g)

Tactic:
simp [← Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst_1 : HasPushout f g
⊢ Eq (α := Y ⟶ pushout f g) (inr ≫ Iso.hom h.isoPushout) (pushout.inr f g)

Tactic:
simp [← Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
⊢ IsPullback snd fst g f

Tactic:
of_isLimit (PullbackCone.flipIsLimit h.isLimit)

Premises used: CategoryTheory.IsPullback.of_isLimit, CategoryTheory.Limits.PullbackCone.flipIsLimit, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
⊢ IsPullback fst snd f g ↔ IsPullback snd fst g f

Tactic:
⟨flip, flip⟩

Premises used: CategoryTheory.IsPullback.flip, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
⊢ IsPushout.{v₁, u₁} (C := Cᵒᵖ) (Z := Opposite.op Z) (X := Opposite.op Y) (Y := Opposite.op X) (P := Opposite.op P) g.op
    f.op snd.op fst.op

Tactic:
IsPushout.of_isColimit
    (IsColimit.ofIsoColimit (Limits.PullbackCone.isLimitEquivIsColimitOp h.flip.cone h.flip.isLimit)
      h.toCommSq.flip.coneOp)

Premises used: Quiver.Hom.op, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.CommSq.flip, CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitOp, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.toCommSq, CategoryTheory.IsPushout.of_isColimit, CategoryTheory.CommSq.coneOp, DFunLike.coe, CategoryTheory.IsPullback.cone, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : Cᵒᵖ
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback.{v₁, u₁} (C := Cᵒᵖ) (P := P) (X := X) (Y := Y) (Z := Z) fst snd f g
⊢ IsPushout g.unop f.unop snd.unop fst.unop

Tactic:
IsPushout.of_isColimit
    (IsColimit.ofIsoColimit
      (Limits.PullbackCone.isLimitEquivIsColimitUnop h.flip.cone h.flip.isLimit)
      h.toCommSq.flip.coneUnop)

Premises used: CategoryTheory.CommSq.coneUnop, Quiver.Hom.unop, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.CommSq.flip, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.toCommSq, CategoryTheory.IsPushout.of_isColimit, DFunLike.coe, CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitUnop, CategoryTheory.IsPullback.cone, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
⊢ IsPushout g f inr inl

Tactic:
of_isColimit (PushoutCocone.flipIsColimit h.isColimit)

Premises used: CategoryTheory.Limits.PushoutCocone.flipIsColimit, CategoryTheory.IsPushout.isColimit, CategoryTheory.IsPushout.of_isColimit