mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
h : φ p = p - 1
hp : 1 < p
⊢ Prime p

Tactic:
rw [totient_eq_card_coprime, range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico hp.le,
    Finset.filter_insert, if_neg (not_coprime_of_dvd_of_dvd hp (dvd_refl p) (dvd_zero p)),
    ← Nat.card_Ico 1 p] at h

Goal state after:
p : ℕ
h : #({a ∈ Ico (0 + 1) p | p.Coprime a}) = #(Ico 1 p)
hp : 1 < p
⊢ Prime p
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ φ n = n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)

Tactic:
rw [multiplicative_factorization φ (@totient_mul) totient_one hn]

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k ↦ φ (p ^ k)) = n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
rw [totient_eq_prod_factorization hn]

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (x : X), x ∈ closure (closure s)) ↔ ∀ (x : X), x ∈ closure s

Tactic:
closure_closure

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (x : X), x ∈ closure s) ↔ ∀ (x : X), x ∈ closure s
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIcoDiv hp a (b - ↑m * p) = toIcoDiv hp a b - m

Tactic:
by
  simpa using toIcoDiv_sub_zsmul hp a b m

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂)

Tactic:
rw [nhdsSet_union]

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ t₁ ⊔ 𝓝ˢ t₂
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ (s ∩ t ∪ s ∩ tᶜ) = 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ)

Tactic:
rw [nhdsSet_union]

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsCoinducing (g ∘ f)
⊢ inst✝ ≤ coinduced g inst✝¹

Tactic:
by grw [hgf.eq_coinduced, ← coinduced_compose, hf.coinduced_le]

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed[inst✝¹] s → s.Nonempty → IsClosed[inst✝] (f '' s)
⊢ IsClosedMap f

Tactic:
by
  intro s hs; rcases eq_empty_or_nonempty s with h2s | h2s
  · simp_rw [h2s, image_empty, isClosed_empty]
  · exact h s hs h2s

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)

Tactic:
← Set.biUnion_of_singleton s

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ comap f (𝓝ˢ (⋃ x ∈ s, {x})) ≤ 𝓝ˢ (f ⁻¹' ⋃ x ∈ s, {x})
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y✝ : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
Y : ι → Type v
inst✝ : (i : ι) → TopologicalSpace (Y i)
h : ∀ (i : ι), IndiscreteTopology (Y i)
x✝ : ι
⊢ induced (fun f ↦ f x✝) (inst✝ x✝) = ⊤

Tactic:
simp only [(h _).eq_top, induced_top]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ ∀ u ∈ insert ∅ s, IsOpen[t] u

Tactic:
rintro _ (rfl | hu)

Goal state after:
case inl
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ IsOpen[t] ∅

case inr
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
u✝ : Set α
hu : u✝ ∈ s
⊢ IsOpen[t] u✝
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
⊢ ContinuousOn f s ↔ ContinuousOn (g ∘ f) s

Tactic:
simp_rw [ContinuousOn, hg.continuousWithinAt_iff]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
⊢ (∀ x ∈ s, s ∈ Filter.pi fun i ↦ 𝓝 (x i)) ↔ ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s

Tactic:
Filter.mem_pi',

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
⊢ (∀ x ∈ s, ∃ I t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ (↑I).pi t ⊆ s) ↔
    ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
⊢ (∀ x ∈ s, s ∈ Filter.pi fun i ↦ 𝓝 (x i)) ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s

Tactic:
Filter.mem_pi',

Goal state after:
case intro
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
⊢ (∀ x ∈ s, ∃ I t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ (↑I).pi t ⊆ s) ↔
    ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case inl
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
j : ι
s : Set (σ j)
hs : IsOpen[inst✝ j] s
⊢ IsOpen[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk j '' s)

Tactic:
preimage_image_eq _ sigma_mk_injective

Goal state after:
case inl
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
j : ι
s : Set (σ j)
hs : IsOpen[inst✝ j] s
⊢ IsOpen[inst✝ j] s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case inl
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
j : ι
s : Set (σ j)
hs : IsClosed[inst✝ j] s
⊢ IsClosed[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk j '' s)

Tactic:
preimage_image_eq _ sigma_mk_injective

Goal state after:
case inl
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
j : ι
s : Set (σ j)
hs : IsClosed[inst✝ j] s
⊢ IsClosed[inst✝ j] s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ Continuous[instTopologicalSpaceSigma, inst✝] f ↔ ∀ (i : ι), Continuous[inst✝¹ i, inst✝] fun a ↦ f ⟨i, a⟩

Tactic:
by
  delta instTopologicalSpaceSigma
  rw [continuous_iSup_dom]
  exact forall_congr' fun _ => continuous_coinduced_dom

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
ht : IsOpen[instTopologicalSpaceSubtype] t
hs : IsOpen[inst✝] s
⊢ IsOpen[inst✝] (Subtype.val '' t)

Tactic:
by
  rcases isOpen_induced_iff.mp ht with ⟨s', hs', rfl⟩
  rw [Subtype.image_preimage_coe]
  exact hs.inter hs'

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝¹] U
h_KU : K ⊆ U
L : Set X
hL : IsCompact L
hKL : K ⊆ interior L
hLU : L ⊆ U
⊢ L ∈ 𝓝ˢ K

Tactic:
← subset_interior_iff_mem_nhdsSet

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝¹] U
h_KU : K ⊆ U
L : Set X
hL : IsCompact L
hKL : K ⊆ interior L
hLU : L ⊆ U
⊢ K ⊆ interior L
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
⊢ p s

Tactic:
by
  let f : Filter X := comk p he (fun _t ht _s hsub ↦ hmono hsub ht) (fun _s hs _t ht ↦ hunion hs ht)
  have : sᶜ ∈ f := hs.compl_mem_sets_of_nhdsWithin (by simpa [f] using hnhds)
  rwa [← compl_compl s]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ SpecializingMap f ↔ ∀ (x : X), IsClosed[inst✝] (f '' closure[inst✝¹] {x})

Tactic:
refine ⟨fun h x ↦ ?_, fun h ↦ specializingMap_iff_stableUnderSpecialization_image_singleton.mpr
    (fun x ↦ (h x).stableUnderSpecialization)⟩
  rw [(specializingMap_iff_closure_singleton hf).mp h x]
  exact isClosed_closure

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
inst✝ : IndiscreteTopology X
u v : Set X
⊢ u = ∅ ∨ u = univ → v = ∅ ∨ v = univ → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty

Tactic:
rintro ⟨h | h⟩ <;> simp_all

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))

Tactic:
· refine ⟨fun hx ↦ ?_, fun _ ↦ H⟩
    simpa [disjoint_iff, nhdsWithin, inf_assoc, hx] using H

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
⊢ codiscreteWithin U₁ ≤ codiscreteWithin U

Tactic:
refine (biSup_mono hU).trans <| iSup₂_mono fun _ _ ↦ ?_
  gcongr

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h₂.hU
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ IsOpen[inst✝] (⋃ i ∈ irreducibleComponents X \ {Z}, i)ᶜ

Tactic:
isOpen_compl_iff

Goal state after:
case h₂.hU
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ IsClosed[inst✝] (⋃ i ∈ irreducibleComponents X \ {Z}, i)
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case inl.inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x y : X
h : Sum.inl x ≠ Sum.inl y
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inl x ∈ u ∧ Sum.inl y ∈ v ∧ Disjoint u v

pp: case inl.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
y : Y
h : Sum.inl x ≠ Sum.inr y
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inl x ∈ u ∧ Sum.inr y ∈ v ∧ Disjoint u v

pp: case inr.inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : Y
y : X
h : Sum.inr x ≠ Sum.inl y
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inr x ∈ u ∧ Sum.inl y ∈ v ∧ Disjoint u v

pp: case inr.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x y : Y
h : Sum.inr x ≠ Sum.inr y
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inr x ∈ u ∧ Sum.inr y ∈ v ∧ Disjoint u v

Tactic:
· exact separated_by_isOpenEmbedding .inl <| ne_of_apply_ne _ h

Goal state after:
case inl.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
y : Y
h : Sum.inl x ≠ Sum.inr y
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inl x ∈ u ∧ Sum.inr y ∈ v ∧ Disjoint u v

case inr.inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : Y
y : X
h : Sum.inr x ≠ Sum.inl y
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inr x ∈ u ∧ Sum.inl y ∈ v ∧ Disjoint u v

case inr.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x y : Y
h : Sum.inr x ≠ Sum.inr y
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inr x ∈ u ∧ Sum.inr y ∈ v ∧ Disjoint u v
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : CompactSpace X
⊢ codiscrete X = cofinite

Tactic:
simpa using! isCompact_univ.codiscreteWithin_eq

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

Goal state before:
pp: case refl
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ IsPreconnected (s i)

Tactic:
exact H i hi

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

Goal state before:
pp: case refine_1.insert.refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
x✝ :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst✝] a → ∀ (b : Set α), IsOpen[inst✝] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst✝] a → ∀ (b : Set α), IsOpen[inst✝] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH : (∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) → (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst✝] u ∧ ∀ x ∈ U, IsOpen[inst✝] x
hsU : s ⊆ u ∪ ⋃₀ ↑U
⊢ s ∩ (u ∩ ⋃₀ ↑U) = ∅

Tactic:
refine subset_empty_iff.1 fun x ⟨hxs, hxu, v, hvU, hxv⟩ => ?_

Goal state after:
case refine_1.insert.refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
x✝¹ :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst✝] a → ∀ (b : Set α), IsOpen[inst✝] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst✝] a → ∀ (b : Set α), IsOpen[inst✝] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH : (∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) → (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst✝] u ∧ ∀ x ∈ U, IsOpen[inst✝] x
hsU : s ⊆ u ∪ ⋃₀ ↑U
x : α
x✝ : x ∈ s ∩ (u ∩ ⋃₀ ↑U)
hxs : x ∈ s
hxu : x ∈ u
v : Set α
hvU : v ∈ ↑U
hxv : x ∈ v
⊢ x ∈ ∅
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
⊢ ∃ t, t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

Tactic:
let ⟨t, ⟨htc, htsub⟩⟩ := hs.elim_nhds_subcover' (fun x _ ↦ U x) hU

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
⊢ ∃ t, t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝²] U
h_KU : K ⊆ U
L : Set X
hL : IsCompact L
hL' : IsClosed[inst✝²] L
hKL : K ⊆ interior L
hLU : L ⊆ U
⊢ L ∈ 𝓝ˢ K

Tactic:
← subset_interior_iff_mem_nhdsSet

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝²] U
h_KU : K ⊆ U
L : Set X
hL : IsCompact L
hL' : IsClosed[inst✝²] L
hKL : K ⊆ interior L
hLU : L ⊆ U
⊢ K ⊆ interior L
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
hs : IsClopen (a ∪ b)
H : IsPreconnected (a ∪ b)
⊢ ((a ∪ b) ∩ b).Nonempty

Tactic:
by rwa [union_inter_cancel_right]

Goal state after:
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsNowhereDense s
⊢ interior (closure[inst✝] (closure[inst✝] s)) = ∅

Tactic:
closure_closure

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsNowhereDense s
⊢ interior (closure[inst✝] s) = ∅
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : PreconnectedSpace α
⊢ Subsingleton (ConnectedComponents α)

Tactic:
by
  refine ⟨fun x y ↦ ?_⟩
  obtain ⟨x, rfl⟩ := surjective_coe x
  obtain ⟨y, rfl⟩ := surjective_coe y
  simp_rw [coe_eq_coe, PreconnectedSpace.connectedComponent_eq_univ, ]

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

Goal state before:
pp: α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
x : α
i : ι
hx : x ∈ U i
⊢ connectedComponentIn (U i) x = connectedComponent x

Tactic:
(hclopen i).connectedComponentIn_eq hx

Goal state after:
α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
x : α
i : ι
hx : x ∈ U i
⊢ connectedComponent x = connectedComponent x
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ DiscreteTopology (ConnectedComponents α) ↔ ∀ (x : α), IsOpen[inst✝] (connectedComponent x)

Tactic:
discreteTopology_iff_isOpen_singleton,

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (a : ConnectedComponents α), IsOpen {a}) ↔ ∀ (x : α), IsOpen[inst✝] (connectedComponent x)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ ConnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ

Tactic:
rw [connectedSpace_iff_univ, IsConnected, ← preconnectedSpace_iff_univ,
    preconnectedSpace_iff_clopen, Set.nonempty_iff_univ_nonempty]

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : Preorder β
u : β → α
h : CauchySeq u
⊢ Tendsto (Prod.map u u) atTop (𝓤 α)

Tactic:
by
  simpa only [Tendsto, prod_map_map_eq', prod_atTop_atTop_eq] using h.right

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
this✝ : Nonempty β
this : Tendsto (Prod.map u u) atTop (𝓤 α)
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Tactic:
rw [← prod_atTop_atTop_eq] at this

Goal state after:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
this✝ : Nonempty β
this : Tendsto (Prod.map u u) (atTop ×ˢ atTop) (𝓤 α)
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: case mpr
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
· rintro ⟨V, V_in, _, V_sub⟩
    exact ⟨V, V_in, V_sub⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ interior s ∈ 𝓤 α

Tactic:
uniformity_eq_uniformity_interior

Goal state after:
α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ interior s ∈ (𝓤 α).lift' interior
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ UniformContinuousOn f s ↔ UniformContinuous (s.domRestrict f)

Tactic:
by
  delta UniformContinuousOn UniformContinuous
  rw [← map_uniformity_set_coe, tendsto_map'_iff]; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsCompact s
this : CompactSpace ↑s
h : TendstoUniformly (fun i x ↦ F i ↑x) (f ∘ Subtype.val) p
⊢ TendstoUniformlyOn F f p s

Tactic:
←
    tendstoUniformlyOn_iff_tendstoUniformly_comp_coe

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsCompact s
this : CompactSpace ↑s
h : TendstoUniformlyOn F f p s
⊢ TendstoUniformlyOn F f p s
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ⊤ ^ (n + 2) = ⊤

Tactic:
pow_succ,

Goal state after:
α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ⊤ ^ (n + 1) * ⊤ = ⊤
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun x ↦ x * c) ⁻¹' Ico a b = Ioc (b / c) (a / c)

Tactic:
by
  simp [← Ici_inter_Iio, ← Ioi_inter_Iic, h, inter_comm]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ closure[inst✝²] K ⊆ K * closure[inst✝²] {1}

Tactic:
· have : IsClosed (K * (closure {1} : Set G)) :=
      IsClosed.smul_left_of_isCompact isClosed_closure hK
    rw [IsClosed.closure_subset_iff this]
    exact subset_mul_closure_one K

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: case cons
α : Type u_3
β : Type u_4
ι : Type u_5
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : ι → β → α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, UniformContinuous (f i)) → UniformContinuous fun x ↦ ∏ i ∈ s, f i x
h : ∀ i ∈ cons a s ha, UniformContinuous (f i)
⊢ UniformContinuous fun x ↦ ∏ i ∈ cons a s ha, f i x

Tactic:
Finset.mem_cons,

Goal state after:
case cons
α : Type u_3
β : Type u_4
ι : Type u_5
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : ι → β → α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, UniformContinuous (f i)) → UniformContinuous fun x ↦ ∏ i ∈ s, f i x
h : ∀ (i : ι), i = a ∨ i ∈ s → UniformContinuous (f i)
⊢ UniformContinuous fun x ↦ ∏ i ∈ cons a s ha, f i x
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
refine topologicalGroup_iInf fun b => ?_

Goal state after:
G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
b : Bool
⊢ IsTopologicalGroup G