Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
⊢ ∀ (j : WithTerminal J),
    ((Cone.postcompose
                  (NatIso.ofComponents
                      (fun i ↦
                        WithTerminal.casesOn i
                          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
                          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star)))
                      ⋯).hom).obj
              (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })).π.app
        j =
      (Iso.refl
            ((Cone.postcompose
                    (NatIso.ofComponents
                        (fun i ↦
                          WithTerminal.casesOn i
                            (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
                            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star)))
                        ⋯).hom).obj
                (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })).pt).hom ≫
        ((Over.forget F).mapCone
                { pt := G,
                  π :=
                    {
                      app := fun i ↦
                        WithTerminal.casesOn i α.app
                          (Over.mkIdTerminal.from (((const (WithTerminal J)).obj G).obj WithTerminal.star)),
                      naturality := ⋯ } }).π.app
          j

Tactic:
rintro ⟨⟩

Goal state after:
case of
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
a✝ : J
⊢ ((Cone.postcompose
                (NatIso.ofComponents
                    (fun i ↦
                      WithTerminal.casesOn i
                        (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
                        (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star)))
                    ⋯).hom).obj
            (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })).π.app
      (WithTerminal.of a✝) =
    (Iso.refl
          ((Cone.postcompose
                  (NatIso.ofComponents
                      (fun i ↦
                        WithTerminal.casesOn i
                          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
                          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star)))
                      ⋯).hom).obj
              (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })).pt).hom ≫
      ((Over.forget F).mapCone
              { pt := G,
                π :=
                  {
                    app := fun i ↦
                      WithTerminal.casesOn i α.app
                        (Over.mkIdTerminal.from (((const (WithTerminal J)).obj G).obj WithTerminal.star)),
                    naturality := ⋯ } }).π.app
        (WithTerminal.of a✝)

case star
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
⊢ ((Cone.postcompose
                (NatIso.ofComponents
                    (fun i ↦
                      WithTerminal.casesOn i
                        (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
                        (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star)))
                    ⋯).hom).obj
            (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })).π.app
      WithTerminal.star =
    (Iso.refl
          ((Cone.postcompose
                  (NatIso.ofComponents
                      (fun i ↦
                        WithTerminal.casesOn i
                          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
                          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star)))
                      ⋯).hom).obj
              (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })).pt).hom ≫
      ((Over.forget F).mapCone
              { pt := G,
                π :=
                  {
                    app := fun i ↦
                      WithTerminal.casesOn i α.app
                        (Over.mkIdTerminal.from (((const (WithTerminal J)).obj G).obj WithTerminal.star)),
                    naturality := ⋯ } }).π.app
        WithTerminal.star