awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
h :
  CategoryStruct.comp (Y := equalizer lhs rhs)
        (CategoryStruct.comp (Y :=
          pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
          (pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯)
          (equalizer.lift
            (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯) ⋯))
        (equalizer.ι lhs rhs) ≫
      pullback.fst s v =
    (𝟙 (equalizer lhs rhs) ≫ equalizer.ι lhs rhs) ≫ pullback.fst s v
h₁ :
  CategoryStruct.comp (Y := equalizer lhs rhs)
        (CategoryStruct.comp (Y :=
          pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
          (pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯)
          (equalizer.lift
            (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯) ⋯))
        (equalizer.ι lhs rhs) ≫
      pullback.snd s v =
    (𝟙 (equalizer lhs rhs) ≫ equalizer.ι lhs rhs) ≫ pullback.snd s v
⊢ CategoryStruct.comp (Y := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
      (pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
        (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯)
      (equalizer.lift (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯)
        ⋯) =
    𝟙 (equalizer lhs rhs)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ CategoryStruct.comp (Y := equalizer lhs rhs)
        (CategoryStruct.comp (Y :=
          pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
          (pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯)
          (equalizer.lift
            (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯) ⋯))
        (equalizer.ι lhs rhs) ≫
      pullback.fst s v =
    (𝟙 (equalizer lhs rhs) ≫ equalizer.ι lhs rhs) ≫ pullback.fst s v

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ CategoryStruct.comp (Y := equalizer lhs rhs)
        (CategoryStruct.comp (Y :=
          pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
          (pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯)
          (equalizer.lift
            (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯) ⋯))
        (equalizer.ι lhs rhs) ≫
      pullback.snd s v =
    (𝟙 (equalizer lhs rhs) ≫ equalizer.ι lhs rhs) ≫ pullback.snd s v

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ CategoryStruct.comp (Y := equalizer f g)
      (CategoryStruct.comp (Y := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
        (CategoryStruct.comp (Y := equalizer lhs rhs)
          (equalizer.lift
            (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯) ⋯)
          (pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯))
        (pullback.fst (equalizer.ι f g) (pullback.fst s v)))
      (equalizer.ι f g) =
    (𝟙 (pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v)) ≫
        pullback.fst (equalizer.ι f g) (pullback.fst s v)) ≫
      equalizer.ι f g

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ CategoryStruct.comp (Y := pullback s v)
      (CategoryStruct.comp (Y := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
        (CategoryStruct.comp (Y := equalizer lhs rhs)
          (equalizer.lift
            (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯) ⋯)
          (pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯))
        (pullback.snd (equalizer.ι f g) (pullback.fst s v)))
      (pullback.fst s v) =
    (𝟙 (pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v)) ≫
        pullback.snd (equalizer.ι f g) (pullback.fst s v)) ≫
      pullback.fst s v

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ CategoryStruct.comp (Y := pullback s v)
      (CategoryStruct.comp (Y := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
        (CategoryStruct.comp (Y := equalizer lhs rhs)
          (equalizer.lift
            (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯) ⋯)
          (pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯))
        (pullback.snd (equalizer.ι f g) (pullback.fst s v)))
      (pullback.snd s v) =
    (𝟙 (pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v)) ≫
        pullback.snd (equalizer.ι f g) (pullback.fst s v)) ≫
      pullback.snd s v

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ Eq (α :=
    equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
        (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
      X)
    (CategoryStruct.comp (Y := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
        (Iso.hom (equalizerPullbackMapIso hf hg v) :
          equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
              (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
            pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
        (pullback.fst (equalizer.ι f g) (pullback.fst s v) ≫ equalizer.ι f g :
          pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ X) :
      equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
          (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
        X)
    (equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ≫ pullback.fst s v :
      equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
          (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
        X)

Tactic:
simp [equalizerPullbackMapIso]

Premises used: CategoryTheory.Limits.equalizerPullbackMapIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ Eq (α :=
    equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
        (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
      X)
    (CategoryStruct.comp (Y := pullback s v)
        (CategoryStruct.comp (Y :=
            pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
            (Iso.hom (equalizerPullbackMapIso hf hg v) :
              equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
                  (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
                pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
            (pullback.snd (equalizer.ι f g) (pullback.fst s v) :
              pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback s v) :
          equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
              (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
            pullback s v)
        (pullback.fst s v : pullback s v ⟶ X) :
      equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
          (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
        X)
    (equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ≫ pullback.fst s v :
      equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
          (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
        X)

Tactic:
simp [equalizerPullbackMapIso]

Premises used: CategoryTheory.Limits.equalizerPullbackMapIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ Eq (α :=
    equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
        (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
      T)
    (CategoryStruct.comp (Y := pullback s v)
        (CategoryStruct.comp (Y :=
            pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
            (Iso.hom (equalizerPullbackMapIso hf hg v) :
              equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
                  (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
                pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
            (pullback.snd (equalizer.ι f g) (pullback.fst s v) :
              pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback s v) :
          equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
              (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
            pullback s v)
        (pullback.snd s v : pullback s v ⟶ T) :
      equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
          (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
        T)
    (equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ≫ pullback.snd s v :
      equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
          (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
        T)

Tactic:
simp [equalizerPullbackMapIso]

Premises used: CategoryTheory.Limits.equalizerPullbackMapIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ X)
    (CategoryStruct.comp (Y :=
        equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
          (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯))
        (Iso.inv (equalizerPullbackMapIso hf hg v) :
          pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶
            equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
              (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯))
        (equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ≫
            pullback.fst s v :
          equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
              (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
            X) :
      pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ X)
    (pullback.fst (equalizer.ι f g) (pullback.fst s v) ≫ equalizer.ι f g :
      pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ X)

Tactic:
simp [equalizerPullbackMapIso]

Premises used: CategoryTheory.Limits.equalizerPullbackMapIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ T)
    (CategoryStruct.comp (Y :=
        equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
          (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯))
        (Iso.inv (equalizerPullbackMapIso hf hg v) :
          pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶
            equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
              (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯))
        (equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ≫
            pullback.snd s v :
          equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
              (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
            T) :
      pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ T)
    (pullback.snd (equalizer.ι f g) (pullback.fst s v) ≫ pullback.snd s v :
      pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ T)

Tactic:
simp [equalizerPullbackMapIso]

Premises used: CategoryTheory.Limits.equalizerPullbackMapIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
F G : Functor.{v_1, v_2, u_1, u_3} J C
α : F ⟶ G
inst_2 : IsIso α
⊢ Equifibered α

Tactic:
fun _ _ f => IsPullback.of_vert_isIso ⟨naturality _ f⟩

Premises used: CategoryTheory.IsPullback.of_vert_isIso, CategoryTheory.CommSq.mk, CategoryTheory.NatTrans.Equifibered, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
F G H : Functor.{v_1, v_2, u_1, u_3} J C
α : F ⟶ G
β : G ⟶ H
hα : Equifibered α
hβ : Equifibered β
⊢ Equifibered (α ≫ β)

Tactic:
fun _ _ f => (hα f).paste_vert (hβ f)

Premises used: CategoryTheory.NatTrans.Equifibered, CategoryTheory.IsPullback.paste_vert
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
⊢ MorphismProperty.RespectsIso (C := Functor.{v_1, v_2, u_1, u_3} J C) Equifibered

Tactic:
MorphismProperty.respectsIso_of_isStableUnderComposition fun _ _ ↦ .of_isIso

Premises used: CategoryTheory.NatTrans.Equifibered.of_isIso, CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_4, u_4} D
F G : Functor.{v_1, v_2, u_1, u_3} J C
α : F ⟶ G
hα : Equifibered α
H : Functor.{v_2, v_4, u_3, u_4} C D
inst_3 : ∀ (i j : J) (f : j ⟶ i), PreservesLimit (cospan (α.app i) (G.map f)) H
⊢ Equifibered (Functor.whiskerRight α H)

Tactic:
fun _ _ f => (hα f).map H

Premises used: CategoryTheory.NatTrans.Equifibered, CategoryTheory.IsPullback.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
F G : Functor.{v_1, v_2, u_1, u_3} J C
α : F ⟶ G
hα : Equifibered α
H : Functor.{v_3, v_1, u_2, u_1} K J
⊢ Equifibered (H.whiskerLeft α)

Tactic:
fun _ _ f => hα (H.map f)

Premises used: CategoryTheory.Functor.map, CategoryTheory.NatTrans.Equifibered
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
C : Type u_3
ι : Type u_5
inst : Category.{v_2, u_3} C
F G : Functor.{u_5, v_2, u_5, u_3} (Discrete ι) C
α : F ⟶ G
i : ι
simp :
  IsPullback (𝟙 (F.obj { as := i })) (α.app { as := i : Discrete ι }) (α.app { as := i : Discrete ι })
    (𝟙 (G.obj { as := i }))
⊢ IsPullback
    (F.map
      { down := { down := ⋯ : PLift ({ as := i : Discrete ι }.as = { as := i : Discrete ι }.as) } :
        ULift.{u_5, 0} (PLift ({ as := i : Discrete ι }.as = { as := i : Discrete ι }.as)) })
    (α.app { as := i }) (α.app { as := i })
    (G.map
      { down := { down := ⋯ : PLift ({ as := i : Discrete ι }.as = { as := i : Discrete ι }.as) } :
        ULift.{u_5, 0} (PLift ({ as := i : Discrete ι }.as = { as := i : Discrete ι }.as)) })

Tactic:
simp only [Discrete.functor_map_id]

Premises used: CategoryTheory.Discrete.functor_map_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
C : Type u_3
ι : Type u_5
inst : Category.{v_2, u_3} C
F G : Functor.{u_5, v_2, u_5, u_3} (Discrete ι) C
α : F ⟶ G
i : ι
rw : α.app { as := i } = α.app { as := i : Discrete ι } ≫ 𝟙 (G.obj { as := i : Discrete ι })
rw₁ rw₂ : Eq (α := F.obj { as := i : Discrete ι } ⟶ G.obj { as := i }) (α.app { as := i }) (α.app { as := i })
⊢ 𝟙 (F.obj { as := i : Discrete ι }) ≫ α.app { as := i : Discrete ι } =
    α.app { as := i : Discrete ι } ≫ 𝟙 (G.obj { as := i })

Tactic:
rw [Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
C : Type u_3
ι : Type u_5
inst : Category.{v_2, u_3} C
F G : Functor.{u_5, v_2, u_5, u_3} (Discrete ι) C
α : F ⟶ G
i : ι
⊢ IsPullback (𝟙 (F.obj { as := i })) (α.app { as := i : Discrete ι }) (α.app { as := i : Discrete ι })
    (𝟙 (G.obj { as := i }))

Tactic:
exact IsPullback.of_horiz_isIso ⟨by rw [Category.id_comp, Category.comp_id]⟩

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.IsPullback.of_horiz_isIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
F G : Functor.{v_1, v_2, u_1, u_3} J C
α : F ⟶ G
inst_2 : IsIso α
⊢ Coequifibered α

Tactic:
fun _ _ f => .of_vert_isIso ⟨naturality _ f⟩

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.NatTrans.naturality, CategoryTheory.IsPushout.of_vert_isIso, CategoryTheory.NatTrans.Coequifibered
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
F G H : Functor.{v_1, v_2, u_1, u_3} J C
α : F ⟶ G
β : G ⟶ H
hα : Coequifibered α
hβ : Coequifibered β
⊢ Coequifibered (α ≫ β)

Tactic:
fun _ _ f => (hα f).paste_vert (hβ f)

Premises used: CategoryTheory.IsPushout.paste_vert, CategoryTheory.NatTrans.Coequifibered
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
⊢ MorphismProperty.RespectsIso (C := Functor.{v_1, v_2, u_1, u_3} J C) Coequifibered

Tactic:
MorphismProperty.respectsIso_of_isStableUnderComposition fun _ _ ↦ .of_isIso

Premises used: CategoryTheory.NatTrans.Coequifibered.of_isIso, CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_4, u_4} D
F G : Functor.{v_1, v_2, u_1, u_3} J C
α : F ⟶ G
hα : Coequifibered α
H : Functor.{v_2, v_4, u_3, u_4} C D
inst_3 : ∀ (i j : J) (f : j ⟶ i), PreservesColimit (span (F.map f) (α.app j)) H
⊢ Coequifibered (Functor.whiskerRight α H)

Tactic:
fun _ _ f => (hα f).map H

Premises used: CategoryTheory.IsPushout.map, CategoryTheory.NatTrans.Coequifibered