-- 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
⊢ ∀ (j : (PointedGaloisObject F)ᵒᵖ)
    (xi :
      (fun (X : Type u₂) ↦ X)
        (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
          (Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F })))
    (xj :
      (fun (X : Type u₂) ↦ X)
        (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) j)),
    Eq (α :=
        (fun (X : Type u₂) ↦ X)
          (Functor.obj
            (Functor.obj (const (PointedGaloisObject F)ᵒᵖ)
              (Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (F :=
                (Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
                (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))))
            (Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F)))
                  (Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F })) :
              (a_1 :
                  (fun (X : Type u₂) ↦ X)
                    ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj
                      (Opposite.op { obj := A, pt := a, isGalois := isGalois }))) →
                (fun (X : Type u₂) ↦ X)
                  (((const (PointedGaloisObject F)ᵒᵖ).obj
                        (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
                    (Opposite.op { obj := A, pt := a, isGalois := isGalois })))
            xi :
          (fun (X : Type u₂) ↦ X)
            (Functor.obj
              (Functor.obj (const (PointedGaloisObject F)ᵒᵖ)
                (Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (F :=
                  (Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
                  (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))))
              (Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))) j) :
              (a : (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj j)) →
                (fun (X : Type u₂) ↦ X)
                  (((const (PointedGaloisObject F)ᵒᵖ).obj
                        (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
                    j))
            xj :
          (fun (X : Type u₂) ↦ X)
            (Functor.obj
              (Functor.obj (const (PointedGaloisObject F)ᵒᵖ)
                (Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (F :=
                  (Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
                  (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))))
              j)) →
      ∃ (k : (PointedGaloisObject F)ᵒᵖ) (f :
        Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F } ⟶ k) (g : j ⟶ k),
        Eq (α :=
          (fun (X : Type u₂) ↦ X)
            (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (map ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) f) :
                (a :
                    (fun (X : Type u₂) ↦ X)
                      ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj
                        (Opposite.op { obj := A, pt := a, isGalois := isGalois }))) →
                  (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj k))
              xi :
            (fun (X : Type u₂) ↦ X)
              (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (map ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) g) :
                (a : (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj j)) →
                  (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj k))
              xj :
            (fun (X : Type u₂) ↦ X)
              (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) k))
have refine_2 : ∀ (B : C) (b : (F.obj B).obj) (isGalois_1 : IsGalois.{u₁, u₂} B)
  (xi :
    (fun (X : Type u₂) ↦ X)
      (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
        (Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F })))
  (xj :
    (fun (X : Type u₂) ↦ X)
      (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
        (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F }))),
  Eq (α :=
      (fun (X : Type u₂) ↦ X)
        (Functor.obj
          (Functor.obj (const (PointedGaloisObject F)ᵒᵖ)
            (Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (F :=
              (Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
              (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))))
          (Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F)))
                (Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F })) :
            (a_1 :
                (fun (X : Type u₂) ↦ X)
                  ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj
                    (Opposite.op { obj := A, pt := a, isGalois := isGalois }))) →
              (fun (X : Type u₂) ↦ X)
                (((const (PointedGaloisObject F)ᵒᵖ).obj (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
                  (Opposite.op { obj := A, pt := a, isGalois := isGalois })))
          xi :
        (fun (X : Type u₂) ↦ X)
          (Functor.obj
            (Functor.obj (const (PointedGaloisObject F)ᵒᵖ)
              (Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (F :=
                (Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
                (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))))
            (Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F)))
                (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F })) :
            (a :
                (fun (X : Type u₂) ↦ X)
                  ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj
                    (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 }))) →
              (fun (X : Type u₂) ↦ X)
                (((const (PointedGaloisObject F)ᵒᵖ).obj (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
                  (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 })))
          xj :
        (fun (X : Type u₂) ↦ X)
          (Functor.obj
            (Functor.obj (const (PointedGaloisObject F)ᵒᵖ)
              (Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (F :=
                (Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
                (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))))
            (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F }))) →
    ∃ (k : (PointedGaloisObject F)ᵒᵖ) (f :
      Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F } ⟶ k) (g :
      Opposite.op { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F } ⟶ k),
      Eq (α :=
        (fun (X : Type u₂) ↦ X)
          (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (map ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) f) :
              (a :
                  (fun (X : Type u₂) ↦ X)
                    ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj
                      (Opposite.op { obj := A, pt := a, isGalois := isGalois }))) →
                (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj k))
            xi :
          (fun (X : Type u₂) ↦ X)
            (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (map ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) g) :
              (a :
                  (fun (X : Type u₂) ↦ X)
                    ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj
                      (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 }))) →
                (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj k))
            xj :
          (fun (X : Type u₂) ↦ X)
            (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) k))
Tactic: ⟨B, b, _⟩