[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : CostructuredArrow (const J) F
f : X✝ ⟶ Y✝
j : J
⊢ f.left ≫ NatTrans.app ((fun c => { pt := c.left, π := c.hom }) Y✝).π j =
    NatTrans.app ((fun c => { pt := c.left, π := c.hom }) X✝).π j
[PROOFSTEP]
convert congr_fun (congr_arg NatTrans.app f.w) j
[GOAL]
case h.e'_3.h.h.e'_7.h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : CostructuredArrow (const J) F
f : X✝ ⟶ Y✝
j : J
e_1✝ :
  (((fun c => { pt := c.left, π := c.hom }) X✝).pt ⟶ F.obj j) =
    (((const J).obj X✝.left).obj j ⟶ ((fromPUnit F).obj Y✝.right).obj j)
e_6✝ : F = (fromPUnit F).obj Y✝.right
⊢ ((fun c => { pt := c.left, π := c.hom }) X✝).π = X✝.hom ≫ (fromPUnit F).map f.right
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_3.h.h.e'_7.h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : CostructuredArrow (const J) F
f : X✝ ⟶ Y✝
j : J
e_1✝ :
  (((fun c => { pt := c.left, π := c.hom }) X✝).pt ⟶ F.obj j) =
    (((const J).obj X✝.left).obj j ⟶ ((fromPUnit F).obj Y✝.right).obj j)
e_6✝ : F = (fromPUnit F).obj Y✝.right
⊢ X✝.hom = X✝.hom ≫ 𝟙 F
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cone F
⊢ Function.LeftInverse
    (fun h s => { toInhabited := { default := IsTerminal.from h s }, uniq := (_ : ∀ (a : s ⟶ c), a = default) })
    fun h => IsTerminal.ofUnique c
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cone F
⊢ Function.RightInverse
    (fun h s => { toInhabited := { default := IsTerminal.from h s }, uniq := (_ : ∀ (a : s ⟶ c), a = default) })
    fun h => IsTerminal.ofUnique c
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : StructuredArrow F (const J)
f : X✝ ⟶ Y✝
j : J
⊢ NatTrans.app ((fun c => { pt := c.right, ι := c.hom }) X✝).ι j ≫ f.right =
    NatTrans.app ((fun c => { pt := c.right, ι := c.hom }) Y✝).ι j
[PROOFSTEP]
convert (congr_fun (congr_arg NatTrans.app f.w) j).symm
[GOAL]
case h.e'_3.h.h.e'_7.h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : StructuredArrow F (const J)
f : X✝ ⟶ Y✝
j : J
e_1✝ :
  (F.obj j ⟶ ((fun c => { pt := c.right, ι := c.hom }) Y✝).pt) =
    (((fromPUnit F).obj X✝.left).obj j ⟶ ((const J).obj Y✝.right).obj j)
e_5✝ : F = (fromPUnit F).obj X✝.left
⊢ ((fun c => { pt := c.right, ι := c.hom }) Y✝).ι = (fromPUnit F).map f.left ≫ Y✝.hom
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_3.h.h.e'_7.h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : StructuredArrow F (const J)
f : X✝ ⟶ Y✝
j : J
e_1✝ :
  (F.obj j ⟶ ((fun c => { pt := c.right, ι := c.hom }) Y✝).pt) =
    (((fromPUnit F).obj X✝.left).obj j ⟶ ((const J).obj Y✝.right).obj j)
e_5✝ : F = (fromPUnit F).obj X✝.left
⊢ Y✝.hom = 𝟙 F ≫ Y✝.hom
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ Function.LeftInverse
    (fun h s => { toInhabited := { default := IsInitial.to h s }, uniq := (_ : ∀ (a : c ⟶ s), a = default) }) fun h =>
    IsInitial.ofUnique c
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ Function.RightInverse
    (fun h s => { toInhabited := { default := IsInitial.to h s }, uniq := (_ : ∀ (a : c ⟶ s), a = default) }) fun h =>
    IsInitial.ofUnique c
[PROOFSTEP]
aesop_cat
