-- Module: Mathlib.Condensed.Light.Epi
Goal:
A : Type u'
inst : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst_1 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_2 : ConcreteCategory.{w, v', u', u_1} A FA (CC := CA)
inst_3 : PreservesFiniteProducts.{v', w, u', w + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
X Y : LightCondensed.{u, v', u'} A
f : X ⟶ Y
simp_rw simp_rw₁ :
  (∀ (X_1 : LightProfinite.{u})
      (y :
        ToType.{w, v', u', u_1} (FC := FA) (CC := CA)
          (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op X_1))),
      ∃ (X' : LightProfinite.{u}) (φ : X' ⟶ X_1) (_ : EffectiveEpi φ) (x :
        ToType.{w, v', u', u_1} (FC := FA) (CC := CA)
          (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op X'))),
        Eq (α := CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op X')))
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.hom.app (Opposite.op X')) :
                (a : CA (X.obj.obj (Opposite.op X'))) → CA (Y.obj.obj (Opposite.op X')))
              x :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op X')))
          ((ConcreteCategory.hom (FC := FA) (CC := CA)
                  (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map (Opposite.op φ)) :
                (a : CA (Y.obj.obj (Opposite.op X_1))) → CA (Y.obj.obj (Opposite.op X')))
              y :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op X')))) ↔
    ∀ (S : LightProfinite.{u})
      (y :
        ToType.{w, v', u', u_1} (FC := FA) (CC := CA)
          (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))),
      ∃ (S' : LightProfinite.{u}) (φ : S' ⟶ S) (_ :
        Function.Surjective (α :=
          (↑(S'.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
          (β :=
          (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
          (⇑(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 : (↑S'.toTop : Type u)) → (↑S.toTop : Type u)))
        (x :
        ToType.{w, v', u', u_1} (FC := FA) (CC := CA)
          (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S'))),
        Eq (α := CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')))
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.hom.app (Opposite.op S')) :
                (a : CA (X.obj.obj (Opposite.op S'))) → CA (Y.obj.obj (Opposite.op S')))
              x :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')))
          ((ConcreteCategory.hom (FC := FA) (CC := CA)
                  (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map (Opposite.op φ)) :
                (a : CA (Y.obj.obj (Opposite.op S))) → CA (Y.obj.obj (Opposite.op S')))
              y :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')))
⊢ (∀ (X_1 : LightProfinite.{u})
      (y :
        ToType.{w, v', u', u_1} (FC := FA) (CC := CA)
          (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op X_1))),
      ∃ (X' : LightProfinite.{u}) (φ : X' ⟶ X_1) (_ : EffectiveEpi φ) (x :
        ToType.{w, v', u', u_1} (FC := FA) (CC := CA)
          (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op X'))),
        Eq (α := CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op X')))
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.hom.app (Opposite.op X')) :
                (a : CA (X.obj.obj (Opposite.op X'))) → CA (Y.obj.obj (Opposite.op X')))
              x :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op X')))
          ((ConcreteCategory.hom (FC := FA) (CC := CA)
                  (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map (Opposite.op φ)) :
                (a : CA (Y.obj.obj (Opposite.op X_1))) → CA (Y.obj.obj (Opposite.op X')))
              y :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op X')))) ↔
    ∀ (S : LightProfinite.{u})
      (y :
        ToType.{w, v', u', u_1} (FC := FA) (CC := CA)
          (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))),
      ∃ (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 :
        ToType.{w, v', u', u_1} (FC := FA) (CC := CA)
          (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S'))),
        Eq (α := CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')))
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.hom.app (Opposite.op S')) :
                (a : CA (X.obj.obj (Opposite.op S'))) → CA (Y.obj.obj (Opposite.op S')))
              x :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')))
          ((ConcreteCategory.hom (FC := FA) (CC := CA)
                  (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map (Opposite.op φ)) :
                (a : CA (Y.obj.obj (Opposite.op S))) → CA (Y.obj.obj (Opposite.op S')))
              y :
            CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')))

Tactic:
simp_rw [LightProfinite.effectiveEpi_iff_surjective]

Premises used: LightProfinite.effectiveEpi_iff_surjective