-- 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 x_1 : PointedGaloisObject F
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
Z : C
f : Z ⟶ Limits.prod.{u₂, u₁} A B
z : (F.obj Z).obj
hgal : IsGalois.{u₁, u₂} Z
hfz :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (Limits.prod.{u₂, u₁} A B)))
    ((@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 : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Z)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (A ⨯ B)))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (Limits.prod.{u₂, u₁} A B)))
    (((Equiv.symm (fiberBinaryProductEquiv F A B) :
            (F.obj A).obj × (F.obj B).obj ≃ (F.obj (Limits.prod.{u₂, u₁} A B)).obj) :
          (a : (F.obj A).obj × (F.obj B).obj) → (F.obj (A ⨯ B)).obj)
        (a, b) :
      (F.obj (Limits.prod.{u₂, u₁} A B)).obj)
refine_1 :
  (@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 ≫ prod.fst)) :
        (a_1 :
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (F.obj { obj := Z, pt := z, isGalois := hgal }.obj)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (F.obj { obj := A, pt := a, isGalois := isGalois }.obj))
      { obj := Z, pt := z, isGalois := hgal : PointedGaloisObject F }.pt =
    { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F }.pt
⊢ ∃ (W : PointedGaloisObject F) (x : W ⟶ { obj := A, pt := a, isGalois := isGalois }) (x :
    W ⟶ { obj := B, pt := b, isGalois := isGalois_1 }), True
have refine_2 : (@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 ≫ prod.snd)) :
      (a :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (F.obj { obj := Z, pt := z, isGalois := hgal }.obj)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (F.obj { obj := B, pt := b, isGalois := isGalois_1 }.obj))
    { obj := Z, pt := z, isGalois := hgal : PointedGaloisObject F }.pt =
  { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F }.pt
Tactic: refine ⟨⟨Z, z, hgal⟩, ⟨f ≫ prod.fst, ?_⟩, ⟨f ≫ prod.snd, ?_⟩, trivial⟩