-- 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 (α := (obj (forget R) (P ⟹ B)).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
    ((GrothendieckTopology.yonedaEquiv (coherentTopology LightProfinite) :
          (a : (coherentTopology LightProfinite).yoneda.obj S ⟶ (forget R).obj (P ⟹ B)) →
            ((forget R).obj (P ⟹ B)).obj.obj (Opposite.op S))
        ((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))) :
      (obj (forget R) (P ⟹ B)).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
    ((GrothendieckTopology.yonedaEquiv (coherentTopology LightProfinite) :
          (a : (coherentTopology LightProfinite).yoneda.obj S ⟶ (forget R).obj (P ⟹ B)) →
            ((forget R).obj (P ⟹ B)).obj.obj (Opposite.op S))
        ((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)) :
      (obj (forget R) (P ⟹ B)).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
⊢ Eq (α := obj (GrothendieckTopology.yoneda (coherentTopology LightProfinite)) S ⟶ obj (forget R) (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)) :
      obj (GrothendieckTopology.yoneda (coherentTopology LightProfinite)) S ⟶ obj (forget R) (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) :
      obj (GrothendieckTopology.yoneda (coherentTopology LightProfinite)) S ⟶ obj (forget R) (P ⟹ B))

Tactic:
apply (coherentTopology LightProfinite.{u}).yonedaEquiv.injective