-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem mapPair_equifibered {F F' : Discrete WalkingPair ⥤ C} (α : F ⟶ F') :
    NatTrans.Equifibered α

Proof state:
C : Type u
inst✝ : Category.{v, u} 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 })

Tactic:
simp only [Category.comp_id, Category.id_comp]

Result:
no goals

Proof state:
case mk.right.mk.up.up
C : Type u
inst✝ : Category.{v, u} C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (F.map { down := { down := ⋯ } }) (α.app { as := WalkingPair.right })
    (α.app { as := { as := WalkingPair.right }.as }) (F'.map { down := { down := ⋯ } })

Tactic:
dsimp

Result:
case mk.right.mk.up.up
C : Type u
inst✝ : Category.{v, u} C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (F.map { down := { down := ⋯ } }) (α.app { as := WalkingPair.right }) (α.app { as := WalkingPair.right })
    (F'.map { down := { down := ⋯ } })

Proof state:
case mk.right.mk.up.up
C : Type u
inst✝ : Category.{v, u} C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (F.map { down := { down := ⋯ } }) (α.app { as := WalkingPair.right }) (α.app { as := WalkingPair.right })
    (F'.map { down := { down := ⋯ } })

Tactic:
simp only [Discrete.functor_map_id]

Result:
case mk.right.mk.up.up
C : Type u
inst✝ : Category.{v, u} 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 }))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ NatTrans.Equifibered α

Tactic:
rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩

Result:
case mk.left.mk.up.up
C : Type u
inst✝ : Category.{v, u} C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (F.map { down := { down := ⋯ } }) (α.app { as := WalkingPair.left })
    (α.app { as := { as := WalkingPair.left }.as }) (F'.map { down := { down := ⋯ } })

case mk.right.mk.up.up
C : Type u
inst✝ : Category.{v, u} C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (F.map { down := { down := ⋯ } }) (α.app { as := WalkingPair.right })
    (α.app { as := { as := WalkingPair.right }.as }) (F'.map { down := { down := ⋯ } })

Proof state:
case mk.left.mk.up.up
C : Type u
inst✝ : Category.{v, u} C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (F.map { down := { down := ⋯ } }) (α.app { as := WalkingPair.left })
    (α.app { as := { as := WalkingPair.left }.as }) (F'.map { down := { down := ⋯ } })

case mk.right.mk.up.up
C : Type u
inst✝ : Category.{v, u} C
F F' : Discrete WalkingPair ⥤ C
α : F ⟶ F'
⊢ IsPullback (F.map { down := { down := ⋯ } }) (α.app { as := WalkingPair.right })
    (α.app { as := { as := WalkingPair.right }.as }) (F'.map { down := { down := ⋯ } })

Tactic:
all_goals
  dsimp; simp only [Discrete.functor_map_id]
  exact IsPullback.of_horiz_isIso ⟨by simp only [Category.comp_id, Category.id_comp]⟩

Result:
no goals

Proof state:
case mk.right.mk.up.up
C : Type u
inst✝ : Category.{v, u} 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 }))

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

Result:
no goals