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

Goal state before:
pp: case inr.i_surj
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
this : d ∣ b
⊢ ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b

Tactic:
rcases this with ⟨q, rfl⟩

Goal state after:
case inr.i_surj
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : (d * x).gcd (d * q) = d
⊢ ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = d * q
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p =
    (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
simp only [prod_primeFactors_prod_factorization, ← Finsupp.prod_mul]

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun a b ↦ a ^ (b - 1) * (a - 1) * a) = n.factorization.prod fun a b ↦ a ^ b * (a - 1)
Module: Mathlib.Data.Nat.Totient

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

Tactic:
rw [totient_mul _, totient_prime hp]
  simpa [h] using coprime_or_dvd_of_prime hp n

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
⊢ (p ^ k) ^ φ (p ^ k) / ∏ q ∈ (p ^ k).primeFactors, q ^ (φ (p ^ k) / (q - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
by
  have h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1)) := by
    rw [mul_left_comm]
    refine le_mul_of_one_le_right (Nat.zero_le _) ?_
    exact Right.one_le_mul hk <| Nat.le_sub_one_of_lt <| hp.one_lt
  simp_rw [Nat.totient_prime_pow hp hk, Nat.primeFactors_prime_pow hk.ne' hp, Finset.prod_singleton,
    Nat.mul_div_left _ (Nat.sub_pos_of_lt hp.one_lt), ← pow_mul]
  rw [Nat.pow_div h hp.pos]
  simp_rw [Nat.sub_mul, one_mul, Nat.mul_sub, mul_one]
  ring_nf

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (closure s).Nonempty ↔ s.Nonempty

Tactic:
simp only [nonempty_iff_ne_empty, Ne, closure_empty_iff]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
⊢ Dense s

Tactic:
intro x
    rw [mem_closure_iff]
    intro U U_op x_in
    exact h U U_op ⟨_, x_in⟩

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hx : F.HasBasis p s
⊢ ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in 𝓝 x, x ∈ s i

Tactic:
simp only [(𝓝 x).basis_sets.clusterPt_iff hx, Filter.frequently_iff]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hx : F.HasBasis p s
⊢ (∀ ⦃i : Set X⦄, i ∈ 𝓝 x → ∀ ⦃j : ι⦄, p j → (id i ∩ s j).Nonempty) ↔
    ∀ (i : ι), p i → ∀ {U : Set X}, U ∈ 𝓝 x → ∃ x ∈ U, x ∈ s i
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case left
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : x₃ ≡ x₂ [PMOD p]
⊢ False

Tactic:
rw [(modEq_iff_toIcoMod_eq_left hp).1 h] at h₁₂₃

Goal state after:
case left
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬x₃ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : x₃ ≡ x₂ [PMOD p]
⊢ False
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (pure x ⊓ F.lift' closure[inst✝]).NeBot → pure x ≤ F.lift' closure[inst✝]

Tactic:
intro h U hU
    simp_rw [← forall_mem_nonempty_iff_neBot, mem_inf_iff] at h
    simpa using h ({x} ∩ U) ⟨{x}, by simp, U, hU, rfl⟩

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 + ↑m * p

Tactic:
by
  simpa using toIcoMod_add_zsmul' hp a b m

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
s : Set (Set α)
hs : {u | GenerateOpen s u} = s
U : Set α
⊢ IsOpen[TopologicalSpace.mkOfClosure s hs] U ↔ IsOpen[generateFrom s] U

Tactic:
exact Set.ext_iff.mp hs.symm U

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : IndiscreteTopology α
a : α
⊢ 𝓝 a = ⊤

Tactic:
cases IndiscreteTopology.eq_top α
  exact nhds_top

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₁ : IsOpenMap f
h₂ : Injective f
h₃ : Continuous[inst✝¹, inst✝] f
s : Set X
hs' : IsClosed[inst✝¹] s
⊢ closure[inst✝¹] s = s

Tactic:
hs'.closure_eq

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : IsOpenMap f
h₂ : Injective f
h₃ : Continuous[inst✝¹, inst✝] f
s : Set X
hs' : IsClosed[inst✝¹] s
⊢ s = s
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun p ↦ f p.1 p.2
⊢ Continuous[instTopologicalSpaceProd, tc1] fun p ↦ f p.1 p.2

Tactic:
by
  have ha := @continuous_inf_dom_right _ _ id ta1 ta2 ta2 (@continuous_id _ (id _))
  have hb := @continuous_inf_dom_right _ _ id tb1 tb2 tb2 (@continuous_id _ (id _))
  have h_continuous_id := @Continuous.prodMap _ _ _ _ ta2 tb2 (ta1 ⊓ ta2) (tb1 ⊓ tb2) _ _ ha hb
  exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ h h_continuous_id

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
x : CofiniteTopology X
⊢ 𝓝 x = pure x ⊔ cofinite

Tactic:
ext U
  simp_rw [mem_nhds_iff, isOpen_iff]
  constructor
  · rintro ⟨V, hVU, V_op, haV⟩
    exact mem_sup.mpr ⟨hVU haV, mem_of_superset (V_op ⟨_, haV⟩) hVU⟩
  · rintro ⟨hU : x ∈ U, hU' : Uᶜ.Finite⟩
    exact ⟨U, Subset.rfl, fun _ => hU', hU⟩

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
t : Set Y
hs : Dense s
ht : Dense t
x : X × Y
⊢ x ∈ closure[instTopologicalSpaceProd] (s ×ˢ t)

Tactic:
rw [closure_prod_eq]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : Dense s
ht : Dense t
x : X × Y
⊢ x ∈ closure[inst✝¹] s ×ˢ closure[inst✝] t
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
exact hg.comp_inter hf

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
⊢ IsTopologicalBasis (⋃ i, image Subtype.val '' b i)

Tactic:
by
  refine isTopologicalBasis_of_isOpen_of_nhds (fun u hu => ?_) ?_
  · simp only [mem_iUnion, mem_image] at hu
    rcases hu with ⟨i, s, sb, rfl⟩
    exact (Uo i).isOpenMap_subtype_val _ ((hb i).isOpen sb)
  · intro a u ha uo
    rcases iUnion_eq_univ_iff.1 Uc a with ⟨i, hi⟩
    lift a to ↥(U i) using hi
    rcases (hb i).exists_subset_of_mem_open ha (uo.preimage continuous_subtype_val) with
      ⟨v, hvb, hav, hvu⟩
    exact ⟨(↑) '' v, mem_iUnion.2 ⟨i, mem_image_of_mem _ hvb⟩, mem_image_of_mem _ hav,
      image_subset_iff.2 hvu⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
⊢ Dense (invFun f '' s)

Tactic:
h'.dense_iff,

Goal state after:
case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
⊢ ∀ (x : α), f x ∈ closure[inst✝¹] (f '' invFun f '' s)
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, s x ⊆ ⋃ x, accumulate s x

Tactic:
exact iUnion_mono fun i => subset_accumulate

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
hx : ∃ i_1 ≤ i, x ∈ s i_1
⊢ x ∉ s j

Tactic:
rcases hx with ⟨k, hk, hx⟩

Goal state after:
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
k : α
hk : k ≤ i
hx : x ∈ s k
⊢ x ∉ s j
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : 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
⊢ s ×ˢ t ⊆ closure[instTopologicalSpaceProd] (cs ×ˢ ct)

Tactic:
rw [closure_prod_eq]

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
⊢ s ×ˢ t ⊆ closure[t✝] cs ×ˢ closure[inst✝] ct
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s✝ t : Set α
p q : α → Prop
f : Ultrafilter α
m : α → Ultrafilter β
s : Set β
⊢ (sᶜ ∉ (↑f).bind fun x ↦ ↑(m x)) ↔ s ∈ (↑f).bind fun x ↦ ↑(m x)

Tactic:
simp only [mem_bind', mem_coe, ← compl_mem_iff_notMem, compl_ofPred, compl_compl]

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Basic

Goal state before:
pp: α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : s ∈ f
⊢ ∃ x ∈ s, f = pure x

Tactic:
rw [← biUnion_of_singleton s] at h'

Goal state after:
α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : ⋃ x ∈ s, {x} ∈ f
⊢ ∃ x ∈ s, f = pure x
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst✝] (s i)
x : X
⊢ ∀ᶠ (y : X) in 𝓝 x, {i | y ∈ s i} ⊆ {i | x ∈ s i}

Tactic:
by
  filter_upwards [hs.iInter_compl_mem_nhds hs' x] with y hy i hi
  push _ ∈ _ at hy
  exact not_imp_not.mp (hy i) hi

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋂₀ S = ⋂ a ∈ S, A ↓∩ a

Tactic:
simp_rw [sInter_eq_biInter, preimage_iInter]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ Disjoint f (cocompact X) ↔ ∃ K ∈ f, IsCompact K

Tactic:
simp_rw [hasBasis_cocompact.disjoint_iff_right, compl_compl]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ (∃ i, IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen[instTopologicalSpaceProd] n
hp : n ∈ 𝓝ˢ (s ×ˢ t)
⊢ ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

Tactic:
hs.nhdsSet_prod_eq ht,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen[instTopologicalSpaceProd] n
hp : n ∈ 𝓝ˢ s ×ˢ 𝓝ˢ t
⊢ ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
f : Filter X
inst✝ : f.NeBot
⊢ ∃ x, ClusterPt x f

Tactic:
simpa using isCompact_univ (show f ≤ 𝓟 univ by simp)

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
⊢ x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 {x}ᶜ ⊓ 𝓟 s)

Tactic:
(finite_singleton _).cofinite_inf_principal_compl

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
⊢ x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ StableUnderSpecialization s ↔ ∃ S, (∀ s ∈ S, IsClosed[inst✝] s) ∧ ⋃₀ S = s

Tactic:
refine ⟨fun H ↦ ⟨(fun x : X ↦ closure {x}) '' s, ?_, ?_⟩, fun ⟨S, hS, e⟩ ↦ e ▸
    stableUnderSpecialization_sUnion S (fun x hx ↦ (hS x hx).stableUnderSpecialization)⟩

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ∀ s_1 ∈ (fun x ↦ closure[inst✝] {x}) '' s, IsClosed[inst✝] s_1

case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ⋃₀ ((fun x ↦ closure[inst✝] {x}) '' s) = s
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 ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Tactic:
obtain ⟨x : X, sx : x ∈ s, hx : map Prod.fst f.1 ≤ 𝓝 x⟩ :=
    hs (f.map Prod.fst) (mem_map.2 <| mem_of_superset hfs fun x => And.left)

Goal state after:
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 : map Prod.fst ↑f ≤ 𝓝 x
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X✝ : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
s t : Set X✝
f : X✝ → Y
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ IsCompact (univ.pi fun i ↦ univ)

Tactic:
exact isCompact_univ_pi fun i => isCompact_univ

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t
s : Set X
sS : s ⊆ S
U : Set X
Uo : IsOpen[inst✝] U
Us : U ∩ S = sᶜ ∩ S
⊢ Uᶜ ∩ S = s

Tactic:
rw [left_eq_inter.mpr sS]; simp_all [Set.ext_iff]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s
s : Set X
sS : s ⊆ S
U : Set X
Uo : IsClosed[inst✝] U
Us : U ∩ S = sᶜ ∩ S
⊢ Uᶜ ∩ S = s

Tactic:
rw [left_eq_inter.mpr sS]; simp_all [Set.ext_iff]

Goal state after:
Module: Mathlib.Order.SuccPred.Relation

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen (swap r) m n

Tactic:
exact reflTransGen_of_succ_of_le (swap r) h hmn

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Finite
⊢ tᶜ ∈ codiscreteWithin s

Tactic:
apply h.induction_on (motive := fun t _ ↦ tᶜ ∈ codiscreteWithin s)

Goal state after:
case empty
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Finite
⊢ ∅ᶜ ∈ codiscreteWithin s

case insert
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Finite
⊢ ∀ {a : X} {s_1 : Set X}, a ∉ s_1 → s_1.Finite → s_1ᶜ ∈ codiscreteWithin s → (insert a s_1)ᶜ ∈ codiscreteWithin s
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a

Tactic:
continuousWithinAt_Ioi_iff_Ici,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ici a) a
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:
by
  simpa using! isCompact_univ.codiscreteWithin_eq

Goal state after:
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ∃ x_1, x < x_1
⊢ ∃ y ∈ s, x ≤ y

Tactic:
rcases hs.exists_mem_open isOpen_Ioi hx with ⟨y, hys, hy : x < y⟩

Goal state after:
case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ∃ x_1, x < x_1
y : α
hys : y ∈ s
hy : x < y
⊢ ∃ y ∈ s, x ≤ y
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
x : α
⊢ IsOpen[inst✝¹] (connectedComponent x)

Tactic:
← connectedComponentIn_univ

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
x : α
⊢ IsOpen[inst✝¹] (connectedComponentIn univ x)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x y : α
F : Set α
h : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F x = connectedComponentIn F y

Tactic:
have hx : x ∈ F := connectedComponentIn_nonempty_iff.mp ⟨y, h⟩

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x y : α
F : Set α
h : y ∈ connectedComponentIn F x
hx : x ∈ F
⊢ connectedComponentIn F x = connectedComponentIn F y
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
F : Set β
hf : ContinuousOn f (f ⁻¹' F)
y : β
⊢ f ⁻¹' connectedComponentIn F y = ⋃ x ∈ f ⁻¹' connectedComponentIn F y, connectedComponentIn (f ⁻¹' F) x

Tactic:
by
  refine subset_antisymm (fun z hz ↦ ?_) (iUnion₂_subset fun x hx z hz ↦ ?_)
  · exact mem_biUnion hz (mem_connectedComponentIn (connectedComponentIn_subset F y hz))
  · rw [mem_preimage, connectedComponentIn_eq hx]
    exact connectedComponentIn_mono _ (image_preimage_subset f F)
      (hf.mapsTo_connectedComponentIn (connectedComponentIn_subset F y hx) hz)

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

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ Disjoint (e '' s) (closure[inst✝¹] (e '' t))

Tactic:
rwa [← subset_compl_iff_disjoint_right, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_right]

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

Goal state before:
pp: case mp
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ∃ s, s.Countable ∧ ⋃ i, (b ∘ f') i = ⋃ i ∈ s, b i

Tactic:
refine ⟨t.image f', Countable.image (ht.1) f', le_antisymm ?_ ?_⟩

Goal state after:
case mp.refine_1
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i

case mp.refine_2
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ⋃ i ∈ f' '' t, b i ⊆ ⋃ i, (b ∘ f') i
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Finite
f : ι → Set X
h : ∀ i ∈ s, IsGδ (f i)
⊢ IsGδ (⋃ i ∈ s, f i)

Tactic:
by
  rw [← sUnion_image]
  exact .sUnion (hs.image _) (forall_mem_image.2 h)

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

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
t' : β
ht' : t' ∈ t
htu : f ⁻¹' {t'} ⊆ u
⊢ t' ∈ T₁ ∨ t' ∈ T₂

Tactic:
left

Goal state after:
case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := ⋯
T₂ : Set β := ⋯
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
t' : β
ht' : t' ∈ t
htu : f ⁻¹' {t'} ⊆ u
⊢ t' ∈ T₁
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
this : Countable ↑I
⊢ ∀ (i : ↑I), IsMeagre (f ↑i)

Tactic:
intro ⟨i, hi⟩

Goal state after:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
this : Countable ↑I
i : ι
hi : i ∈ I
⊢ IsMeagre (f ↑⟨i, hi⟩)