awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Light.Small
Goal:
C : Type w
inst : Category.{v, w} C
R : Type u
inst_1 : CommRing R
⊢ sheafCompose
      (inducedTopology (Equivalence.inverse (equivSmallModel LightProfinite)) (coherentTopology LightProfinite))
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
        (CC := ModuleCat.carrier)) ≅
    Equivalence.inverse (equivSmall (ModuleCat R)) ⋙
      forget R ⋙ Equivalence.inverse (CategoryTheory.Equivalence.symm (equivSmall (Type u)))

Tactic:
refine NatIso.ofComponents
    (fun X ↦ (fullyFaithfulSheafToPresheaf _ _).preimageIso
      (isoWhiskerRight ((equivSmallModel LightProfinite).op.invFunIdAssoc _).symm _ ≪≫
        (Functor.associator _ _ _)))
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X : LightCondSet
S : LightProfinite
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)
suffices :
  ∀
    (i :
      (T : LightProfinite.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op T)),
    Continuous (Y :=
      X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
      fun
        (a :
          (↑(i.fst (β := fun (T : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op T)).toTop
                (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u)) ↦
      X.coinducingCoprod
        (Sigma.mk (β :=
          fun
            (i :
              (S : LightProfinite.{u}) ×
                X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) ↦
          (↑(i.fst (β := fun (S : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)).toTop
                (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
          i a)
⊢ Continuous (Y := X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    fun
      (a :
        (↑((Sigma.fst (β := fun (S : LightProfinite.{u}) ↦
                  X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
                  (Sigma.mk (β := fun (S : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) S x)).toTop
              (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u)) ↦
    X.coinducingCoprod
      (Sigma.mk (β :=
        fun
          (i :
            (S : LightProfinite.{u}) ×
              X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) ↦
        (↑(i.fst (β := fun (S : LightProfinite.{u}) ↦
                  X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)).toTop
              (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u))
        (Sigma.mk (β := fun (S : LightProfinite.{u}) ↦
          X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) S x)
        a)

Tactic:
suffices ∀ (i : (T : LightProfinite.{u}) × X.obj.obj ⟨T⟩),
      Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from this ⟨_, _⟩
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X : LightCondSet
S : LightProfinite
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)
rw : Continuous X.coinducingCoprod
⊢ ∀
    (i :
      (T : LightProfinite.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op T)),
    Continuous (Y :=
      X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
      fun
        (a :
          (↑(i.fst (β := fun (T : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op T)).toTop
                (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u)) ↦
      X.coinducingCoprod
        (Sigma.mk (β :=
          fun
            (i :
              (S : LightProfinite.{u}) ×
                X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) ↦
          (↑(i.fst (β := fun (S : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)).toTop
                (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
          i a)

Tactic:
rw [← continuous_sigma_iff]

Premises used: continuous_sigma_iff
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X : LightCondSet
S : LightProfinite
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)
⊢ Continuous X.coinducingCoprod

Tactic:
apply continuous_coinduced_rng

Premises used: continuous_coinduced_rng
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X Y : LightCondSet
f : X ⟶ Y
rw :
  Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1})))) :
        (a : (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
          (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1})))) ∘
      X.coinducingCoprod)
⊢ Continuous (X := X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1})))) :
      (a : (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
        (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1}))))

Tactic:
rw [continuous_coinduced_dom]

Premises used: continuous_coinduced_dom
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X Y : LightCondSet
f : X ⟶ Y
hf :
  ∀
    (i :
      (S : LightProfinite.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)),
    Continuous (Y :=
      Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
      fun
        (a :
          (↑(i.fst (β := fun (S : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)).toTop
                (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u)) ↦
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1})))) :
            (a : (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
              (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1})))) ∘
          X.coinducingCoprod)
        (Sigma.mk (β :=
          fun
            (i :
              (S : LightProfinite.{u}) ×
                X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) ↦
          (↑(i.fst (β := fun (S : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)).toTop
                (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
          i a)
⊢ Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1})))) :
        (a : (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
          (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1})))) ∘
      X.coinducingCoprod)

Tactic:
apply continuous_sigma

Premises used: continuous_sigma
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X Y : LightCondSet
f : X ⟶ Y
S : LightProfinite
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)
hf :
  Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    fun
      (a :
        (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1}))) :
        (a : X.obj.obj (Opposite.op (of PUnit.{u + 1}))) → Y.obj.obj (Opposite.op (of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
                (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                    (of PUnit.{u + 1}) a).op) :
            (a : X.obj.obj (Opposite.op S)) → X.obj.obj (Opposite.op (of PUnit.{u + 1})))
          x :
        X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
⊢ Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    fun
      (a :
        (↑((Sigma.fst (β := fun (S : LightProfinite.{u}) ↦
                  X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
                  (Sigma.mk (β := fun (S : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) S x)).toTop
              (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u)) ↦
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1})))) :
          (a : (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
            (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1})))) ∘
        X.coinducingCoprod)
      (Sigma.mk (β :=
        fun
          (i :
            (S : LightProfinite.{u}) ×
              X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) ↦
        (↑(i.fst (β := fun (S : LightProfinite.{u}) ↦
                  X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)).toTop
              (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u))
        (Sigma.mk (β := fun (S : LightProfinite.{u}) ↦
          X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) S x)
        a)

Tactic:
simp only [Function.comp_apply, coinducingCoprod]

Premises used: _private.0.LightCondSet.coinducingCoprod, Function.comp_apply
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X Y : LightCondSet
f : X ⟶ Y
S : LightProfinite
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)
hf :
  Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    fun
      (a :
        (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
            (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                (of PUnit.{u + 1}) a).op) :
        (a : Y.obj.obj (Opposite.op S)) → Y.obj.obj (Opposite.op (of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op S)) :
            (a : X.obj.obj (Opposite.op S)) → Y.obj.obj (Opposite.op S))
          x :
        Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
⊢ Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    fun
      (a :
        (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1}))) :
        (a : X.obj.obj (Opposite.op (of PUnit.{u + 1}))) → Y.obj.obj (Opposite.op (of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
                (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                    (of PUnit.{u + 1}) a).op) :
            (a : X.obj.obj (Opposite.op S)) → X.obj.obj (Opposite.op (of PUnit.{u + 1})))
          x :
        X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))

Tactic:
rw
        [show (fun (a : S) ↦ f.hom.app ⟨of PUnit⟩ (X.obj.map ((of PUnit.{u + 1}).const a).op x)) = _
        from funext fun a ↦ NatTrans.naturality_apply f.hom ((of PUnit.{u + 1}).const a).op x]
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X Y : LightCondSet
f : X ⟶ Y
S : LightProfinite
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)
⊢ Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    fun
      (a :
        (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
            (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                (of PUnit.{u + 1}) a).op) :
        (a : Y.obj.obj (Opposite.op S)) → Y.obj.obj (Opposite.op (of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op S)) :
            (a : X.obj.obj (Opposite.op S)) → Y.obj.obj (Opposite.op S))
          x :
        Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))

Tactic:
continuous_coinducingCoprod _ _

Premises used: LightCondSet.continuous_coinducingCoprod, _private.0.LightCondSet.coinducingCoprod
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X Y : LightCondSet
f : X ⟶ Y
S : LightProfinite
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)
⊢ Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    fun
      (a :
        (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
            (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                (of PUnit.{u + 1}) a).op) :
        (a : Y.obj.obj (Opposite.op S)) → Y.obj.obj (Opposite.op (of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op S)) :
            (a : X.obj.obj (Opposite.op S)) → Y.obj.obj (Opposite.op S))
          x :
        Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))

Tactic:
exact continuous_coinducingCoprod _ _

Premises used: LightCondSet.continuous_coinducingCoprod
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : TopCat
rw :
  Continuous.{u + 1, u} (X :=
    (i :
      (S : LightProfinite.{u}) ×
        X.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) ×
      (↑(i.fst (β := fun (S : LightProfinite.{u}) ↦
                X.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
                  (Opposite.op S)).toTop
            (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
        Type u))
    (Y := (↑X : Type u))
    ((fun
          (x :
            X.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
              (Opposite.op (of PUnit.{u + 1}))) ↦
        x.toFun PUnit.unit) ∘
      X.toLightCondSet.coinducingCoprod)
⊢ Continuous (Y := (↑X : Type u))
    fun
      (x :
        X.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
          (Opposite.op (of PUnit.{u + 1}))) ↦
    x.toFun PUnit.unit

Tactic:
rw [continuous_coinduced_dom]

Premises used: continuous_coinduced_dom
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : TopCat
⊢ Continuous.{u + 1, u} (X :=
    (i :
      (S : LightProfinite.{u}) ×
        X.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) ×
      (↑(i.fst (β := fun (S : LightProfinite.{u}) ↦
                X.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
                  (Opposite.op S)).toTop
            (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
        Type u))
    (Y := (↑X : Type u))
    ((fun
          (x :
            X.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
              (Opposite.op (of PUnit.{u + 1}))) ↦
        x.toFun PUnit.unit) ∘
      X.toLightCondSet.coinducingCoprod)

Tactic:
continuity
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X : TopCat
⊢ Function.Bijective (α := (↑X.toLightCondSet.toTopCat : Type u)) (β := (↑X : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (topCatAdjunctionCounit X)) :
      (a : (↑X.toLightCondSet.toTopCat : Type u)) → (↑X : Type u))

Tactic:
(topCatAdjunctionCounitEquiv X).bijective

Premises used: LightCondSet.topCatAdjunctionCounitEquiv, Equiv.bijective
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : LightCondSet
S : LightProfiniteᵒᵖ
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj S
suffices :
  ∀
    (i :
      (T : LightProfinite.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op T)),
    Continuous (Y :=
      X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
      fun
        (a :
          (↑(i.fst (β := fun (T : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op T)).toTop
                (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u)) ↦
      X.coinducingCoprod
        (Sigma.mk (β :=
          fun
            (i :
              (S : LightProfinite.{u}) ×
                X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) ↦
          (↑(i.fst (β := fun (S : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)).toTop
                (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
          i a)
⊢ Continuous (Y := (↑X.toTopCat : Type u))
    fun
      (s :
        (↑(Functor.obj
              (CompHausLike.compHausLikeToTop fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
              (Opposite.unop S)) :
          Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
            (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                (of PUnit.{u + 1}) s).op) :
        (a : (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (Opposite.unop S)))) →
          (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1}))))
      x

Tactic:
suffices ∀ (i : (T : LightProfinite.{u}) × X.obj.obj ⟨T⟩),
          Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from this ⟨_, _⟩
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : LightCondSet
S : LightProfiniteᵒᵖ
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj S
rw : Continuous X.coinducingCoprod
⊢ ∀
    (i :
      (T : LightProfinite.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op T)),
    Continuous (Y :=
      X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
      fun
        (a :
          (↑(i.fst (β := fun (T : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op T)).toTop
                (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u)) ↦
      X.coinducingCoprod
        (Sigma.mk (β :=
          fun
            (i :
              (S : LightProfinite.{u}) ×
                X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) ↦
          (↑(i.fst (β := fun (S : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)).toTop
                (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
          i a)

Tactic:
rw [← continuous_sigma_iff]

Premises used: continuous_sigma_iff
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : LightCondSet
S : LightProfiniteᵒᵖ
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj S
⊢ Continuous X.coinducingCoprod

Tactic:
apply continuous_coinduced_rng

Premises used: continuous_coinduced_rng