mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case pos
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : ⋂ n, ⋂ m, ⋂ (_ : m ≤ n), C m = ∅
n : ℕ
g : (dissipate C n).Nonempty
⊢ dissipate C n ∈ S ∨ dissipate C n = ∅

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : ⋂ n, ⋂ m, ⋂ (_ : m ≤ n), C m = ∅
n : ℕ
g : (dissipate C n).Nonempty
⊢ dissipate C n = ∅ ∨ dissipate C n ∈ S
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), C i ∈ {s | IsCompact s ∧ IsClosed s}
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ IsCompact (dissipate C 0)

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), C i ∈ {s | IsCompact s ∧ IsClosed s}
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ IsCompact (C 0)
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
s : Set α
⊢ IsCompact s ↔ IsCompact s ∧ IsClosed s

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
s : Set α
⊢ IsCompact s → IsClosed s
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case neg
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
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding (↑↑q).head! < o

Tactic:
exact Products.prop_of_isGood C _ q.prop q.val.val.head! (List.head!_mem_self h)

Goal state after:
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 : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
hfin✝ : tα.Finite
htα : univ ⊆ ⋃ x ∈ tα, U x
val✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
hfin : tβ.Finite
htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂
val✝ : Fintype ↑tβ
y : β
⊢ ∃ z ∈ tβ, dist y z < ε₂

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
hfin✝ : tα.Finite
htα : univ ⊆ ⋃ x ∈ tα, U x
val✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
hfin : tβ.Finite
htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂
val✝ : Fintype ↑tβ
y : β
⊢ ∃ z ∈ tβ, dist y z < ε₂
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : NonUnitalNormedRing γ
inst✝ : Nontrivial γ
h : C_cb(α, γ) = ⊤
x : γ
hx : x ≠ 0
⊢ IsCompact univ

Tactic:
simpa using

Goal state after:
α : Type u_1
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : NonUnitalNormedRing γ
inst✝ : Nontrivial γ
h : C_cb(α, γ) = ⊤
x : γ
hx : x ≠ 0
⊢ IsCompact univ
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a atTop x
f : Filter E
x✝¹ : f.NeBot
x✝ : f.IsCountablyGenerated
hle : f ≤ 𝓟 A
x : ℕ → E
hx : Tendsto x atTop f
⊢ ∀ᶠ (n : ℕ) in atTop, x n ∈ A

Tactic:
simpa using

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a atTop x
f : Filter E
x✝¹ : f.NeBot
x✝ : f.IsCountablyGenerated
hle : f ≤ 𝓟 A
x : ℕ → E
hx : Tendsto x atTop f
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → x b ∈ A
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
hb : b.Countable
U : ι → Set E
hUo : ∀ i ∈ b, IsOpen[inst✝] (U i)
hAU : A ⊆ ⋃ i ∈ b, U i
this : Countable ↑b
⊢ A ⊆ ⋃ i, U ↑i

Tactic:
simpa using

Goal state after:
ι : Type u_1
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
hb : b.Countable
U : ι → Set E
hUo : ∀ i ∈ b, IsOpen[inst✝] (U i)
hAU : A ⊆ ⋃ i ∈ b, U i
this : Countable ↑b
⊢ A ⊆ ⋃ i ∈ b, U i
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha✝ : a ∈ A ∧ MapClusterPt a atTop x
this : ∀ (k : ℕ), ∃ n > k, a ∈ closure[inst✝³] {x n}
φ : ℕ → ℕ
hφ1 : StrictMono φ
hφ2 : ∀ (n : ℕ), a ∈ closure[inst✝³] {x (φ n)}
U : Set E
ha : a ∈ U
hUo : IsOpen[inst✝³] U
n : ℕ
x✝ : 0 ≤ n
⊢ (x ∘ φ) n ∈ U

Tactic:
simpa using

Goal state after:
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha✝ : a ∈ A ∧ MapClusterPt a atTop x
this : ∀ (k : ℕ), ∃ n > k, a ∈ closure[inst✝³] {x n}
φ : ℕ → ℕ
hφ1 : StrictMono φ
hφ2 : ∀ (n : ℕ), a ∈ closure[inst✝³] {x (φ n)}
U : Set E
ha : a ∈ U
hUo : IsOpen[inst✝³] U
n : ℕ
x✝ : 0 ≤ n
⊢ x (φ n) ∈ U
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.support ⊆ {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 : Products I
hq : q ∈ m.support
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) (term I ho :: ↑q) ↑↑l

Tactic:
rw [max_eq_o_cons_tail C hsC ho l]

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.support ⊆ {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 : Products I
hq : q ∈ m.support
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) (term I ho :: ↑q) (term I ho :: ↑(↑l).Tail)
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
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
h : LinearIndependent ℤ (eval (C' C ho))
⊢ LinearIndependent ℤ fun (l : ↑(MaxProducts C ho)) ↦ Products.eval (C' C ho) (↑l).Tail

Tactic:
let f := MaxToGood C hC hsC ho h₁

Goal state after:
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
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
h : LinearIndependent ℤ (eval (C' C ho))
f : ↑(MaxProducts C ho) → ↑(GoodProducts (C' C ho)) := MaxToGood C hC hsC ho h₁
⊢ LinearIndependent ℤ fun (l : ↑(MaxProducts C ho)) ↦ Products.eval (C' C ho) (↑l).Tail
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case empty
ι : Type u_1
E : Type u_2
inst✝ : TopologicalSpace E
f : ι → Set E
hf : ∀ i ∈ ∅, IsCountablyCompact (f i)
⊢ IsCountablyCompact (⋃ i ∈ ∅, f i)

Tactic:
simpa using

Goal state after:
case empty
ι : Type u_1
E : Type u_2
inst✝ : TopologicalSpace E
f : ι → Set E
hf : ∀ i ∈ ∅, IsCountablyCompact (f i)
⊢ IsCountablyCompact ∅
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case insert
ι : Type u_1
E : Type u_2
inst✝ : TopologicalSpace E
f : ι → Set E
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, IsCountablyCompact (f i)) → IsCountablyCompact (⋃ i ∈ s, f i)
hf : ∀ i ∈ insert a s, IsCountablyCompact (f i)
⊢ IsCountablyCompact (⋃ i ∈ insert a s, f i)

Tactic:
simpa using

Goal state after:
case insert
ι : Type u_1
E : Type u_2
inst✝ : TopologicalSpace E
f : ι → Set E
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, IsCountablyCompact (f i)) → IsCountablyCompact (⋃ i ∈ s, f i)
hf : ∀ i ∈ insert a s, IsCountablyCompact (f i)
⊢ IsCountablyCompact (f a ∪ ⋃ x ∈ s, f x)
Module: Mathlib.Topology.ContinuousMap.Sigma

Goal state before:
pp: X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
i : ι
g g' : C(X, Y i)
h : (fun g ↦ (sigmaMk g.fst).comp g.snd) ⟨i, g⟩ = (fun g ↦ (sigmaMk g.fst).comp g.snd) ⟨i, g'⟩
hg : ⇑g ≍ ⇑g'
⊢ ⟨i, g⟩ = ⟨i, g'⟩

Tactic:
simpa using

Goal state after:
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
i : ι
g g' : C(X, Y i)
h : (fun g ↦ (sigmaMk g.fst).comp g.snd) ⟨i, g⟩ = (fun g ↦ (sigmaMk g.fst).comp g.snd) ⟨i, g'⟩
hg : ⇑g ≍ ⇑g'
⊢ g = g'
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
s : Set α
⊢ IsOpen {l | s ∈ l}

Tactic:
simpa using

Goal state after:
α : Type u_2
s : Set α
⊢ IsOpen {l | s ∈ l}
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ 𝓝 l = l.lift' fun s ↦ {l' | s ∈ l'}

Tactic:
simpa using

Goal state after:
α : Type u_2
l : Filter α
⊢ 𝓝 l = l.lift' fun s ↦ {l' | s ∈ l'}
Module: Mathlib.Topology.Filter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (𝓝 l).HasBasis p fun i ↦ {l' | s i ∈ l'}

Tactic:
simpa using

Goal state after:
ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (𝓝 l).HasBasis p fun i ↦ {l' | s i ∈ l'}
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
⊢ IsGeneratedBy X ↑U

Tactic:
have hg (a) : Continuous (g a) := a.2.continuous.restrictPreimage

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
⊢ IsGeneratedBy X ↑U
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
⊢ IsGeneratedBy X ↑F

Tactic:
have hg (a) : Continuous (g a) := a.2.continuous.restrictPreimage

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
⊢ IsGeneratedBy X ↑F
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
θ : ↑I
γ : Path x y
⊢ γ (qRight (0, θ)) = x

Tactic:
by
    rw [qRight_zero_left, γ.source]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
⊢ StronglyLocallyContractibleSpace (X × Y)

Tactic:
by
  refine .of_bases (ι := Set X × Set Y)
    (p := fun (x, y) (Ux, Uy) =>
      (Ux ∈ 𝓝 x ∧ ContractibleSpace Ux) ∧ (Uy ∈ 𝓝 y ∧ ContractibleSpace Uy))
    (s := fun _ (Ux, Uy) => Ux ×ˢ Uy) ?_ ?_
  · intro (x, y)
    rw [nhds_prod_eq]
    exact (contractible_basis x).prod (contractible_basis y)
  · intro (x, y) (Ux, Uy) ⟨hUx, hUy⟩
    have : ContractibleSpace Ux := hUx.2
    have : ContractibleSpace Uy := hUy.2
    exact (Homeomorph.Set.prod Ux Uy).contractibleSpace

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 : ℕ
⊢ (logSizeBallSeq J hJ a c (i + 1)).finset ⊆ (logSizeBallSeq J hJ a c i).finset

Tactic:
simp [finset_logSizeBallSeq_add_one]

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.ENatENNReal

Goal state before:
pp: case refine_1
a : ENNReal
⊢ IsOpen (toENNReal ⁻¹' Set.Ioi a)

Tactic:
simpa using

Goal state after:
case refine_1
a : ENNReal
⊢ IsOpen (Set.Ioi ⌊a⌋ₑ)
Module: Mathlib.Topology.Instances.ENNReal.ENatENNReal

Goal state before:
pp: case refine_2
a : ENNReal
⊢ IsOpen (toENNReal ⁻¹' Set.Iio a)

Tactic:
simpa using

Goal state after:
case refine_2
a : ENNReal
⊢ IsOpen (Set.Iio ⌈a⌉ₑ)
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: ⊢ ¬(cocompact ℚ).IsCountablyGenerated

Tactic:
intro H
  rcases exists_seq_tendsto (cocompact ℚ ⊓ 𝓝 0) with ⟨x, hx⟩
  rw [tendsto_inf] at hx; rcases hx with ⟨hxc, hx0⟩
  obtain ⟨n, hn⟩ : ∃ n : ℕ, x n ∉ insert (0 : ℚ) (range x) :=
    (hxc.eventually hx0.isCompact_insert_range.compl_mem_cocompact).exists
  exact hn (Or.inr ⟨n, rfl⟩)

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

Goal state before:
pp: case hab
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 + 1)).finset ⊆ (logSizeBallSeq J hJ a c i).finset

Tactic:
simp [finset_logSizeBallSeq_add_one]

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
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ M X x)
y : N → ↑I
x✝ : y ∈ Cube.boundary N
n : N
hn : y n = 0 ∨ y n = 1
⊢ ((↑p).comp { toFun := fun t m ↦ t (e m), continuous_toFun := ⋯ }) y = x

Tactic:
simpa using

Goal state after:
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝¹ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ M X x)
y : N → ↑I
x✝ : y ∈ Cube.boundary N
n : N
hn : y n = 0 ∨ y n = 1
⊢ (p fun m ↦ y (e m)) = x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝¹ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ M X x)
y : N → ↑I
x✝ : y ∈ Cube.boundary N
n : N
hn : y n = 0 ∨ y n = 1
⊢ y (e (e.symm n)) = 0 ∨ y (e (e.symm n)) = 1

Tactic:
simpa using

Goal state after:
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝¹ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ M X x)
y : N → ↑I
x✝ : y ∈ Cube.boundary N
n : N
hn : y n = 0 ∨ y n = 1
⊢ y n = 0 ∨ y n = 1
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝¹ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ N X x)
y : M → ↑I
x✝ : y ∈ Cube.boundary M
m : M
hm : y m = 0 ∨ y m = 1
⊢ ((↑p).comp { toFun := fun t n ↦ t (e.symm n), continuous_toFun := ⋯ }) y = x

Tactic:
simpa using

Goal state after:
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝¹ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ N X x)
y : M → ↑I
x✝ : y ∈ Cube.boundary M
m : M
hm : y m = 0 ∨ y m = 1
⊢ (p fun n ↦ y (e.symm n)) = x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝¹ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ N X x)
y : M → ↑I
x✝ : y ∈ Cube.boundary M
m : M
hm : y m = 0 ∨ y m = 1
⊢ y (e.symm (e m)) = 0 ∨ y (e.symm (e m)) = 1

Tactic:
simpa using

Goal state after:
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝¹ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ N X x)
y : M → ↑I
x✝ : y ∈ Cube.boundary M
m : M
hm : y m = 0 ∨ y m = 1
⊢ y m = 0 ∨ y m = 1
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ_card : ↑(#J) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
⊢ ∃ i < #J, (s, t) ∈ pairSetSeq J a c i

Tactic:
simpa using

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ_card : ↑(#J) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
⊢ ∃ i < #J, (s, t) ∈ pairSetSeq J a c i
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case inr
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
hN : y ∘ Sum.inr ∈ Cube.boundary N
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x

Tactic:
simpa using

Goal state after:
case inr
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
hN : y ∘ Sum.inr ∈ Cube.boundary N
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x
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
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
P : ℕ → Prop := ⋯
l : ℕ := ⋯
⊢ P 0

Tactic:
simpa using

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
⊢ s ∈ J ∧ t ∈ J
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ.refine_1
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
n : ℕ
ih : IsClosed (preCantorSet n)
⊢ IsClosed ((fun x ↦ x / 3) '' preCantorSet n)

Tactic:
simpa using

Goal state after:
case succ.refine_1
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
n : ℕ
ih : IsClosed (preCantorSet n)
⊢ IsClosed ((fun a ↦ 3⁻¹ * a) '' preCantorSet n)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ.refine_2
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
n : ℕ
ih : IsClosed (preCantorSet n)
⊢ IsClosed ((fun x ↦ (2 + x) / 3) '' preCantorSet n)

Tactic:
simpa using

Goal state after:
case succ.refine_2
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
n : ℕ
ih : IsClosed (preCantorSet n)
⊢ IsClosed ((fun a ↦ 3⁻¹ * (2 + a)) '' preCantorSet n)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ H (t.1, (Cube.insertAt i✝) (t.2, y)) = x

Tactic:
H.eq_fst,

Goal state after:
case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ ↑p ((Cube.insertAt i✝) (t.2, y)) = x

case refine_1.hx
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ (Cube.insertAt i✝) (t.2, y) ∈ Cube.boundary N
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h✝ : ofDigits a = ofDigits b
h : ∃ a_1, a a_1 ≠ b a_1
n0 : ℕ := Nat.find h
n : ℕ
hn : n < n0
⊢ a n = b n

Tactic:
simpa using

Goal state after:
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h✝ : ofDigits a = ofDigits b
h : ∃ a_1, a a_1 ≠ b a_1
n0 : ℕ := Nat.find h
n : ℕ
hn : n < n0
⊢ a n = b n
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h✝ : ofDigits a = ofDigits b
h : ∃ a_1, a a_1 ≠ b a_1
n0 : ℕ := Nat.find h
h1 : ∀ n < n0, a n = b n
⊢ a n0 ≠ b n0

Tactic:
simpa using

Goal state after:
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h✝ : ofDigits a = ofDigits b
h : ∃ a_1, a a_1 ≠ b a_1
n0 : ℕ := Nat.find h
h1 : ∀ n < n0, a n = b n
⊢ ¬a n0 = b n0