awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Light.Instances
Goal:
A : Type u'
inst : Category.{u, u'} A
inst_1 : HasLimits.{u, u'} A
inst_2 : HasColimits.{u, u'} A
FA : A → A → Type v
CA : A → Type u
inst_3 : (X Y : A) → FunLike.{v + 1, u + 1, u + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory A FA (CC := CA)
inst_5 : PreservesFilteredColimits (forget A (FC := FA) (CC := CA))
inst_6 : PreservesLimits (forget A (FC := FA) (CC := CA))
inst_7 : Functor.ReflectsIsomorphisms (forget A (FC := FA) (CC := CA))
⊢ HasSheafify (coherentTopology LightProfinite) (Type u)

Tactic:
hasSheafifyEssentiallySmallSite _ _

Premises used: CategoryTheory.hasSheafifyEssentiallySmallSite
-- Module: Mathlib.Condensed.Light.Instances
Goal:
A : Type u'
inst : Category.{u, u'} A
inst_1 : HasLimits.{u, u'} A
inst_2 : HasColimits.{u, u'} A
FA : A → A → Type v
CA : A → Type u
inst_3 : (X Y : A) → FunLike.{v + 1, u + 1, u + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory A FA (CC := CA)
inst_5 : PreservesFilteredColimits (forget A (FC := FA) (CC := CA))
inst_6 : PreservesLimits (forget A (FC := FA) (CC := CA))
inst_7 : Functor.ReflectsIsomorphisms (forget A (FC := FA) (CC := CA))
⊢ GrothendieckTopology.WEqualsLocallyBijective (coherentTopology LightProfinite) A (FA := FA) (CA := CA)

Tactic:
GrothendieckTopology.WEqualsLocallyBijective.ofEssentiallySmall _

Premises used: CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.ofEssentiallySmall
-- Module: Mathlib.Condensed.Light.InternallyProjective
Goal:
R : Type u
inst : CommRing R
A B : LightCondMod R
S : LightProfinite
x : (↑((A ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u)
⊢ Eq (α :=
    tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) A
        (obj (free R) S.toCondensed) ⟶
      B)
    ((ihomPoints R A B S : (a : (↑((A ⟹ B).obj.obj (Opposite.op S)) : Type u)) → A ⊗ (free R).obj S.toCondensed ⟶ B) x :
      tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) A
          (obj (free R) S.toCondensed) ⟶
        B)
    (MonoidalClosed.uncurry
        ((Equiv.symm
              (Adjunction.homEquiv (freeForgetAdjunction R)
                (obj (GrothendieckTopology.yoneda (coherentTopology LightProfinite)) S) (A ⟹ B)) :
            (a : (coherentTopology LightProfinite).yoneda.obj S ⟶ (forget R).obj (A ⟹ B)) →
              (free R).obj ((coherentTopology LightProfinite).yoneda.obj S) ⟶ A ⟹ B)
          ((Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology LightProfinite)) :
              (a : ((forget R).obj (A ⟹ B)).obj.obj (Opposite.op S)) →
                (coherentTopology LightProfinite).yoneda.obj S ⟶ (forget R).obj (A ⟹ B))
            x)) :
      tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) A
          (obj (free R) (obj (GrothendieckTopology.yoneda (coherentTopology LightProfinite)) S)) ⟶
        B)

Tactic:
rfl

Premises used: CategoryTheory.MonoidalClosed.uncurry, rfl
-- Module: Mathlib.Condensed.Light.InternallyProjective
Goal:
R : Type u
inst : CommRing R
A B : LightCondMod R
S : LightProfinite
x :
  tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) A
      (obj (free R) S.toCondensed) ⟶
    B
⊢ Eq (α := (↑((A ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u))
    (((ihomPoints R A B S).symm :
          (a : A ⊗ (free R).obj S.toCondensed ⟶ B) → (↑((A ⟹ B).obj.obj (Opposite.op S)) : Type u))
        x :
      (↑((A ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u))
    ((GrothendieckTopology.yonedaEquiv (coherentTopology LightProfinite) :
          (a : (coherentTopology LightProfinite).yoneda.obj S ⟶ (forget R).obj (A ⟹ B)) →
            ((forget R).obj (A ⟹ B)).obj.obj (Opposite.op S))
        ((Adjunction.homEquiv (freeForgetAdjunction R)
              (obj (GrothendieckTopology.yoneda (coherentTopology LightProfinite)) S) (A ⟹ B) :
            (a : (free R).obj ((coherentTopology LightProfinite).yoneda.obj S) ⟶ A ⟹ B) →
              (coherentTopology LightProfinite).yoneda.obj S ⟶ (forget R).obj (A ⟹ B))
          (MonoidalClosed.curry x)) :
      (obj (forget R) (A ⟹ B)).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Condensed.Light.InternallyProjective
Goal:
R : Type u
inst : CommRing R
A B P : LightCondMod R
S : LightProfinite
e : A ⟶ B
x : (↑((P ⟹ A).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u)
⊢ Eq (α := (obj (forget R) (P ⟹ B)).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
    ((GrothendieckTopology.yonedaEquiv (coherentTopology LightProfinite) :
          (a : (coherentTopology LightProfinite).yoneda.obj S ⟶ (forget R).obj (P ⟹ B)) →
            ((forget R).obj (P ⟹ B)).obj.obj (Opposite.op S))
        ((Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology LightProfinite)) :
            (a : ((forget R).obj (P ⟹ B)).obj.obj (Opposite.op S)) →
              (coherentTopology LightProfinite).yoneda.obj S ⟶ (forget R).obj (P ⟹ B))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (X :=
                  (P ⟹ A).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
                  (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map (ihom P) e)) (Opposite.op S)) :
                (a : (↑((P ⟹ A).obj.obj (Opposite.op S)) : Type u)) → (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u))
              x :
            (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u))) :
      (obj (forget R) (P ⟹ B)).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
    ((GrothendieckTopology.yonedaEquiv (coherentTopology LightProfinite) :
          (a : (coherentTopology LightProfinite).yoneda.obj S ⟶ (forget R).obj (P ⟹ B)) →
            ((forget R).obj (P ⟹ B)).obj.obj (Opposite.op S))
        ((Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology LightProfinite)) :
              (a : ((forget R).obj (P ⟹ A)).obj.obj (Opposite.op S)) →
                (coherentTopology LightProfinite).yoneda.obj S ⟶ (forget R).obj (P ⟹ A))
            x ≫
          CategoryTheory.Functor.map (forget R) (CategoryTheory.Functor.map (ihom P) e)) :
      (obj (forget R) (P ⟹ B)).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))

Tactic:
simp [dsimp% GrothendieckTopology.yonedaEquiv_comp]

Premises used: CategoryTheory.GrothendieckTopology.yonedaEquiv_comp
-- Module: Mathlib.Condensed.Light.InternallyProjective
Goal:
R : Type u
inst : CommRing R
B P : LightCondMod R
S S' : LightProfinite
π : S ⟶ S'
f :
  tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
      (obj (free R) S'.toCondensed) ⟶
    B
⊢ Eq (α := (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u))
    (((ihomPoints R P B S).symm :
          (a : P ⊗ (free R).obj S.toCondensed ⟶ B) → (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u))
        (P ◁ CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map π) ≫ f) :
      (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map π.op) :
          (a : (↑((P ⟹ B).obj.obj (Opposite.op S')) : Type u)) → (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u))
        (((ihomPoints R P B S').symm :
              (a : P ⊗ (free R).obj S'.toCondensed ⟶ B) → (↑((P ⟹ B).obj.obj (Opposite.op S')) : Type u))
            f :
          (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u)) :
      (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u))

Tactic:
simpa [ihomPoints_symm_apply, MonoidalClosed.curry_natural_left, Adjunction.homEquiv_apply] using
    (GrothendieckTopology.yonedaEquiv_naturality _ _ _).symm

Premises used: CategoryTheory.MonoidalClosed.curry_natural_left, CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality, LightCondensed.ihomPoints_symm_apply, CategoryTheory.Adjunction.homEquiv_apply, Eq.symm
-- Module: Mathlib.Condensed.Light.InternallyProjective
Goal:
R : Type u
inst : CommRing R
P : LightCondMod R
h_1 : InternallyProjective P
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g :
  tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
      (obj (free R) S.toCondensed) ⟶
    B
h : isInternallyProjective P
⊢ Epi (X := P ⟹ A) (CategoryTheory.Functor.map (ihom P) e)

Tactic:
have hh := h.1 e
-- Module: Mathlib.Condensed.Light.InternallyProjective
Goal:
R : Type u
inst : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g :
  tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite)))
      (obj (free R) S.toCondensed) P ⟶
    B
S' : LightProfinite
π : S' ⟶ S
hπ :
  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)
g' :
  tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
      (obj (free R) S'.toCondensed) ⟶
    A
hh :
  P ◁ CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫
      Iso.hom (β_ P (obj (free R) S.toCondensed)) ≫ g =
    g' ≫ e
⊢ CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ▷ P ≫ g =
    (Iso.inv (β_ P (obj (free R) S'.toCondensed)) ≫ g') ≫ e

Tactic:
simp [← hh]
-- Module: Mathlib.Condensed.Light.InternallyProjective
Goal:
R : Type u
inst : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g :
  tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
      (obj (free R) S.toCondensed) ⟶
    B
S' : LightProfinite
π : S' ⟶ S
hπ :
  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)
g' :
  tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite)))
      (obj (free R) S'.toCondensed) P ⟶
    A
hh :
  CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ▷ P ≫
      Iso.inv (β_ P (obj (free R) S.toCondensed)) ≫ g =
    g' ≫ e
⊢ P ◁ CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫ g =
    (Iso.hom (β_ P (obj (free R) S'.toCondensed)) ≫ g') ≫ e

Tactic:
simp [← hh]
-- Module: Mathlib.Condensed.Light.Module
Goal:
R : Type u
inst : Ring R
X : LightCondMod R
S T : LightProfiniteᵒᵖ
f : S ⟶ T
a : (↑((Functor.obj (sheafToPresheaf (coherentTopology LightProfinite) (ModuleCat R)) X).obj S) : Type u)
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      ((Functor.obj (forget R) X).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj T))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.obj (forget R) X).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map f) :
          (a : (fun (X : Type u) ↦ X) (((forget R).obj X).obj.obj S)) →
            (fun (X : Type u) ↦ X) (((forget R).obj X).obj.obj T))
        a :
      (fun (X : Type u) ↦ X)
        ((Functor.obj (forget R) X).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj T))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map f) :
          (a : (↑(X.obj.obj S) : Type u)) → (↑(X.obj.obj T) : Type u))
        a :
      (↑(X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj T) : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Condensed.Light.Module
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f : X ⟶ Y
S : LightProfiniteᵒᵖ
a : (↑((Functor.obj (sheafToPresheaf (coherentTopology LightProfinite) (ModuleCat R)) X).obj S) : Type u)
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      ((Functor.obj (forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj S))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map (forget R) f)) S) :
          (a : (fun (X : Type u) ↦ X) (((forget R).obj X).obj.obj S)) →
            (fun (X : Type u) ↦ X) (((forget R).obj Y).obj.obj S))
        a :
      (fun (X : Type u) ↦ X)
        ((Functor.obj (forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj S))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (f.hom.app S) :
          (a : (↑(X.obj.obj S) : Type u)) → (↑(Y.obj.obj S) : Type u))
        a :
      (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj S) : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Condensed.Light.Module
Goal:
R : Type u
inst : Ring R
⊢ Functor.IsLeftAdjoint (D := LightCondMod R) (free R)

Tactic:
freeForgetAdjunction R |>.isLeftAdjoint

Premises used: LightCondensed.freeForgetAdjunction, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.Condensed.Light.Module
Goal:
R : Type u
inst : Ring R
⊢ Functor.IsRightAdjoint (D := LightCondMod R) (LightCondensed.forget R)

Tactic:
freeForgetAdjunction R |>.isRightAdjoint

Premises used: LightCondensed.freeForgetAdjunction, CategoryTheory.Adjunction.isRightAdjoint
-- Module: Mathlib.Condensed.Light.Module
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f : X ⟶ Y
S T : LightProfiniteᵒᵖ
g : S ⟶ T
x : (↑(X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj S) : Type u)
⊢ Eq (α := (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj T) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (f.hom.app T) :
          (a : (↑(X.obj.obj T) : Type u)) → (↑(Y.obj.obj T) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map g) :
              (a : (↑(X.obj.obj S) : Type u)) → (↑(X.obj.obj T) : Type u))
            x :
          (↑(X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj T) : Type u)) :
      (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj T) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map g) :
          (a : (↑(Y.obj.obj S) : Type u)) → (↑(Y.obj.obj T) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (f.hom.app S) :
              (a : (↑(X.obj.obj S) : Type u)) → (↑(Y.obj.obj S) : Type u))
            x :
          (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj S) : Type u)) :
      (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj T) : Type u))

Tactic:
NatTrans.naturality_apply f.hom g x

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Condensed.Light.Monoidal
Goal:
R : Type u
inst : CommRing R
⊢ MorphismProperty.IsMonoidal (C := LightProfiniteᵒᵖ ⥤ ModuleCat R)
    (GrothendieckTopology.W (coherentTopology LightProfinite))

Tactic:
GrothendieckTopology.W.transport_isMonoidal _ _
    ((equivSmallModel.{u} LightProfinite.{u}).inverse.inducedTopology
      (coherentTopology LightProfinite.{u}))
    (equivSmallModel.{u} LightProfinite.{u}).inverse

Premises used: CategoryTheory.Functor.inducedTopology, CategoryTheory.GrothendieckTopology.W.transport_isMonoidal, LightProfinite, CategoryTheory.equivSmallModel, CategoryTheory.coherentTopology, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
R : Type
inst : CommRing R
X Y : LightProfinite
y :
  (↑(Y.toTop (P := fun (X : TopCat.{u_1}) ↦
        TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
    Type u_1)
f : X ⟶ Y
⊢ Continuous (X :=
    (fun
          (X :
            CompHausLike fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
          Type u_1))
      X)
    (Y :=
    (fun
          (X :
            CompHausLike fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
          Type u_1))
      Y)
    (⇑(ConcreteCategory.hom (FC :=
          fun
            (x1 x2 :
              CompHausLike fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
              Type u_1),
            (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
              Type u_1)))
          (CC :=
          fun
            (X :
              CompHausLike fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
            Type u_1))
          f) :
      (a :
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
              (↑X.toTop : Type u_1))
            X) →
        (fun
              (X :
                CompHausLike fun (X : TopCat) ↦
                  TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
            (↑X.toTop : Type u_1))
          Y)

Tactic:
fun_prop
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
t : T
⊢ t ∈ fibres π σ ↔ (π t).2 = none ∨ ∃ (x : X) (s : S), σ (Option.some x) s = t

Tactic:
simp [fibres]

Premises used: _private.0.InternalProjectivityProof.fibres
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
h :
  ∀ (x : T),
    x ∈ (fibres π σ)ᶜ ↔
      Membership.mem (γ := Set T) (⋃ (i : X), (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)}) x
⊢ (fibres π σ)ᶜ = ⋃ (i : X), (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)}

Tactic:
ext x