-- 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
f g : End F
A : PointedGaloisObject F
⊢ Eq.{u₂ + 1} (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj))
    ((fun (f : Aut A.obj) ↦
        ((@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.hom) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj))
            A.pt :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj)))
      ((AutGalois.π F A : (a : AutGalois F) → Aut A.obj) ((endEquivAutGalois F : (a : End F) → AutGalois F) (g ≫ f))))
    ((fun (f : Aut A.obj) ↦
        ((@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.hom) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj))
            A.pt :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj)))
      ((AutGalois.π F A : (a : AutGalois F) → Aut A.obj)
        (HMul.hMul (α := AutGalois F) (β := AutGalois F)
          ((endEquivAutGalois F : (a : End F) → AutGalois F) g : AutGalois F)
          ((endEquivAutGalois F : (a : End F) → AutGalois F) f : AutGalois F))))
have simp : Eq (α := (F.obj A.obj).obj)
  ((@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))
          _ _ _ (g.app A.obj ≫ f.app A.obj : F.obj A.obj ⟶ F.obj A.obj) :
        (a : (F.obj A.obj).obj) → (F.obj A.obj).obj)
      A.pt :
    (F.obj A.obj).obj)
  ((@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
              (CategoryStruct.comp (Y := A.obj)
                (Iso.hom
                  ((AutGalois.π F A : (a : AutGalois F) → Aut A.obj)
                    ((endEquivAutGalois F : (a : End F) → AutGalois F) f)))
                (Iso.hom
                  ((AutGalois.π F A : (a : AutGalois F) → Aut A.obj)
                    ((endEquivAutGalois F : (a : End F) → AutGalois F) g)))) :
            F.obj A.obj ⟶ F.obj A.obj) :
        (a : (F.obj A.obj).obj) → (F.obj A.obj).obj)
      A.pt :
    (F.obj A.obj).obj)
Tactic: simp only [map_mul, endEquivAutGalois_π, Aut.Aut_mul_def, NatTrans.comp_app, Iso.trans_hom]