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)
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)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
a : Fiber ⇑(map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f)
⊢ {
        toFun := fun g ↦
          comap
            (TopCat.Hom.hom
              (isTerminalPUnit.from
                  (fiber (map (⇑(ConcreteCategory.hom (↾fun x ↦ LocallyConstant.const PUnit.{u + 1} x))) f) a)).hom)
            g }
      (Fiber.image (⇑(map (⇑(ConcreteCategory.hom (↾fun x ↦ LocallyConstant.const PUnit.{u + 1} x))) f)) a) =
    {
        toFun := fun g ↦
          comap
            (TopCat.Hom.hom
              (sigmaIncl (map (⇑(ConcreteCategory.hom (↾fun x ↦ LocallyConstant.const PUnit.{u + 1} x))) f) a).hom)
            g }
      f

Tactic:
ext x

Goal state after:
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)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
a : Fiber ⇑(map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f)
x : ↑↑a
⊢ ({
          toFun := fun g ↦
            comap
              (TopCat.Hom.hom
                (isTerminalPUnit.from
                    (fiber (map (⇑(ConcreteCategory.hom (↾fun x ↦ LocallyConstant.const PUnit.{u + 1} x))) f) a)).hom)
              g }
        (Fiber.image (⇑(map (⇑(ConcreteCategory.hom (↾fun x ↦ LocallyConstant.const PUnit.{u + 1} x))) f)) a))
      x =
    ({
          toFun := fun g ↦
            comap
              (TopCat.Hom.hom
                (sigmaIncl (map (⇑(ConcreteCategory.hom (↾fun x ↦ LocallyConstant.const PUnit.{u + 1} x))) f) a).hom)
              g }
        f)
      x
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:
ext x

Goal state after:
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : SequentialSpace X✝
X Y : Sequential
f : ↑X.toTop ≃ₜ ↑Y.toTop
x : ↑X.toTop
⊢ (ConcreteCategory.hom
        (InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f, continuous_toFun := ⋯ }) ≫
          InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ })))
      x =
    (ConcreteCategory.hom (𝟙 X)) x
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:
ext x

Goal state after:
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : SequentialSpace X✝
X Y : Sequential
f : ↑X.toTop ≃ₜ ↑Y.toTop
x : ↑Y.toTop
⊢ (ConcreteCategory.hom
        (InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ }) ≫
          InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f, continuous_toFun := ⋯ })))
      x =
    (ConcreteCategory.hom (𝟙 Y)) x
Module: Mathlib.Topology.Category.CompHausLike.Cartesian

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

Tactic:
ext x

Goal state after:
case fst
P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop × ↑Y.toTop)
x✝¹ : BinaryFan X Y
x✝ : x✝¹.pt ⟶ of P (↑X.toTop × ↑Y.toTop)
h₁ : x✝ ≫ ofHom P { toFun := Prod.fst, continuous_toFun := ⋯ } = x✝¹.fst
h₂ : x✝ ≫ ofHom P { toFun := Prod.snd, continuous_toFun := ⋯ } = x✝¹.snd
x : ↑x✝¹.pt.toTop
⊢ ((ConcreteCategory.hom x✝) x).1 =
    ((ConcreteCategory.hom
          (ofHom P
            { toFun := fun x ↦ ((ConcreteCategory.hom x✝¹.fst) x, (ConcreteCategory.hom x✝¹.snd) x),
              continuous_toFun := ⋯ }))
        x).1

case snd
P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop × ↑Y.toTop)
x✝¹ : BinaryFan X Y
x✝ : x✝¹.pt ⟶ of P (↑X.toTop × ↑Y.toTop)
h₁ : x✝ ≫ ofHom P { toFun := Prod.fst, continuous_toFun := ⋯ } = x✝¹.fst
h₂ : x✝ ≫ ofHom P { toFun := Prod.snd, continuous_toFun := ⋯ } = x✝¹.snd
x : ↑x✝¹.pt.toTop
⊢ ((ConcreteCategory.hom x✝) x).2 =
    ((ConcreteCategory.hom
          (ofHom P
            { toFun := fun x ↦ ((ConcreteCategory.hom x✝¹.fst) x, (ConcreteCategory.hom x✝¹.snd) x),
              continuous_toFun := ⋯ }))
        x).2
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_2
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)
i j : I
fi : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toProfinite).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 : I
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
⊢ { toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toProfinite.map (F.map ki)).hom) g } fi =
    { toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toProfinite.map (F.map kj)).hom) g } fj

Tactic:
ext x

Goal state after:
case refine_2
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)
i j : I
fi : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toProfinite).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 : I
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x : ↑(toProfinite.obj (F.obj k)).toTop
⊢ ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toProfinite.map (F.map ki)).hom) g } fi) x =
    ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toProfinite.map (F.map kj)).hom) g } fj) x
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:
ext x

Goal state after:
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 : ↑(fintypeCatAsCofan X).pt.toTop
⊢ (ConcreteCategory.hom x✝) x =
    (ConcreteCategory.hom
        (ConcreteCategory.ofHom
          { toFun := fun x ↦ (ConcreteCategory.hom (x✝¹.inj x)) PUnit.unit, continuous_toFun := ⋯ }))
      x
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
⊢ f ∘ ⇑(ConcreteCategory.hom g) =
    (ConcreteCategory.hom (isoFinYonedaComponents F X).hom)
      ((ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f))

Tactic:
ext x

Goal state after:
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
x : ↑X.toTop
⊢ (f ∘ ⇑(ConcreteCategory.hom g)) x =
    (ConcreteCategory.hom (isoFinYonedaComponents F X).hom)
      ((ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f)) x
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
⊢ { toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map ki)).hom) g } fi =
    { toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map kj)).hom) g } fj

Tactic:
ext x

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
⊢ ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map ki)).hom) g } fi) x =
    ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map kj)).hom) g } fj) x
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:
ext x

Goal state after:
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 : ↑(fintypeCatAsCofan X).pt.toTop
⊢ (ConcreteCategory.hom x✝) x =
    (ConcreteCategory.hom
        (ConcreteCategory.ofHom
          { toFun := fun x ↦ (ConcreteCategory.hom (x✝¹.inj x)) PUnit.unit, continuous_toFun := ⋯ }))
      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
⊢ f ∘ ⇑(ConcreteCategory.hom g) =
    (ConcreteCategory.hom (isoFinYonedaComponents F X).hom)
      ((ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f))

Tactic:
ext x

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 (isoFinYonedaComponents F X).hom)
      ((ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f)) x
Module: Mathlib.Topology.Category.CompactlyGenerated

Goal state before:
pp: X✝ : Type w
inst✝¹ : TopologicalSpace X✝
inst✝ : UCompactlyGeneratedSpace X✝
X Y : CompactlyGenerated
f : ↑X.toTop ≃ₜ ↑Y.toTop
⊢ ofHom { toFun := ⇑f, continuous_toFun := ⋯ } ≫ ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ } = 𝟙 X

Tactic:
ext x

Goal state after:
X✝ : Type w
inst✝¹ : TopologicalSpace X✝
inst✝ : UCompactlyGeneratedSpace X✝
X Y : CompactlyGenerated
f : ↑X.toTop ≃ₜ ↑Y.toTop
x : ↑X.toTop
⊢ (ConcreteCategory.hom
        (ofHom { toFun := ⇑f, continuous_toFun := ⋯ } ≫ ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ }))
      x =
    (ConcreteCategory.hom (𝟙 X)) x
Module: Mathlib.Topology.Category.CompactlyGenerated

Goal state before:
pp: X✝ : Type w
inst✝¹ : TopologicalSpace X✝
inst✝ : UCompactlyGeneratedSpace X✝
X Y : CompactlyGenerated
f : ↑X.toTop ≃ₜ ↑Y.toTop
⊢ ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ } ≫ ofHom { toFun := ⇑f, continuous_toFun := ⋯ } = 𝟙 Y

Tactic:
ext x

Goal state after:
X✝ : Type w
inst✝¹ : TopologicalSpace X✝
inst✝ : UCompactlyGeneratedSpace X✝
X Y : CompactlyGenerated
f : ↑X.toTop ≃ₜ ↑Y.toTop
x : ↑Y.toTop
⊢ (ConcreteCategory.hom
        (ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ } ≫ ofHom { toFun := ⇑f, continuous_toFun := ⋯ }))
      x =
    (ConcreteCategory.hom (𝟙 Y)) x
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: case refine_3
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
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
h_glue : ∀ (i j : S), ∀ x ∈ C i, x ∈ C j → i = j
⊢ liftCover C (fun i x ↦ i) h_glue C_cover_univ ∘ f = g

Tactic:
ext x

Goal state after:
case refine_3
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
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
h_glue : ∀ (i j : S), ∀ x ∈ C i, x ∈ C j → i = j
x : X
⊢ (liftCover C (fun i x ↦ i) h_glue C_cover_univ ∘ f) x = g x
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : Profinite
inst✝¹ : Nonempty ↑S.toTop
inst✝ : Finite ↑S.toTop
X Y : Profinite
g : X ⟶ S
f : X ⟶ Y
x✝ : Mono f
this : ∀ (T : Profinite) [Nonempty ↑T.toTop], IsSplitEpi (CompHausLike.isTerminalPUnit.from T)
k : Y ⟶ S
left✝ : k ≫ CompHausLike.isTerminalPUnit.from S = CompHausLike.isTerminalPUnit.from Y
h2 : f ≫ k = g
⊢ ∃ h, f ≫ h = g

Tactic:
exact ⟨k, h2⟩

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

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := fun n ↦ { k // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) := fun n k ↦ ⟨⋯.choose, ⋯⟩
⊢ ∃ h, f ≫ h = g

Tactic:
let k_seq (n : Nat) : lifts n := Nat.rec ⟨k0, h_down0⟩ next n

Goal state after:
S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := fun n ↦ { k // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) := fun n k ↦ ⟨⋯.choose, ⋯⟩
k_seq : (n : ℕ) → lifts n := fun n ↦ Nat.rec ⟨k0, h_down0⟩ next n
⊢ ∃ h, f ≫ h = g
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
⊢ (fibres π σ)ᶜ = ⋃ i, (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {↑i}

Tactic:
ext x

Goal state after:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
⊢ x ∈ (fibres π σ)ᶜ ↔ x ∈ ⋃ i, (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {↑i}
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u_1} 0
β : TypeVec.{u_2} 0
f : α ⟹ β
⊢ f = nilFun

Tactic:
ext x

Goal state after:
α : TypeVec.{u_1} 0
β : TypeVec.{u_2} 0
f : α ⟹ β
x : Fin2 0
x✝ : α x
⊢ f x x✝ = nilFun x x✝
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u_1} 0
⊢ id = nilFun

Tactic:
ext x

Goal state after:
α : TypeVec.{u_1} 0
x : Fin2 0
x✝ : α x
⊢ id x x✝ = nilFun x x✝
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case h_fst
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) := ⋯
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S := ⋯
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := ⋯
n : ↑ℕ∪{∞}.toTop
⊢ ((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ fst S ℕ∪{∞} =
    (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
          (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
        y' ▷ ℕ∪{∞}) ≫
      fst S ℕ∪{∞}

Tactic:
ext x

Goal state after:
case h_fst
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
n : ↑ℕ∪{∞}.toTop
x : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop
⊢ (ConcreteCategory.hom (((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ fst S ℕ∪{∞})) x =
    (ConcreteCategory.hom
        ((lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
              (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
            y' ▷ ℕ∪{∞}) ≫
          fst S ℕ∪{∞}))
      x
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case h_snd
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) := ⋯
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S := ⋯
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := ⋯
n : ↑ℕ∪{∞}.toTop
⊢ ((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ snd S ℕ∪{∞} =
    (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
          (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
        y' ▷ ℕ∪{∞}) ≫
      snd S ℕ∪{∞}

Tactic:
ext x

Goal state after:
case h_snd
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
n : ↑ℕ∪{∞}.toTop
x : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop
⊢ (ConcreteCategory.hom (((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ snd S ℕ∪{∞})) x =
    (ConcreteCategory.hom
        ((lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
              (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
            y' ▷ ℕ∪{∞}) ≫
          snd S ℕ∪{∞}))
      x
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
f : Filter α
F : f.Realizer
⊢ (¬∀ (a : F.σ), (F.F.f a).Nonempty) ↔ f ≤ ⊥

Tactic:
F.le_iff Realizer.bot,

Goal state after:
α : Type u_1
f : Filter α
F : f.Realizer
⊢ (¬∀ (a : F.σ), (F.F.f a).Nonempty) ↔ ∀ (b : Realizer.bot.σ), ∃ a, F.F.f a ⊆ Realizer.bot.F.f b