-- Module: Mathlib.Condensed.Light.InternallyProjective
Goal:
R : Type u
inst : CommRing R
A B P : LightCondMod R
S : LightProfinite
e : A ⟶ B
x : (↑((P ⟹ A).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u)
a :
  Eq (α :=
    tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
        (obj (free R) S.toCondensed) ⟶
      B)
    (MonoidalClosed.uncurry
        ((Equiv.symm
              (Adjunction.homEquiv (freeForgetAdjunction R)
                (obj (GrothendieckTopology.yoneda (coherentTopology LightProfinite)) S) (P ⟹ B)) :
            (a : (coherentTopology LightProfinite).yoneda.obj S ⟶ (forget R).obj (P ⟹ B)) →
              (free R).obj ((coherentTopology LightProfinite).yoneda.obj S) ⟶ P ⟹ B)
          ((Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology LightProfinite)) :
              (a : ((forget R).obj (P ⟹ B)).obj.obj (Opposite.op S)) →
                (coherentTopology LightProfinite).yoneda.obj S ⟶ (forget R).obj (P ⟹ B))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (X :=
                    (P ⟹ A).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
                    (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map (ihom P) e)) (Opposite.op S)) :
                  (a : (↑((P ⟹ A).obj.obj (Opposite.op S)) : Type u)) → (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u))
                x :
              (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) :
                Type u)))) :
      tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
          (obj (free R) (obj (GrothendieckTopology.yoneda (coherentTopology LightProfinite)) S)) ⟶
        B)
    (MonoidalClosed.uncurry
        ((Equiv.symm
              (Adjunction.homEquiv (freeForgetAdjunction R)
                (obj (GrothendieckTopology.yoneda (coherentTopology LightProfinite)) S) (P ⟹ B)) :
            (a : (coherentTopology LightProfinite).yoneda.obj S ⟶ (forget R).obj (P ⟹ B)) →
              (free R).obj ((coherentTopology LightProfinite).yoneda.obj S) ⟶ P ⟹ B)
          ((Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology LightProfinite)) :
                (a : ((forget R).obj (P ⟹ A)).obj.obj (Opposite.op S)) →
                  (coherentTopology LightProfinite).yoneda.obj S ⟶ (forget R).obj (P ⟹ A))
              x ≫
            CategoryTheory.Functor.map (forget R) (CategoryTheory.Functor.map (ihom P) e))) :
      tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
          (obj (free R) (obj (GrothendieckTopology.yoneda (coherentTopology LightProfinite)) S)) ⟶
        B)
⊢ Eq (α :=
    tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
        (obj (free R) S.toCondensed) ⟶
      B)
    ((ihomPoints R P B S : (a : (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u)) → P ⊗ (free R).obj S.toCondensed ⟶ B)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X :=
                (P ⟹ A).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
                (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map (ihom P) e)) (Opposite.op S)) :
              (a : (↑((P ⟹ A).obj.obj (Opposite.op S)) : Type u)) → (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u))
            x :
          (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u)) :
      tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
          (obj (free R) S.toCondensed) ⟶
        B)
    ((ihomPoints R P B S : (a : (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u)) → P ⊗ (free R).obj S.toCondensed ⟶ B)
        (((ihomPoints R P B S).symm :
              (a : P ⊗ (free R).obj S.toCondensed ⟶ B) → (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u))
            ((ihomPoints R P A S :
                  (a : (↑((P ⟹ A).obj.obj (Opposite.op S)) : Type u)) → P ⊗ (free R).obj S.toCondensed ⟶ A)
                x ≫
              e) :
          (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u)) :
      tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
          (obj (free R) S.toCondensed) ⟶
        B)

Tactic:
simp only [ihomPoints_apply, ← MonoidalClosed.uncurry_natural_right,
    ← Adjunction.homEquiv_naturality_right_symm, Equiv.apply_symm_apply]

Premises used: LightCondensed.ihomPoints_apply, Equiv.apply_symm_apply, CategoryTheory.MonoidalClosed.uncurry_natural_right, CategoryTheory.Adjunction.homEquiv_naturality_right_symm