-- Lean 4 proof step from Mathlib.Condensed.Light.InternallyProjective (hypothesis)
Goal:
R : Type u
inst : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u)
S' : LightProfinite
π : S' ⟶ S
hπ :
  Function.Surjective (α :=
    (fun
          (X :
            CompHausLike fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u))
      S')
    (β :=
    (fun
          (X :
            CompHausLike fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u))
      S)
    (⇑(ConcreteCategory.hom (FC :=
          fun
            (x1 x2 :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u)))
          (CC :=
          fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
          π) :
      (a :
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
              (↑X.toTop : Type u))
            S') →
        (fun
              (X :
                CompHausLike fun (X : TopCat) ↦
                  TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
            (↑X.toTop : Type u))
          S)
g' :
  tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
      (obj (free R) S'.toCondensed) ⟶
    A
hh :
  P ◁ CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫
      (ihomPoints R P B S : (a : (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u)) → P ⊗ (free R).obj S.toCondensed ⟶ B)
        g =
    g' ≫ e
⊢ Eq (α := (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u))
    (((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)
            (((ihomPoints R P A S').symm :
                  (a : P ⊗ (free R).obj S'.toCondensed ⟶ A) → (↑((P ⟹ A).obj.obj (Opposite.op S')) : Type u))
                g' :
              (↑((P ⟹ A).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) :
                Type u)) ≫
          e) :
      (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier)
            ((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map (Opposite.op π)) :
          (a : (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u)) → (↑((P ⟹ B).obj.obj (Opposite.op S')) : Type u))
        g :
      (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u))
have this : Eq (α := (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u))
  (((ihomPoints R P B S').symm :
        (a : P ⊗ (free R).obj S'.toCondensed ⟶ B) → (↑((P ⟹ B).obj.obj (Opposite.op S')) : Type u))
      (P ◁ CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map π) ≫
        (ihomPoints R P B S : (a : (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u)) → P ⊗ (free R).obj S.toCondensed ⟶ B)
          g) :
    (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) ((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map π.op) :
        (a : (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u)) → (↑((P ⟹ B).obj.obj (Opposite.op S')) : Type u))
      (((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 B S :
              (a : (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u)) → P ⊗ (free R).obj S.toCondensed ⟶ B)
            g) :
        (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u)) :
    (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u))
Tactic: have := ihomPoints_symm_comp R B P S' S π ((ihomPoints R P B S) g)