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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝¹ : Add α
inst✝ : Add γ
h : Periodic f c
g : γ →ₙ+ α
g_inv : α → γ
hg : RightInverse g_inv ⇑g
x : γ
⊢ (f ∘ ⇑g) (x + g_inv c) = (f ∘ ⇑g) x

Tactic:
simp only [hg c, h (g x), map_add, comp_apply]

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : NonAssocRing α
h : Periodic f c
n : ℕ
⊢ f (↑n * c - x) = f (-x)

Tactic:
simpa only [sub_eq_neg_add] using h.nat_mul n (-x)

Goal state after:
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
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(extensionOfMax i f).toLinearPMap (fst i x) + (extendIdealTo i f h y) (snd i x) =
    ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ +
      (extendIdealTo i f h y) (snd i x)

Tactic:
← (extensionOfMax i f).toLinearPMap.map_add,

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(extensionOfMax i f).toLinearPMap (fst i x) + (extendIdealTo i f h y) (snd i x) =
    ↑(extensionOfMax i f).toLinearPMap (⟨a, ha⟩ + ⟨r • y - snd i x • y, ⋯⟩) + (extendIdealTo i f h y) (snd i x)
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case prime_pow
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ (p n : ℕ), Prime p → 0 < n → p ^ n ≠ 0 → f (p ^ n) = (p ^ n).factorization.prod fun p k ↦ f (p ^ k)

Tactic:
rintro p k hp - -

Goal state after:
case prime_pow
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ k) = (p ^ k).factorization.prod fun p k ↦ f (p ^ k)
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case one
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ 1 ≠ 0 → f 1 = (factorization 1).prod fun p k ↦ f (p ^ k)

Tactic:
rintro -

Goal state after:
case one
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ f 1 = (factorization 1).prod fun p k ↦ f (p ^ k)
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
⊢ s ∩ t ∈ insert univ S

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst✝ : l.IsCountablyGenerated
hxy : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, x n ∉ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), x (y n) ∉ s
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (ms : ℕ → ℕ), ¬Tendsto (fun n ↦ x (ns (ms n))) atTop f

Tactic:
refine ⟨y, hy_tendsto, fun ms hms_tendsto ↦ ?_⟩

Goal state after:
α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst✝ : l.IsCountablyGenerated
hxy : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, x n ∉ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), x (y n) ∉ s
ms : ℕ → ℕ
hms_tendsto : Tendsto (fun n ↦ x (y (ms n))) atTop f
⊢ False
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 : α
this : toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)

Tactic:
by
    rwa [neg_add, ← sub_eq_add_neg, toIocDiv_sub_eq_toIocDiv_add', toIocDiv_add_right] at this

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen[inst✝] s₁
h₂ : IsOpen[inst✝] s₂
⊢ IsOpen[inst✝] (s₁ ∪ s₂)

Tactic:
rw [union_eq_iUnion]; exact isOpen_iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
z : ℤ
⊢ toIocMod hp a a = a + p

Tactic:
toIocMod_apply_left

Goal state after:
case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
z : ℤ
⊢ a + p = a + p
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (frontier s) ⊆ interior s

Tactic:
rw [A]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (s \ interior s) ⊆ interior s
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier sᶜ = closure sᶜ \ interior sᶜ

Tactic:
closure_sdiff_interior

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier sᶜ = frontier sᶜ
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 : α
⊢ a < b - -(↑⌊(a + p - b) / p⌋ * p) ∧ b - -(↑⌊(a + p - b) / p⌋ * p) ≤ a + p

Tactic:
sub_neg_eq_add,

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ 𝓝ˢ {x} ⊔ 𝓝ˢ s = 𝓝 x ⊔ 𝓝ˢ s

Tactic:
nhdsSet_singleton

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ 𝓝 x ⊔ 𝓝ˢ s = 𝓝 x ⊔ 𝓝ˢ s
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
⊢ IsOpen[inst✝²] (p ⁻¹' U) ↔ ∃ V, IsOpen[inst✝] V ∧ g ⁻¹' V = U

Tactic:
simp_rw [hf.isOpen_iff,
    (Set.image_surjective.mpr hq.surjective).exists,
    ← hq.isQuotientMap.isOpen_preimage]

Goal state after:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
⊢ (∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = p ⁻¹' U) ↔ ∃ x, IsOpen[inst✝¹] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U
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
⊢ ⨆ i ∈ s, comap f (𝓝ˢ {i}) ≤ ⨆ i ∈ s, 𝓝ˢ (f ⁻¹' {i})

Tactic:
nhdsSet_singleton

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
⊢ ⨆ i ∈ s, comap f (𝓝 i) ≤ ⨆ i ∈ s, 𝓝ˢ (f ⁻¹' {i})
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case inr.mp.refine_2
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
⊢ IsOpen[inst✝] t

Tactic:
simpa only [snd_image_prod st.1 t] using isOpenMap_snd _ H

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
a : α
⊢ ContinuousWithinAt f {a} a

Tactic:
simpa only [ContinuousWithinAt, nhdsWithin_singleton, tendsto_pure_left] using fun s =>
      mem_of_mem_nhds

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[univ] s = 𝓝ˢ s

Tactic:
simp [nhdsSetWithin]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[s] univ = 𝓟 s

Tactic:
simp [nhdsSetWithin]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[∅] s = ⊥

Tactic:
simp [nhdsSetWithin]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[s] ∅ = ⊥

Tactic:
simp [nhdsSetWithin]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X ⊕ Y)
⊢ IsClosed[instTopologicalSpaceSum] s ↔ IsClosed[inst✝¹] (inl ⁻¹' s) ∧ IsClosed[inst✝] (inr ⁻¹' s)

Tactic:
simp only [← isOpen_compl_iff, isOpen_sum_iff, preimage_compl]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
x : α × β
⊢ ContinuousAt f x ↔ ContinuousAt (fun x_1 ↦ f (x.1, x_1)) x.2

Tactic:
simp_rw [← continuousWithinAt_univ]; exact continuousWithinAt_prod_of_discrete_left

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
⊢ SeparableSpace ((i : ι) → X i)

Tactic:
choose t htc htd using (exists_countable_dense <| X ·)
  have := fun i ↦ (htc i).to_subtype
  nontriviality ∀ i, X i; inhabit ∀ i, X i
  classical
    set f : (Σ I : Finset ι, ∀ i : I, t i) → ∀ i, X i := fun ⟨I, g⟩ i ↦
      if hi : i ∈ I then g ⟨i, hi⟩ else (default : ∀ i, X i) i
    refine ⟨⟨range f, countable_range f, dense_iff_inter_open.2 fun U hU ⟨g, hg⟩ ↦ ?_⟩⟩
    rcases isOpen_pi_iff.1 hU g hg with ⟨I, u, huo, huU⟩
    have : ∀ i : I, ∃ y ∈ t i, y ∈ u i := fun i ↦
      (htd i).exists_mem_open (huo i i.2).1 ⟨_, (huo i i.2).2⟩
    choose y hyt hyu using this
    lift y to ∀ i : I, t i using hyt
    refine ⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self (f := f) ⟨I, y⟩⟩
    simp only [f, dif_pos hi]
    exact hyu ⟨i, _⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
ht : IsSeparable t
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure[t✝] cs
⊢ IsSeparable (s ×ˢ t)

Tactic:
rcases ht with ⟨ct, ct_count, hct⟩

Goal state after:
α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure[t✝] cs
ct : Set β
ct_count : ct.Countable
hct : t ⊆ closure[inst✝] ct
⊢ IsSeparable (s ×ˢ t)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
s : Set ((i : ι) → X i)
x✝ : s ∈ {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
t : (a : ι) → Set (X a)
ht : ∀ (a : ι), t a ∈ g a
Eq : s = univ.pi t
⊢ (∀ a ∈ Finset.univ, t a ∈ g a) ∧ s = (↑Finset.univ).pi t

Tactic:
simp [ht, Eq]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t✝] v
⊢ ∃ v_1 ∈ ⋃ u ∈ countableBasis α, s u, x ∈ v_1 ∧ v_1 ⊆ v

Tactic:
simp only [mem_iUnion, exists_prop]

Goal state after:
case h_nhds
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t✝] v
⊢ ∃ v_1, (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝] t
f : Filter X
⊢ ∀ [f.NeBot], f ≤ 𝓟 (s ∩ t) → ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
hnf

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝] t
f : Filter X
hnf : f.NeBot
⊢ f ≤ 𝓟 (s ∩ t) → ∃ x ∈ s ∩ t, ClusterPt x f
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A B C : Set α
hB : B ⊆ A
hC : C ⊆ A
h : A ↓∩ B = A ↓∩ C
⊢ B = C

Tactic:
by
  simp only [← inter_eq_right] at hB hC
  simp only [Subtype.preimage_val_eq_preimage_val_iff, hB, hC] at h
  exact h

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

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ (ι : Type u) (U : ι → ↑S), s ⊆ ⋃ i, ↑(U i) → ∃ J, J.Finite ∧ s ⊆ ⋃ i ∈ J, ↑(U i)
P : Set (Set X)
hP : P ⊆ S
hs : s ⊆ ⋃₀ P
J : Set ↑P
hJ : J.Finite
cover : s ⊆ ⋃ i ∈ J, ↑⟨↑i, ⋯⟩
⊢ s ⊆ ⋃₀ ((fun x ↦ ↑x) '' J)

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
h : x ∈ s
b : α
x✝ : (fun x ↦ x ∈ { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }) b
hbx : b ≤ x
a : α
has : a ∈ s
hab : a ≤ b
⊢ x ≤ b

Tactic:
← hs.eq has h (hab.trans hbx)

Goal state after:
case refine_2
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
h : x ∈ s
b : α
x✝ : (fun x ↦ x ∈ { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }) b
hbx : b ≤ x
a : α
has : a ∈ s
hab : a ≤ b
⊢ a ≤ b
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsClosed[inst✝¹] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst✝¹] t → t = s
⊢ s.Subsingleton

Tactic:
refine fun x hx y hy => of_not_not fun hxy => ?_
  rcases exists_isOpen_xor_mem hxy with ⟨U, hUo, hU⟩
  wlog h : x ∈ U ∧ y ∉ U
  · refine this hs hmin y hy x hx (Ne.symm hxy) U hUo hU.symm (hU.resolve_left h)
  obtain ⟨hxU, hyU⟩ := h
  have : s \ U = s := hmin (s \ U) sdiff_subset ⟨y, hy, hyU⟩ (hs.sdiff hUo)
  exact (this.symm.subset hx).2 hxU

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ IsDiscrete Set.univ

Tactic:
isDiscrete_univ_iff

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ DiscreteTopology X
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case pos
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub

Tactic:
have : Nonempty { U // U ∈ c } := ⟨⟨U₀, hU₀⟩⟩

Goal state after:
case pos
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
⊢ IsDiscrete (s ∩ U)

Tactic:
rw [(by simp : ((s ∩ U) : Set X) = ((sᶜ ∪ Uᶜ)ᶜ : Set X)), isDiscrete_iff_nhdsNE]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
⊢ ∀ x ∈ (sᶜ ∪ Uᶜ)ᶜ, 𝓝[≠] x ⊓ 𝓟 (sᶜ ∪ Uᶜ)ᶜ = ⊥
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst✝] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
⊢ ∀ u_1 ∈ {U, u, v}, (t ∩ u_1).Nonempty

Tactic:
intro U H

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
t S U✝ : Set X
hU' : IsOpen[inst✝] U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U✝
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
H : U ∈ {U✝, u, v}
⊢ (t ∩ U).Nonempty
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
⊢ {x}ᶜ ∈ 𝓝ˢ s ↔ x ∉ s

Tactic:
rw [isOpen_compl_singleton.mem_nhdsSet, subset_compl_singleton_iff]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ 𝓝ˢ s ≤ 𝓝ˢ t → s ⊆ t

Tactic:
Filter.le_def

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ (∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s) → s ⊆ t
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Subsingleton
z : X
hz : z ∈ t
⊢ univ \ t ∩ (t \ s) = ∅

Tactic:
by aesop

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x z : X
hz : z ∈ s
⊢ univ \ {x} ∩ (s \ {x}ᶜ) = ∅

Tactic:
by aesop

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
hI : I.Finite
hs : ∀ i ∈ I, IsDiscrete (s i)
hsc : ∀ i ∈ I, IsClosed[inst✝] (s i)
⊢ IsDiscrete (⋃ i ∈ I, s i)

Tactic:
have := hI.to_subtype
  simp only [biUnion_eq_iUnion, Subtype.forall'] at *
  exact .iUnion hs hsc

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst✝¹] K)
this : SeparatedNhds (closure[inst✝¹] K \ U) (closure[inst✝¹] K \ V)
O₁ O₂ : Set X
h1O₁ : IsOpen[inst✝¹] O₁
h1O₂ : IsOpen[inst✝¹] O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ K = K \ (O₁ ∩ O₂)

Tactic:
hO.inter_eq,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst✝¹] K)
this : SeparatedNhds (closure[inst✝¹] K \ U) (closure[inst✝¹] K \ V)
O₁ O₂ : Set X
h1O₁ : IsOpen[inst✝¹] O₁
h1O₂ : IsOpen[inst✝¹] O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ K = K \ ∅
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
by_cases! hTd : ∃ t ∈ T, Disjoint (@nhds X t x) (@nhds X t y)

Goal state after:
case pos
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
hTd : ∃ t ∈ T, Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

case neg
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
hTd : ∀ t ∈ T, ¬Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst✝] t
f : Filter X
⊢ ∀ [f.NeBot] [CountableInterFilter f], f ≤ 𝓟 (s ∩ t) → ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
hnf

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst✝] t
f : Filter X
hnf : f.NeBot
⊢ ∀ [CountableInterFilter f], f ≤ 𝓟 (s ∩ t) → ∃ x ∈ s ∩ t, ClusterPt x f
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
H : ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
a : X
s : Set X
hs : s ∈ 𝓝 a
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst✝] t ∧ t ⊆ s

Tactic:
← H

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
H : ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
a : X
s : Set X
hs : s ∈ (𝓝 a).lift' closure[inst✝]
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst✝] t ∧ t ⊆ s
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
⊢ (s ∩ (a ∩ b)).Nonempty

Tactic:
· rw [nonempty_iff_ne_empty]
    intro h
    exact H (s ∩ a) (s ∩ b)
      (isClopen_inter_of_disjoint_cover_clopen' hs hsab ha hb (by grind))
      (isClopen_inter_of_disjoint_cover_clopen' hs (by grind) hb ha (by grind))
      hsa hsb (by grind [Set.disjoint_iff_inter_eq_empty]) (by grind)

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

Goal state before:
pp: case mpr
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
U : Set X
⊢ (∃ s, s.Countable ∧ U = ⋃ i ∈ s, b i) → IsLindelof U ∧ IsOpen[inst✝] U

Tactic:
rintro ⟨s, hs, rfl⟩

Goal state after:
case mpr
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
s : Set ι
hs : s.Countable
⊢ IsLindelof (⋃ i ∈ s, b i) ∧ IsOpen[inst✝] (⋃ i ∈ s, b i)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case mpr.right
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
s : Set ι
hs : s.Countable
⊢ IsOpen[inst✝] (⋃ i ∈ s, b i)

Tactic:
exact isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _)

Goal state after: