awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : LightCondSet
x x_1 : LightProfiniteᵒᵖ
x_2 : x ⟶ x_1
x_3 : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj x
⊢ {
      toFun :=
        fun
          (s :
            (↑(Functor.obj
                  (CompHausLike.compHausLikeToTop fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                  (Opposite.unop x_1)) :
              Type u)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
                (x_2 ≫
                  (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                      (of PUnit.{u + 1}) s).op)) :
            (a : X.obj.obj x) → X.obj.obj (Opposite.op (of PUnit.{u + 1})))
          x_3,
      continuous_toFun := ⋯ :
      C((↑(Functor.obj
              (CompHausLike.compHausLikeToTop fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
              (Opposite.unop x_1)) :
          Type u),
        X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1}))) } =
    {
          toFun :=
            fun
              (s :
                (↑(Functor.obj
                      (CompHausLike.compHausLikeToTop fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                      (Opposite.unop x)) :
                  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 : X.obj.obj x) → X.obj.obj (Opposite.op (of PUnit.{u + 1})))
              x_3,
          continuous_toFun := ⋯ :
          C((↑(Functor.obj
                  (CompHausLike.compHausLikeToTop fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                  (Opposite.unop x)) :
              Type u),
            X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1}))) }.comp
      (TopCat.Hom.hom x_2.unop.hom)

Tactic:
rfl
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X Y_1 : LightCondSet
f : X ⟶ Y_1
Y : LightCondSet
w :
  ∀ (x : (↑(lightCondSetToTopCat.obj Y) : Type u)),
    Eq (α := (↑(lightCondSetToTopCat.obj Y) : Type u))
      (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (X := lightCondSetToTopCat.obj Y) (Y := lightCondSetToTopCat.obj Y)
                (CategoryStruct.comp (Y :=
                    lightCondSetToTopCat.obj (topCatToLightCondSet.obj (lightCondSetToTopCat.obj Y)))
                    (lightCondSetToTopCat.map
                      (NatTrans.app { app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 } Y))
                    (NatTrans.app { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }
                      (lightCondSetToTopCat.obj Y)) :
                  lightCondSetToTopCat.obj Y ⟶ lightCondSetToTopCat.obj Y) :
              C((↑(lightCondSetToTopCat.obj Y) : Type u), (↑(lightCondSetToTopCat.obj Y) : Type u))) :
            (a : (↑(lightCondSetToTopCat.obj Y) : Type u)) → (↑(lightCondSetToTopCat.obj Y) : Type u))
          x :
        (↑(lightCondSetToTopCat.obj Y) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (𝟙 (lightCondSetToTopCat.obj Y)) :
            (a : (↑(lightCondSetToTopCat.obj Y) : Type u)) → (↑(lightCondSetToTopCat.obj Y) : Type u))
          x :
        (↑(lightCondSetToTopCat.obj Y) : Type u))
⊢ Eq (α := lightCondSetToTopCat.obj Y ⟶ lightCondSetToTopCat.obj Y)
    (CategoryStruct.comp (Y := lightCondSetToTopCat.obj (topCatToLightCondSet.obj (lightCondSetToTopCat.obj Y)))
        (lightCondSetToTopCat.map
          (NatTrans.app { app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 } Y))
        (NatTrans.app { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }
          (lightCondSetToTopCat.obj Y)) :
      lightCondSetToTopCat.obj Y ⟶ lightCondSetToTopCat.obj Y)
    (𝟙 (lightCondSetToTopCat.obj Y) : lightCondSetToTopCat.obj Y ⟶ lightCondSetToTopCat.obj Y)

Tactic:
ext
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X Y_1 : LightCondSet
f : X ⟶ Y_1
Y : LightCondSet
x : (↑(lightCondSetToTopCat.obj Y) : Type u)
w :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
        (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
              (𝟙 (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1})))))) :
          (a : (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1})))))) →
            (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
        x :
      (fun (X : Type u) ↦ X)
        (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
          (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (𝟙 (lightCondSetToTopCat.obj Y)) :
          (a : (↑(lightCondSetToTopCat.obj Y) : Type u)) → (↑(lightCondSetToTopCat.obj Y) : Type u))
        x :
      (↑(lightCondSetToTopCat.obj Y) : Type u))
⊢ Eq (α := (↑(lightCondSetToTopCat.obj Y) : Type u))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := lightCondSetToTopCat.obj Y) (Y := lightCondSetToTopCat.obj Y)
              (CategoryStruct.comp (Y :=
                  lightCondSetToTopCat.obj (topCatToLightCondSet.obj (lightCondSetToTopCat.obj Y)))
                  (lightCondSetToTopCat.map
                    (NatTrans.app { app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 } Y))
                  (NatTrans.app { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }
                    (lightCondSetToTopCat.obj Y)) :
                lightCondSetToTopCat.obj Y ⟶ lightCondSetToTopCat.obj Y) :
            C((↑(lightCondSetToTopCat.obj Y) : Type u), (↑(lightCondSetToTopCat.obj Y) : Type u))) :
          (a : (↑(lightCondSetToTopCat.obj Y) : Type u)) → (↑(lightCondSetToTopCat.obj Y) : Type u))
        x :
      (↑(lightCondSetToTopCat.obj Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (𝟙 (lightCondSetToTopCat.obj Y)) :
          (a : (↑(lightCondSetToTopCat.obj Y) : Type u)) → (↑(lightCondSetToTopCat.obj Y) : Type u))
        x :
      (↑(lightCondSetToTopCat.obj Y) : Type u))

Tactic:
change Y.obj.map (𝟙 _) _ = _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.id, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, DFunLike.coe
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X Y_1 : LightCondSet
f : X ⟶ Y_1
Y : LightCondSet
x : (↑(lightCondSetToTopCat.obj Y) : Type u)
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
        (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
              (𝟙 (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1})))))) :
          (a : (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1})))))) →
            (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
        x :
      (fun (X : Type u) ↦ X)
        (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
          (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (𝟙 (lightCondSetToTopCat.obj Y)) :
          (a : (↑(lightCondSetToTopCat.obj Y) : Type u)) → (↑(lightCondSetToTopCat.obj Y) : Type u))
        x :
      (↑(lightCondSetToTopCat.obj Y) : Type u))

Tactic:
simp
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : TopCat
rw :
  Function.Surjective (α := (↑((topCatToLightCondSet ⋙ lightCondSetToTopCat).obj X) : Type u_1)) (β :=
    (↑(Functor.obj (𝟭 TopCat) X) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
          TopCat.carrier) (topCatAdjunction.counit.app X)) :
      (a : (↑((topCatToLightCondSet ⋙ lightCondSetToTopCat).obj X) : Type u_1)) → (↑((𝟭 TopCat).obj X) : Type u_1))
⊢ Epi (topCatAdjunction.counit.app X)

Tactic:
rw [TopCat.epi_iff_surjective]

Premises used: TopCat.epi_iff_surjective
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : TopCat
⊢ Function.Surjective (α := (↑((topCatToLightCondSet ⋙ lightCondSetToTopCat).obj X) : Type u_1)) (β :=
    (↑(Functor.obj (𝟭 TopCat) X) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
          TopCat.carrier) (topCatAdjunction.counit.app X)) :
      (a : (↑((topCatToLightCondSet ⋙ lightCondSetToTopCat).obj X) : Type u_1)) → (↑((𝟭 TopCat).obj X) : Type u_1))

Tactic:
(topCatAdjunctionCounit_bijective _).2

Premises used: LightCondSet.topCatAdjunctionCounit_bijective, And.right
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : TopCat
⊢ Function.Surjective (α := (↑((topCatToLightCondSet ⋙ lightCondSetToTopCat).obj X) : Type u_1)) (β :=
    (↑(Functor.obj (𝟭 TopCat) X) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
          TopCat.carrier) (topCatAdjunction.counit.app X)) :
      (a : (↑((topCatToLightCondSet ⋙ lightCondSetToTopCat).obj X) : Type u_1)) → (↑((𝟭 TopCat).obj X) : Type u_1))

Tactic:
exact (topCatAdjunctionCounit_bijective _).2

Premises used: LightCondSet.topCatAdjunctionCounit_bijective, And.right
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X Y : LightCondSet
f : X ⟶ Y
⊢ topCatToLightCondSet.Faithful

Tactic:
topCatAdjunction.faithful_R_of_epi_counit_app

Premises used: LightCondSet.topCatAdjunction, CategoryTheory.Adjunction.faithful_R_of_epi_counit_app
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : LightCondSet
⊢ SequentialSpace.{u} (↑X.toTopCat : Type u)

Tactic:
apply SequentialSpace.coinduced

Premises used: SequentialSpace.coinduced
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : LightCondSet
⊢ SequentialSpace.{u} (↑(lightCondSetToTopCat.obj X) : Type u)

Tactic:
inferInstanceAs (SequentialSpace X.toTopCat)

Premises used: _private.0.LightCondSet.instSequentialSpaceCarrierObjTopCatLightCondSetToTopCat._proof_1
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : TopCat
inst : SequentialSpace (↑X : Type)
hf : SeqContinuous (topCatAdjunctionCounitEquiv X).invFun
⊢ Continuous (topCatAdjunctionCounitEquiv X).invFun

Tactic:
apply SeqContinuous.continuous

Premises used: SeqContinuous.continuous
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f_1 : X_1 ⟶ Y
X : TopCat
inst : SequentialSpace (↑X : Type)
f : ℕ → (↑X : Type)
p : (↑X : Type)
h : Filter.Tendsto f Filter.atTop (nhds p)
g : OnePoint ℕ → (↑X.toLightCondSet.toTopCat : Type) :=
  (topCatAdjunctionCounitEquiv X).invFun ∘ (⇑(OnePoint.continuousMapMkNat f p h) : (a : OnePoint ℕ) → (↑X : Type))
hf : Filter.Tendsto (fun (n : ℕ) ↦ g (↑n : OnePoint ℕ)) Filter.atTop (nhds ((topCatAdjunctionCounitEquiv X).invFun p))
⊢ Filter.Tendsto ((topCatAdjunctionCounitEquiv X).invFun ∘ f) Filter.atTop
    (nhds ((topCatAdjunctionCounitEquiv X).invFun p))

Tactic:
change Filter.Tendsto (fun n : ℕ ↦ g n) _ _

Premises used: OnePoint.some, Filter.Tendsto
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f_1 : X_1 ⟶ Y
X : TopCat
inst : SequentialSpace (↑X : Type)
f : ℕ → (↑X : Type)
p : (↑X : Type)
h : Filter.Tendsto f Filter.atTop (nhds p)
g : OnePoint ℕ → (↑X.toLightCondSet.toTopCat : Type) :=
  (topCatAdjunctionCounitEquiv X).invFun ∘ (⇑(OnePoint.continuousMapMkNat f p h) : (a : OnePoint ℕ) → (↑X : Type))
hf : Continuous g
⊢ Filter.Tendsto (fun (n : ℕ) ↦ g (↑n : OnePoint ℕ)) Filter.atTop (nhds ((topCatAdjunctionCounitEquiv X).invFun p))

Tactic:
erw [← OnePoint.continuous_iff_from_nat]

Premises used: OnePoint.continuous_iff_from_nat
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f_1 : X_1 ⟶ Y
X : TopCat
inst : SequentialSpace (↑X : Type)
f : ℕ → (↑X : Type)
p : (↑X : Type)
h : Filter.Tendsto f Filter.atTop (nhds p)
g : OnePoint ℕ → (↑X.toLightCondSet.toTopCat : Type) :=
  (topCatAdjunctionCounitEquiv X).invFun ∘ (⇑(OnePoint.continuousMapMkNat f p h) : (a : OnePoint ℕ) → (↑X : Type))
x : X.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op ℕ∪{∞}) :=
  OnePoint.continuousMapMkNat f p h
⊢ Continuous g

Tactic:
continuous_coinducingCoprod X.toLightCondSet x

Premises used: LightCondSet.continuous_coinducingCoprod, TopCat.toLightCondSet, ContinuousMap.comp, _private.0.LightCondSet.coinducingCoprod, ContinuousMap.const, OnePoint
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f_1 : X_1 ⟶ Y
X : TopCat
inst : SequentialSpace (↑X : Type)
f : ℕ → (↑X : Type)
p : (↑X : Type)
h : Filter.Tendsto f Filter.atTop (nhds p)
g : OnePoint ℕ → (↑X.toLightCondSet.toTopCat : Type) :=
  (topCatAdjunctionCounitEquiv X).invFun ∘ (⇑(OnePoint.continuousMapMkNat f p h) : (a : OnePoint ℕ) → (↑X : Type))
x : X.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op ℕ∪{∞}) :=
  OnePoint.continuousMapMkNat f p h
⊢ Continuous g

Tactic:
exact continuous_coinducingCoprod X.toLightCondSet x

Premises used: LightCondSet.continuous_coinducingCoprod, TopCat.toLightCondSet
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X Y : LightCondSet
f : X ⟶ Y
rw : ∀ (X : Sequential.{0}), IsIso (sequentialAdjunction.counit.app X)
⊢ IsIso sequentialAdjunction.counit

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : Sequential
⊢ IsIso (sequentialAdjunction.counit.app X)

Tactic:
inferInstanceAs (IsIso (sequentialAdjunctionCounitIso X).hom)

Premises used: _private.0.LightCondSet.instIsIsoFunctorSequentialCounitSequentialAdjunction._proof_1
-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : Sequential
⊢ IsIso (sequentialAdjunction.counit.app X)

Tactic:
exact inferInstanceAs (IsIso (sequentialAdjunctionCounitIso X).hom)
-- Module: Mathlib.Condensed.Limits
Goal:
⊢ HasLimits.{u + 1, u + 2} (Sheaf (coherentTopology CompHaus) (Type (u + 1)))

Tactic:
infer_instance
-- Module: Mathlib.Condensed.Limits
Goal:
⊢ HasLimitsOfSize.{u, u + 1, u + 1, u + 2} CondensedSet

Tactic:
hasLimitsOfSizeShrink.{u, u + 1, u + 1, u} _

Premises used: CategoryTheory.Limits.hasLimitsOfSizeShrink
-- Module: Mathlib.Condensed.Limits
Goal:
R : Type (u + 1)
inst : Ring R
⊢ HasLimits.{u + 1, u + 2} (CondensedMod R)

Tactic:
inferInstanceAs (HasLimits (Sheaf _ _))

Premises used: _private.0.instHasLimitsCondensedMod._proof_1
-- Module: Mathlib.Condensed.Limits
Goal:
R : Type (u + 1)
inst : Ring R
⊢ HasColimits.{u + 1, u + 2} (CondensedMod R)

Tactic:
inferInstanceAs (HasColimits (Sheaf _ _))

Premises used: _private.0.instHasColimitsCondensedMod._proof_1
-- Module: Mathlib.Condensed.Limits
Goal:
R : Type (u + 1)
inst : Ring R
⊢ HasLimitsOfSize.{u, u + 1, u + 1, u + 2} (CondensedMod R)

Tactic:
hasLimitsOfSizeShrink.{u, u + 1, u + 1, u} _

Premises used: CategoryTheory.Limits.hasLimitsOfSizeShrink
-- Module: Mathlib.Condensed.Limits
Goal:
R : Type (u + 1)
inst : Ring R
A : Type u_1
J : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} J
inst_3 : HasColimitsOfShape.{v_2, u_2, v_1, u_1} J A
inst_4 : HasWeakSheafify.{u, v_1, u + 1, u_1} (coherentTopology CompHaus) A
⊢ HasColimitsOfShape J (Condensed.{u, v_1, u_1} A)

Tactic:
inferInstanceAs (HasColimitsOfShape J (Sheaf _ _))

Premises used: _private.0.instHasColimitsOfShapeCondensedOfHasWeakSheafifyCompHausCoherentTopology._proof_1
-- Module: Mathlib.Condensed.Limits
Goal:
R : Type (u + 1)
inst : Ring R
A : Type u_1
J : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} J
inst_3 : HasLimitsOfShape.{v_2, u_2, v_1, u_1} J A
⊢ HasLimitsOfShape J (Condensed.{u, v_1, u_1} A)

Tactic:
inferInstanceAs (HasLimitsOfShape J (Sheaf _ _))

Premises used: _private.0.instHasLimitsOfShapeCondensed._proof_1
-- Module: Mathlib.Condensed.Limits
Goal:
R : Type (u + 1)
inst : Ring R
A : Type u_1
inst_1 : Category.{v_1, u_1} A
inst_2 : HasFiniteLimits.{v_1, u_1} A
⊢ HasFiniteLimits (Condensed.{u, v_1, u_1} A)

Tactic:
inferInstanceAs (HasFiniteLimits (Sheaf _ _))

Premises used: _private.0.instHasFiniteLimitsCondensed._proof_1
-- Module: Mathlib.Condensed.Limits
Goal:
R : Type (u + 1)
inst : Ring R
A : Type u_1
inst_1 : Category.{v_1, u_1} A
inst_2 : HasFiniteColimits.{v_1, u_1} A
inst_3 : HasWeakSheafify.{u, v_1, u + 1, u_1} (coherentTopology CompHaus) A
⊢ HasFiniteColimits (Condensed.{u, v_1, u_1} A)

Tactic:
inferInstanceAs (HasFiniteColimits (Sheaf _ _))

Premises used: _private.0.instHasFiniteColimitsCondensedOfHasWeakSheafifyCompHausCoherentTopology._proof_1
-- Module: Mathlib.Condensed.Module
Goal:
R : Type (u + 1)
inst : Ring R
X Y : CondensedMod R
f : X ⟶ Y
S T : CompHausᵒᵖ
g : S ⟶ T
x : (↑(X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj S) : Type (u + 1))
⊢ Eq (α := (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj T) : Type (u + 1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC :=
            ModuleCat.carrier) (f.hom.app T) :
          (a : (↑(X.obj.obj T) : Type (u + 1))) → (↑(Y.obj.obj T) : Type (u + 1)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1)))
                (CC := ModuleCat.carrier) (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map g) :
              (a : (↑(X.obj.obj S) : Type (u + 1))) → (↑(X.obj.obj T) : Type (u + 1)))
            x :
          (↑(X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj T) : Type (u + 1))) :
      (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj T) : Type (u + 1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC :=
            ModuleCat.carrier) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map g) :
          (a : (↑(Y.obj.obj S) : Type (u + 1))) → (↑(Y.obj.obj T) : Type (u + 1)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1)))
                (CC := ModuleCat.carrier) (f.hom.app S) :
              (a : (↑(X.obj.obj S) : Type (u + 1))) → (↑(Y.obj.obj S) : Type (u + 1)))
            x :
          (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj S) : Type (u + 1))) :
      (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj T) : Type (u + 1)))

Tactic:
NatTrans.naturality_apply f.hom g x

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Condensed.Solid
Goal:
R : Type (u + 1)
inst : Ring R
⊢ Functor.IsRightKanExtension (H := CondensedMod R) (FintypeCat.toProfinite.rightKanExtension (finFree R))
    (FintypeCat.toProfinite.rightKanExtensionCounit (finFree R))

Tactic:
infer_instance
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X : CondensedSet
S : CompHaus
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)
suffices :
  ∀ (i : (T : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op T)),
    Continuous (Y := X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
      fun
        (a :
          (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op T)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u)) ↦
      X.coinducingCoprod
        (Sigma.mk (β :=
          fun (i : (S : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) ↦
          (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u))
          i a)
⊢ Continuous (Y := X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
    fun
      (a :
        (↑((Sigma.fst (β := fun (S : CompHaus.{u}) ↦
                  X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S))
                  (Sigma.mk (β := fun (S : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) S x)).toTop
              (P := fun (x : TopCat.{u}) ↦ True)) :
          Type u)) ↦
    X.coinducingCoprod
      (Sigma.mk (β :=
        fun (i : (S : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) ↦
        (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                  X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
              (P := fun (x : TopCat.{u}) ↦ True)) :
          Type u))
        (Sigma.mk (β := fun (S : CompHaus.{u}) ↦
          X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) S x)
        a)

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

Tactic:
rw [← continuous_sigma_iff]

Premises used: continuous_sigma_iff