-- Lean 4 proof step from Mathlib.Condensed.Epi (goal)
Goal:
A : Type u'
inst : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst_1 : (X Y : A) → FunLike.{u_1 + 1, v' + 1, v' + 1} (FA X Y) (CA X) (CA Y)
inst_2 : ConcreteCategory A FA (CC := CA)
inst_3 : HasFunctorialSurjectiveInjectiveFactorization A (FC := FA) (CC := CA)
X Y : Condensed.{u, v', u'} A
f : X ⟶ Y
inst_4 : PreservesFiniteProducts (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_5 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v', u'} (StructuredArrow X Stonean.toCompHaus.op) A
inst_6 : GrothendieckTopology.WEqualsLocallyBijective (extensiveTopology Stonean) A (FA := FA) (CA := CA)
inst_7 : HasSheafify.{u, v', u + 1, u'} (extensiveTopology Stonean) A
inst_8 :
  GrothendieckTopology.HasSheafCompose (extensiveTopology Stonean) (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_9 : Balanced (Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)
⊢ Epi f ↔
    ∀ (S : Stonean.{u}),
      Function.Surjective.{v' + 1, v' + 1} (α :=
        CA (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S.compHaus))) (β :=
        CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S.compHaus)))
        (⇑(hom (FC := FA) (CC := CA) (f.hom.app (op S.compHaus))) :
          (a : CA (X.obj.obj (op S.compHaus))) → CA (Y.obj.obj (op S.compHaus)))
have rw : IsLocallySurjective (J := extensiveTopology Stonean) (FA := FA) (CA := CA) (F₁ :=
    (Functor.obj
        (Equivalence.functor Presheaf.coherentExtensiveEquivalence :
          Sheaf.{u, v', u + 1, u'} (coherentTopology Stonean) A ⥤
            Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)
        (Functor.obj (Equivalence.inverse (StoneanCompHaus.equivalence A)) X) :
      Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A))
    (F₂ :=
    (Functor.obj
        (Equivalence.functor Presheaf.coherentExtensiveEquivalence :
          Sheaf.{u, v', u + 1, u'} (coherentTopology Stonean) A ⥤
            Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)
        (Functor.obj (Equivalence.inverse (StoneanCompHaus.equivalence A)) Y) :
      Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A))
    (CategoryTheory.Functor.map (Equivalence.functor Presheaf.coherentExtensiveEquivalence)
        (CategoryTheory.Functor.map (Equivalence.inverse (StoneanCompHaus.equivalence A)) f) :
      Quiver.Hom (V := Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)
        (Functor.obj
            (Equivalence.functor Presheaf.coherentExtensiveEquivalence :
              Sheaf.{u, v', u + 1, u'} (coherentTopology Stonean) A ⥤
                Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)
            (Functor.obj (Equivalence.inverse (StoneanCompHaus.equivalence A)) X) :
          Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)
        (Functor.obj
            (Equivalence.functor Presheaf.coherentExtensiveEquivalence :
              Sheaf.{u, v', u + 1, u'} (coherentTopology Stonean) A ⥤
                Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)
            (Functor.obj (Equivalence.inverse (StoneanCompHaus.equivalence A)) Y) :
          Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)) ↔
  ∀ (S : Stonean.{u}),
    Function.Surjective.{v' + 1, v' + 1} (α :=
      CA (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S.compHaus))) (β :=
      CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S.compHaus)))
      (⇑(hom (FC := FA) (CC := CA) (f.hom.app (op S.compHaus))) :
        (a : CA (X.obj.obj (op S.compHaus))) → CA (Y.obj.obj (op S.compHaus)))
Tactic: rw [← (StoneanCompHaus.equivalence A).inverse.epi_map_iff_epi,
    ← Presheaf.coherentExtensiveEquivalence.functor.epi_map_iff_epi,
    ← isLocallySurjective_iff_epi']