-- Module: Mathlib.Condensed.Light.InternallyProjective
Goal:
R : Type u
inst : CommRing R
P : LightCondSet
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g :
  obj (free R)
      (tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
        S.toCondensed) ⟶
    B
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)))
      (obj (free R) P) (obj (free R) S'.toCondensed) ⟶
    A
hh :
  obj (free R) P ◁ CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫
      Iso.hom (μIso (free R) P S.toCondensed) ≫ g =
    g' ≫ e
⊢ CategoryTheory.Functor.map (free R) (P ◁ lightProfiniteToLightCondSet.map π) ≫ g =
    CategoryStruct.comp (Y :=
        tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite)))
          (obj (free R) P) (obj (lightProfiniteToLightCondSet ⋙ free R) S))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite)))
            (obj (free R) P) (obj (free R) S'.toCondensed))
          (Iso.inv (μIso (free R) P S'.toCondensed))
          (obj (free R) P ◁ CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π))
        (Iso.hom (μIso (free R) P S.toCondensed)) ≫
      g

Tactic:
simp only [μIso_hom, μIso_inv, Functor.comp_map, δ_natural_right, assoc, δ_μ, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.Monoidal.δ_μ, CategoryTheory.Category.comp_id, CategoryTheory.Functor.Monoidal.μIso_hom, CategoryTheory.Functor.Monoidal.μIso_inv, CategoryTheory.Functor.OplaxMonoidal.δ_natural_right, CategoryTheory.Functor.comp_map