mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g✝ : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
g : X ⟶ Y
⊢ ((sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj (op (of P PUnit.{u + 1})) ⋙
            functor P hs).map
        g ≫
      ObjectProperty.homMk (counitApp Y.obj) =
    ObjectProperty.homMk (counitApp X.obj) ≫ (𝟭 (Sheaf (coherentTopology (CompHausLike P)) (Type (max u w)))).map g

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
⊢ (∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))) →
    Condensed.IsDiscrete M

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (max u w)
inst✝² : Ring R
inst✝¹ : HasExplicitFiniteCoproducts P
inst✝ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
X : ModuleCat R
⊢ Presheaf.IsSheaf (coherentTopology (CompHausLike P)) ((functorToPresheaves R).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
tfae_7_to_1 :
  (∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))) →
    Condensed.IsDiscrete M
⊢ Condensed.IsDiscrete M →
    ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
M : ModuleCat R
⊢ IsIso ((Condensed.forget R).map ((discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj M)))

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
⊢ [Condensed.IsDiscrete M, IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (Condensed.discrete (ModuleCat R)).essImage M, (functor R).essImage M,
      IsIso ((LocallyConstant.adjunction R).counit.app M),
      Sheaf.IsConstant (coherentTopology Profinite)
        ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))].TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: X : LightCondSet
h : (S : LightProfinite) → IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ LocallyConstant.functor.essImage X

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: X : LightCondSet
⊢ [LightCondensed.IsDiscrete X, IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X),
      (LightCondensed.discrete (Type u)).essImage X, functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      ∀ (S : LightProfinite), Nonempty (IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
⊢ functorToPresheaves.map ((unit P hs).app X) ≫ ((counit P hs).app ((functor P hs).obj X)).hom =
    𝟙 (functorToPresheaves.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
⊢ ∀ (X : Type (max u w)),
    (functor P hs).map ((unit P hs).app X) ≫ (counit P hs).app ((functor P hs).obj X) = 𝟙 ((functor P hs).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (functor R).map f ≫ (functorIsoDiscreteComponents R Y✝).symm.hom =
    (functorIsoDiscreteComponents R X✝).symm.hom ≫ (discrete (ModuleCat R)).map f

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
⊢ (∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    LightCondensed.IsDiscrete M

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_6_to_1 :
  (∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    LightCondensed.IsDiscrete M
⊢ LightCondensed.IsDiscrete M →
    ∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : LightCondMod R
⊢ [LightCondensed.IsDiscrete M, IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (LightCondensed.discrete (ModuleCat R)).essImage M, (functor R).essImage M,
      IsIso ((LocallyConstant.adjunction R).counit.app M),
      ∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
x : X.obj.obj (op (of P PUnit.{u + 1}))
this✝ : Preregular (CompHausLike P)
this : PreservesFiniteProducts ((sheafToPresheaf (coherentTopology (CompHausLike P)) (Type (max u w))).obj X) :=
  @CompHausLike.LocallyConstant.adjunction._proof_2 P inst✝² inst✝¹ hs X this✝
a : Fiber ⇑((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x)
⊢ PUnit.unit ∈ ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Epi

Goal state before:
pp: A : Type u'
inst✝⁸ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁷ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁶ : ConcreteCategory A FA
inst✝⁵ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁴ : (coherentTopology CompHaus).WEqualsLocallyBijective A
inst✝³ : HasSheafify (coherentTopology CompHaus) A
inst✝² : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)
inst✝¹ : Balanced (Sheaf (coherentTopology CompHaus) A)
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
⊢ Epi f ↔
    ∀ (S : CompHaus) (y : ToType (Y.obj.obj (op S))),
      ∃ S' φ, ∃ (_ : Function.Surjective ⇑(hom φ)), ∃ x, (hom (f.hom.app (op S'))) x = (hom (Y.obj.map (op φ))) y

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
⊢ IsIso ((LightCondensed.forget R).map ((discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj M)))

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Epi

Goal state before:
pp: A : Type u'
inst✝⁹ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁸ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁷ : ConcreteCategory A FA
inst✝⁶ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁵ : PreservesFiniteProducts (CategoryTheory.forget A)
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝³ : (extensiveTopology Stonean).WEqualsLocallyBijective A
inst✝² : HasSheafify (extensiveTopology Stonean) A
inst✝¹ : (extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)
inst✝ : Balanced (Sheaf (extensiveTopology Stonean) A)
⊢ Epi f ↔ ∀ (S : Stonean), Function.Surjective ⇑(hom (f.hom.app (op S.compHaus)))

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝² : Category.{v_1, u_1} A
inst✝¹ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
F : Stoneanᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts F
⊢ IsSheaf (coherentTopology Stonean) F

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : ReflectsFiniteProducts (CategoryTheory.forget A)
F : Stoneanᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
⊢ IsSheaf (coherentTopology Stonean) F

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝² : Category.{v_1, u_1} A
inst✝¹ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X profiniteToCompHaus.op) A
F : Profiniteᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ IsSheaf (coherentTopology Profinite) F

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
⊢ (unit P hs).app
        (((sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj (op (of P PUnit.{u + 1}))).obj X) ≫
      ((sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj (op (of P PUnit.{u + 1}))).map
        ((counit P hs).app X) =
    𝟙 (((sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj (op (of P PUnit.{u + 1}))).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X profiniteToCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : ReflectsFiniteLimits (CategoryTheory.forget A)
F : Profiniteᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)
⊢ IsSheaf (coherentTopology Profinite) F

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
F : CompHausᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ IsSheaf (coherentTopology CompHaus) F

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.EffectiveEpi

Goal state before:
pp: X✝ Y✝ : CompHaus
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi (compHausToCondensed.map f)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝⁴ : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : ReflectsFiniteLimits (CategoryTheory.forget A)
F : CompHausᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)
⊢ IsSheaf (coherentTopology CompHaus) F

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (functor R).map f ≫ (functorIsoDiscreteComponents R Y✝).symm.hom =
    (functorIsoDiscreteComponents R X✝).symm.hom ≫ (discrete (ModuleCat R)).map f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.Sequential

Goal state before:
pp: X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : SequentialSpace X✝
X Y : Sequential
f : ↑X.toTop ≃ₜ ↑Y.toTop
⊢ InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f, continuous_toFun := ⋯ }) ≫
      InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ }) =
    𝟙 X

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.Sequential

Goal state before:
pp: X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : SequentialSpace X✝
X Y : Sequential
f : ↑X.toTop ≃ₜ ↑Y.toTop
⊢ InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ }) ≫
      InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f, continuous_toFun := ⋯ }) =
    𝟙 Y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Cartesian

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop × ↑Y.toTop)
⊢ ∀ (s : BinaryFan X Y),
    ofHom P
          { toFun := fun x ↦ ((ConcreteCategory.hom s.fst) x, (ConcreteCategory.hom s.snd) x), continuous_toFun := ⋯ } ≫
        ofHom P { toFun := Prod.fst, continuous_toFun := ⋯ } =
      s.fst

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Cartesian

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop × ↑Y.toTop)
⊢ ∀ (s : BinaryFan X Y),
    ofHom P
          { toFun := fun x ↦ ((ConcreteCategory.hom s.fst) x, (ConcreteCategory.hom s.snd) x), continuous_toFun := ⋯ } ≫
        ofHom P { toFun := Prod.snd, continuous_toFun := ⋯ } =
      s.snd

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Cartesian

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop × ↑Y.toTop)
⊢ IsLimit (X.productCone Y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Cartesian

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop ⊕ ↑Y.toTop)
⊢ ∀ (s : BinaryCofan X Y),
    ofHom P { toFun := Sum.inl, continuous_toFun := ⋯ } ≫
        ofHom P
          { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ } =
      s.inl

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Cartesian

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop ⊕ ↑Y.toTop)
⊢ ∀ (s : BinaryCofan X Y),
    ofHom P { toFun := Sum.inr, continuous_toFun := ⋯ } ≫
        ofHom P
          { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ } =
      s.inr

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Cartesian

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop ⊕ ↑Y.toTop)
⊢ IsColimit (X.coproductCocone Y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Sequence

Goal state before:
pp: ⊢ IsClosedEmbedding ⇑natUnionInftyEmbedding

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X : LightCondSet
S : LightProfinite
x : X.obj.obj (Opposite.op S)
⊢ Continuous fun a ↦ X.coinducingCoprod ⟨⟨S, x⟩, a⟩

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
⊢ IsColimit ((locallyConstantPresheaf X).mapCocone c.op)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
⊢ Continuous ⇑(ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1}))))

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
s : Cocone ((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X)
i : I
f : LocallyConstant (↑(toProfinite.obj (F.obj i)).toTop) X
⊢ (ConcreteCategory.hom ((isColimitLocallyConstantPresheaf c X hc).desc s))
      (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) f) =
    (ConcreteCategory.hom (s.ι.app (Opposite.op i))) f

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : TopCat
⊢ Continuous fun x ↦ x.toFun PUnit.unit

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : LightCondSet
S : LightProfiniteᵒᵖ
x : X.obj.obj S
⊢ Continuous fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : LightCondSet
x✝² x✝¹ : LightProfiniteᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (X.obj.map x✝ ≫
      ↾fun x ↦
        { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x,
          continuous_toFun := ⋯ }) =
    (↾fun x ↦
        { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x,
          continuous_toFun := ⋯ }) ≫
      X.toTopCat.toLightCondSet.obj.map x✝

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ (lanPresheafExt i).hom.app S = colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.hom)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X Y✝ : LightCondSet
f : X ⟶ Y✝
Y : LightCondSet
⊢ lightCondSetToTopCat.map ({ app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 }.app Y) ≫
      { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }.app (lightCondSetToTopCat.obj Y) =
    𝟙 (lightCondSetToTopCat.obj Y)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : TopCat
⊢ Epi (topCatAdjunction.counit.app X)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : LightCondSet
⊢ SequentialSpace ↑X.toTopCat

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ (lanPresheafExt i).inv.app S = colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.inv)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : TopCat
inst✝ : SequentialSpace ↑X
⊢ Continuous (topCatAdjunctionCounitEquiv X).invFun

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
⊢ IsIso sequentialAdjunction.counit

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : IsColimit (F.mapCocone S.asLimitCone.op)
⊢ (lanPresheafIso hF).hom =
    colimit.desc (CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ F)
      (Profinite.Extend.cocone F S)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : (S : Profinite) → IsColimit (F.mapCocone S.asLimitCone.op)
X✝ Y✝ : Profiniteᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : CostructuredArrow toProfinite.op X✝
⊢ colimit.ι (CostructuredArrow.proj toProfinite.op X✝ ⋙ toProfinite.op ⋙ F) x✝ ≫
      colimit.desc (CostructuredArrow.proj toProfinite.op X✝ ⋙ toProfinite.op ⋙ F)
          { pt := colimit (CostructuredArrow.proj toProfinite.op Y✝ ⋙ toProfinite.op ⋙ F),
            ι :=
              {
                app := fun g ↦
                  colimit.ι (CostructuredArrow.proj toProfinite.op Y✝ ⋙ toProfinite.op ⋙ F)
                    ((CostructuredArrow.map x✝¹).obj g),
                naturality := ⋯ } } ≫
        colimit.desc (CostructuredArrow.proj toProfinite.op Y✝ ⋙ toProfinite.op ⋙ F)
          (Profinite.Extend.cocone F (Opposite.unop Y✝)) =
    colimit.ι (CostructuredArrow.proj toProfinite.op X✝ ⋙ toProfinite.op ⋙ F) x✝ ≫
      colimit.desc (CostructuredArrow.proj toProfinite.op X✝ ⋙ toProfinite.op ⋙ F)
          (Profinite.Extend.cocone F (Opposite.unop X✝)) ≫
        F.map x✝¹

Tactic:
by

Goal state after: