mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
⊢ Baer R Q

Tactic:
intro I g

Goal state after:
R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
p : α → Prop
⊢ (∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in atTop, p x

Tactic:
refine ⟨fun h ↦ h.mono fun x hx ↦ hx x le_rfl, fun h ↦ ?_⟩

Goal state after:
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p n : ℕ
hp : Prime p
h : p ∣ n
⊢ φ (p * n) = p * φ n

Tactic:
have h1 := totient_gcd_mul_totient_mul p n
  rw [gcd_eq_left h, mul_assoc] at h1
  simpa [(totient_pos.2 hp.pos).ne', mul_comm] using h1

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp a (b + -(m • p)) = toIcoDiv hp a b - m

Tactic:
← neg_smul,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp a (b + -m • p) = toIcoDiv hp a b - m
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp (a + -(m • p)) b = toIcoDiv hp a b + m

Tactic:
← neg_smul,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp (a + -m • p) b = toIcoDiv hp a b + m
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp a (b + -(m • p)) = toIocDiv hp a b - m

Tactic:
← neg_smul,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp a (b + -m • p) = toIocDiv hp a b - m
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp (a + -(m • p)) b = toIocDiv hp a b + m

Tactic:
← neg_smul,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp (a + -m • p) b = toIocDiv hp a b + m
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp a (b + -(m • p)) = toIcoMod hp a b

Tactic:
← neg_smul,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp a (b + -m • p) = toIcoMod hp a b
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp (a + -(m • p)) b = toIcoMod hp a b + -(m • p)

Tactic:
← neg_smul,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp (a + -m • p) b = toIcoMod hp a b + -m • p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp a (b + -(m • p)) = toIocMod hp a b

Tactic:
← neg_smul,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp a (b + -m • p) = toIocMod hp a b
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp (a + -(m • p)) b = toIocMod hp a b + -(m • p)

Tactic:
← neg_smul,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp (a + -m • p) b = toIocMod hp a b + -m • p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp (a + p) b = p + toIocMod hp a b

Tactic:
toIocMod_add_right',

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b + p = p + toIocMod hp a b
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
x : X
inst✝ : (𝓝[≠] x).NeBot
⊢ Dense {x}ᶜ

Tactic:
intro y
  rcases eq_or_ne y x with (rfl | hne)
  · rwa [mem_closure_iff_nhdsWithin_neBot]
  · exact subset_closure hne

Goal state after:
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 : ℤ
⊢ toIcoMod hp a (↑m * p + b) = toIcoMod hp a b

Tactic:
by
  simpa using toIcoMod_zsmul_add hp a b m

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = a + p - Int.fract ((a + p - b) / p) * p

Tactic:
rw [toIocMod, toIocDiv_eq_neg_floor, Int.fract]

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - -⌊(a + p - b) / p⌋ • p = a + p - ((a + p - b) / p - ↑⌊(a + p - b) / p⌋) * p
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : NontrivialTopology α
⊢ Nontrivial α

Tactic:
contrapose! h

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
h : Subsingleton α
⊢ IndiscreteTopology α
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen[t] {b}

Tactic:
by
  simp only [le_nhdsAdjoint_iff', @isOpen_singleton_iff_nhds_eq_pure α t]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set β
h : IsClosed[t] s
⊢ IsClosed[induced f t] (f ⁻¹' s)

Tactic:
simp_rw [← isOpen_compl_iff]
  exact isOpen_induced h.isOpen_compl

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
this : ⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v
⊢ TopologicalSpace.IsOpen (⋃ u ∈ s, u ×ˢ v)

Tactic:
exact
              isOpen_iUnion fun u =>
                isOpen_iUnion fun hu => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
⊢ ContinuousWithinAt f univ x ↔ ContinuousAt f x

Tactic:
continuousWithinAt_univ

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
⊢ ContinuousAt f x ↔ ContinuousAt f x
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
h : s ∈ 𝓝 x
⊢ ContinuousWithinAt f univ x ↔ ContinuousAt f x

Tactic:
continuousWithinAt_univ

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
h : s ∈ 𝓝 x
⊢ ContinuousAt f x ↔ ContinuousAt f x
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ closure[inst✝] (s ∩ t) ⊆ s ∩ t ↔ s ∩ closure[inst✝] (s ∩ t) ⊆ t

pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ t ⊆ s ∩ closure[inst✝] (s ∩ t)

Tactic:
Set.subset_inter_iff,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ closure[inst✝] (s ∩ t) ⊆ s ∧ s ∩ closure[inst✝] (s ∩ t) ⊆ t ↔ s ∩ closure[inst✝] (s ∩ t) ⊆ t

X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ t ⊆ s ∩ closure[inst✝] (s ∩ t)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : IsInducing f
h : IsTopologicalBasis T
a : α
⊢ (𝓝 a).HasBasis (fun t ↦ t ∈ preimage f '' T ∧ a ∈ t) id

Tactic:
convert! (hf.basis_nhds (h.nhds_hasBasis (a := f a))).to_image_id with s
    aesop

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
⊢ Continuous[t, inst✝] f ↔ ∀ s ∈ B, IsOpen[t] (f ⁻¹' s)

Tactic:
hB.eq_generateFrom,

Goal state after:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
⊢ Continuous[t, generateFrom B] f ↔ ∀ s ∈ B, IsOpen[t] (f ⁻¹' s)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
⊢ ContinuousOn f (s ∪ t)

Tactic:
classical
  refine fun x hx ↦ .union ?_ ?_
  · refine if hx : x ∈ s then hfs x hx else continuousWithinAt_of_notMem_closure ?_
    rwa [hs.closure_eq]
  · refine if hx : x ∈ t then hft x hx else continuousWithinAt_of_notMem_closure ?_
    rwa [ht.closure_eq]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case h
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∉ I
⊢ univ ⊆ univ ∧ IsOpen[T i] univ ∧ a i ∈ univ

Tactic:
exact ⟨Subset.rfl, isOpen_univ, mem_univ _⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
n : Type u_9
m : Type u_10
f : m → n
hf : Surjective f
⊢ IsEmbedding fun x ↦ x ∘ f

Tactic:
by
  refine ⟨isInducing_iff_nhds.mpr fun x ↦ ?_, hf.injective_comp_right⟩
  simp only [nhds_pi, Filter.pi, Filter.comap_iInf, ← hf.iInf_congr, Filter.comap_comap,
    Function.comp_def]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : SecondCountableTopology α
inst✝ : SecondCountableTopology β
b : Set (Set (α ⊕ β)) := (fun u ↦ Sum.inl '' u) '' countableBasis α ∪ (fun u ↦ Sum.inr '' u) '' countableBasis β
⊢ SecondCountableTopology (α ⊕ β)

Tactic:
have A : IsTopologicalBasis b := (isBasis_countableBasis α).sum (isBasis_countableBasis β)

Goal state after:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : SecondCountableTopology α
inst✝ : SecondCountableTopology β
b : Set (Set (α ⊕ β)) := (fun u ↦ Sum.inl '' u) '' countableBasis α ∪ (fun u ↦ Sum.inr '' u) '' countableBasis β
A : IsTopologicalBasis b
⊢ SecondCountableTopology (α ⊕ β)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset ↑s
hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)
x : X
hx : x ∈ s
⊢ ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝 x

Tactic:
rcases mem_iUnion₂.1 (hst hx) with ⟨y, hyt, hy⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset ↑s
hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)
x : X
hx : x ∈ s
y : ↑s
hyt : y ∈ t
hy : x ∈ interior (U ↑y ⋯)
⊢ ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝 x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst✝] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
a : Finset ↑t
⊢ (s ∩ ⋂ i ∈ a, ↑i).Nonempty

Tactic:
simpa using h (Subtype.val '' (a : Set t)) (by simp) (a.finite_toSet.image _)

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen[inst✝] (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x f

Tactic:
contrapose! h

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
h : ∀ x ∈ s, ¬ClusterPt x f
⊢ ∃ ι U, (∀ (i : ι), IsOpen[inst✝] (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg.inl.hs
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) (s ∩ {a | p a}) x

Tactic:
exact (hf x hx).congr (fun y hy => if_pos hy.2) (if_pos hx.2)

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
x₁ x₂ : X
y₁ y₂ : Y
⊢ ((x₁, y₁) ~ᵢ (x₂, y₂)) ↔ (x₁ ~ᵢ x₂) ∧ (y₁ ~ᵢ y₂)

Tactic:
simp only [Inseparable, nhds_prod_eq, Filter.prod_inj]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ↑f ≤ 𝓝 x ×ˢ 𝓝 y

Tactic:
exact le_inf hx hy

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

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
hy : x ≠ y
⊢ 𝓝[≠] x ≤ 𝓝[{y}ᶜ] x

Tactic:
rw [Ne.nhdsWithin_compl_singleton hy]

Goal state after:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
hy : x ≠ y
⊢ 𝓝[≠] x ≤ 𝓝 x
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ s ⊓ 𝓝ˢ t ≤ 𝓝ˢ (s ∩ t)

Tactic:
simp_rw [hs.nhdsSet_inf_eq_biSup, ht.inf_nhdsSet_eq_biSup, nhdsSet, sSup_image]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ ⨆ x ∈ s, ⨆ x_2 ∈ t, 𝓝 x ⊓ 𝓝 x_2 ≤ ⨆ a ∈ s ∩ t, 𝓝 a
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
⊢ (∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) → ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite

Tactic:
intro h z h₁z

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
⊢ (∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite) → ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅

Tactic:
intro h z h₁z

Goal state after:
case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
z : X
h₁z : z ∈ U
⊢ ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
⊢ IsPreirreducible S → ∀ x ∈ S, S ⊆ closure[inst✝¹] {x}

Tactic:
intro h x hx y hy

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
⊢ y ∈ closure[inst✝¹] {x}
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
a : α
⊢ 𝓝[≠] a ≤ cofinite

Tactic:
refine le_cofinite_iff_compl_singleton_mem.mpr fun x ↦ ?_

Goal state after:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
a x : α
⊢ {x}ᶜ ∈ 𝓝[≠] a
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case empty
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ i ∈ ∅, IsOpen[inst✝¹] (U i)
hsC : s ⊆ ⋃ i ∈ ∅, U i
⊢ ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ ∅, K i

Tactic:
refine ⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, ?_⟩

Goal state after:
case empty
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ i ∈ ∅, IsOpen[inst✝¹] (U i)
hsC : s ⊆ ⋃ i ∈ ∅, U i
⊢ s = ⋃ i ∈ ∅, (fun x ↦ ∅) i
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ ((∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t) → IsConnected s

Tactic:
rintro (⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩)

Goal state after:
case refine_2.inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set α
ht : IsConnected t
⊢ IsConnected (inl '' t)

case refine_2.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsConnected t
⊢ IsConnected (inr '' t)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ ((∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t) → IsPreconnected s

Tactic:
rintro (⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩)

Goal state after:
case refine_2.inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set α
ht : IsPreconnected t
⊢ IsPreconnected (inl '' t)

case refine_2.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsPreconnected t
⊢ IsPreconnected (inr '' t)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case inl
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hsu : s ∩ u = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
exact Or.inr ((Set.disjoint_iff_inter_eq_empty.2 hsu).subset_right_of_subset_union hsuv)

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen[inst✝] (U i)) → s ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
⊢ f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f

Tactic:
contrapose! h

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
h : f ≤ 𝓟 s ∧ ∀ x ∈ s, ¬ClusterPt x f
⊢ ∃ ι U, (∀ (i : ι), IsOpen[inst✝] (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Set ι), t.Countable → ¬s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
c : I.Countable
A : ι → Set X
h : ¬IsMeagre (⋃ i ∈ I, A i)
⊢ ∃ i ∈ I, ¬IsMeagre (A i)

Tactic:
contrapose! h

Goal state after:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
c : I.Countable
A : ι → Set X
h : ∀ i ∈ I, IsMeagre (A i)
⊢ IsMeagre (⋃ i ∈ I, A i)
Module: Mathlib.Topology.UniformSpace.DiscreteUniformity

Goal state before:
pp: X : Type u_1
u : UniformSpace X
inst✝² : DiscreteUniformity X
Y : Type u_2
inst✝¹ : UniformSpace Y
inst✝ : DiscreteUniformity Y
⊢ DiscreteUniformity (X × Y)

Tactic:
by
  simp [discreteUniformity_iff_eq_principal_setRelId, uniformity_prod_eq_comap_prod,
    eq_principal_setRelId, SetRel.id, Set.prod_eq, Prod.ext_iff, Set.ofPred_and]

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

Goal state before:
pp: α : Type ua
u : UniformSpace α
a : α
⊢ 𝓝 a = 𝓝 a

Tactic:
by
    rw [u.nhds_eq_comap_uniformity, u.toCore.nhds_toTopologicalSpace]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
⊢ V ∈ 𝓝 (x, x)

Tactic:
apply mem_of_superset this

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
⊢ ball x w ×ˢ ball x w ⊆ V
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
b : Bool
x : ↑(S b)
⊢ ∃ i, Disjoint (ball (↑x) ((B i).comp (B i).inv)) (S !b)

Tactic:
have hST : Disjoint (S b) (closure (S !b)) := b.casesOn (false := hsT) (true := hSt.symm)

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
b : Bool
x : ↑(S b)
hST : Disjoint (S b) (closure[inst✝¹.toTopologicalSpace] (S !b))
⊢ ∃ i, Disjoint (ball (↑x) ((B i).comp (B i).inv)) (S !b)
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SetRel.IsSymm V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
⊢ z = y

Tactic:
by_contra hzy

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SetRel.IsSymm V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
hzy : ¬z = y
⊢ False