-- Module: Mathlib.Condensed.Light.Sequence
Goal:
R : Type
inst : CommRing R
rw :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite.{0})
    (g :
      obj (free R)
          (tensorObj (𝒞 :=
              CompHausLike.category fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
              S ℕ∪{∞}).toCondensed ⟶
        B),
    ∃ (S' : LightProfinite.{0}) (π : S' ⟶ S) (_ :
      Function.Surjective (α :=
        (fun
              (X :
                CompHausLike fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
              Type))
          S')
        (β :=
        (fun
              (X :
                CompHausLike fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
              Type))
          S)
        (⇑(ConcreteCategory.hom (FC :=
              fun
                (x1 x2 :
                  CompHausLike fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type),
                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type)))
              (CC :=
              fun
                (X :
                  CompHausLike fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                Type))
              π) :
          (a :
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑X.toTop : Type))
                S') →
            (fun
                  (X :
                    CompHausLike fun (X : TopCat) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                (↑X.toTop : Type))
              S))
      (g' :
      obj (free R)
          (tensorObj (𝒞 :=
              CompHausLike.category fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
              S' ℕ∪{∞}).toCondensed ⟶
        A),
      CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map (π ▷ ℕ∪{∞})) ≫ g = g' ≫ e
⊢ InternallyProjective (C := LightCondMod R) (obj (free R) ℕ∪{∞}.toCondensed)

Tactic:
rw [free_lightProfinite_internallyProjective_iff_tensor_condition' R ℕ∪{∞}]

Premises used: LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', LightProfinite.NatUnionInfty