case mk.left.mk.up.up
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (F.map { down := { down := (_ : { as := WalkingPair.left }.as = { as := WalkingPair.left }.as) } })
    (α.app { as := WalkingPair.left }) (α.app { as := { as := WalkingPair.left }.as })
    (F'.map { down := { down := (_ : { as := WalkingPair.left }.as = { as := WalkingPair.left }.as) } })

case mk.right.mk.up.up
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (F.map { down := { down := (_ : { as := WalkingPair.right }.as = { as := WalkingPair.right }.as) } })
    (α.app { as := WalkingPair.right }) (α.app { as := { as := WalkingPair.right }.as })
    (F'.map { down := { down := (_ : { as := WalkingPair.right }.as = { as := WalkingPair.right }.as) } })
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ NatTrans.Equifibered α
rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩
no goals
case mk.left.mk.up.up
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (F.map { down := { down := (_ : { as := WalkingPair.left }.as = { as := WalkingPair.left }.as) } })
    (α.app { as := WalkingPair.left }) (α.app { as := { as := WalkingPair.left }.as })
    (F'.map { down := { down := (_ : { as := WalkingPair.left }.as = { as := WalkingPair.left }.as) } })

case mk.right.mk.up.up
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (F.map { down := { down := (_ : { as := WalkingPair.right }.as = { as := WalkingPair.right }.as) } })
    (α.app { as := WalkingPair.right }) (α.app { as := { as := WalkingPair.right }.as })
    (F'.map { down := { down := (_ : { as := WalkingPair.right }.as = { as := WalkingPair.right }.as) } })
all_goals
  dsimp; simp only [Discrete.functor_map_id]
  exact IsPullback.of_horiz_isIso ⟨by simp only [Category.comp_id, Category.id_comp]⟩
case mk.right.mk.up.up
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (F.map { down := { down := (_ : WalkingPair.right = WalkingPair.right) } })
    (α.app { as := WalkingPair.right }) (α.app { as := WalkingPair.right })
    (F'.map { down := { down := (_ : WalkingPair.right = WalkingPair.right) } })
case mk.right.mk.up.up
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (F.map { down := { down := (_ : { as := WalkingPair.right }.as = { as := WalkingPair.right }.as) } })
    (α.app { as := WalkingPair.right }) (α.app { as := { as := WalkingPair.right }.as })
    (F'.map { down := { down := (_ : { as := WalkingPair.right }.as = { as := WalkingPair.right }.as) } })
dsimp
case mk.right.mk.up.up
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (𝟙 (F.obj { as := WalkingPair.right })) (α.app { as := WalkingPair.right })
    (α.app { as := WalkingPair.right }) (𝟙 (F'.obj { as := WalkingPair.right }))
case mk.right.mk.up.up
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (F.map { down := { down := (_ : WalkingPair.right = WalkingPair.right) } })
    (α.app { as := WalkingPair.right }) (α.app { as := WalkingPair.right })
    (F'.map { down := { down := (_ : WalkingPair.right = WalkingPair.right) } })
simp only [Discrete.functor_map_id]
no goals
case mk.right.mk.up.up
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (𝟙 (F.obj { as := WalkingPair.right })) (α.app { as := WalkingPair.right })
    (α.app { as := WalkingPair.right }) (𝟙 (F'.obj { as := WalkingPair.right }))
exact IsPullback.of_horiz_isIso ⟨by simp only [Category.comp_id, Category.id_comp]⟩
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ 𝟙 (F.obj { as := WalkingPair.right }) ≫ α.app { as := WalkingPair.right } =
    α.app { as := WalkingPair.right } ≫ 𝟙 (F'.obj { as := WalkingPair.right })
simp only [Category.comp_id, Category.id_comp]