mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case refine_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
a✝ : a ∉ s
h1 : ↑s ⊆ S → ⋂₀ ↑s ∈ S
h2 : ↑(insert a s) ⊆ S
⊢ ⋂₀ ↑(insert a s) ∈ S

Tactic:
suffices a ∩ ⋂₀ ↑s ∈ S by simpa

Goal state after:
case refine_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
a✝ : a ∉ s
h1 : ↑s ⊆ S → ⋂₀ ↑s ∈ S
h2 : ↑(insert a s) ⊆ S
⊢ a ∩ ⋂₀ ↑s ∈ S
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: ι : Type u_2
X : Type u_3
s : ι → Set X
⊢ ⋃ i ∈ ∅, s i = ∅

Tactic:
by
  simp

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

Goal state before:
pp: case mpr
m n : ℕ
⊢ (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2 → (φ m).Coprime (φ n)

Tactic:
· simp_rw [← totient_eq_one_iff]
    rintro (h | h) <;> rw [h]
    exacts [Nat.coprime_one_left _, Nat.coprime_one_right _]

Goal state after:
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : f.HasBasis p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ s ∈ f.lift g ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s

Tactic:
refine (mem_biInf_of_directed ?_ ⟨univ, univ_sets _⟩).trans ?_
  · intro t₁ ht₁ t₂ ht₂
    exact ⟨t₁ ∩ t₂, inter_mem ht₁ ht₂, gm inter_subset_left, gm inter_subset_right⟩
  · simp only [← (hg _).mem_iff]
    exact hf.exists_iff fun t₁ t₂ ht H => gm ht H

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
p q : X → Prop
hp : IsOpen[inst✝] {x | p x}
hq : IsClosed[inst✝] {x | q x}
⊢ IsClosed[inst✝] {x | p x → q x}

Tactic:
simpa only [imp_iff_not_or] using! hp.isClosed_compl.union hq

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 : ℤ
⊢ toIocMod hp a (b - m • p) = toIocMod hp a b

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIocMod_add_zsmul]

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 : α
⊢ toIocMod hp (-a) b = p - toIcoMod hp a (-b)

Tactic:
simpa only [neg_neg] using toIocMod_neg hp (-a) (-b)

Goal state after:
Module: Mathlib.Topology.Closure

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

Tactic:
rw [Dense, Dense, closure_closure]

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ Y
⊢ IsOpenMap ⇑e.symm ↔ Continuous[inst✝¹, inst✝] ⇑e

Tactic:
simp_rw [← Equiv.continuous_symm_iff, Equiv.symm_symm]

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (∀ (x : Set Y), IsOpen[inst✝] xᶜ → IsOpen[inst✝¹] (f ⁻¹' xᶜ)) ↔
    ∀ (s : Set Y), IsClosed[inst✝] s → IsClosed[inst✝¹] (f ⁻¹' s)

Tactic:
by
    simp only [isOpen_compl_iff, preimage_compl]

Goal state after:
Module: Mathlib.Topology.Closure

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

Tactic:
← sdiff_eq,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier sᶜ = closure sᶜ \ interior sᶜ
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
⊢ x ∈ C ∨ AccPt x (𝓟 C)

Tactic:
by_contra! hc

Goal state after:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
hc : x ∉ C ∧ ¬AccPt x (𝓟 C)
⊢ False
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst✝] s ↔ (comap Subtype.val (𝓝 x)).NeBot

Tactic:
simp_rw [mem_closure_iff_nhds, comap_neBot_iff, Set.inter_nonempty_iff_exists_right,
    SetCoe.exists, exists_prop]

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
⊢ toIcoMod hp a b - b = -↑(toIcoDiv hp a b) * p

Tactic:
by
  simp

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
⊢ toIocMod hp a b - b = -↑(toIocDiv hp a b) * p

Tactic:
by
  simp

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
⊢ b - toIcoMod hp a b = ↑(toIcoDiv hp a b) * p

Tactic:
by
  simp

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
⊢ b - toIocMod hp a b = ↑(toIocDiv hp a b) * p

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ Disjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure[inst✝] t)

Tactic:
disjoint_comm,

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ Disjoint (𝓟 t) (𝓝ˢ s) ↔ Disjoint s (closure[inst✝] t)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ ContinuousWithinAt f s x

Tactic:
rw [ContinuousWithinAt, hx]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ Tendsto f ⊥ (𝓝 (f x))
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X × Y → Prop
x : X
y : Y
h : ∀ᶠ (x : X × Y) in 𝓝 x ×ˢ 𝓝 y, p x
⊢ ∀ᶠ (x' : X) in 𝓝 x, ∀ᶠ (y' : Y) in 𝓝 y, p (x', y')

Tactic:
exact h.curry

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ t ∈ 𝓝[insert a s] a ↔ a ∈ t ∧ t ∈ 𝓝[s] a

Tactic:
by
  simp

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 : α × β → γ
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f ↔ ∀ (a : α), Continuous[inst✝², inst✝¹] fun x ↦ f (a, x)

Tactic:
simp_rw [← continuousOn_univ]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (a : α), ContinuousOn (fun x ↦ f (a, x)) univ
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 : α × β → γ
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f ↔ ∀ (b : β), Continuous[inst✝³, inst✝¹] fun x ↦ f (x, b)

Tactic:
simp_rw [← continuousOn_univ]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (b : β), ContinuousOn (fun x ↦ f (x, b)) univ
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
i : ι
s : Set (A i)
hs : s ∈ g i
⊢ (∀ a ∈ {i}, update (fun i ↦ univ) i s a ∈ g a) ∧ (fun f ↦ f i) ⁻¹' s = (↑{i}).pi (update (fun i ↦ univ) i s)

Tactic:
simp [hs]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case mpr
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
U : ι → Set β
F : Finset ι
hSU : S = ⋂ i ∈ F, U i
U' : (i : ι) → Set (X i)
hU' : ∀ i ∈ F, U' i ∈ T i
hUU' : ∀ i ∈ F, f i ⁻¹' U' i = U i
⊢ ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i

Tactic:
exact ⟨U', F, hU', hSU ▸ (.symm <| iInter₂_congr hUU')⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t

Tactic:
by
  rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩
  refine ⟨(t ∪ ({ x | IsBot x } ∪ { x | IsTop x })) ∩ s, ?_, ?_, ?_, ?_, ?_⟩
  exacts [inter_subset_right,
    (htc.union ((countable_isBot α).union (countable_isTop α))).mono inter_subset_left,
    htd.mono (subset_inter subset_union_left hts), fun x hx hxs => ⟨Or.inr <| Or.inl hx, hxs⟩,
    fun x hx hxs => ⟨Or.inr <| Or.inr hx, hxs⟩]

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
⊢ (𝓝ˢ K).HasBasis (fun L ↦ L ∈ 𝓝ˢ K ∧ IsCompact L) id

Tactic:
by
  rw [hasBasis_self, (hasBasis_nhdsSet _).forall_iff (by grind)]
  intro U ⟨hU, h_KU⟩
  obtain ⟨L, hL, hKL, hLU⟩ := exists_compact_between hK hU h_KU
  exact ⟨L, by rwa [← subset_interior_iff_mem_nhdsSet], hL, hLU⟩

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

Goal state before:
pp: α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋂₀ S = ⋂₀ {x | ∃ B ∈ S, A ↓∩ B = x}

Tactic:
by
  rw [← Set.image, sInter_image]
  simp_rw [sInter_eq_biInter, preimage_iInter]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_3
κ : ι → Sort u_4
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Ici (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, Ici (f i j)

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_2
A : Set α
T : Set (Set ↑A)
hT : T.Nonempty
⊢ Subtype.val '' ⋂ i ∈ T, i = ⋂ a ∈ T, Subtype.val '' a

Tactic:
Subtype.val_injective.injOn.image_biInter_eq hT

Goal state after:
α : Type u_2
A : Set α
T : Set (Set ↑A)
hT : T.Nonempty
⊢ ⋂ i ∈ T, Subtype.val '' i = ⋂ a ∈ T, Subtype.val '' a
Module: Mathlib.Order.UpperLower.Closure

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

Tactic:
rwa [h.eq_of_ge ⟨a, has, rfl.le⟩ hax]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
a : α
f : (i : ι) → κ i → UpperSet α
⊢ a ∈ ⨆ i, ⨆ j, f i j ↔ ∀ (i : ι) (j : κ i), a ∈ f i j

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
a : α
f : (i : ι) → κ i → UpperSet α
⊢ a ∈ ⨅ i, ⨅ j, f i j ↔ ∃ i j, a ∈ f i j

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ¬x ⤳ y ↔ ∃ S, IsClosed[inst✝] S ∧ x ∈ S ∧ y ∉ S

Tactic:
specializes_iff_forall_closed

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (¬∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) ↔ ∃ S, IsClosed[inst✝] S ∧ x ∈ S ∧ y ∉ S
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsIrreducible s
u : Set X
hu : IsPreirreducible u ∧ s ⊆ u ∧ ∀ (u_1 : Set X), IsPreirreducible u_1 → u ⊆ u_1 → u_1 = u
⊢ ∃ u ∈ irreducibleComponents X, s ⊆ u

Tactic:
use u, ⟨⟨hs.left.mono hu.right.left,hu.left⟩,fun _ h hl => (hu.right.right _ h.right hl).le⟩

Goal state after:
case right
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsIrreducible s
u : Set X
hu : IsPreirreducible u ∧ s ⊆ u ∧ ∀ (u_1 : Set X), IsPreirreducible u_1 → u ⊆ u_1 → u_1 = u
⊢ s ⊆ u
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPreirreducible s
⊢ IsPreirreducible univ

Tactic:
by
    rintro _ _ ⟨u, hu, rfl⟩ ⟨v, hv, rfl⟩ ⟨⟨x, hxs⟩, -, hxu⟩ ⟨⟨y, hys⟩, -, hyv⟩
    rcases h u v hu hv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩ with ⟨x, hxs, ⟨hxu, hxv⟩⟩
    exact ⟨⟨x, hxs⟩, ⟨Set.mem_univ _, ⟨hxu, hxv⟩⟩⟩

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✝
X : Type u_3
inst✝ : Infinite X
u v : Set (CofiniteTopology X)
⊢ (u.Nonempty → uᶜ.Finite) → (v.Nonempty → vᶜ.Finite) → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty

Tactic:
intro hu hv hu' hv'

Goal state after:
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
s t : Set X✝
X : Type u_3
inst✝ : Infinite X
u v : Set (CofiniteTopology X)
hu : u.Nonempty → uᶜ.Finite
hv : v.Nonempty → vᶜ.Finite
hu' : u.Nonempty
hv' : v.Nonempty
⊢ (u ∩ v).Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsIrreducible s ↔ ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed[inst✝] z) → s ⊆ ⋃₀ ↑t → ∃ z ∈ t, s ⊆ z

Tactic:
by
  simp only [isIrreducible_iff_sInter]
  refine ((@compl_involutive (Set X) _).toPerm _).finsetCongr.forall_congr fun {t} => ?_
  simp_rw [Equiv.finsetCongr_apply, Finset.forall_mem_map, Finset.mem_map, Finset.coe_map,
    sUnion_image, Equiv.coe_toEmbedding, Function.Involutive.coe_toPerm, isClosed_compl_iff,
    exists_exists_and_eq_and]
  refine forall_congr' fun _ => Iff.trans ?_ not_imp_not
  simp only [not_exists, not_and, ← compl_iInter₂, ← sInter_eq_biInter,
    subset_compl_iff_disjoint_right, not_disjoint_iff_nonempty_inter]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

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

Tactic:
by
  intro s hs
  rw [← compl_compl s, compl_mem_codiscrete_iff]
  exact ⟨hs.isClosed, hs.isDiscrete⟩

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a b : α
H : a ⋖ b
⊢ 𝓝[≤] b = pure b

Tactic:
rw [← Iio_insert, nhdsWithin_insert, H.nhdsLT, sup_bot_eq]

Goal state after:
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: α : Type u_2
g : Set (Set α)
s✝ s : Set α
hs : s ∈ g
⊢ {s} ⊆ g ∧ {s}.Countable ∧ ⋂₀ {s} ⊆ s

Tactic:
simp [hs]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
⊢ ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i

Tactic:
intro _ _ hst ⟨r, ⟨hrcountable, hsub⟩⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
s✝ t✝ : Set X
hst : s✝ ⊆ t✝
r : Set ι
hrcountable : r.Countable
hsub : t✝ ⊆ ⋃ i ∈ r, U i
⊢ ∃ r, r.Countable ∧ s✝ ⊆ ⋃ i ∈ r, U i
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
⊢ Disjoint (Subtype.val ⁻¹' closure[inst✝] s) (Subtype.val ⁻¹' closure[inst✝] t)

Tactic:
rw [disjoint_left]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
⊢ ∀ ⦃a : { x // x ∈ e }⦄, a ∈ Subtype.val ⁻¹' closure[inst✝] s → a ∉ Subtype.val ⁻¹' closure[inst✝] t
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
hst : Disjoint (Subtype.val ⁻¹' closure[inst✝] s) (Subtype.val ⁻¹' closure[inst✝] t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
obtain ⟨U, V, hU, hV, hsU, htV, hUV⟩ := normal_separation
    (isClosed_closure.preimage continuous_subtype_val)
    (isClosed_closure.preimage continuous_subtype_val) hst

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
hst : Disjoint (Subtype.val ⁻¹' closure[inst✝] s) (Subtype.val ⁻¹' closure[inst✝] t)
U V : Set { x // x ∈ e }
hU : IsOpen[instTopologicalSpaceSubtype] U
hV : IsOpen[instTopologicalSpaceSubtype] V
hsU : Subtype.val ⁻¹' closure[inst✝] s ⊆ U
htV : Subtype.val ⁻¹' closure[inst✝] t ⊆ V
hUV : Disjoint U V
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
g : β → γ
di : IsDenseInducing i
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
⊢ ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s

Tactic:
refine eventually_comap.2 ((hg.eventually hs).mono ?_)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
g : β → γ
di : IsDenseInducing i
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
⊢ ∀ (x : β), s (g x) → ∀ (a : α), i a = x → g (i a) ∈ s
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
hf' : ∀ (y : β), IsConnected (f ⁻¹' {y})
⊢ Bijective ⋯.connectedComponentsMap

Tactic:
by
  refine ⟨fun x y h ↦ ?_, Continuous.connectedComponentsMap_surjective _ fun y ↦ (hf' y).nonempty⟩
  obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe x
  obtain ⟨y, rfl⟩ := ConnectedComponents.surjective_coe y
  simp_all [← hf.preimage_connectedComponent hf']

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsOpen[instTopologicalSpaceProd] s
t : Set α
⊢ IsOpen[inst✝] (⋃ i ∈ t, {x | (i, x) ∈ s})

Tactic:
exact isOpen_biUnion fun _ _ => hs.preimage <| .prodMk_right _

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x y : α
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis (fun s ↦ s ∈ 𝓤 α ∧ SetRel.IsSymm s) fun s ↦ ball x s ×ˢ ball y s

Tactic:
apply (hasBasis_nhds x).prod_same_index (hasBasis_nhds y)

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x y : α
⊢ ∀ {i j : SetRel α α},
    i ∈ 𝓤 α ∧ i.IsSymm → j ∈ 𝓤 α ∧ j.IsSymm → ∃ k, (k ∈ 𝓤 α ∧ k.IsSymm) ∧ ball x k ⊆ ball x i ∧ ball y k ⊆ ball y j
Module: Mathlib.Topology.UniformSpace.Defs

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

Tactic:
rintro ⟨V, V_in, V_sub⟩
    use SetRel.symmetrize V, symmetrize_mem_uniformity V_in, inferInstance
    exact Subset.trans (ball_mono SetRel.symmetrize_subset_self x) V_sub

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

Goal state before:
pp: case h
α : Type ua
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ ⋂ (_ : ?i ∈ {V | V ∈ 𝓤 α ∧ SetRel.IsSymm V}), ?i ○ w ○ ?i ⊆ w ○ w ○ w

pp: case i
α : Type ua
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ Set (α × α)

Tactic:
apply iInter_subset

Goal state after:
case h
α : Type ua
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ w ∈ {V | V ∈ 𝓤 α ∧ SetRel.IsSymm V}
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ (∀ x ∈ Iic (𝓟 s), Cauchy x → ∃ x_1 ∈ m '' s, map m x ≤ 𝓝 x_1) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x

Tactic:
exists_mem_image,

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ (∀ x ∈ Iic (𝓟 s), Cauchy x → ∃ x_1 ∈ s, map m x ≤ 𝓝 (m x_1)) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
ι' : Sort u_2
ι : Sort u_3
p : ι' → Prop
V : ι' → Set (α × α)
U : ι → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hopen : ∀ (j : ι), IsOpen[inst✝.toTopologicalSpace] (U j)
hcover : K ⊆ ⋃ j, U j
⊢ ∃ i, p i ∧ ∀ x ∈ K, ∃ j, ball x (V i) ⊆ U j

Tactic:
by
  refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma hK hopen hcover)
  exact fun s t hst ht x hx ↦ (ht x hx).imp fun i hi ↦ Subset.trans (ball_mono hst _) hi

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
ι' : Sort u_2
p : ι' → Prop
V : ι' → Set (α × α)
U : α → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝[K] x
⊢ ∃ i, p i ∧ ∀ x ∈ K, ∃ y, ball x (V i) ∩ K ⊆ U y

Tactic:
refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhdsWithin hK hU)

Goal state after:
α : Type ua
inst✝ : UniformSpace α
K : Set α
ι' : Sort u_2
p : ι' → Prop
V : ι' → Set (α × α)
U : α → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝[K] x
⊢ ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ y, ball x t ∩ K ⊆ U y) → ∀ x ∈ K, ∃ y, ball x s ∩ K ⊆ U y
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst✝.toTopologicalSpace] B
h : Disjoint A B
this : Bᶜ ∈ 𝓝ˢ A
⊢ ∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)

Tactic:
rw [(hA.nhdsSet_basis_uniformity (Filter.basis_sets _)).mem_iff] at this

Goal state after:
α : Type ua
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst✝.toTopologicalSpace] B
h : Disjoint A B
this : ∃ i ∈ 𝓤 α, ⋃ x ∈ A, ball x (id i) ⊆ Bᶜ
⊢ ∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : HasCompactMulSupport f
hf₂ : HasCompactMulSupport f₂
hm : m 1 1 = 1
⊢ HasCompactMulSupport fun x ↦ m (f x) (f₂ x)

Tactic:
rw [hasCompactMulSupport_iff_eventuallyEq] at hf hf₂ ⊢

Goal state after:
α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
⊢ (fun x ↦ m (f x) (f₂ x)) =ᶠ[coclosedCompact α] 1