awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Eq (α := (span f g ⋙ F).obj none ⟶ (span (F.map f) (F.map g)).obj none)
    ((span f g ⋙ F).map (WidePushoutShape.Hom.id none) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f g ⋙ F).obj x ≅ (span (F.map f) (F.map g)).obj x) none
          (Iso.refl ((span f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f g ⋙ F).obj (some x) ≅ (span (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f g ⋙ F).obj x ≅ (span (F.map f) (F.map g)).obj x) none
          (Iso.refl ((span f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f g ⋙ F).obj (some x) ≅ (span (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (F.map f) (F.map g)).map (WidePushoutShape.Hom.id none))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Eq (α := (span f g ⋙ F).obj none ⟶ (span (F.map f) (F.map g)).obj (some WalkingPair.left))
    ((span f g ⋙ F).map (init WalkingPair.left) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f g ⋙ F).obj x ≅ (span (F.map f) (F.map g)).obj x)
          (some WalkingPair.left) (Iso.refl ((span f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f g ⋙ F).obj (some x) ≅ (span (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f g ⋙ F).obj x ≅ (span (F.map f) (F.map g)).obj x) none
          (Iso.refl ((span f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f g ⋙ F).obj (some x) ≅ (span (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (F.map f) (F.map g)).map (init WalkingPair.left))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Eq (α := (span f g ⋙ F).obj none ⟶ (span (F.map f) (F.map g)).obj (some WalkingPair.right))
    ((span f g ⋙ F).map (init WalkingPair.right) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f g ⋙ F).obj x ≅ (span (F.map f) (F.map g)).obj x)
          (some WalkingPair.right) (Iso.refl ((span f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f g ⋙ F).obj (some x) ≅ (span (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f g ⋙ F).obj x ≅ (span (F.map f) (F.map g)).obj x) none
          (Iso.refl ((span f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f g ⋙ F).obj (some x) ≅ (span (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (F.map f) (F.map g)).map (init WalkingPair.right))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Eq (α := (span f g ⋙ F).obj (some WalkingPair.left) ⟶ (span (F.map f) (F.map g)).obj (some WalkingPair.left))
    ((span f g ⋙ F).map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f g ⋙ F).obj x ≅ (span (F.map f) (F.map g)).obj x)
          (some WalkingPair.left) (Iso.refl ((span f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f g ⋙ F).obj (some x) ≅ (span (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f g ⋙ F).obj x ≅ (span (F.map f) (F.map g)).obj x)
          (some WalkingPair.left) (Iso.refl ((span f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f g ⋙ F).obj (some x) ≅ (span (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (F.map f) (F.map g)).map (WidePushoutShape.Hom.id (some WalkingPair.left)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Eq (α := (span f g ⋙ F).obj (some WalkingPair.right) ⟶ (span (F.map f) (F.map g)).obj (some WalkingPair.right))
    ((span f g ⋙ F).map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f g ⋙ F).obj x ≅ (span (F.map f) (F.map g)).obj x)
          (some WalkingPair.right) (Iso.refl ((span f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f g ⋙ F).obj (some x) ≅ (span (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f g ⋙ F).obj x ≅ (span (F.map f) (F.map g)).obj x)
          (some WalkingPair.right) (Iso.refl ((span f g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f g ⋙ F).obj (some x) ≅ (span (F.map f) (F.map g)).obj (some x)) val
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (F.map f) (F.map g)).map (WidePushoutShape.Hom.id (some WalkingPair.right)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (spanCompIso F f g).app WalkingSpan.left = Iso.refl ((span f g ⋙ F).obj WalkingSpan.left)

Tactic:
rfl

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (spanCompIso F f g).app WalkingSpan.right = Iso.refl ((span f g ⋙ F).obj WalkingSpan.right)

Tactic:
rfl

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (spanCompIso F f g).app WalkingSpan.zero = Iso.refl ((span f g ⋙ F).obj WalkingSpan.zero)

Tactic:
rfl

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (spanCompIso F f g).hom.app WalkingSpan.left = 𝟙 ((span f g ⋙ F).obj WalkingSpan.left)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (spanCompIso F f g).hom.app WalkingSpan.right = 𝟙 ((span f g ⋙ F).obj WalkingSpan.right)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (spanCompIso F f g).hom.app WalkingSpan.zero = 𝟙 ((span f g ⋙ F).obj WalkingSpan.zero)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (spanCompIso F f g).inv.app WalkingSpan.left = 𝟙 ((span (F.map f) (F.map g)).obj WalkingSpan.left)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (spanCompIso F f g).inv.app WalkingSpan.right = 𝟙 ((span (F.map f) (F.map g)).obj WalkingSpan.right)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (spanCompIso F f g).inv.app WalkingSpan.zero = 𝟙 ((span (F.map f) (F.map g)).obj WalkingSpan.zero)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : Functor.{0, v, 0, u} WalkingCospan C
z : F.obj WalkingCospan.one ⟶ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ⟶ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ⟶ G.obj WalkingCospan.right
hl : F.map inl ≫ z = l ≫ G.map inl
hr : F.map inr ≫ z = r ≫ G.map inr
⊢ F.obj none ⟶ G.obj none

Tactic:
exacts [z, l, r]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : Functor.{0, v, 0, u} WalkingCospan C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ F.obj none ≅ G.obj none

Tactic:
exacts [z, l, r]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).app WalkingCospan.left = iX

Tactic:
rfl

Premises used: CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).app WalkingCospan.right = iY

Tactic:
rfl

Premises used: CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).app WalkingCospan.one = iZ

Tactic:
rfl

Premises used: CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.left = iX.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.right = iY.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.one = iZ.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.left = iX.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.right = iY.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.one = iZ.inv

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : Functor.{0, v, 0, u} WalkingSpan C
z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right
hl : F.map fst ≫ l = z ≫ G.map fst
hr : F.map snd ≫ r = z ≫ G.map snd
⊢ F.obj none ⟶ G.obj none

Tactic:
exacts [z, l, r]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : Functor.{0, v, 0, u} WalkingSpan C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ F.obj none ≅ G.obj none

Tactic:
exacts [z, l, r]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).app WalkingSpan.left = iY

Tactic:
rfl

Premises used: CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).app WalkingSpan.right = iZ

Tactic:
rfl

Premises used: CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).app WalkingSpan.zero = iX

Tactic:
rfl

Premises used: CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).hom.app WalkingSpan.left = iY.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).hom.app WalkingSpan.right = iZ.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).hom.app WalkingSpan.zero = iX.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).inv.app WalkingSpan.left = iY.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).inv.app WalkingSpan.right = iZ.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).inv.app WalkingSpan.zero = iX.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
h₁ :
  Eq (α := equalizer f g ⟶ Y) (CategoryStruct.comp (Y := prod.{v, u} Y Y) (equalizer.ι f g ≫ prod.lift f g) prod.fst)
    (CategoryStruct.comp (Y := prod.{v, u} Y Y) ((equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)) prod.fst)
h₂ :
  Eq (α := equalizer f g ⟶ Y) (CategoryStruct.comp (Y := prod.{v, u} Y Y) (equalizer.ι f g ≫ prod.lift f g) prod.snd)
    (CategoryStruct.comp (Y := prod.{v, u} Y Y) ((equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)) prod.snd)
⊢ Eq (α := equalizer f g ⟶ prod.{v, u} Y Y) (equalizer.ι f g ≫ prod.lift f g)
    ((equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
⊢ Eq (α := equalizer f g ⟶ Y) (CategoryStruct.comp (Y := prod.{v, u} Y Y) (equalizer.ι f g ≫ prod.lift f g) prod.fst)
    (CategoryStruct.comp (Y := prod.{v, u} Y Y) ((equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)) prod.fst)

Tactic:
simp [equalizer.condition f g]

Premises used: CategoryTheory.Limits.equalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
⊢ Eq (α := equalizer f g ⟶ Y) (CategoryStruct.comp (Y := prod.{v, u} Y Y) (equalizer.ι f g ≫ prod.lift f g) prod.snd)
    (CategoryStruct.comp (Y := prod.{v, u} Y Y) ((equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)) prod.snd)

Tactic:
simp [equalizer.condition f g]

Premises used: CategoryTheory.Limits.equalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
refine_1 : (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))) → s.pt ⟶ equalizer f g
refine_2 :
  ∀ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))),
    CategoryStruct.comp (Y := equalizer f g) (equalizer.lift s.fst ⋯) (equalizer.ι f g) = s.fst
refine_3 :
  ∀ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))),
    CategoryStruct.comp (Y := equalizer f g) (equalizer.lift s.fst ⋯) (equalizer.ι f g ≫ f) = s.snd
refine_4 :
  ∀ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))) (m : s.pt ⟶ equalizer f g),
    m ≫ equalizer.ι f g = s.fst → m ≫ equalizer.ι f g ≫ f = s.snd → m = equalizer.lift s.fst ⋯
⊢ IsPullback (P := equalizer f g) (Z := prod.{v, u} Y Y) (equalizer.ι f g) (equalizer.ι f g ≫ f) (prod.lift f g)
    (prod.lift (𝟙 Y) (𝟙 Y))

Tactic:
refine ⟨⟨by ext <;> simp [equalizer.condition f g]⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
refine_1 : ∀ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))), s.fst ≫ f = s.fst ≫ g
⊢ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))) → s.pt ⟶ equalizer f g

Tactic:
refine fun s ↦ equalizer.lift s.fst ?_

Premises used: CategoryTheory.Limits.equalizer.lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ s.fst ≫ f = s.snd

Tactic:
simpa using congr($s.condition ≫ prod.fst)

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Limits.prod.fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ s.fst ≫ f = s.snd

Tactic:
have H₁ : s.fst ≫ f = s.snd := by simpa using congr($s.condition ≫ prod.fst)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
H₁ : s.fst ≫ f = s.snd
⊢ s.fst ≫ g = s.snd

Tactic:
simpa using congr($s.condition ≫ prod.snd)

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Limits.prod.snd