mathlib-initiative/mathlib-tactics huggingface dataset:
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 : 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
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
closed' : ∀ A ⊆ C, (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) → IsClosed[inst✝] A
union' : ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
n : ℕ
i : cell n
⊢ ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)

Tactic:
use fun m ↦ finite_univ.toFinset (s := (univ : Set (cell m)))
    simp only [Finite.mem_toFinset, mem_univ, iUnion_true]
    exact mapsTo n i

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

Tactic:
use fun m ↦ finite_univ.toFinset (s := (univ : Set (cell m)))
    simp only [Finite.mem_toFinset, mem_univ, iUnion_true]
    exact mapsTo n i

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A B : Set X
⊢ derivedSet (A ∪ B) = derivedSet A ∪ derivedSet B

Tactic:
by
  ext x
  simp [derivedSet, ← sup_principal, accPt_sup]

Goal state after:
Module: Mathlib.Topology.DerivedSet

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

Tactic:
refine le_antisymm (fun x hx => ?_) (derivedSet_mono _ _ subset_closure)
  rw [mem_derivedSet, AccPt, (nhdsWithin_basis_open x {x}ᶜ).inf_principal_neBot_iff] at hx ⊢
  peel hx with u hu _
  obtain ⟨-, hu_open⟩ := hu
  exact mem_closure_iff.mp this.some_mem.2 (u ∩ {x}ᶜ) (hu_open.inter isOpen_compl_singleton)
    this.some_mem.1

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)
a✝¹ : ⟨n, i⟩ ∈ univ
m : ℕ
j : ↑(E.I m)
a✝ : ⟨m, j⟩ ∈ univ
⊢ ⟨n, i⟩ ≠ ⟨m, j⟩ → Function.onFun Disjoint (fun ni ↦ ↑(map ni.fst ↑ni.snd) '' ball 0 1) ⟨n, i⟩ ⟨m, j⟩

Tactic:
hne

Goal state after:
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)
a✝¹ : ⟨n, i⟩ ∈ univ
m : ℕ
j : ↑(E.I m)
a✝ : ⟨m, j⟩ ∈ univ
hne : ⟨n, i⟩ ≠ ⟨m, j⟩
⊢ Function.onFun Disjoint (fun ni ↦ ↑(map ni.fst ↑ni.snd) '' ball 0 1) ⟨n, i⟩ ⟨m, j⟩
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 { l // List.IsChain (fun x1 x2 ↦ x1 > x2) l } fun l m ↦ List.Lex (fun x1 x2 ↦ x1 < x2) ↑l ↑m

Tactic:
(by rfl : (· > · : I → _) = flip (· < ·))

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 { l // List.IsChain (flip fun x1 x2 ↦ x1 < x2) l } fun l m ↦ List.Lex (fun x1 x2 ↦ x1 < x2) ↑l ↑m
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: D : CompHaus
x✝ : Set (Compactum.ofTopologicalSpace ↑D.toTop).A
h1 : IsOpen x✝
⊢ IsOpen (id ⁻¹' x✝)

Tactic:
rw [isOpen_iff_ultrafilter']
          intro _ h2
          exact h1 _ h2

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

Goal state before:
pp: case refine_1
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
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
y : I → Bool
hyC : y ∈ C
⊢ Proj (fun x ↦ ord I x < o) y ∈ C0 C ho ∨ Proj (fun x ↦ ord I x < o) y ∈ π (C1 C ho) fun x ↦ ord I x < o

Tactic:
rw [← union_C0C1_eq C ho] at hyC

Goal state after:
case refine_1
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
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
y : I → Bool
hyC : y ∈ C0 C ho ∪ C1 C ho
⊢ Proj (fun x ↦ ord I x < o) y ∈ C0 C ho ∨ Proj (fun x ↦ ord I x < o) y ∈ π (C1 C ho) fun x ↦ ord I x < o
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h.refine_1
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
⊢ (πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩) ∈ range (π C fun x ↦ ord I x < o₂)

Tactic:
use ⟨l, Products.isGood_mono C h gl⟩

Goal state after:
case h
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, ⋯⟩ = (πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩)
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
⊢ ⇑(ConcreteCategory.hom
        (CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
            { toFun := Ultrafilter.extend t, continuous_toFun := hh } ≫
          g)) =
    ⇑(ConcreteCategory.hom f)

Tactic:
convert! denseRange_pure.equalizer (g.hom.hom.continuous.comp hh) f.hom.hom.continuous _

Goal state after:
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
⊢ (⇑(TopCat.Hom.hom g.hom) ∘ h) ∘ pure = ⇑(TopCat.Hom.hom f.hom) ∘ pure
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 : Set X
inst✝ : CWComplex C
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : ⋃ n, ⋃ j, openCell n ↑j = E
⊢ ∅ ∪ ⋃ n, ⋃ j, openCell n ↑j = E

Tactic:
rw [empty_union]

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

Tactic:
rw [empty_union]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C✝ D : Set X
inst✝¹ : T2Space X
C : Set X
h : CWComplex C
E : Set X
I : (n : ℕ) → Set (cell C n)
inst✝ : CWComplex E
union : ⋃ n, ⋃ j, openCell n ↑j = E
⊢ ⋃ n, ⋃ j, openCell n ↑j = E
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: case refine_2
α : 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β
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g : (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨f, hf⟩ = (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨g, hg⟩
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ dist (g x) (g x') < ε₂

Tactic:
exact (hU x').2.2 _ hx' _ (hU x').1 hg

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β
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g : (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨f, hf⟩ = (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨g, hg⟩
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
F_f_g : F (f x') = F (g x')
⊢ dist (f x') (F (f x')) + dist (g x') (F (f x')) = dist (f x') (F (f x')) + dist (g x') (F (g x'))

Tactic:
rw [F_f_g]

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

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
⊢ IsCountablyCompact A ↔ IsCountablyCompact (Subtype.val '' univ)

Tactic:
image_univ,

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
⊢ IsCountablyCompact A ↔ IsCountablyCompact (range Subtype.val)
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
x : X
hx : x ∈ K
⊢ ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f) L (⋃₀ t)

Tactic:
rcases hKT hx with ⟨V, hVt, hxV⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
x : X
hx : x ∈ K
V : Set Y
hVt : V ∈ t
hxV : f x ∈ V
⊢ ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f) L (⋃₀ t)
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
⊢ IsSeqCompact A ↔ IsSeqCompact (Subtype.val '' univ)

Tactic:
image_univ,

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
⊢ IsSeqCompact A ↔ IsSeqCompact (range Subtype.val)
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:
simp_rw [mapClusterPt_iff_frequently, frequently_cofinite_iff_infinite]

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 | x a ∈ s}.Infinite
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

Goal state after:
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 : Set Y
hV : V ∈ countableBasis Y
hx : f x ∈ V
⊢ ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
x : X
hxV : x ∈ ⇑f ⁻¹' V
⊢ ∃ U ∈ countableBasis X, x ∈ U ∧ U ⊆ ⇑f ⁻¹' V

Tactic:
← (isBasis_countableBasis _).mem_nhds_iff

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
x : X
hxV : x ∈ ⇑f ⁻¹' V
⊢ ⇑f ⁻¹' V ∈ 𝓝 x
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
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : ↑(#J) ≤ a ^ n
i : ℕ
⊢ (logSizeBallSeq J hJ a c 0).radius ≤ n

Tactic:
simp only [radius_logSizeBallSeq_zero, logSizeRadius, ha, ↓reduceDIte]
    exact Nat.find_min' _ ⟨hn, le_trans (by gcongr; apply Finset.filter_subset) hJ_card⟩

Goal state after:
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
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : ↑(#J) ≤ a ^ n
i✝ i : ℕ
⊢ Nat.find ⋯ ≤ n

Tactic:
refine Nat.find_min' _ ⟨hn, le_trans ?_ hJ_card⟩

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : ↑(#J) ≤ a ^ n
i✝ i : ℕ
⊢ ↑(#({x ∈ (logSizeBallSeq J hJ a c (i + 1)).finset | edist (logSizeBallSeq J hJ a c (i + 1)).point x ≤ ↑n * c})) ≤
    ↑(#J)
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: ⊢ TotallyDisconnectedSpace ℚ

Tactic:
refine ⟨fun s hsu hs x hx y hy => ?_⟩

Goal state after:
s : Set ℚ
hsu : s ⊆ univ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
⊢ x = y
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 j : ℕ
hij : i ≠ j
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)

Tactic:
by
  wlog! h : i < j generalizing i j
  · exact Disjoint.symm <| this hij.symm <| (ne_iff_lt_iff_le.mpr h).mp hij.symm
  apply Finset.disjoint_of_subset_right
  · exact (Finset.filter_subset _ _).trans (antitone_logSizeBallSeq_add_one_subset hJ h)
  simp [finset_logSizeBallSeq_add_one, Finset.disjoint_sdiff]

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

Goal state before:
pp: case inl
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)
hM : y ∘ Sum.inl ∈ Cube.boundary M
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x

Tactic:
have : p (y ∘ Sum.inl) = const := p.property (y ∘ Sum.inl) hM
    simp [this]

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 : ↑(Ω^ N X x)
⊢ ⟨((↑p).comp ↑(Cube.insertAt i)).curry 1, ⋯⟩ = const

Tactic:
by ext t; refine p.property (Cube.insertAt i (1, t)) ⟨i, Or.inr ?_⟩; simp

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: a : ℕ → Fin 3
h : ∀ (n : ℕ), a n ≠ 1
i : ℕ
⊢ ofDigits a ∈ preCantorSet i

Tactic:
induction i generalizing a with
  | zero =>
    simp only [preCantorSet_zero, Set.mem_Icc]
    exact ⟨ofDigits_nonneg a, ofDigits_le_one a⟩
  | succ i ih =>
    simp only [preCantorSet, Set.mem_union, Set.mem_image, ← exists_or]
    use ofDigits (fun i ↦ a (i + 1))
    have : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i := ih (by solve_by_elim)
    simp only [this, ofDigits_eq_sum_add_ofDigits a 1, Finset.range_one, ofDigitsTerm,
      Nat.cast_ofNat, Finset.sum_singleton, zero_add, pow_one, true_and, field]
    specialize h 0
    generalize a 0 = x at h
    fin_cases x <;> simp at ⊢ h

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
x : (i : ↑S) → α ↑i
y : (a : ↑Sᶜ) → α ↑a
left✝¹ : ∃ x ∈ s, Sᶜ.domRestrict x = y
z : (a : ι) → α a
hz_mem : z ∈ s
left✝ : (∃ x ∈ s, Sᶜ.domRestrict x = Sᶜ.domRestrict z) ∧ Sᶜ.domRestrict z = y
hzx : (fun i ↦ z ↑i) = x
⊢ ∃ x_1 ∈ s, S.domRestrict x_1 = x

Tactic:
exact ⟨z, hz_mem, hzx⟩

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
⊢ cantorStep x ∈ cantorSet

Tactic:
simp only [cantorStep]

Goal state after:
x : ℝ
hx : x ∈ cantorSet
⊢ (if x ∈ Set.Icc 0 (1 / 3) then 3 * x else 3 * x - 2) ∈ cantorSet
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem :
  0 ≤ (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∧
    (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ≤ 1
⊢ x - 3⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i

Tactic:
← mul_le_mul_iff_left₀ (show 0 < (3 : ℝ) ^ n by positivity),

Goal state after:
x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem :
  0 ≤ (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∧
    (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ≤ 1
⊢ (x - 3⁻¹ ^ n) * 3 ^ n ≤ (∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i) * 3 ^ n
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mpr.refine_4
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
H : ((genLoopEquivOfUnique N) a₁).Homotopy ((genLoopEquivOfUnique N) a₂)
⊢ ∀ (t : ↑I),
    ∀ x_1 ∈ Cube.boundary N,
      {
            toFun := fun x_2 ↦
              { toFun := fun tx ↦ H (tx.1, tx.2 default), continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        ↑a₁ x_1

Tactic:
· rintro t y ⟨i, iH⟩
      cases Unique.eq_default i
      exact (H.eq_fst _ iH).trans (congr_arg a₁ (eq_const_of_unique y).symm)

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
⊢ x ∈ A → ∃ y ∈ maximalSeparatedSet ε A, (x, y) ∈ {(x, y) | edist x y ≤ ↑ε}

Tactic:
hxA

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
⊢ ∃ y ∈ maximalSeparatedSet ε A, (x, y) ∈ {(x, y) | edist x y ≤ ↑ε}
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
⊢ ⨅ C, ⨅ (_ : C ⊆ f '' A), ⨅ (_ : IsCover ε (f '' A) C), C.encard ≤ C.encard

Tactic:
refine (iInf_le _ (C.image f)).trans ?_

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
⊢ ⨅ (_ : f '' C ⊆ f '' A), ⨅ (_ : IsCover ε (f '' A) (f '' C)), (f '' C).encard ≤ C.encard
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ {x, y}.einfsep ≤ edist y x

Tactic:
by
  rw [pair_comm]; exact einfsep_pair_le_left hxy.symm

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep < ∞

Tactic:
rw [lt_top_iff_ne_top]
  exact hs.einfsep_ne_top

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
⊢ {x, y}.infsep = (edist x y).toReal

Tactic:
by
  by_cases hxy : x = y
  · rw [hxy]
    simp only [infsep_singleton, pair_eq_singleton, edist_self, ENNReal.toReal_zero]
  · rw [infsep, einfsep_pair hxy]

Goal state after: