awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
inst_2 : HasPullback f g
simp : Eq (α := pullback f g ⟶ Z) ((pullback.fst f g ≫ f) ≫ i) ((pullback.snd f g ≫ g) ≫ i)
⊢ Eq (α := pullback f g ⟶ Z) (pullback.fst f g ≫ f ≫ i) (pullback.snd f g ≫ g ≫ i)

Tactic:
simp only [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
inst_2 : HasPullback f g
rw : Eq (α := pullback f g ⟶ W) (pullback.fst f g ≫ f) (pullback.snd f g ≫ g)
⊢ Eq (α := pullback f g ⟶ Z) ((pullback.fst f g ≫ f) ≫ i) ((pullback.snd f g ≫ g) ≫ i)

Tactic:
rw [cancel_mono]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
inst_2 : HasPullback f g
⊢ Eq (α := pullback f g ⟶ W) (pullback.fst f g ≫ f) (pullback.snd f g ≫ g)

Tactic:
apply pullback.condition

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
inst_2 : HasPullback f g
⊢ HasPullback (f ≫ i) (g ≫ i)

Tactic:
⟨⟨⟨_, pullbackIsPullbackOfCompMono f g i⟩⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Limits.pullbackIsPullbackOfCompMono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
⊢ HasPullback i (f ≫ i)

Tactic:
simpa only [Category.id_comp] using hasPullback_of_comp_mono (𝟙 Z) f i

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.hasPullback_of_comp_mono, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
⊢ Eq (α := limit (cospan (𝟙 Z ≫ i) (f ≫ i)) ⟶ (cospan (𝟙 Z ≫ i) (f ≫ i)).obj WalkingCospan.right)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (𝟙 Z ≫ i) (f ≫ i))
        (LimitCone.cone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (NatTrans.app
        (Cone.π
          (LimitCone.cone
            { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
              isLimit :=
                (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                  IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                    (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
        WalkingCospan.right))
    (limit.π (cospan (𝟙 Z ≫ i) (f ≫ i)) WalkingCospan.right)

Tactic:
have := limit.isoLimitCone_hom_π ⟨_, pullbackIsPullbackOfCompMono (𝟙 _) f i⟩ WalkingCospan.right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (𝟙 Z ≫ i) (f ≫ i)) ⟶ (cospan (𝟙 Z ≫ i) (f ≫ i)).obj WalkingCospan.right)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (𝟙 Z ≫ i) (f ≫ i))
        (LimitCone.cone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (NatTrans.app
        (Cone.π
          (LimitCone.cone
            { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
              isLimit :=
                (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                  IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                    (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
        WalkingCospan.right))
    (limit.π (cospan (𝟙 Z ≫ i) (f ≫ i)) WalkingCospan.right)
⊢ IsIso (X := limit (cospan (𝟙 Z ≫ i) (f ≫ i))) (limit.π (cospan (𝟙 Z ≫ i) (f ≫ i)) WalkingCospan.right)

Tactic:
(congrArg IsIso (show _ ≫ pullback.snd (𝟙 Z) f = _ from this)).mp inferInstance

Premises used: CategoryTheory.IsIso, congrArg, inferInstance, Eq.mp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (𝟙 Z ≫ i) (f ≫ i)) ⟶ (cospan (𝟙 Z ≫ i) (f ≫ i)).obj WalkingCospan.right)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (𝟙 Z ≫ i) (f ≫ i))
        (LimitCone.cone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (NatTrans.app
        (Cone.π
          (LimitCone.cone
            { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
              isLimit :=
                (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                  IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                    (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
        WalkingCospan.right))
    (limit.π (cospan (𝟙 Z ≫ i) (f ≫ i)) WalkingCospan.right)
h : i = 𝟙 Z ≫ i
h₁ : pullback i (f ≫ i) = limit (cospan (𝟙 Z ≫ i) (f ≫ i)) → i = 𝟙 Z ≫ i
⊢ IsIso (X := pullback i (f ≫ i)) (pullback.snd i (f ≫ i))

Tactic:
convert! (congrArg IsIso (show _ ≫ pullback.snd (𝟙 Z) f = _ from this)).mp inferInstance

Premises used: CategoryTheory.IsIso, congrArg, inferInstance, Eq.mp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (𝟙 Z ≫ i) (f ≫ i)) ⟶ (cospan (𝟙 Z ≫ i) (f ≫ i)).obj WalkingCospan.right)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (𝟙 Z ≫ i) (f ≫ i))
        (LimitCone.cone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (NatTrans.app
        (Cone.π
          (LimitCone.cone
            { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
              isLimit :=
                (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                  IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                    (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
        WalkingCospan.right))
    (limit.π (cospan (𝟙 Z ≫ i) (f ≫ i)) WalkingCospan.right)
⊢ i = 𝟙 Z ≫ i

Tactic:
(Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (𝟙 Z ≫ i) (f ≫ i)) ⟶ (cospan (𝟙 Z ≫ i) (f ≫ i)).obj WalkingCospan.right)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (𝟙 Z ≫ i) (f ≫ i))
        (LimitCone.cone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (NatTrans.app
        (Cone.π
          (LimitCone.cone
            { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
              isLimit :=
                (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                  IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                    (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
        WalkingCospan.right))
    (limit.π (cospan (𝟙 Z ≫ i) (f ≫ i)) WalkingCospan.right)
⊢ i = 𝟙 Z ≫ i

Tactic:
exact (Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (𝟙 Z ≫ i) (f ≫ i)) ⟶ (cospan (𝟙 Z ≫ i) (f ≫ i)).obj WalkingCospan.right)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (𝟙 Z ≫ i) (f ≫ i))
        (LimitCone.cone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (NatTrans.app
        (Cone.π
          (LimitCone.cone
            { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
              isLimit :=
                (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                  IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                    (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
        WalkingCospan.right))
    (limit.π (cospan (𝟙 Z ≫ i) (f ≫ i)) WalkingCospan.right)
e_3 : pullback i (f ≫ i) = limit (cospan (𝟙 Z ≫ i) (f ≫ i))
⊢ i = 𝟙 Z ≫ i

Tactic:
(Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (𝟙 Z ≫ i) (f ≫ i)) ⟶ (cospan (𝟙 Z ≫ i) (f ≫ i)).obj WalkingCospan.right)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (𝟙 Z ≫ i) (f ≫ i))
        (LimitCone.cone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (NatTrans.app
        (Cone.π
          (LimitCone.cone
            { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
              isLimit :=
                (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                  IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                    (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
        WalkingCospan.right))
    (limit.π (cospan (𝟙 Z ≫ i) (f ≫ i)) WalkingCospan.right)
e_3 : pullback i (f ≫ i) = limit (cospan (𝟙 Z ≫ i) (f ≫ i))
⊢ i = 𝟙 Z ≫ i

Tactic:
exact (Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
⊢ HasPullback (f ≫ i) i

Tactic:
simpa only [Category.id_comp] using hasPullback_of_comp_mono f (𝟙 Z) i

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.hasPullback_of_comp_mono, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
⊢ Eq (α := limit (cospan (f ≫ i) (𝟙 Z ≫ i)) ⟶ (cospan (f ≫ i) (𝟙 Z ≫ i)).obj WalkingCospan.left)
    (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                  (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) }) ≫
      { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit :=
                  (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                    IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                      (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) :
                LimitCone (cospan (f ≫ i) (𝟙 Z ≫ i)) }.cone.π.app
        WalkingCospan.left)
    (limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left)

Tactic:
have := limit.isoLimitCone_hom_π ⟨_, pullbackIsPullbackOfCompMono f (𝟙 _) i⟩ WalkingCospan.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (f ≫ i) (𝟙 Z ≫ i)) ⟶ (cospan (f ≫ i) (𝟙 Z ≫ i)).obj WalkingCospan.left)
    (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                  (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) }) ≫
      { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit :=
                  (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                    IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                      (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) :
                LimitCone (cospan (f ≫ i) (𝟙 Z ≫ i)) }.cone.π.app
        WalkingCospan.left)
    (limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left)
⊢ IsIso (X := limit (cospan (f ≫ i) (𝟙 Z ≫ i))) (limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left)

Tactic:
(congrArg IsIso (show _ ≫ pullback.fst f (𝟙 Z) = _ from this)).mp inferInstance

Premises used: CategoryTheory.IsIso, congrArg, inferInstance, Eq.mp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (f ≫ i) (𝟙 Z ≫ i)) ⟶ (cospan (f ≫ i) (𝟙 Z ≫ i)).obj WalkingCospan.left)
    (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                  (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) }) ≫
      { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit :=
                  (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                    IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                      (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) :
                LimitCone (cospan (f ≫ i) (𝟙 Z ≫ i)) }.cone.π.app
        WalkingCospan.left)
    (limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left)
h : i = 𝟙 Z ≫ i
h₁ : pullback (f ≫ i) i = limit (cospan (f ≫ i) (𝟙 Z ≫ i)) → i = 𝟙 Z ≫ i
⊢ IsIso (X := pullback (f ≫ i) i) (pullback.fst (f ≫ i) i)

Tactic:
convert! (congrArg IsIso (show _ ≫ pullback.fst f (𝟙 Z) = _ from this)).mp inferInstance

Premises used: CategoryTheory.IsIso, congrArg, inferInstance, Eq.mp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (f ≫ i) (𝟙 Z ≫ i)) ⟶ (cospan (f ≫ i) (𝟙 Z ≫ i)).obj WalkingCospan.left)
    (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                  (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) }) ≫
      { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit :=
                  (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                    IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                      (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) :
                LimitCone (cospan (f ≫ i) (𝟙 Z ≫ i)) }.cone.π.app
        WalkingCospan.left)
    (limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left)
⊢ i = 𝟙 Z ≫ i

Tactic:
(Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (f ≫ i) (𝟙 Z ≫ i)) ⟶ (cospan (f ≫ i) (𝟙 Z ≫ i)).obj WalkingCospan.left)
    (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                  (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) }) ≫
      { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit :=
                  (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                    IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                      (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) :
                LimitCone (cospan (f ≫ i) (𝟙 Z ≫ i)) }.cone.π.app
        WalkingCospan.left)
    (limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left)
⊢ i = 𝟙 Z ≫ i

Tactic:
exact (Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (f ≫ i) (𝟙 Z ≫ i)) ⟶ (cospan (f ≫ i) (𝟙 Z ≫ i)).obj WalkingCospan.left)
    (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                  (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) }) ≫
      { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit :=
                  (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                    IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                      (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) :
                LimitCone (cospan (f ≫ i) (𝟙 Z ≫ i)) }.cone.π.app
        WalkingCospan.left)
    (limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left)
e_3 : pullback (f ≫ i) i = limit (cospan (f ≫ i) (𝟙 Z ≫ i))
⊢ i = 𝟙 Z ≫ i

Tactic:
(Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (f ≫ i) (𝟙 Z ≫ i)) ⟶ (cospan (f ≫ i) (𝟙 Z ≫ i)).obj WalkingCospan.left)
    (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                  (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) }) ≫
      { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit :=
                  (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                    IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                      (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) :
                LimitCone (cospan (f ≫ i) (𝟙 Z ≫ i)) }.cone.π.app
        WalkingCospan.left)
    (limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left)
e_3 : pullback (f ≫ i) i = limit (cospan (f ≫ i) (𝟙 Z ≫ i))
⊢ i = 𝟙 Z ≫ i

Tactic:
exact (Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
inst_1 : Mono f
⊢ HasPullback f f

Tactic:
⟨⟨⟨_, PullbackCone.isLimitMkIdId f⟩⟩⟩

Premises used: CategoryTheory.Limits.PullbackCone.isLimitMkIdId, Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
t : PullbackCone f f
⊢ t.fst = t.snd

Tactic:
(cancel_mono f).1 t.condition

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.cancel_mono, Iff.mp