-- Module: Mathlib.Condensed.Epi
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 : GrothendieckTopology.WEqualsLocallyBijective (coherentTopology CompHaus) A (FA := FA) (CA := CA)
inst_5 : HasSheafify.{u, v', u + 1, u'} (coherentTopology CompHaus) A
inst_6 :
  GrothendieckTopology.HasSheafCompose (coherentTopology CompHaus) (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_7 : Balanced (Sheaf.{u, v', u + 1, u'} (coherentTopology CompHaus) A)
inst_8 : PreservesFiniteProducts (CategoryTheory.forget A (FC := FA) (CC := CA))
simp_rw simp_rw₁ :
  (∀ (X_1 : CompHaus.{u})
      (y : ToType (FC := FA) (CC := CA) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op X_1))),
      ∃ (X' : CompHaus.{u}) (φ : X' ⟶ X_1) (_ : EffectiveEpi φ) (x :
        ToType (FC := FA) (CC := CA) (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op X'))),
        Eq (α := CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op X')))
          ((hom (FC := FA) (CC := CA) (f.hom.app (op X')) : (a : CA (X.obj.obj (op X'))) → CA (Y.obj.obj (op X'))) x :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op X')))
          ((hom (FC := FA) (CC := CA) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map (op φ)) :
                (a : CA (Y.obj.obj (op X_1))) → CA (Y.obj.obj (op X')))
              y :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op X')))) ↔
    ∀ (S : CompHaus.{u})
      (y : ToType (FC := FA) (CC := CA) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S))),
      ∃ (S' : CompHaus.{u}) (φ : S' ⟶ S) (_ :
        Function.Surjective (α := (↑(S'.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) (β :=
          (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          (⇑(hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                  (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
                (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) φ) :
            (a : (↑S'.toTop : Type u)) → (↑S.toTop : Type u)))
        (x : ToType (FC := FA) (CC := CA) (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S'))),
        Eq (α := CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S')))
          ((hom (FC := FA) (CC := CA) (f.hom.app (op S')) : (a : CA (X.obj.obj (op S'))) → CA (Y.obj.obj (op S'))) x :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S')))
          ((hom (FC := FA) (CC := CA) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map (op φ)) :
                (a : CA (Y.obj.obj (op S))) → CA (Y.obj.obj (op S')))
              y :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S')))
⊢ (∀ (X_1 : CompHaus.{u})
      (y : ToType (FC := FA) (CC := CA) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op X_1))),
      ∃ (X' : CompHaus.{u}) (φ : X' ⟶ X_1) (_ : EffectiveEpi φ) (x :
        ToType (FC := FA) (CC := CA) (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op X'))),
        Eq (α := CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op X')))
          ((hom (FC := FA) (CC := CA) (f.hom.app (op X')) : (a : CA (X.obj.obj (op X'))) → CA (Y.obj.obj (op X'))) x :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op X')))
          ((hom (FC := FA) (CC := CA) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map (op φ)) :
                (a : CA (Y.obj.obj (op X_1))) → CA (Y.obj.obj (op X')))
              y :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op X')))) ↔
    ∀ (S : CompHaus.{u})
      (y : ToType (FC := FA) (CC := CA) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S))),
      ∃ (S' : CompHaus.{u}) (φ : S' ⟶ S) (_ :
        Function.Surjective (α :=
          (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
            S')
          (β :=
          (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
            S)
          (⇑(hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                  (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
                (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) φ) :
            (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) S') →
              (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) S))
        (x : ToType (FC := FA) (CC := CA) (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S'))),
        Eq (α := CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S')))
          ((hom (FC := FA) (CC := CA) (f.hom.app (op S')) : (a : CA (X.obj.obj (op S'))) → CA (Y.obj.obj (op S'))) x :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S')))
          ((hom (FC := FA) (CC := CA) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map (op φ)) :
                (a : CA (Y.obj.obj (op S))) → CA (Y.obj.obj (op S')))
              y :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S')))

Tactic:
simp_rw [((CompHaus.effectiveEpi_tfae _).out 0 2 :)]

Premises used: List.TFAE.out, CompHaus.effectiveEpi_tfae, OfNat.ofNat