mathlib-initiative/mathlib-tactics huggingface dataset:
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✝
⊢ (lanPresheaf F).map x✝ ≫
      (match Y✝ with
        | Opposite.op S => lanPresheafIso (hF S)).hom =
    (match X✝ with
        | Opposite.op S => lanPresheafIso (hF S)).hom ≫
      F.map x✝

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Type (u + 1)
⊢ Presheaf.IsSheaf (coherentTopology Profinite) (lanPresheaf (locallyConstantPresheaf X))

Tactic:
by

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

Goal state before:
pp: S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Profinite
inst✝ : Finite ↑X.toTop
⊢ ∀ (t : Cofan fun x ↦ Profinite.of PUnit.{?u.15 + 1}) (j : ↑X.toTop),
    (fintypeCatAsCofan X).inj j ≫
        ConcreteCategory.ofHom { toFun := fun x ↦ (ConcreteCategory.hom (t.inj x)) PUnit.unit, continuous_toFun := ⋯ } =
      t.inj j

Tactic:
by

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

Goal state before:
pp: S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Profinite
inst✝ : Finite ↑X.toTop
x✝¹ : Cofan fun x ↦ Profinite.of PUnit.{?u.15 + 1}
x✝ : (fintypeCatAsCofan X).pt ⟶ x✝¹.pt
h : ∀ (j : ↑X.toTop), (fintypeCatAsCofan X).inj j ≫ x✝ = x✝¹.inj j
⊢ x✝ = ConcreteCategory.ofHom { toFun := fun x ↦ (ConcreteCategory.hom (x✝¹.inj x)) PUnit.unit, continuous_toFun := ⋯ }

Tactic:
by

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

Goal state before:
pp: F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝² : PreservesFiniteProducts F
X Y : Profinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))
g : X ⟶ Y
⊢ (ConcreteCategory.hom (isoFinYonedaComponents F X).inv) (f ∘ ⇑(ConcreteCategory.hom g)) =
    (ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f)

Tactic:
by

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

Goal state before:
pp: S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts F
X✝ Y✝ : FintypeCatᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (toProfinite.op ⋙ F).map x✝ ≫ (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop Y✝))).hom =
    (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop X✝))).hom ≫ (finYoneda F).map x✝

Tactic:
by

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

Goal state before:
pp: X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
this :
  ?m.112 ≫ (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (locallyConstantPresheaf
            (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))).map
        g ≫
      counitAppApp (Opposite.unop S) X
⊢ colimit.ι
        (CostructuredArrow.proj toProfinite.op S ⋙
          toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
        S =
    colimit.ι
        (CostructuredArrow.proj toProfinite.op S ⋙
          toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafNatIso fun x ↦
                isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) x).hom ≫
            counitApp X).app
        S

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.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 : LightProfiniteᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)
⊢ IsSheaf (coherentTopology LightProfinite) F

Tactic:
by

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

Goal state before:
pp: X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
⊢ (isoLocallyConstantOfIsColimit X hX).inv = counitApp X

Tactic:
by

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

Goal state before:
pp: A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
X Y : LightCondensed A
f : X ⟶ Y
⊢ IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : ToType (Y.obj.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y

Tactic:
by

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

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
⊢ Epi f ↔
    ∀ (S : LightProfinite) (y : Y.obj.obj (Opposite.op S)),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
⊢ Epi f ↔
    ∀ (S : LightProfinite) (y : ↑(Y.obj.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f✝ : X ⟶ Y
X✝ Y✝ : LightCondMod R
f : X✝ ⟶ Y✝
hf : Epi ((LightCondensed.forget R).map f)
⊢ Epi f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f✝ : X ⟶ Y
X✝ Y✝ : LightCondMod R
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi ((LightCondensed.forget R).map f)

Tactic:
by

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ IsColimit ((locallyConstantPresheaf X).mapCocone c.op)

Tactic:
by

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
s : Cocone ((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X)
n : ℕᵒᵖ
f : LocallyConstant (↑(toLightProfinite.obj (F.obj n)).toTop) X
⊢ (ConcreteCategory.hom ((isColimitLocallyConstantPresheaf c X hc).desc s))
      (LocallyConstant.comap (TopCat.Hom.hom (c.π.app n).hom) f) =
    (ConcreteCategory.hom (s.ι.app (Opposite.op n))) f

Tactic:
by

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

Goal state before:
pp: X : Type u
S : LightProfinite
s : Cocone (S.diagram.rightOp ⋙ locallyConstantPresheaf X)
n : ℕ
f : LocallyConstant (↑(S.diagram.obj (Opposite.op n)).toTop) X
⊢ (ConcreteCategory.hom ((isColimitLocallyConstantPresheafDiagram X S).desc s))
      (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app (Opposite.op n)).hom) f) =
    (ConcreteCategory.hom (s.ι.app n)) f

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ lanPresheaf F ≅ F

Tactic:
by

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

Goal state before:
pp: F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
⊢ (lanPresheafNatIso hF).hom.app S =
    colimit.desc (CostructuredArrow.proj toLightProfinite.op (Opposite.op (Opposite.unop S)) ⋙ toLightProfinite.op ⋙ F)
      (LightProfinite.Extend.cocone F (Opposite.unop S))

Tactic:
by

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

Goal state before:
pp: S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
X : Type u
⊢ Presheaf.IsSheaf (coherentTopology LightProfinite) (lanPresheaf (locallyConstantPresheaf X))

Tactic:
by

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

Goal state before:
pp: S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
X : LightProfinite
inst✝ : Finite ↑X.toTop
⊢ ∀ (t : Cofan fun x ↦ LightProfinite.of PUnit.{?u.15 + 1}) (j : ↑X.toTop),
    (fintypeCatAsCofan X).inj j ≫
        ConcreteCategory.ofHom { toFun := fun x ↦ (ConcreteCategory.hom (t.inj x)) PUnit.unit, continuous_toFun := ⋯ } =
      t.inj j

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
⊢ ∃ T π g, Epi π ∧ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p = g ≫ f

Tactic:
by

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

Goal state before:
pp: S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
X : LightProfinite
inst✝ : Finite ↑X.toTop
x✝¹ : Cofan fun x ↦ LightProfinite.of PUnit.{?u.15 + 1}
x✝ : (fintypeCatAsCofan X).pt ⟶ x✝¹.pt
h : ∀ (j : ↑X.toTop), (fintypeCatAsCofan X).inj j ≫ x✝ = x✝¹.inj j
⊢ x✝ = ConcreteCategory.ofHom { toFun := fun x ↦ (ConcreteCategory.hom (x✝¹.inj x)) PUnit.unit, continuous_toFun := ⋯ }

Tactic:
by

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

Goal state before:
pp: F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
⊢ (ConcreteCategory.hom (isoFinYonedaComponents F X).inv) (f ∘ ⇑(ConcreteCategory.hom g)) =
    (ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi (c.π.app (Opposite.op 0))

Tactic:
by

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

Goal state before:
pp: S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts F
X✝ Y✝ : FintypeCatᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (toLightProfinite.op ⋙ F).map x✝ ≫ (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop Y✝))).hom =
    (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop X✝))).hom ≫ (finYoneda F).map x✝

Tactic:
by

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

Goal state before:
pp: n✝ : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi ((Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op)

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f✝ : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f✝ n)
X✝ Y✝ : Discrete ℕ ⥤ LightCondMod R
f : X✝ ⟶ Y✝
x✝ : Epi f
⊢ lim.map f = (Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom

Tactic:
by

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

Goal state before:
pp: X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
this :
  ?m.112 ≫ (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (locallyConstantPresheaf
            (X.obj
              (Opposite.op
                (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
                  PUnit.{u + 1})))).map
        g ≫
      counitAppApp (Opposite.unop S) X
⊢ colimit.ι
        (CostructuredArrow.proj toLightProfinite.op S ⋙
          toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
        S =
    colimit.ι
        (CostructuredArrow.proj toLightProfinite.op S ⋙
          toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafNatIso fun x ↦
                isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x).hom ≫
            counitApp X).app
        S

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f✝ : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f✝ n)
X✝ Y✝ : Discrete ℕ ⥤ LightCondMod R
f : X✝ ⟶ Y✝
x✝ : Epi f
⊢ Epi (lim.map f)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B P : LightCondMod R
S : LightProfinite
e : A ⟶ B
x : ↑((P ⟹ A).obj.obj (Opposite.op S))
⊢ (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S))) x =
    (ihomPoints R P B S).symm ((ihomPoints R P A S) x ≫ e)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
B P : LightCondMod R
S S' : LightProfinite
π : S ⟶ S'
f : P ⊗ (free R).obj S'.toCondensed ⟶ B
⊢ (ihomPoints R P B S).symm (P ◁ (free R).map (lightProfiniteToLightCondSet.map π) ≫ f) =
    (ConcreteCategory.hom ((P ⟹ B).obj.map π.op)) ((ihomPoints R P B S').symm f)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
⊢ univ.PairwiseDisjoint Z

Tactic:
by

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

Goal state before:
pp: X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ (isoLocallyConstantOfIsColimit X hX).inv = counitApp X

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
i : S
⊢ Z i ⊆ D i

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
⊢ univ ⊆ ⋃ i, D i

Tactic:
by

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

Goal state before:
pp: C : Type w
inst✝¹ : Category.{v, w} C
R : Type u
inst✝ : CommRing R
⊢ sheafCompose ((equivSmallModel LightProfinite).inverse.inducedTopology (coherentTopology LightProfinite))
      (CategoryTheory.forget (ModuleCat R)) ≅
    (equivSmall (ModuleCat R)).inverse ⋙ forget R ⋙ (equivSmall (Type u)).symm.inverse

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : ∀ ⦃i : S⦄, i ∈ univ → ∀ ⦃j : S⦄, j ∈ univ → (C i ∩ C j).Nonempty → i = j
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ i ∈ univ

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Solid

Goal state before:
pp: R : Type (u + 1)
inst✝ : Ring R
⊢ (profiniteSolid R).IsRightKanExtension (profiniteSolidCounit R)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : ∀ ⦃i : S⦄, i ∈ univ → ∀ ⦃j : S⦄, j ∈ univ → (C i ∩ C j).Nonempty → i = j
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ j ∈ univ

Tactic:
by

Goal state after: