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

Goal state before:
pp: case refine_2.refine_1
ι : 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 : ι
⊢ ∃ t_1 ⊆ (fun a ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1

Tactic:
by_cases hi : i ∈ I
      · use t i
        simp_rw [if_pos hi]
        exact ⟨Subset.rfl, (h1 i) hi⟩
      · use univ
        simp_rw [if_neg hi]
        exact ⟨Subset.rfl, isOpen_univ, mem_univ _⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen[t] (s i)
hne : ∀ (i : ι), (s i).Nonempty
⊢ Countable ι

Tactic:
rcases exists_countable_dense α with ⟨u, u_countable, u_dense⟩
  choose f hfu hfs using fun i ↦ u_dense.exists_mem_open (ho i) (hne i)
  have f_inj : Injective f := fun i j hij ↦
    hd.eq <| not_disjoint_iff.2 ⟨f i, hfs i, hij.symm ▸ hfs j⟩
  have := u_countable.to_subtype
  exact (f_inj.codRestrict hfu).countable

Goal state after:
Module: Mathlib.Topology.Constructions

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

Tactic:
refine forall₂_congr fun a _ => ⟨?_, ?_⟩

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

case intro.refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
a : (a : ι) → A a
x✝ : a ∈ s
⊢ (∃ u, (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
⊢ a ∈ u → IsOpen[⨅ i, t i] u → ∃ v ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, a ∈ v ∧ v ⊆ u

Tactic:
ha

Goal state after:
case refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
⊢ IsOpen[⨅ i, t i] u → ∃ v ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, a ∈ v ∧ v ⊆ u
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
F : Filter α
u : α → X
⊢ (map u (comap u (𝓝 x) ⊓ F)).NeBot ↔ ∃ U, ↑U ≤ F ∧ Tendsto u (↑U) (𝓝 x)

Tactic:
map_neBot_iff,

Goal state after:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
F : Filter α
u : α → X
⊢ (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ U, ↑U ≤ F ∧ Tendsto u (↑U) (𝓝 x)
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst✝] (f i)
x : X
this : IsClosed[inst✝] (⋃ i, f ↑i)
⊢ IsOpen[inst✝] (⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ)

Tactic:
by
    rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst✝] (f i)
x : X
⊢ IsOpen[inst✝] (⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ)

Tactic:
suffices IsClosed (⋃ i : { i // x ∉ f i }, f i) by
    rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this

Goal state after:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst✝] (f i)
x : X
⊢ IsClosed[inst✝] (⋃ i, f ↑i)
Module: Mathlib.Topology.Irreducible

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

Tactic:
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: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
⊢ IsOpen[inst✝] a → IsOpen[inst✝] b → (S ∩ a).Nonempty → (S ∩ b).Nonempty → (S ∩ (a ∩ b)).Nonempty

Tactic:
ha

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
⊢ IsOpen[inst✝] b → (S ∩ a).Nonempty → (S ∩ b).Nonempty → (S ∩ (a ∩ b)).Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
Z : Set X
hZ : Z ∈ irreducibleComponents X
S : Set (Set X)
hS : S.Finite
hSα : S ⊆ irreducibleComponents X
hZS : Z ⊆ ⋃₀ S
⊢ Z ∈ S

Tactic:
obtain ⟨W, hWS, hZW⟩ := isIrreducible_iff_sUnion_isClosed.mp hZ.1 hS.toFinset
    (fun W hW ↦ isClosed_of_mem_irreducibleComponents W (hSα (hS.mem_toFinset.mp hW)))
    (hS.coe_toFinset.symm ▸ hZS)

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
Z : Set X
hZ : Z ∈ irreducibleComponents X
S : Set (Set X)
hS : S.Finite
hSα : S ⊆ irreducibleComponents X
hZS : Z ⊆ ⋃₀ S
W : Set X
hWS : W ∈ hS.toFinset
hZW : Z ⊆ W
⊢ Z ∈ S
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
⊢ (a ∈ {x}ᶜ → a ∉ U \ s) → a ∈ (U \ s)ᶜ

Tactic:
ha

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : a ∈ {x}ᶜ → a ∉ U \ s
⊢ a ∈ (U \ s)ᶜ
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : ι → Prop
t : ι → Set X
s : Set X
hs : IsDiscrete s
x : X
hb : (𝓝 x).HasBasis p t
hx : x ∈ s
i : ι
hi : p i
hix : t i ∩ s ⊆ {x}
⊢ ∃ i, p i ∧ t i ∩ s = {x}

Tactic:
exact ⟨i, hi, hix.antisymm <| singleton_subset_iff.2 ⟨mem_of_mem_nhds <| hb.mem_of_mem hi, hx⟩⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
⊢ IsPreconnected (⋃ n ∈ t, s n)

Tactic:
by
  have h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t := fun hi hj hk =>
    ht.out hi hj (Ico_subset_Icc_self hk)
  have h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t := fun hi hj hk =>
    ht.out hi hj ⟨hk.1.trans <| le_succ _, succ_le_of_lt hk.2⟩
  have h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty :=
    fun hi hj hk => K _ (h1 hi hj hk) (h2 hi hj hk)
  refine IsPreconnected.biUnion_of_reflTransGen H fun i hi j hj => ?_
  exact reflTransGen_of_succ _ (fun k hk => ⟨h3 hi hj hk, h1 hi hj hk⟩) fun k hk =>
      ⟨by rw [inter_comm]; exact h3 hj hi hk, h2 hj hi hk⟩

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
P : α → α → Prop
inst✝ : Std.Symm P
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : IsTrans α P
x y z a : α
⊢ P z a → P z a ∧ P a z

Tactic:
ha

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
P : α → α → Prop
inst✝ : Std.Symm P
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : IsTrans α P
x y z a : α
ha : P z a
⊢ P z a ∧ P a z
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
z : α
hz : z ∈ s
a : α
⊢ P z a → a ∈ s → P z a ∧ P a z

Tactic:
ha

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
z : α
hz : z ∈ s
a : α
ha : P z a
⊢ a ∈ s → P z a ∧ P a z
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
⊢ IsPreconnected (Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s)

Tactic:
· exact (ht.image _ (by fun_prop)).union (a₁, b₂) ⟨b₂, hb₂, rfl⟩
      ⟨a₁, ha₁, rfl⟩ (hs.image _ (Continuous.prodMk_left _).continuousOn)

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

Goal state before:
pp: 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

Tactic:
rintro i hi

Goal state after:
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 : ι
hi : i ∈ f' '' t
⊢ b i ⊆ ⋃ i, (b ∘ f') i
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case refine_3
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 : Set X
hU : IsOpen[inst✝] U
hsU : closure[inst✝] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst✝] V
htV : closure[inst✝] t ∩ e ⊆ V ∩ e
hUV : ∀ ⦃a : { x // x ∈ e }⦄, a ∈ Subtype.val ⁻¹' U → a ∉ Subtype.val ⁻¹' V
⊢ ∀ ⦃a : X⦄, a ∈ U ∩ e → a ∉ V ∩ e

Tactic:
intro x hxU hxV

Goal state after:
case refine_3
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 : Set X
hU : IsOpen[inst✝] U
hsU : closure[inst✝] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst✝] V
htV : closure[inst✝] t ∩ e ⊆ V ∩ e
hUV : ∀ ⦃a : { x // x ∈ e }⦄, a ∈ Subtype.val ⁻¹' U → a ∉ Subtype.val ⁻¹' V
x : X
hxU : x ∈ U ∩ e
hxV : x ∈ V ∩ e
⊢ False
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
c : Continuous[inst✝¹, inst✝] i
dense : ∀ (x : β), x ∈ closure[inst✝] (range i)
H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (i a), ∀ (b : α), i b ∈ t → b ∈ s
a : α
⊢ comap i (𝓝 (i a)) ≤ 𝓝 a

Tactic:
by simpa [Filter.le_def] using! H a

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝¹] (U i)
this : IsLindelof (⋃ i, U i)
⊢ ∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i

Tactic:
rcases this.elim_countable_subcover U h (Eq.subset rfl) with ⟨t, ⟨htc, htu⟩⟩

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝¹] (U i)
this : IsLindelof (⋃ i, U i)
t : Set ι
htc : t.Countable
htu : ⋃ i, U i ⊆ ⋃ i ∈ t, U i
⊢ ∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
⊢ IsClosed[inst✝²] a → IsClosed[inst✝²] b → ⋂ s, ↑s ⊆ a ∪ b → Disjoint a b → ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b

Tactic:
ha

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
⊢ IsClosed[inst✝²] b → ⋂ s, ↑s ⊆ a ∪ b → Disjoint a b → ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
⊢ (map f l).NeBot ∧ map f l ×ˢ map f l ≤ 𝓤 α ↔ l.NeBot ∧ Tendsto (fun p ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)

Tactic:
map_neBot_iff,

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
⊢ l.NeBot ∧ map f l ×ˢ map f l ≤ 𝓤 α ↔ l.NeBot ∧ Tendsto (fun p ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
p : β × β
⊢ p ∈ V ○ M ○ W ↔ (ball p.1 V ×ˢ ball p.2 W ∩ M).Nonempty

Tactic:
by
  obtain ⟨x, y⟩ := p
  constructor
  · rintro ⟨z, ⟨w, hpw, hwz⟩, hzy⟩
    exact ⟨(w, z), ⟨hpw, by rwa [mem_ball_symmetry]⟩, hwz⟩
  · rintro ⟨⟨w, z⟩, ⟨w_in, z_in⟩, hwz⟩
    rw [mem_ball_symmetry] at z_in
    exact ⟨z, ⟨w, w_in, hwz⟩, z_in⟩

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

Goal state before:
pp: case h
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
⊢ a ≥ N + k → ∀ l ≥ N + k, (u a, u l) ∈ V

Tactic:
ha

Goal state after:
case h
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
⊢ ∀ l ≥ N + k, (u a, u l) ∈ V
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
⊢ comap (fun p ↦ (MulOpposite.op p.1, MulOpposite.op p.2)) (𝓤 αᵐᵒᵖ) = 𝓤 α

Tactic:
simpa [uniformity_mulOpposite, comap_comap, (· ∘ ·)] using! comap_id

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
⊢ a ∈ 𝓤 α → ∃ t, t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ a}

Tactic:
ha

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
⊢ ∃ t, t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ a}
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
x : (ι × ι') × ι × ι'
hx :
  (∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧
    ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w
a : α
b : α'
⊢ a ∈ s → b ∈ s' → ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u

Tactic:
ha

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
x : (ι × ι') × ι × ι'
hx :
  (∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧
    ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w
a : α
b : α'
ha : a ∈ s
⊢ b ∈ s' → ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : IsUniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
a : α
⊢ Tendsto f (comap e (𝓝 a)) (𝓝 (⋯.extend f a))

Tactic:
by
  simpa only [IsDenseInducing.extend] using
    tendsto_nhds_limUnder (uniformly_extend_exists h_e ‹_› h_f _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s'
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s'] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
exact ⟨t, nhdsWithin_mono x h' ht, H.mono fun n => id⟩

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
⊢ EquicontinuousOn F S ↔ ∀ (k : κ), EquicontinuousOn F S

Tactic:
by
  simp_rw [EquicontinuousOn, equicontinuousWithinAt_iInf_rng, @forall_comm _ κ]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
a : α
b : β
⊢ map₂ m (pure a) (pure b) = pure (m a b)

Tactic:
by rw [map₂_pure_right, map_pure]

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
⊢ f * ⊤ = ⊤

Tactic:
refine top_le_iff.1 fun s => ?_
  simp only [mem_mul, mem_top, exists_eq_left]
  rintro ⟨t, ht, hs⟩
  rwa [mul_univ_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
⊢ (Ioo 0 a)⁻¹ = Ioi a⁻¹

Tactic:
by
  ext x
  exact ⟨fun h ↦ inv_lt_of_inv_lt₀ (inv_pos.1 h.1) h.2,
         fun h ↦ ⟨inv_pos.2 <| (inv_pos.2 ha).trans h, inv_lt_of_inv_lt₀ ha h⟩⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
⊢ 0 • g ≤ 0

Tactic:
by
  refine fun s hs => mem_smul_filter.2 ?_
  convert! @univ_mem _ g
  refine eq_univ_iff_forall.2 fun a => ?_
  rwa [mem_preimage, zero_smul]

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

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, (map f (comap f (𝓝 y) ⊓ ℱ)).NeBot → ∃ x, f x = y ∧ (𝓝 x ⊓ ℱ).NeBot

Tactic:
map_neBot_iff,

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, (comap f (𝓝 y) ⊓ ℱ).NeBot → ∃ x, f x = y ∧ (𝓝 x ⊓ ℱ).NeBot
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
h'l : l ≤ (𝓝 0).coprod (𝓝 0)
⊢ Tendsto (fun x ↦ x.1 * x.2) l (𝓝 0)

Tactic:
simpa [inf_eq_right.mpr h'l] using tendsto_mul_coprod_nhds_zero_inf_of_disjoint_cocompact hl

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
p : ι → Prop
hc : ∀ (i : ι), p i → Continuous[inst✝³, inst✝²] (f i)
hf : LocallyFinite fun i ↦ mulSupport (f i)
⊢ Continuous[inst✝³, inst✝²] fun x ↦ ∏ᶠ (i : ι) (_ : p i), f i x

Tactic:
by
  simp only [← finprod_subtype_eq_finprod_cond]
  exact continuous_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)

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

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
⊢ RegularSpace G

Tactic:
by
  refine .of_exists_mem_nhds_isClosed_subset fun a s hs ↦ ?_
  have : Tendsto (fun p : G × G => p.1 * p.2) (𝓝 (a, 1)) (𝓝 a) :=
    continuous_mul.tendsto' _ _ (mul_one a)
  rcases mem_nhds_prod_iff.mp (this hs) with ⟨U, hU, V, hV, hUV⟩
  rw [← image_subset_iff, image_prod] at hUV
  refine ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, ?_⟩
  calc
    closure U ⊆ closure U * interior V := subset_mul_left _ (mem_interior_iff_mem_nhds.2 hV)
    _ = U * interior V := isOpen_interior.closure_mul U
    _ ⊆ U * V := mul_subset_mul_left interior_subset
    _ ⊆ s := hUV

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

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ g ∈ (fun x ↦ g * x) '' connectedComponent h

Tactic:
← connectedComponent_eq hh

Goal state after:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ g ∈ (fun x ↦ g * x) '' connectedComponent 1
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
⊢ ∀ {K L : Set G}, IsCompact K → IsCompact L → {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite

Tactic:
by
      intro K L hK hL
      have : Continuous fun p : G × G => (p.1⁻¹, p.2) := continuous_inv.prodMap continuous_id
      have H : Set.Finite _ :=
        hS ((hK.prod hL).image (continuous_mul.comp this)).compl_mem_cocompact
      simp only [preimage_compl, compl_compl, coe_subtype, comp_apply] at H
      apply Finite.of_preimage _ (equivOp S).surjective
      convert! H using 1
      ext x
      simp only [image_smul, mem_ofPred_eq, mem_preimage, mem_image, Prod.exists]
      exact Set.op_smul_inter_nonempty_iff

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

Goal state before:
pp: case refine_2
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
x : G
n : ℕ
hn : denseSeq G n ∈ (fun y ↦ x * y) ⁻¹' L
⊢ ∃ i, x ∈ (fun x ↦ x * denseSeq G i) ⁻¹' L

Tactic:
exact ⟨n, hn⟩

Goal state after: