mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Light.EffectiveEpi

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

Tactic:
]

Goal state after:
X✝ Y✝ : LightProfinite
f : X✝ ⟶ Y✝
hf : Epi f
⊢ ∀ (S : LightProfinite) (y : (lightProfiniteToLightCondSet.obj Y✝).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom ((lightProfiniteToLightCondSet.map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom ((lightProfiniteToLightCondSet.obj Y✝).obj.map (Opposite.op φ))) y
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✝
⊢ (↾fun f ↦ ⇑f) ≫ (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (counitApp X).app (toProfinite.op.obj Y) ≫ X.map g

Tactic:
]

Goal state after:
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✝
⊢ (↾fun f ↦ ⇑f) ≫ (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (counitApp X).app (toProfinite.op.obj Y) ≫ X.map g
Module: Mathlib.Condensed.Light.EffectiveEpi

Goal state before:
pp: X✝ Y✝ : LightProfinite
f : X✝ ⟶ Y✝
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
S : LightProfinite
g : (lightProfiniteToLightCondSet.obj Y✝).obj.obj (Opposite.op S)
y : ↑S.toTop
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g)) a = y

Tactic:
]

Goal state after:
X✝ Y✝ : LightProfinite
f : X✝ ⟶ Y✝
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
S : LightProfinite
g : (lightProfiniteToLightCondSet.obj Y✝).obj.obj (Opposite.op S)
y : ↑S.toTop
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g)) a = y
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
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
]

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
F : LightProfiniteᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F
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)
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A) ∧ EqualizerCondition (F ⋙ CategoryTheory.forget A)

Tactic:
]

Goal state after:
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)
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A) ∧ EqualizerCondition (F ⋙ CategoryTheory.forget A)
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case e_a
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✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    counitAppAppImage f x

Tactic:
]

Goal state after:
case e_a
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✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    counitAppAppImage f x
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case e_a
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✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
this : Finite ↑(fiber f x).toTop
y : ↑(fiber f x).toTop
⊢ (ConcreteCategory.hom (X.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) y ≫ sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom (X.map (𝟙 (Profinite.of PUnit.{u + 1})).op)) (Function.Fiber.image (⇑f) x)

Tactic:
]

Goal state after:
case e_a
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✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
this : Finite ↑(fiber f x).toTop
y : ↑(fiber f x).toTop
⊢ (ConcreteCategory.hom (X.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) y ≫ sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom (X.map (𝟙 (Profinite.of PUnit.{u + 1})).op)) (Function.Fiber.image (⇑f) x)
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
⊢ (∀ (X_1 : LightProfinite) (y : ToType (Y.obj.obj (Opposite.op X_1))),
      ∃ X' φ,
        ∃ (_ : EffectiveEpi φ),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op X'))) x =
              (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y) ↔
    ∀ (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:
]

Goal state after:
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
⊢ (∀ (X_1 : LightProfinite) (y : ToType (Y.obj.obj (Opposite.op X_1))),
      ∃ X' φ,
        ∃ (_ : EffectiveEpi φ),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op X'))) x =
              (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y) ↔
    ∀ (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
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toLightProfinite.obj (F.obj k)).toTop
x : ↑(((const ℕᵒᵖ).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
⊢ ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map ki)).hom) g } fi)
      ((ConcreteCategory.hom (c.π.app k)) x) =
    ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map kj)).hom) g } fj)
      ((ConcreteCategory.hom (c.π.app k)) x)

Tactic:
]

Goal state after:
case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toLightProfinite.obj (F.obj k)).toTop
x : ↑(((const ℕᵒᵖ).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
⊢ ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map ki)).hom) g } fi)
      ((ConcreteCategory.hom (c.π.app k)) x) =
    ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map kj)).hom) g } fj)
      ((ConcreteCategory.hom (c.π.app k)) x)
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
⊢ IsLocallySurjective 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:
]

Goal state after:
X Y : LightCondSet
f : X ⟶ Y
⊢ IsLocallySurjective 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
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
⊢ IsLocallySurjective 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:
]

Goal state after:
R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
⊢ IsLocallySurjective 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
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 : IsLocallySurjective ((LightCondensed.forget R).map f)
⊢ IsLocallySurjective f

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f✝ : X ⟶ Y
X✝ Y✝ : LightCondMod R
f : X✝ ⟶ Y✝
hf : IsLocallySurjective ((LightCondensed.forget R).map f)
⊢ IsLocallySurjective f
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 : IsLocallySurjective f
⊢ IsLocallySurjective ((LightCondensed.forget R).map f)

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f✝ : X ⟶ Y
X✝ Y✝ : LightCondMod R
f : X✝ ⟶ Y✝
hf : IsLocallySurjective f
⊢ IsLocallySurjective ((LightCondensed.forget R).map f)
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
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
⊢ ∃ T π g, Epi π ∧ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p = g ≫ f

Tactic:
]

Goal state after:
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
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
⊢ ∃ T π g, Epi π ∧ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p = g ≫ f
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h✝¹ :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toLightProfinite.obj (F.obj k)).toTop
x : ↑(((const ℕᵒᵖ).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
h :
  (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi) x =
    (LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj) x
⊢ fi ((ConcreteCategory.hom (c.π.app i)) x) = fj ((ConcreteCategory.hom (c.π.app j)) x)

Tactic:
]

Goal state after:
case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h✝¹ :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toLightProfinite.obj (F.obj k)).toTop
x : ↑(((const ℕᵒᵖ).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
h :
  (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi) x =
    (LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj) x
⊢ fi ((ConcreteCategory.hom (c.π.app i)) x) = fj ((ConcreteCategory.hom (c.π.app j)) x)
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 (s.ι.app (Opposite.op n))) f = (ConcreteCategory.hom (s.ι.app (Opposite.op n))) f

Tactic:
]

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 (s.ι.app n)) f = (ConcreteCategory.hom (s.ι.app n)) f

Tactic:
]

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
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ (lightProfiniteToLightCondSet.map π ≫
        ((LightCondensed.freeForgetAdjunction R).homEquiv (lightProfiniteToLightCondSet.obj S) Y) p).hom =
    ((coherentTopology LightProfinite).yonedaEquiv.symm (Quiver.Hom.unop (Opposite.op π)) ≫
        ((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p).hom

Tactic:
]

Goal state after:
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
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ (lightProfiniteToLightCondSet.map π ≫
        ((LightCondensed.freeForgetAdjunction R).homEquiv (lightProfiniteToLightCondSet.obj S) Y) p).hom =
    ((coherentTopology LightProfinite).yonedaEquiv.symm (Quiver.Hom.unop (Opposite.op π)) ≫
        ((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p).hom
Module: Mathlib.Condensed.Discrete.Colimit

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

Tactic:
]

Goal state after:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
X : Type u
⊢ Presheaf.IsSheaf (coherentTopology LightProfinite) (locallyConstantPresheaf X)
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
x : ↑X.toTop
⊢ (f ∘ ⇑(ConcreteCategory.hom g)) x =
    (ConcreteCategory.hom (F.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) x).op))
      ((ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f))

Tactic:
]

Goal state after:
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
x : ↑X.toTop
⊢ (f ∘ ⇑(ConcreteCategory.hom g)) x =
    (ConcreteCategory.hom (F.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) x).op))
      ((ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f))
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))
⊢ (lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom =
    (lanPresheafNatIso fun x ↦
          isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x).hom ≫
      counitApp X

Tactic:
]

Goal state after:
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ (lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom =
    (lanPresheafNatIso fun x ↦
          isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x).hom ≫
      counitApp X
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
this : lim.map f = (Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom
⊢ Epi ((Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom)

Tactic:
]

Goal state after:
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
this : lim.map f = (Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom
⊢ Epi ((Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom)
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✝
⊢ (↾fun f ↦ ⇑f) ≫ (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (counitApp X).app (toLightProfinite.op.obj Y) ≫ X.map g

Tactic:
]

Goal state after:
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✝
⊢ (↾fun f ↦ ⇑f) ≫ (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (counitApp X).app (toLightProfinite.op.obj Y) ≫ X.map g