case w
C✝ : Type u₁
inst✝³ : Category C✝
J : Type u_1
inst✝² : Category J
C : Type u_3
inst✝¹ : Category C
inst✝ : HasTerminal C
j : J
⊢ ∀ (j_1 : Discrete PEmpty),
    (limitConstTerminal.inv ≫ limit.π ((Functor.const J).obj (⊤_ C)) j) ≫ limit.π (Functor.empty C) j_1 =
      terminal.from (⊤_ C) ≫ limit.π (Functor.empty C) j_1
C✝ : Type u₁
inst✝³ : Category C✝
J : Type u_1
inst✝² : Category J
C : Type u_3
inst✝¹ : Category C
inst✝ : HasTerminal C
j : J
⊢ limitConstTerminal.inv ≫ limit.π ((Functor.const J).obj (⊤_ C)) j = terminal.from (⊤_ C)
apply Limits.limit.hom_ext
no goals
case w
C✝ : Type u₁
inst✝³ : Category C✝
J : Type u_1
inst✝² : Category J
C : Type u_3
inst✝¹ : Category C
inst✝ : HasTerminal C
j : J
⊢ ∀ (j_1 : Discrete PEmpty),
    (limitConstTerminal.inv ≫ limit.π ((Functor.const J).obj (⊤_ C)) j) ≫ limit.π (Functor.empty C) j_1 =
      terminal.from (⊤_ C) ≫ limit.π (Functor.empty C) j_1
aesop_cat