-- Mathlib/CategoryTheory/Galois/Prorepresentability.lean
theorem endEquivAutGalois_mul (f g : End F) :
    (endEquivAutGalois F) (g ≫ f) = (endEquivAutGalois F g) * (endEquivAutGalois F f)

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
A : PointedGaloisObject F
⊢ f.app A.obj (g.app A.obj A.pt) = (f.app A.obj ≫ F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom) A.pt

Tactic:
rw [← f.naturality, FintypeCat.comp_apply, endEquivAutGalois_π]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
A : PointedGaloisObject F
⊢ (g.app A.obj ≫ f.app A.obj) A.pt =
    F.map (((AutGalois.π F A) ((endEquivAutGalois F) f)).hom ≫ ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom) A.pt

Tactic:
simp only [map_comp, FintypeCat.comp_apply, endEquivAutGalois_π]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
A : PointedGaloisObject F
⊢ f.app A.obj (g.app A.obj A.pt) = F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom (f.app A.obj A.pt)

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
A : PointedGaloisObject F
⊢ (fun f => F.map f.hom A.pt) ((AutGalois.π F A) ((endEquivAutGalois F) (g ≫ f))) =
    (fun f => F.map f.hom A.pt) ((AutGalois.π F A) ((endEquivAutGalois F) g * (endEquivAutGalois F) f))

Tactic:
simp only [map_mul, endEquivAutGalois_π, Aut.Aut_mul_def, NatTrans.comp_app, Iso.trans_hom]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
A : PointedGaloisObject F
⊢ (g.app A.obj ≫ f.app A.obj) A.pt =
    F.map (((AutGalois.π F A) ((endEquivAutGalois F) f)).hom ≫ ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom) A.pt

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
⊢ (endEquivAutGalois F) (g ≫ f) = (endEquivAutGalois F) g * (endEquivAutGalois F) f

Tactic:
refine AutGalois.ext F (fun A ↦ evaluation_aut_injective_of_isConnected F A A.pt ?_)

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
A : PointedGaloisObject F
⊢ (fun f => F.map f.hom A.pt) ((AutGalois.π F A) ((endEquivAutGalois F) (g ≫ f))) =
    (fun f => F.map f.hom A.pt) ((AutGalois.π F A) ((endEquivAutGalois F) g * (endEquivAutGalois F) f))

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
A : PointedGaloisObject F
⊢ f.app A.obj (g.app A.obj A.pt) = F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom (f.app A.obj A.pt)

Tactic:
change f.app A (g.app A A.pt) =
  (f.app A ≫ F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom) A.pt

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
A : PointedGaloisObject F
⊢ f.app A.obj (g.app A.obj A.pt) = (f.app A.obj ≫ F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom) A.pt