mathlib-initiative/mathlib-tactics huggingface dataset:
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
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
⊢ ∀ (S : Set (Set X)),
    S.Countable → (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i

Tactic:
intro S hS hsr

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
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
hsr : ∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
⊢ ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : Disjoint s (⋂ i, (U i)ᶜ)
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i

Tactic:
disjoint_iff

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Set ι✝
ht : t.Countable ∧ s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ t.Countable ∧ Disjoint s (⋂ i ∈ t, (U i)ᶜ)

Tactic:
disjoint_iff

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Set ι✝
ht : t.Countable ∧ s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ t.Countable ∧ s ⊓ ⋂ i ∈ t, (U i)ᶜ = ⊥
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : Disjoint u v
⊢ s ∩ ∅ = ∅

Tactic:
inter_empty

Goal state after:
case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : Disjoint u v
⊢ ∅ = ∅
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set X
hs : IsCompact s
⊢ closure[inst✝¹] s = nhdsKer s

Tactic:
apply subset_antisymm
  · rw [nhdsKer, ← hs.lift'_closure_nhdsSet]
    simp +contextual [Filter.lift', Filter.lift, closure_mono, subset_of_mem_nhdsSet]
  · intro y hy
    by_contra! hy'
    rw [← _root_.disjoint_nhdsSet_nhds, Filter.disjoint_iff] at hy'
    obtain ⟨t, hts, t', ht'y, H⟩ := hy'
    exact Set.disjoint_iff.mp H ⟨hy t hts, mem_of_mem_nhds ht'y⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
b : Bool
⊢ IsLindelof (bif b then s else t)

Tactic:
by cases b <;> assumption

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

Goal state before:
pp: case a
α : 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}
t' : β
ht' : t' ∈ t
⊢ f ⁻¹' {t'} ∩ ∅ = ∅

Tactic:
inter_empty

Goal state after:
case a
α : 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}
t' : β
ht' : t' ∈ t
⊢ ∅ = ∅
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case neg
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
rcases hKc.image hfc (le_principal_iff.2 this) with ⟨y, hy, hyl⟩

Goal state after:
case neg
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y✝ : Y
hf : Tendsto f (coLindelof X) (𝓝 y✝)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y✝ (range f))
s : Set Y
hsy : s ∈ 𝓝 y✝
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
y : Y
hy : y ∈ f '' K
hyl : ClusterPt y l
⊢ ∃ x ∈ insert y✝ (range f), ClusterPt x l
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝¹] (C i)
t : Set ι
| ⋂ i ∈ t, C i = ⋂ i, C i

Tactic:
rw [← compl_inj_iff]

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝¹] (C i)
t : Set ι
| (⋂ i ∈ t, C i)ᶜ = (⋂ i, C i)ᶜ
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝²] (C i)
k : ℕ → ι
| ⋂ n, C (k n) = ⋂ i, C i

Tactic:
rw [← compl_inj_iff]

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝²] (C i)
k : ℕ → ι
| (⋂ n, C (k n))ᶜ = (⋂ i, C i)ᶜ
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
⊢ t ∩ ∅ = ∅

Tactic:
inter_empty

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
⊢ ∅ = ∅
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x,
      ((∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsOpen[inst✝] x_1ᶜ ∧ Dense x_1ᶜ) ∧ (compl '' x).Countable) ∧ ⋂₀ (compl '' x) ⊆ sᶜ) ↔
    ∃ S, ((∀ t ∈ S, IsNowhereDense t) ∧ S.Countable) ∧ s ⊆ ⋃₀ S

Tactic:
← isClosed_isNowhereDense_iff_compl,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x,
      ((∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable) ∧
        ⋂₀ (compl '' x) ⊆ sᶜ) ↔
    ∃ S, ((∀ t ∈ S, IsNowhereDense t) ∧ S.Countable) ∧ s ⊆ ⋃₀ S
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : 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_decomp : t ⊆ T₁ ∪ T₂
⊢ f ⁻¹' t ∩ ∅ = ∅

Tactic:
inter_empty

Goal state after:
α : 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_decomp : t ⊆ T₁ ∪ T₂
⊢ ∅ = ∅
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u_2
i : TopologicalSpace α
u : UniformSpace α
h : i = u.toTopologicalSpace
x : α
⊢ 𝓝 x = comap (Prod.mk x) UniformSpace.uniformity

Tactic:
by rw [h, u.nhds_eq_comap_uniformity]

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun s ↦ g (Prod.swap ⁻¹' s)) ≤ f
⊢ (𝓤 α).lift (g ∘ image Prod.swap) ≤ f

Tactic:
image_swap_eq_preimage_swap

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun s ↦ g (Prod.swap ⁻¹' s)) ≤ f
⊢ (𝓤 α).lift (g ∘ preimage Prod.swap) ≤ f
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
a : α
hu : Tendsto u atTop (𝓝 a)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → b ∈ u ⁻¹' ball a (Prod.swap ⁻¹' V 0)
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφV : ∀ (n_1 : ℕ), ((u ∘ fun a ↦ a + n) (φ (n_1 + 1)), (u ∘ fun a ↦ a + n) (φ n_1)) ∈ V (n_1 + 1)
⊢ ∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)

Tactic:
exact ⟨fun k => φ k + n, φ_mono.add_const _, hn _ le_add_self, hφV⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen[instTopologicalSpaceProd] (t p a) ∧ p ∈ t p a
x✝ : α × α
a b : α
hp : (a, b) ∈ s
⊢ ∃ a_1 b_1, ∃ (i : (a_1, b_1) ∈ s), (a, b) ∈ t (a_1, b_1) i

Tactic:
exact ⟨a, b, hp, (ht (a, b) hp).right.right⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ interior s ∈ 𝓤 α

Tactic:
rw [uniformity_eq_uniformity_interior]; exact mem_lift' hs

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

Goal state before:
pp: α : Type ua
β : Type ub
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
ι' : Sort u_2
p : ι → Prop
s : ι → SetRel α α
ha : (𝓤 α).HasBasis p s
q : ι' → Prop
t : ι' → Set (β × β)
hb : (𝓤 β).HasBasis q t
f : α → β
S : Set α
⊢ (∀ (ib : ι'), q ib → ∃ ia, p ia ∧ ∀ (a b : α), (a, b) ∈ S ×ˢ S ∩ s ia → (f a, f b) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ (a b : α), a ∈ S → b ∈ S → (a, b) ∈ s j → (f a, f b) ∈ t i

Tactic:
mem_inter_iff,

Goal state after:
α : Type ua
β : Type ub
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
ι' : Sort u_2
p : ι → Prop
s : ι → SetRel α α
ha : (𝓤 α).HasBasis p s
q : ι' → Prop
t : ι' → Set (β × β)
hb : (𝓤 β).HasBasis q t
f : α → β
S : Set α
⊢ (∀ (ib : ι'), q ib → ∃ ia, p ia ∧ ∀ (a b : α), (a, b) ∈ S ×ˢ S ∧ (a, b) ∈ s ia → (f a, f b) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ (a b : α), a ∈ S → b ∈ S → (a, b) ∈ s j → (f a, f b) ∈ t i
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_2
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
g : ↑u → α
hgs : ∀ (x : ↑u), g x ∈ s
hgr : ∀ (x : ↑u), (g x, ↑x) ∈ r
this : Fintype ↑u
⊢ (range g).Finite

Tactic:
exact finite_range g

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ T0Space α ↔ (𝓤 α).ker = diagonal α

Tactic:
t0Space_iff_uniformity,

Goal state after:
α : Type u
inst✝ : UniformSpace α
⊢ (∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y) ↔ (𝓤 α).ker = diagonal α
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (lift' f)

Tactic:
rwa [lift', dif_pos hf, uniformContinuous_lift]

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 : Set α
p : Filter ι
x✝³ : α
x✝² : x✝³ ∈ s
x✝¹ : Set (β × β)
x✝ : x✝¹ ∈ 𝓤 β
⊢ (∃ t ∈ 𝓝[s] x✝³, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x✝¹) ↔
    x✝¹ ∈ map (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x✝³)

Tactic:
simp_rw [mem_map, mem_prod_iff_right, mem_preimage]

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

Goal state before:
pp: case hnhds
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
v : Set α
hv : v ∈ 𝓝[s] q
w : Set β
hw : w ∈ 𝓝[k] x
hvw : v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z | (f q x, z) ∈ u'}
p : α
hp : p ∈ v
y : β
hy : y ∈ w
A : (f q x, f p y) ∈ u'
B : (f q x, f q y) ∈ u'
⊢ (f p y, f q y) ∈ u

Tactic:
exact hu' <| SetRel.prodMk_mem_comp (u'_symm A) B

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set X
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p s
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
equicontinuousWithinAt_iff_continuousWithinAt,

Goal state after:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set X
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p s
⊢ ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hα : (𝓤 α).HasBasis p s
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k

Tactic:
equicontinuousWithinAt_iff_continuousWithinAt,

Goal state after:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hα : (𝓤 α).HasBasis p s
⊢ ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
equicontinuousWithinAt_iff_continuousWithinAt,

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀ ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ | ((fun x ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite ↑Γ₀
u v : ↑Γ₀ → Set T
hu : ∀ (γ : ↑Γ₀), u γ ∈ 𝓝 (↑γ • x)
hv : ∀ (γ : ↑Γ₀), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : ↑Γ₀), Disjoint (u γ) (v γ)
γ : Γ
z : T
hz : z ∈ V ∩ ⋂ γ, (fun x ↦ ↑γ • x) ⁻¹' u γ ∩ v γ
hγz : (fun x ↦ γ • x) z ∈ V ∩ ⋂ γ, (fun x ↦ ↑γ • x) ⁻¹' u γ ∩ v γ
h : ¬γ • x = x
⊢ False

Tactic:
mem_inter_iff,

Goal state after:
Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ | ((fun x ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite ↑Γ₀
u v : ↑Γ₀ → Set T
hu : ∀ (γ : ↑Γ₀), u γ ∈ 𝓝 (↑γ • x)
hv : ∀ (γ : ↑Γ₀), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : ↑Γ₀), Disjoint (u γ) (v γ)
γ : Γ
z : T
hz : z ∈ V ∧ z ∈ ⋂ γ, (fun x ↦ ↑γ • x) ⁻¹' u γ ∩ v γ
hγz : (fun x ↦ γ • x) z ∈ V ∧ (fun x ↦ γ • x) z ∈ ⋂ γ, (fun x ↦ ↑γ • x) ⁻¹' u γ ∩ v γ
h : ¬γ • x = x
⊢ False
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: α : Type u_6
β : Type u_7
F : Type u_8
inst✝⁴ : FunLike F α β
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : MulHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousMul β
f : F
⊢ ContinuousMul α

Tactic:
let tα := tβ.induced f
  refine ⟨continuous_induced_rng.2 ?_⟩
  simp only [Function.comp_def, map_mul]
  fun_prop

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

Goal state before:
pp: M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
x : M
hx : x ≠ 0
hxW : x ∈ W
⊢ 1 ∈ univ * W

Tactic:
simpa [hx] using Set.mul_mem_mul (Set.mem_univ x⁻¹) hxW

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ map (fun x ↦ c * x) (𝓝[>] a) = 𝓝[>] (c * a)

Tactic:
convert! (Homeomorph.mulLeft c).isEmbedding.map_nhdsWithin_eq .. using 2
  simp [mul_comm]

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ map (fun x ↦ c * x) (𝓝[<] a) = 𝓝[<] (c * a)

Tactic:
convert! (Homeomorph.mulLeft c).isEmbedding.map_nhdsWithin_eq .. using 2
  simp [mul_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x ↦ f x / r) l atTop ↔ Tendsto f l atTop

Tactic:
simpa only [div_eq_mul_inv] using tendsto_mul_const_atTop_of_pos (inv_pos.2 hr)

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this :
  (fun x ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) = (fun p ↦ p.1 * p.2⁻¹) ∘ fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)
⊢ Tendsto ((fun p ↦ p.1 * p.2⁻¹) ∘ fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
    (comap (fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) (𝓝 (1, 1))) (𝓝 1)

Tactic:
apply Tendsto.comp ?_ tendsto_comap

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this :
  (fun x ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) = (fun p ↦ p.1 * p.2⁻¹) ∘ fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)
⊢ Tendsto (fun p ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.GroupTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
⊢ Continuous[t, (coinduced f).toTopologicalSpace] f

Tactic:
continuous_sInf_rng

Goal state after:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
⊢ ∀ t_1 ∈ toTopologicalSpace '' {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}, Continuous[t, _] f
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: case refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
j : ι
⊢ update f i (x i) j = x j

Tactic:
obtain rfl | hij := eq_or_ne i j

Goal state after:
case refine_3.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
⊢ update f i (x i) i = x i

case refine_3.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
j : ι
hij : i ≠ j
⊢ update f i (x i) j = x j
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a ε : G
ε0 : ε > 1
x : G
hx : |x / a|ₘ < ε
⊢ |x⁻¹ / (fun a ↦ a⁻¹) a|ₘ < ε

Tactic:
rwa [inv_div_inv, mabs_div_comm]

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : y = ↑e x
⊢ ↑e.symm y = x

Tactic:
by rw [← e.left_inv hx, h]

Goal state after: