-- Lean 4 proof step from Mathlib.Condensed.Light.InternallyProjective (goal)
Goal:
R : Type u
inst : CommRing R
P : LightCondMod R
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite.{u})
    (g :
      tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
          (obj (free R) S.toCondensed) ⟶
        B),
    ∃ (S' : LightProfinite.{u}) (π : S' ⟶ S) (_ :
      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),
      P ◁ CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
⊢ Epi (X := P ⟹ A) (CategoryTheory.Functor.map (ihom P) e)
have refine_2 : ∀ (S : LightProfinite.{u})
  (y : (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u)),
  ∃ (S' : LightProfinite.{u}) (φ : S' ⟶ S) (_ :
    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))
    (x : (↑((P ⟹ A).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u)),
    Eq (α := (↑((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) (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))
      ((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))
          y :
        (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u))
Tactic: rw [LightCondMod.epi_iff_locallySurjective_on_lightProfinite]