mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ IsWellFounded (Products I) fun x1 x2 ↦ x1 < x2

Tactic:
this

Goal state after:
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
⊢ IsWellFounded (Products I) fun l m ↦ List.Lex (fun x1 x2 ↦ x1 < x2) ↑l ↑m
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
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
⊢ ∀ (n : ℕ) (j : cell C n), IsClosed[t] (A ∩ closedCell n j)

Tactic:
intro n j

Goal state after:
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), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
j : cell C n
⊢ IsClosed[t] (A ∩ closedCell n j)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
this : eval (π C J) l = 0
⊢ eval (π C J) l ∈ Submodule.span ℤ (eval (π C J) '' {m | m < l})

Tactic:
this

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
this : eval (π C J) l = 0
⊢ 0 ∈ Submodule.span ℤ (eval (π C J) '' {m | m < l})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h✝ : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
w✝ : I → Bool
left✝ : w✝ ∈ C
h : ∀ i ∈ ↑l, ↑⟨Proj J w✝, ⋯⟩ i = true
⊢ False

Tactic:
simpa [Proj, h'] using h i hi

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
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
this : Products.eval C '' {m | m < l} ⊆ ↑(Submodule.span ℤ (Set.range (eval C)))
⊢ L l

Tactic:
← span_le

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
this : Submodule.span ℤ (Products.eval C '' {m | m < l}) ≤ Submodule.span ℤ (Set.range (eval C))
⊢ L l
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case h.inr.inl
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (n + 1) i
l : ℕ
hln : l < n.succ
j : cell C l
hp : x ∈ D ∪ ⋃ m, ⋃ (_ : m < l), ⋃ j_1 ∈ p l ⋯ j m, openCell m j_1
hj : j ∈ J l
hxj : x ∈ cellFrontier l j
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell i i_1

Tactic:
[

Goal state after:
case h.inr.inl
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (n + 1) i
l : ℕ
hln : l < n.succ
j : cell C l
hp : x ∈ D ∪ ⋃ m, ⋃ (_ : m < l), ⋃ j_1 ∈ p l ⋯ j m, openCell m j_1
hj : j ∈ J l
hxj : x ∈ cellFrontier l j
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell i i_1
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
⊢ E ⊆ C

Tactic:
[

Goal state after:
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
⊢ E ⊆ C
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}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ Set.range (sum_to C ho) = GoodProducts (π C fun x ↦ ord I x < o) ∪ MaxProducts C ho

Tactic:
have : Set.range (sum_to C ho) = _ ∪ _ := Set.Sum.elim_range _ _

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
this : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
⊢ Set.range (sum_to C ho) = GoodProducts (π C fun x ↦ ord I x < o) ∪ MaxProducts C ho
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case neg
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
n : ℕ
x✝ : 0 < n
j : cell C n
h : j ∉ I n
⊢ Disjoint E (openCell n j)

Tactic:
[

Goal state after:
case neg
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
n : ℕ
x✝ : 0 < n
j : cell C n
h : j ∉ I n
⊢ Disjoint E (openCell n j)
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 ⊆ C

Tactic:
[

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ ↑E ⊆ C
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
⊢ D ⊆ ↑E

Tactic:
[

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ D ⊆ ↑E
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
⊢ l = ⟨term I ho :: ↑l.Tail, hlc⟩

Tactic:
[

Goal state after:
I : Type u
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
⊢ l = ⟨term I ho :: ↑l.Tail, hlc⟩
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
l : ℕ
i : cell C l
hi : i ∈ {x | ↑l < n}
⊢ closedCell l ↑⟨i, hi⟩ ⊆ ⋃ j, closedCell l j

Tactic:
exact subset_iUnion _ _

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
n m : ℕ∞
h : m ≤ n
⊢ ↑(skeletonLT C m) ⊆ ↑(skeletonLT C n)

Tactic:
[

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
⊢ ↑(skeletonLT C m) ⊆ ↑(skeletonLT C n)
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
n m : ℕ∞
h : m ≤ n
x : X
xmem : x ∈ ⋃ m_1, ⋃ (_ : ↑m_1 < m), ⋃ j, closedCell m_1 j
⊢ x ∈ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
[

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
x : X
xmem : x ∈ ⋃ m_1, ⋃ (_ : ↑m_1 < m), ⋃ j, closedCell m_1 j
⊢ x ∈ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j
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
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ x ∈ ⋃ m, ⋃ (_ : ↑m < ↑n + 1), ⋃ j, closedCell m j

Tactic:
[

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ x ∈ ⋃ m, ⋃ (_ : ↑m < ↑n + 1), ⋃ j, closedCell m j
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 ⊆ ⋃ i, ↑(skeletonLT C ↑i)

Tactic:
[

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ C ⊆ ⋃ i, ↑(skeletonLT C ↑i)
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 ⊆ ⋃ i, ↑(skeleton C ↑i)

Tactic:
[

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ C ⊆ ⋃ i, ↑(skeleton C ↑i)
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
n : ℕ∞
x : X
this : ∀ (m : ℕ), ↑m < n + 1 ↔ ↑m ≤ n
⊢ (x ∈ D ∨ ∃ m, ∃ (_ : ↑m < n + 1), ∃ j, x ∈ openCell m j) ↔ x ∈ D ∨ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ openCell m j

Tactic:
[

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
x : X
this : ∀ (m : ℕ), ↑m < n + 1 ↔ ↑m ≤ n
⊢ (x ∈ D ∨ ∃ m, ∃ (_ : ↑m < n + 1), ∃ j, x ∈ openCell m j) ↔ x ∈ D ∨ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ openCell m j
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
n : ℕ∞
x : X
this : ∀ (m : ℕ), ↑m < n + 1 ↔ ↑m ≤ n
⊢ (x ∈ D ∨ ∃ m, ∃ (_ : ↑m < n + 1), ∃ j, x ∈ openCell m j) ↔ x ∈ D ∨ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ openCell m j

Tactic:
this

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
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ Disjoint (↑(skeletonLT C n)) (openCell m j)

Tactic:
[

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ Disjoint (↑(skeletonLT C n)) (openCell m j)
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
⊢ Disjoint (interior D) (⋃ n, ⋃ j, closedCell n j)

Tactic:
[

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ Disjoint (interior D) (⋃ n, ⋃ j, closedCell n j)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
⊢ univ.PairwiseDisjoint fun ni ↦
    (fun a ↦
        ↑(match ni.fst, ni.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1

Tactic:
[

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
⊢ univ.PairwiseDisjoint fun ni ↦
    (fun a ↦
        ↑(match ni.fst, ni.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ IsCompactSystem S ↔
    ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty

Tactic:
[

Goal state after:
α : Type u_1
S : Set (Set α)
⊢ IsCompactSystem S ↔
    ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty
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).Nonempty
⊢ ∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty

Tactic:
[

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).Nonempty
⊢ ∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty
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 = ∅
⊢ dissipate C n = ∅

Tactic:
[

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 = ∅
⊢ dissipate C n = ∅
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : Equicontinuous fun x ↦ ⇑↑x
⊢ IsCompact A

Tactic:
[

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : Equicontinuous fun x ↦ ⇑↑x
⊢ IsCompact A
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case neg
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
a : E
haA : a ∈ A
hacc : AccPt a (𝓟 (range x ∩ A))
⊢ MapClusterPt a cofinite x

Tactic:
[

Goal state after:
case neg
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
a : E
haA : a ∈ A
hacc : AccPt a (𝓟 (range x ∩ A))
⊢ MapClusterPt a cofinite x
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case neg
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
a : E
haA : a ∈ A
hacc : AccPt a (𝓟 (range x ∩ A))
⊢ MapClusterPt a cofinite x

Tactic:
mapClusterPt_iff_frequently,

Goal state after:
case neg
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
a : E
haA : a ∈ A
hacc : AccPt a (𝓟 (range x ∩ A))
⊢ ∀ s ∈ 𝓝 a, ∃ᶠ (a : ℕ) in cofinite, x a ∈ s
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
⊢ IsCountablyCompact A

Tactic:
refine IsCountablyCompact.of_seq_clusterPt fun x hx => ?_
    rw [← Nat.cofinite_eq_atTop] at hx ⊢
    by_cases! hfin : (Set.range x).Finite
    · -- Case 1: Finite range
      suffices ∃ a ∈ range x ∩ A, MapClusterPt a cofinite x by aesop
      exact hfin.inter_of_left A |>.isCompact.exists_mapClusterPt_of_frequently <|
        hx.frequently.mp (by simp)
    · -- Case 2: Infinite range
      obtain ⟨a, haA, hacc⟩ := h (Set.range x ∩ A) inter_subset_right <| by
        rw [eventually_iff, mem_cofinite, compl_ofPred] at hx
        exact hfin.inter_of_finite_sdiff (hx.image x |>.subset (by grind))
      refine ⟨a, haA, ?_⟩
      simp_rw [mapClusterPt_iff_frequently, frequently_cofinite_iff_infinite]
      exact fun s hs ↦ Infinite.of_accPt (hacc.nhds_inter hs) |>.mono (by grind) |>.of_image x

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

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS : ∀ (f : C(X, Y)) (V : Set Y), IsOpen[inst✝¹] V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
⊢ ∀ (f : C(X, Y)) (x : X), ∀ V ∈ countableBasis Y, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V

Tactic:
intro f x V hV hx
      apply hS
      exacts [isOpen_of_mem_countableBasis hV, hx]

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ ⋂₀ {s | s ∈ 𝓝 l} = Iic l

Tactic:
[

Goal state after:
α : Type u_2
l : Filter α
⊢ ⋂₀ {s | s ∈ 𝓝 l} = Iic l
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
a : X
ha : a ∈ f ⁻¹' s
b : Y
hb : f =ᶠ[𝓝 a] fun x ↦ b
x : X
hx : x ∈ {x | (fun x ↦ f x = (fun x ↦ b) x) x}
this : f x = f a
⊢ f x ∈ s

Tactic:
this

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
a : X
ha : a ∈ f ⁻¹' s
b : Y
hb : f =ᶠ[𝓝 a] fun x ↦ b
x : X
hx : x ∈ {x | (fun x ↦ f x = (fun x ↦ b) x) x}
this : f x = f a
⊢ f a ∈ s
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p ↦ (eHmul (p.1, p.2.1), eHmul (p.1, p.2.2))
hG : Continuous G
t : ↑I
x : X
y : Y
h : x = e ∧ y = e
⊢ { toFun := fun x ↦ { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ }.toFun (t, x),
        continuous_toFun := ⋯ }
      (x, y) =
    ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
        ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y))))
      (x, y)

Tactic:
exact Prod.ext (HSpace.eHmul.2 t x h.1) (HSpace.eHmul.2 t y h.2)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c i).point ∈ (logSizeBallSeq J hJ a c i).finset

Tactic:
by
  match i with
  | 0 => simp [point_logSizeBallSeq_zero, finset_logSizeBallSeq_zero, Exists.choose_spec]
  | i + 1 => simp [point_logSizeBallSeq_add_one, h, Exists.choose_spec]

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
⊢ toLoop i (fromLoop i p) = p

Tactic:
[

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
⊢ toLoop i (fromLoop i p) = p
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: ⊢ ⋂ n, preCantorSet n = (⋂ i, (fun x ↦ x / 3) '' preCantorSet i) ∪ ⋂ i, (fun x ↦ (2 + x) / 3) '' preCantorSet i

Tactic:
[

Goal state after:
⊢ ⋂ n, preCantorSet n = (⋂ i, (fun x ↦ x / 3) '' preCantorSet i) ∪ ⋂ i, (fun x ↦ (2 + x) / 3) '' preCantorSet i
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h :
  (∑ x ∈ Finset.range n1, ofDigitsTerm a x + ofDigitsTerm a n1 +
      (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ a (i + (n1 + 1))) =
    ∑ x ∈ Finset.range n1, ofDigitsTerm b x + ofDigitsTerm b n1 + (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ b (i + (n1 + 1))
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
⊢ False

Tactic:
this

Goal state after:
n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h :
  (∑ x ∈ Finset.range n1, ofDigitsTerm b x + ofDigitsTerm a n1 +
      (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ a (i + (n1 + 1))) =
    ∑ x ∈ Finset.range n1, ofDigitsTerm b x + ofDigitsTerm b n1 + (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ b (i + (n1 + 1))
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
⊢ False
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: case inr
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
⊢ (s.sup f) x z ≤ max ((s.sup f) x y) ((s.sup f) y z)

Tactic:
[

Goal state after:
case inr
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
⊢ (s.sup f) x z ≤ max ((s.sup f) x y) ((s.sup f) y z)
Module: Mathlib.Topology.List

Goal state before:
pp: case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
⊢ Tendsto prod (𝓝 (x :: l)) (𝓝 (x :: l).prod)

Tactic:
[

Goal state after:
case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
⊢ Tendsto prod (𝓝 (x :: l)) (𝓝 (x :: l).prod)
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: case inr.refine_1
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
H : (f i) x z ≤ (f i) x y
⊢ ∃ b ∈ s, (f i) x z ≤ (f b) x y

Tactic:
exact ⟨i, hi, H⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: case inr.refine_2
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
H : (f i) x z ≤ (f i) y z
⊢ ∃ b ∈ s, (f i) x z ≤ (f b) y z

Tactic:
exact ⟨i, hi, H⟩

Goal state after: