Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case w_fiber
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) := ⋯
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ eqToHom ⋯ ≫
      ((StructuredArrow.mk
              { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f }.fiber) }).hom ≫
          (pre F G).map { base := _root_.id (𝟙 bj), fiber := eqToHom ⋯ ≫ gfj }).fiber =
    (StructuredArrow.hom
        { left := { as := PUnit.unit }, right := { base := bj, fiber := fj },
          hom := { base := gbj, fiber := gfj } }).fiber

pp: case w_base
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) := ⋯
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ ((StructuredArrow.mk { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f }.fiber) }).hom ≫
        (pre F G).map { base := _root_.id (𝟙 bj), fiber := eqToHom ⋯ ≫ gfj }).base =
    (StructuredArrow.hom
        { left := { as := PUnit.unit }, right := { base := bj, fiber := fj },
          hom := { base := gbj, fiber := gfj } }).base

Tactic:
<;>

Goal state after:
case w_fiber
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) := ⋯
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ eqToHom ⋯ ≫
      ((StructuredArrow.mk
              { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f }.fiber) }).hom ≫
          (pre F G).map { base := _root_.id (𝟙 bj), fiber := eqToHom ⋯ ≫ gfj }).fiber =
    (StructuredArrow.hom
        { left := { as := PUnit.unit }, right := { base := bj, fiber := fj },
          hom := { base := gbj, fiber := gfj } }).fiber

case w_base
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) := ⋯
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ ((StructuredArrow.mk { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f }.fiber) }).hom ≫
        (pre F G).map { base := _root_.id (𝟙 bj), fiber := eqToHom ⋯ ≫ gfj }).base =
    (StructuredArrow.hom
        { left := { as := PUnit.unit }, right := { base := bj, fiber := fj },
          hom := { base := gbj, fiber := gfj } }).base