-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : C ⥤ FintypeCat
inst_2 : FiberFunctor F
X A : C
a : (F.obj A).obj
isGalois : IsGalois.{u₁, u₂} A
B : C
b : (F.obj B).obj
isGalois_1 : IsGalois.{u₁, u₂} B
u : A ⟶ X
v : B ⟶ X
h :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map u) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map v) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        b :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
Z : C
z : (F.obj Z).obj
isGalois_2 : IsGalois.{u₁, u₂} Z
f :
  (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 : PointedGaloisObject F })).obj ⟶
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F })).obj
hf :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map f) :
        (a_1 :
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (F.obj (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 })).obj)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (F.obj (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).obj))
      (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 : PointedGaloisObject F })).pt =
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F })).pt
h_1 : True
g :
  (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 : PointedGaloisObject F })).obj ⟶
    (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ : PointedGaloisObject F })).obj
hg :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map g) :
        (a :
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (F.obj (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 })).obj)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (F.obj (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).obj))
      (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 : PointedGaloisObject F })).pt =
    (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ : PointedGaloisObject F })).pt
refine_2 :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map f ≫ F.map u) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 })).obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map (g ≫ v)) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 })).obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
refine_2₁ :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map u) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                _ _ _ (F.map f) :
              (a_1 :
                  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                    (F.obj (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 })).obj)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                  (F.obj (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).obj))
            z :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (F.obj (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F })).obj)) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map (g ≫ v)) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 })).obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
refine_2₂ :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map u) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F })).pt :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map (g ≫ v)) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 })).obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map (f ≫ u)) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 })).obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map (g ≫ v)) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 })).obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
have refine_2₃ : Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
  ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map u) :
        (a :
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (F.obj (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := sorry })).obj)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := sorry : PointedGaloisObject F })).pt :
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
  ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map g ≫ F.map v) :
        (a :
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (F.obj (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 })).obj)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      z :
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
Tactic: rw [map_comp, FintypeCat.comp_apply, hf, map_comp, FintypeCat.comp_apply, hg, h]