mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
this : IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)
⊢ IsCompact (range ((⋃₀ 𝔖).domRestrict ∘ F))

Tactic:
rw [← forall_sUnion] at F_pointwiseCompact

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ x ∈ ⋃₀ 𝔖, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
this : IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)
⊢ IsCompact (range ((⋃₀ 𝔖).domRestrict ∘ F))
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
e : P ≅ limit P.diagram := P.isoLimittoFiniteQuotientFunctor
⊢ eta G ≫
      (forget₂ ProfiniteGrp.{u} GrpCat).map
        (((limitConeIsLimit P.diagram).liftConeMorphism
              { pt := ofProfinite (Profinite.limitCone (diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite)).pt,
                π :=
                  {
                    app := fun H ↦
                      {
                          hom' :=
                            { toFun := fun x ↦ ↑x (preimage f H), map_one' := ⋯, map_mul' := ⋯,
                              continuous_toFun := ⋯ } } ≫
                        ofFiniteGrpHom (quotientMap f H),
                    naturality := ⋯ } }).hom ≫
          𝟙 (limit P.diagram)) =
    f ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map e.hom

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] F →ₗ[S] F
e : E
f : M → F
hL : ∀ (y : F), (L e) y = y
x : M
⊢ (1, x) ∈ mulFiber x

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (L y) e = y
x : M
⊢ (x, 1) ∈ mulFiber x

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
α : Type u_7
l : Filter α
f : α → E
x : E
hB_inj : Function.Injective ⇑B
⊢ Tendsto ((fun x1 x2 ↦ (B x1) x2) ∘ f) l (𝓝 fun x2 ↦ (B x) x2) ↔ Tendsto (fun i ↦ ⇑(B (f i))) l (𝓝 ⇑(B x))

Tactic:
Function.comp_def

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
α : Type u_7
l : Filter α
f : α → E
x : E
hB_inj : Function.Injective ⇑B
⊢ Tendsto (fun x x2 ↦ (B (f x)) x2) l (𝓝 fun x2 ↦ (B x) x2) ↔ Tendsto (fun i ↦ ⇑(B (f i))) l (𝓝 ⇑(B x))
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module S E
inst✝⁵ : Module S E'
F : Type u_10
inst✝⁴ : AddCommMonoid F
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousConstSMul S F
inst✝ : T2Space F
c : S
f : M → E
g : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
⊢ (c • f ⋆[L] g) x = c • (f ⋆[L] g) x

Tactic:
by
  simpa [convolution] using hfg.tsum_const_smul c

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module S E
inst✝⁵ : Module S E'
F : Type u_10
inst✝⁴ : AddCommMonoid F
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousConstSMul S F
inst✝ : T2Space F
c : S
f : M → E
g : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
⊢ (f ⋆[L] c • g) x = c • (f ⋆[L] g) x

Tactic:
by
  simpa [convolution] using hfg.tsum_const_smul c

Goal state after:
Module: Mathlib.Topology.Algebra.Ring.Compact

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsDedekindDomain R
hR : ¬IsField R
H : IsOpen ↑⊥
this : DiscreteTopology R
⊢ False

Tactic:
exact hR (Finite.isField_of_domain R)

Goal state after:
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: case compl
α : Type u_1
inst✝² : TopologicalSpace α
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
ht✝ : MeasurableSet s
ihs : ∃ u, IsOpen[inst✝²] u ∧ s =ᶠ[residual α] u
⊢ ∃ u, IsOpen[inst✝²] u ∧ sᶜ =ᶠ[residual α] u

Tactic:
obtain ⟨U, Uo, hsU⟩ := ihs
    use (closure U)ᶜ, isClosed_closure.isOpen_compl
    exact .compl <| hsU.trans <| .symm <| closure_residualEq Uo.isLocallyClosed

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
x : X
hx : x ∈ derivedSet (closure[inst✝¹] A)
⊢ x ∈ derivedSet A

Tactic:
mem_derivedSet,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
x : X
hx : AccPt x (𝓟 (closure[inst✝¹] A))
⊢ AccPt x (𝓟 A)
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
⊢ derivedSet U ⊆ U ∧ U ⊆ derivedSet U ↔ U = derivedSet U

Tactic:
← subset_antisymm_iff,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
⊢ derivedSet U = U ↔ U = derivedSet U
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h : (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty (cell b)
this : IsClosed[inst✝] (A ∩ (D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1))
n : ℕ
i : n < N
⊢ ⋃ j, ↑(map (↑⟨n, i⟩) j) '' closedBall 0 1 ⊆ ⋃ j, ↑(map n j) '' closedBall 0 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h : (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty (cell b)
this : IsClosed[inst✝] (A ∩ (D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1))
n : ℕ
⊢ ⋃ j, ↑(map n j) '' closedBall 0 1 = ⋃ (hx : n < N), ⋃ j, ↑(map (↑⟨n, hx⟩) j) '' closedBall 0 1

Tactic:
refine subset_antisymm ?_ (iUnion_subset (fun i ↦ by rfl))

Goal state after:
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h : (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty (cell b)
this : IsClosed[inst✝] (A ∩ (D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1))
n : ℕ
⊢ ⋃ j, ↑(map n j) '' closedBall 0 1 ⊆ ⋃ (hx : n < N), ⋃ j, ↑(map (↑⟨n, hx⟩) j) '' closedBall 0 1
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
⊢ openCell n i = openCell n ↑i

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
⊢ closedCell n i = closedCell n ↑i

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
⊢ cellFrontier n i = cellFrontier n ↑i

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: case inr
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : _root_.Finite ((n : ℕ) × cell C n)
h✝ : Nonempty ((n : ℕ) × cell C n)
x✝ : Fintype ((n : ℕ) × cell C n)
A : Finset ℕ := Finset.image Sigma.fst Finset.univ
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → IsEmpty (cell C b)

Tactic:
use A.max' (Finset.image_nonempty.2 Finset.univ_nonempty) + 1

Goal state after:
case h
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : _root_.Finite ((n : ℕ) × cell C n)
h✝ : Nonempty ((n : ℕ) × cell C n)
x✝ : Fintype ((n : ℕ) × cell C n)
A : Finset ℕ := ⋯
⊢ ∀ (b : ℕ), A.max' ⋯ + 1 ≤ b → IsEmpty (cell C b)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
x : X.A
⊢ (ConcreteCategory.hom (𝟙 X.A)) x = x

Tactic:
rfl

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

Goal state before:
pp: X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (ConcreteCategory.hom (β.map f.f ≫ Y.a)) xs = Y.str (Ultrafilter.map (⇑(ConcreteCategory.hom f)) xs)

Tactic:
rfl

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

Goal state before:
pp: X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ (ConcreteCategory.hom (β.map X.a ≫ X.a)) uux = X.str (Ultrafilter.map X.str uux)

Tactic:
rfl

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

Goal state before:
pp: case mp
X : Compactum
S : Set X.A
⊢ IsOpen Sᶜ → ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

Tactic:
intro cond F h
    by_contra c
    specialize cond F c
    rw [compl_mem_iff_notMem] at cond
    contradiction

Goal state after:
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
⊢ ⨆ i, ⨆ f, coinduced (⇑f) inferInstance =
    ⨆ i, ⨆ j, coinduced (fun x ↦ x.fst.snd x.snd) (coinduced (Sigma.mk ⟨i, j⟩) (inst✝ ⟨i, j⟩.fst))

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
⊢ Continuous[tY, inst✝¹] g ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, inst✝¹] (g ∘ ⇑f)

Tactic:
rw [(homeomorph (X := X)).isQuotientMap.continuous_iff,
    WithGeneratedByTopology.continuous_from_iff]
  simp [Function.comp_assoc g, ← Function.comp_assoc WithGeneratedByTopology.equiv]

Goal state after:
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
⊢ ContinuousGeneratedBy X g ↔
    ∀ ⦃i : ι⦄ (f : C(X i, Y)),
      Continuous[inst✝² i, inst✝] ((g ∘ ⇑WithGeneratedByTopology.equiv) ∘ ⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K✝ : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
hc : ∀ (J : Finset ι) (s : ↑(obj C fun x ↦ x ∈ J)), IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})
J K : Finset ι
h : J ⊆ K
x : ↑C
hx : (π_app C fun x ↦ x ∈ K) x ∈ {↑a (op K)}
⊢ (map C h) (↑a (op K)) ∈
    {(ConcreteCategory.hom (((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).map (homOfLE h).op)) (↑a (op K))}

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
⊢ Fintype ↑(π C fun x ↦ x ∈ s)

Tactic:
by
  let f : π C (· ∈ s) → (s → Bool) := fun x j ↦ x.val j.val
  refine Fintype.ofInjective f ?_
  intro ⟨_, x, hx, rfl⟩ ⟨_, y, hy, rfl⟩ h
  ext i
  by_cases hi : i ∈ s
  · exact congrFun h ⟨i, hi⟩
  · simp only [Proj, if_neg hi]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ
a✝ : f ∈ ⊤
x : ↑(π C fun x ↦ x ∈ s)
⊢ ((Finsupp.onFinset Finset.univ f.toFun ⋯).sum fun i a ↦ a • spanFinBasis C s i) x = f x

Tactic:
change LocallyConstant.evalₗ ℤ x _ = _

Goal state after:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ
a✝ : f ∈ ⊤
x : ↑(π C fun x ↦ x ∈ s)
⊢ (LocallyConstant.evalₗ ℤ x) ((Finsupp.onFinset Finset.univ f.toFun ⋯).sum fun i a ↦ a • spanFinBasis C s i) = f x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ
a✝ : f ∈ ⊤
x : ↑(π C fun x ↦ x ∈ s)
h : ¬(Finsupp.onFinset Finset.univ f.toFun ⋯) x = 0
⊢ ↑((Finsupp.onFinset Finset.univ f.toFun ⋯) x) x = f x

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
hn : n ≠ 0
j : cell C n
⊢ (cellFrontier n j).Nonempty

Tactic:
by
  let : NeZero n := ⟨hn⟩
  use map n j (Pi.single 0 1)
  simp only [cellFrontier, mem_image, mem_sphere_iff_norm, sub_zero]
  use Pi.single 0 1, by simp [Pi.norm_single]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x z : cell C 0
h : (fun x ↦ ↑(map 0 x) ![]) x = (fun x ↦ ↑(map 0 x) ![]) z
hne : ¬x = z
⊢ ⟨0, x⟩ ≠ ⟨0, z⟩

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ C ⊆ C

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
⊢ Disjoint D (⋃ n, ⋃ j, openCell n j)

Tactic:
simp_rw [disjoint_iff_inter_eq_empty, inter_iUnion, iUnion_eq_empty]
  intro n i
  rw [inter_comm, (disjointBase n i).inter_eq]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J✝ K L : I → Prop
inst✝³ : (i : I) → Decidable (J✝ i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
J : (Finset I)ᵒᵖ
⊢ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := id, continuous_toFun := ⋯ } =
    𝟙 (of ↑(π C fun x ↦ x ∈ unop J))

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝³ : (i : I) → Decidable (J i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
X Y : (Finset I)ᵒᵖ
h : X ⟶ Y
⊢ 𝟙 (of ↑C) ≫
      ConcreteCategory.ofHom
        { toFun := ProjRestricts C ⋯ ∘ ProjRestrict C (Membership.mem (unop X)), continuous_toFun := ⋯ } =
    ConcreteCategory.ofHom { toFun := ProjRestrict C fun x ↦ x ∈ unop X, continuous_toFun := ⋯ } ≫
      (spanFunctor hC).map h

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
this : (fun x1 x2 ↦ x1 < x2) = fun l m ↦ List.Lex (fun x1 x2 ↦ x1 < x2) ↑l ↑m
⊢ (fun x1 x2 ↦ x1 > x2) = flip fun x1 x2 ↦ x1 < x2

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case inl
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h✝ : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
hn : 0 < n
j : cell C n
h : Disjoint A (openCell n j)
⊢ IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

Tactic:
left
    rw [disjoint_iff_inter_eq_empty.1 h]
    exact isClosed_empty

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : ord I i < o
⊢ x i = x i

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x ↦ false} ℤ
a✝ : f ∈ ⊤
⊢ ↑(f default) default = f default

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ (fun p ↦ ↑p) ∘ (range_equiv_smaller C o).toFun = ⇑(πs C o) ∘ fun p ↦ ↑p

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
i : I
ho : ord I i < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ term I ho = i

Tactic:
by
  simp only [term, ord, Ordinal.enum_typein]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ ((eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩).toFun ∘ ProjRestrict C fun x ↦ ord I x < o₁) =
    ⇑(eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩) ∘ ProjRestrict C fun x ↦ ord I x < o₁

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
f : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
⊢ ⇑((πs C o) f) = ⇑f ∘ ProjRestrict C fun x ↦ ord I x < o

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
f : LocallyConstant ↑(π C fun x ↦ ord I x < o₁) ℤ
⊢ ((πs' C h) f).toFun = f.toFun ∘ ProjRestricts C ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ E.carrier = ↑E

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
E : Subcomplex C
⊢ ⋃ n, ⋃ j, openCell n ↑j = ↑E

Tactic:
have := RelCWComplex.Subcomplex.union E (C := C)
  rw [empty_union] at this
  exact this

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Projective

Goal state before:
pp: case h
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
this : ⇑(ConcreteCategory.hom g.hom) ∘ g' = id
⊢ ⇑(ConcreteCategory.hom f) ∘ pure = ⇑(TopCat.Hom.hom f.hom) ∘ pure

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC✝ : contained C (Order.succ o)
ho✝ : o < Ordinal.type fun x1 x2 ↦ x1 < x2
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ Set.range (sum_to C ho) = GoodProducts C

Tactic:
rw [sum_to_range C ho, union_succ C hsC ho]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
val✝ : Products I
property✝ : val✝ ∈ GoodProducts (π C fun x ↦ ord I x < o)
x✝ : ↑C
⊢ ((eval C ∘ (sum_equiv C hsC ho).toFun) (Sum.inl ⟨val✝, property✝⟩)) x✝ =
    (Sum.elim (fun l ↦ Products.eval C ↑l) (fun l ↦ Products.eval C ↑l) (Sum.inl ⟨val✝, property✝⟩)) x✝

Tactic:
rfl

Goal state after: