-- Mathlib/CategoryTheory/Galois/Prorepresentability.lean
@[simp]
lemma endEquivSectionsFibers_π (f : End F) (A : PointedGaloisObject F) :
    (endEquivSectionsFibers F f).val A = f.app A A.pt

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ (((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f).app A.obj
      ((colimit.ι ((incl F).op ⋙ coyoneda) (Opposite.op A) ≫
            (colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).hom).app
        A.obj (𝟙 A.obj)) =
    f.app A.obj A.pt

Tactic:
simp

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ (((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f).app A.obj A.pt = 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 : End F
A : PointedGaloisObject F
⊢ (↑((Types.limitEquivSections (incl F ⋙ (F ⋙ FintypeCat.incl) ⋙ uliftFunctor.{u₁, u₂}))
            ((colimitCoyonedaHomIsoLimit' (incl F) (F ⋙ FintypeCat.incl)).hom
              ((colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).hom ≫
                ((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f)))
        A).down =
    f.app A.obj A.pt

Tactic:
erw [Types.limitEquivSections_apply]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ (limit.π (incl F ⋙ (F ⋙ FintypeCat.incl) ⋙ uliftFunctor.{u₁, u₂}) A
        ((colimitCoyonedaHomIsoLimit' (incl F) (F ⋙ FintypeCat.incl)).hom
          ((colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).hom ≫
            ((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f))).down =
    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 : End F
A : PointedGaloisObject F
⊢ ↑((endEquivSectionsFibers F) f) A = f.app A.obj A.pt

Tactic:
dsimp [endEquivSectionsFibers, Types.sectionsEquiv]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ (↑((Types.limitEquivSections (incl F ⋙ (F ⋙ FintypeCat.incl) ⋙ uliftFunctor.{u₁, u₂}))
            ((colimitCoyonedaHomIsoLimit' (incl F) (F ⋙ FintypeCat.incl)).hom
              ((colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).hom ≫
                ((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f)))
        A).down =
    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 : End F
A : PointedGaloisObject F
⊢ (limit.π (incl F ⋙ (F ⋙ FintypeCat.incl) ⋙ uliftFunctor.{u₁, u₂}) A
        ((colimitCoyonedaHomIsoLimit' (incl F) (F ⋙ FintypeCat.incl)).hom
          ((colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).hom ≫
            ((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f))).down =
    f.app A.obj A.pt

Tactic:
simp only [colimitCoyonedaHomIsoLimit'_π_apply, incl_obj, comp_obj, FintypeCat.incl_obj, op_obj,
  FunctorToTypes.comp]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ (((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f).app A.obj
      ((colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).hom.app A.obj
        ((colimit.ι ((incl F).op ⋙ coyoneda) (Opposite.op A)).app A.obj (𝟙 A.obj))) =
    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 : End F
A : PointedGaloisObject F
⊢ (((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f).app A.obj
      ((colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).hom.app A.obj
        ((colimit.ι ((incl F).op ⋙ coyoneda) (Opposite.op A)).app A.obj (𝟙 A.obj))) =
    f.app A.obj A.pt

Tactic:
change (((FullyFaithful.whiskeringRight (FullyFaithful.ofFullyFaithful
    FintypeCat.incl) C).homEquiv) f).app A
  (((colimit.ι _ _) ≫ (colimit.isoColimitCocone ⟨cocone F, isColimit F⟩).hom).app
    A _) = f.app A A.pt

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ (((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f).app A.obj
      ((colimit.ι ((incl F).op ⋙ coyoneda) (Opposite.op A) ≫
            (colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).hom).app
        A.obj (𝟙 A.obj)) =
    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 : End F
A : PointedGaloisObject F
⊢ (((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f).app A.obj A.pt = f.app A.obj A.pt

Tactic:
rfl

Result:
no goals