Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case refine_1
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cone D
hc : IsLimit c
j : J
inst✝ : (Over.forget j).Initial
this : Nonempty (Over j)
c'' : Cone
  (Over.lift (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)) :=
  Over.liftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯
hc'' : IsLimit c'' :=
  Over.isLimitLiftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯ ((Functor.Initial.isLimitWhiskerEquiv (Over.forget j) c).symm hc)
⊢ Over.lift (Over.forget j ⋙ D)
      (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom) ≅
    Over.post D

pp: case refine_2
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cone D
hc : IsLimit c
j : J
inst✝ : (Over.forget j).Initial
this : Nonempty (Over j)
c'' : Cone
  (Over.lift (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)) :=
  Over.liftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯
hc'' : IsLimit c'' :=
  Over.isLimitLiftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯ ((Functor.Initial.isLimitWhiskerEquiv (Over.forget j) c).symm hc)
⊢ (Cone.postcompose (Iso.hom ?refine_1)).obj c'' ≅ c.overPost j

Tactic:
· exact NatIso.ofComponents (fun k ↦ CategoryTheory.Over.isoMk (Iso.refl _))

Goal state after:
case refine_2
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cone D
hc : IsLimit c
j : J
inst✝ : (Over.forget j).Initial
this : Nonempty (Over j)
c'' : Cone
  (Over.lift (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)) :=
  Over.liftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯
hc'' : IsLimit c'' :=
  Over.isLimitLiftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯ ((Functor.Initial.isLimitWhiskerEquiv (Over.forget j) c).symm hc)
⊢ (Cone.postcompose
          (NatIso.ofComponents
              (fun k ↦
                Over.isoMk
                  (Iso.refl
                    ((Over.lift (Over.forget j ⋙ D)
                            (Functor.whiskerRight (Over.forgetCocone j).ι D ≫
                              (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)).obj
                        k).left)
                  ⋯)
              ⋯).hom).obj
      c'' ≅
    c.overPost j