mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: case h
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
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)
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
n : ℕ
i : cell n
⊢ MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ (fun m ↦ ⋯.toFinset) m, ↑(map m j) '' closedBall 0 1)

Tactic:
simp only [Finite.mem_toFinset, mem_univ, iUnion_true]

Goal state after:
case h
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
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)
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
n : ℕ
i : cell n
⊢ MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
Module: Mathlib.Topology.CWComplex.Classical.Graph

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
h : (cellFrontier 1 e).Subsingleton
x y : cell C 0
hxy : cellFrontier 1 e = {↑(map 0 y) ![], ↑(map 0 x) ![]}
⊢ (fun x ↦ ↑(map 0 x) ![]) x ∈ {↑(map 0 y) ![], ↑(map 0 x) ![]}

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
h : (cellFrontier 1 e).Subsingleton
x y : cell C 0
hxy : cellFrontier 1 e = {↑(map 0 y) ![], ↑(map 0 x) ![]}
⊢ (fun x ↦ ↑(map 0 x) ![]) y ∈ {↑(map 0 y) ![], ↑(map 0 x) ![]}

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous[inst✝¹, inst✝] f
hf2 : Function.Injective f
y : X
hy1 : AccPt y (𝓟 A)
⊢ f y ∈ derivedSet (f '' A) ↔ AccPt (f y) (map f (𝓟 A))

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
⊢ Preperfect U ↔ U = relDerivedSet U

Tactic:
by
  simp [preperfect_iff_subset_derivedSet]

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: case pos.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ IsClosed[inst✝¹] (derivedSet a)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: case pos.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ IsClosed[inst✝¹] (derivedSet b)

Tactic:
simp

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)),
    ∃ I, MapsTo (↑(map n ↑i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m ↑j) '' closedBall 0 1)

Tactic:
intro n i
    rcases cellFrontier_subset_finite_openCell (C := C) n i with ⟨J, hJ⟩
    use fun m ↦ Finset.preimage (J m) Subtype.val Subtype.val_injective.injOn
    rw [mapsTo_iff_image_subset]
    intro x hx
    specialize hJ hx
    simp_rw [iUnion_coe_set, mem_union, mem_iUnion, Finset.mem_preimage, exists_prop,
      Decidable.or_iff_not_imp_left] at hJ ⊢
    intro h
    specialize hJ h
    obtain ⟨m, hmn, j, hj, hxj⟩ := hJ
    suffices j ∈ E.I m from ⟨m, hmn, j, this, hj, openCell_subset_closedCell _ _ hxj⟩
    have : x ∈ (E : Set X) := E.cellFrontier_subset_of_mem i.2 hx
    by_contra hj'
    exact E.disjoint_openCell_subcomplex_of_not_mem hj' |>.notMem_of_mem_left hxj this

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

Goal state before:
pp: X : Compactum
A : Set X.A
a : X.A
ha : a ∈ A
⊢ X.str (X.incl a) = a

Tactic:
simp

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
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
⊢ ∀ ⦃i_1 : ι⦄ (f_1 : C(X i_1, X i)), Continuous[inst✝¹ i_1, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f) ∘ ⇑f_1)

Tactic:
intro j

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
j : ι
⊢ ∀ (f_1 : C(X j, X i)), Continuous[inst✝¹ j, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f) ∘ ⇑f_1)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type u_1
t₁ t₂ : TopologicalSpace Y
h₁ : IsGeneratedBy X Y
h₂ : IsGeneratedBy X Y
⊢ IsGeneratedBy X Y

Tactic:
rw [sup_eq_iSup]
  exact .iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩

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

Goal state before:
pp: case refine_2
ι : 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
b : ↑C
hb : ∀ (J : Finset ι), (π_app C fun x ↦ x ∈ J) b = ↑a (op J)
⊢ ∃ a_1, (ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) a_1 = a

Tactic:
use b
          apply Subtype.ext
          apply funext
          intro J
          exact hb (unop J)

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
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ContinuousOn (↑(map n j)) (closedBall 0 1)

Tactic:
exact continuousOn n j

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 y : cell C 0
h : closedCell 0 x = closedCell 0 y
⊢ x = y

Tactic:
closedCell_zero_eq_singleton,

Goal state after:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x y : cell C 0
h : {↑(map 0 x) ![]} = closedCell 0 y
⊢ x = y
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 y : cell C 0
h : {↑(map 0 x) ![]} = closedCell 0 y
⊢ x = y

Tactic:
closedCell_zero_eq_singleton,

Goal state after:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x y : cell C 0
h : {↑(map 0 x) ![]} = {↑(map 0 y) ![]}
⊢ x = y
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
⊢ ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst✝²] U → U ∈ F

Tactic:
intro U F h1 hU

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
U : Set X
F : Ultrafilter X
h1 : F.lim ∈ U
hU : IsOpen[inst✝²] U
⊢ U ∈ F
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case cons
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
a : I
as : List I
ih :
  ∃ l ∈ Finsupp.supported ℤ ℤ {m | ↑m ≤ as},
    (Finsupp.linearCombination ℤ (Products.eval (π C fun x ↦ x ∈ s))) l =
      (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
⊢ (if ↑x a = true then e (π C fun x ↦ x ∈ s) a else 1 - e (π C fun x ↦ x ∈ s) a) *
      (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
simp only [Finsupp.mem_supported, Finsupp.linearCombination_apply] at ih

Goal state after:
case cons
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
ih :
  ∃ l,
    ↑l.support ⊆ {m | ↑m ≤ as} ∧
      (l.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) =
        (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod
⊢ (if ↑x a = true then e (π C fun x ↦ x ∈ s) a else 1 - e (π C fun x ↦ x ∈ s) a) *
      (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
inst✝ : LinearOrder I
l m : Products I
⊢ l < m ↔ List.Lex (fun x1 x2 ↦ x1 < x2) ↑l ↑m

Tactic:
simp

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
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
⊢ IsClosed[t] (A ∩ ∅)

Tactic:
simp

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
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
⊢ IsClosed[t] (A ∩ ∅)

Tactic:
simp

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

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

Tactic:
subst h
    exact term_ord_aux ho

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

Goal state before:
pp: S : Profinite
C : { C // IsClopen C }
x : ↑S.toTop
⊢ x ∈ ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {false})ᶜ ↔ x ∈ ↑C

Tactic:
simp

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

Goal state before:
pp: X✝ Y✝ : UniformSpaceCat
f✝ : X✝.Hom Y✝
⊢ { hom' := ⟨↑f✝.hom' ∘ ↑{ hom' := ⟨id, ⋯⟩ }.hom', ⋯⟩ }.hom' = f✝.hom'

Tactic:
simp

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

Goal state before:
pp: X✝ Y✝ : UniformSpaceCat
f✝ : X✝.Hom Y✝
⊢ { hom' := ⟨↑{ hom' := ⟨id, ⋯⟩ }.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom' = f✝.hom'

Tactic:
simp

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

Goal state before:
pp: W✝ X✝ Y✝ Z✝ : UniformSpaceCat
f✝ : W✝.Hom X✝
g✝ : X✝.Hom Y✝
h✝ : Y✝.Hom Z✝
x✝ : W✝.carrier
⊢ ↑{ hom' := ⟨↑h✝.hom' ∘ ↑{ hom' := ⟨↑g✝.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom', ⋯⟩ }.hom' x✝ =
    ↑{ hom' := ⟨↑{ hom' := ⟨↑h✝.hom' ∘ ↑g✝.hom', ⋯⟩ }.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom' x✝

Tactic:
simp

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

Goal state before:
pp: X : UniformSpaceCat
Y : CpltSepUniformSpace
f : completionFunctor.obj X ⟶ Y
⊢ ((fun f ↦ extensionHom f) ((fun f ↦ X.completionHom ≫ f.hom) f)).hom = f.hom

Tactic:
simp

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

Goal state before:
pp: case top
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
x : X
m : ℕ
⊢ ↑m < ⊤ + 1 ↔ ↑m ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case inl
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
hα : IsEmpty α
⊢ IsCompactSystem (insert Set.univ S)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
x✝ : α
⊢ x✝ ∈ ⋂ i, s i ↔ x✝ ∈ ⋂ i, s' i

Tactic:
simp

Goal state after:
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
x✝ : α
⊢ (∀ (i : ℕ), x✝ ∈ s i) ↔ ∀ (i : ℕ), x✝ ∈ s' i
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : ⋂ i, s i = ⋂ i, s' i
j : ℕ
hj : dissipate s' j = ∅
v : ℕ
hv : n ≤ v
x✝ : α
⊢ x✝ ∈ dissipate s v ↔ x✝ ∈ dissipate s' v

Tactic:
simp

Goal state after:
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : ⋂ i, s i = ⋂ i, s' i
j : ℕ
hj : dissipate s' j = ∅
v : ℕ
hv : n ≤ v
x✝ : α
⊢ (∀ y ≤ v, x✝ ∈ s y) ↔ ∀ y ≤ v, x✝ ∈ s' y
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case zero
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
⊢ ∀
    (j :
      match 0 with
      | 0 => ↑D
      | n.succ => PEmpty.{u_1 + 1}),
    ↑(match 0, j with
          | 0, i => PartialEquiv.single ![] ↑i
          | n.succ, i => PEmpty.elim i) ''
        closedBall 0 1 ⊆
      D

Tactic:
simp

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

Goal state before:
pp: case succ
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n✝ : ℕ
⊢ ∀
    (j :
      match n✝ + 1 with
      | 0 => ↑D
      | n.succ => PEmpty.{u_1 + 1}),
    ↑(match n✝ + 1, j with
          | 0, i => PartialEquiv.single ![] ↑i
          | n.succ, i => PEmpty.elim i) ''
        closedBall 0 1 ⊆
      D

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
hi : ∀ (i : ℕ), C i ∈ S
h' : ∀ (n : ℕ), dissipate C n ≠ ∅
n : ℕ
g : ⋂ k, ⋂ (_ : k < n), C k ⊆ ∅
x : α
⊢ x ∈ ⋂ y, ⋂ (_ : y ≤ n), C y → x ∈ ⋂ k, ⋂ (_ : k < n), C k

Tactic:
simp

Goal state after:
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
hi : ∀ (i : ℕ), C i ∈ S
h' : ∀ (n : ℕ), dissipate C n ≠ ∅
n : ℕ
g : ⋂ k, ⋂ (_ : k < n), C k ⊆ ∅
x : α
⊢ (∀ i ≤ n, x ∈ C i) → ∀ i < n, x ∈ C i
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
hy : Infinite (ConnectedComponents X)
m : ℕ
⊢ 0 < m + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
hy : Infinite (ConnectedComponents X)
m : ℕ
U : Fin (m + 1) → Set X
hU1 : ∀ (i : Fin (m + 1)), IsClopen (U i)
hU2 : ∀ (i : Fin (m + 1)), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : ⋃ i, U i = Set.univ
⊢ ↑m ≤ ↑(m + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : ⋃ i, U i = Set.univ
heq : f ⁻¹' {y} = ⋃ i, U i ∩ f ⁻¹' {y}
⊢ ↑n ≤ ∑ i, 1

Tactic:
simp

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

Goal state before:
pp: case h₁
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
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
q : { l // Products.isGood (π C fun x ↦ ord I x < o) l }
a✝ : w q ≠ 0
⊢ (πs C o) (Products.eval (π C fun x ↦ ord I x < o) ↑q) ∈ Products.eval C '' {m | m < ↑l}

Tactic:
Products.eval_πs C (Products.prop_of_isGood _ _ q.prop)

Goal state after:
case h₁
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
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
q : { l // Products.isGood (π C fun x ↦ ord I x < o) l }
a✝ : w q ≠ 0
⊢ Products.eval C ↑q ∈ Products.eval C '' {m | m < ↑l}
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case refine_1
ι : Type u_1
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
U : ι → Set E
this : Countable ↑b
t : Finset ↑b
ht : A ⊆ ⋃ i ∈ t, U ↑i
hUo : ∀ (x : { a // a ∈ b }), IsOpen[inst✝] (U ↑x)
hAU : A ⊆ ⋃ x, U ↑x
hb : Countable ↑b
d : Finset { a // a ∈ b }
hd : A ⊆ ⋃ i ∈ d, U ↑i
⊢ Subtype.val '' ↑d ⊆ b

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
⊢ IsCountablyCompact A ↔
    ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i

Tactic:
simp [isCountablyCompact_iff_countable_open_cover, Finset.exists]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.LocallyConstant

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Monoid Y
inst✝ : ContinuousMul Y
a✝ : X
⊢ ↑1 a✝ = 1 a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.LocallyConstant

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Monoid Y
inst✝ : ContinuousMul Y
x y : LocallyConstant X Y
a✝ : X
⊢ ↑(x * y) a✝ = (↑x * ↑y) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.LocallyConstant

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : ContinuousAdd Y
inst✝ : ContinuousConstSMul R Y
x : R
y : LocallyConstant X Y
a✝ : X
⊢ ↑(x • y) a✝ = ((RingHom.id R) x • ↑y) a✝

Tactic:
simp

Goal state after: