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

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
⊢ 𝓝[≠] x ≤ 𝓝[≠] x

Tactic:
exact Eq.le rfl

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s : Set X
hxy : x ≠ y
⊢ 𝓝[insert y s] x = 𝓝[s] x

Tactic:
refine le_antisymm (Filter.le_def.2 fun t ht => ?_) (nhdsWithin_mono x <| subset_insert y s)

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
⊢ t ∈ 𝓝[insert y s] x
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst✝¹] K)
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Tactic:
have : SeparatedNhds (closure K \ U) (closure K \ V) := by
    apply SeparatedNhds.of_isCompact_isCompact_isClosed (hK'.diff hU) (hK'.diff hV)
      (isClosed_closure.sdiff hV)
    rw [disjoint_iff_inter_eq_empty, sdiff_inter_sdiff, sdiff_eq_empty]
    exact hK.closure_subset_of_isOpen (hU.union hV) h2K

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst✝¹] K)
this : SeparatedNhds (closure[inst✝¹] K \ U) (closure[inst✝¹] K \ V)
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: α : Type u_1
s : Set α
t : Set Bool
⊢ s.boolIndicator ⁻¹' t = univ ∨ s.boolIndicator ⁻¹' t = s ∨ s.boolIndicator ⁻¹' t = sᶜ ∨ s.boolIndicator ⁻¹' t = ∅

Tactic:
simp only [preimage_boolIndicator_eq_union]
  split_ifs <;> simp [s.union_compl_self]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
t : OrderClosedTopology α
inst✝ : Preorder β
⊢ IsClosed[Pi.topologicalSpace] {f | Monotone f}

Tactic:
simp_rw [← monotoneOn_univ]
  exact isClosed_monotoneOn

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
⊢ LocallyConnectedSpace β

Tactic:
refine locallyConnectedSpace_iff_connectedComponentIn_open.2 fun F hF y _ ↦ ?_
  rw [← hf.isOpen_preimage, hf.continuous.continuousOn.preimage_connectedComponentIn]
  exact isOpen_biUnion fun x _ ↦ (hF.preimage hf.continuous).connectedComponentIn

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

Goal state before:
pp: case refine_1.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t

Tactic:
have h : s ⊆ range Sum.inr :=
        hs.isPreconnected.subset_isClopen isClopen_range_inr ⟨.inr x, hx, x, rfl⟩

Goal state after:
case refine_1.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : i ≠ j
⊢ False

Tactic:
replace h_ne : s i ∩ s j = ∅ := by
    simpa only [← bot_eq_empty, eq_bot_iff, ← inf_eq_inter, ← disjoint_iff_inf_le] using h_disj h_ne

Goal state after:
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
⊢ False
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr.inl
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u
x : α
hxs : x ∈ s
hxv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨x, hxs, ⟨h hxs, hxv⟩⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure[inst✝] s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst✝] s,
      ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s, ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x,
      ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x].TFAE

Tactic:
by
  tfae_have 1 ↔ 5 := by
    rw [regularSpace_iff, (@compl_surjective (Set X) _).forall, forall_comm]
    simp only [isClosed_compl_iff, mem_compl_iff, Classical.not_not, @and_comm (_ ∈ _),
      (nhds_basis_opens _).lift'_closure.le_basis_iff (nhds_basis_opens _), and_imp,
      (nhds_basis_opens _).disjoint_iff_right, ← subset_interior_iff_mem_nhdsSet,
      interior_compl, compl_subset_compl]
  tfae_have 5 → 6 := fun h a => (h a).antisymm (𝓝 _).le_lift'_closure
  tfae_have 6 → 4
  | H, a, s, hs => by
    rw [← H] at hs
    rcases (𝓝 a).basis_sets.lift'_closure.mem_iff.mp hs with ⟨U, hU, hUs⟩
    exact ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, hUs⟩
  tfae_have 4 → 2
  | H, s, a, ha => by
    have ha' : sᶜ ∈ 𝓝 a := by rwa [← mem_interior_iff_mem_nhds, interior_compl]
    rcases H _ _ ha' with ⟨U, hU, hUc, hUs⟩
    refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ hU
    rwa [← subset_interior_iff_mem_nhdsSet, hUc.isOpen_compl.interior_eq, subset_compl_comm]
  tfae_have 2 → 3 := by
    refine fun H a s => ⟨fun hd has => mem_closure_iff_nhds_ne_bot.mp has ?_, H s a⟩
    exact (hd.symm.mono_right <| @principal_le_nhdsSet _ _ s).eq_bot
  tfae_have 3 → 1 := fun H => ⟨fun hs ha => (H _ _).mpr <| hs.closure_eq.symm ▸ ha⟩
  tfae_finish

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

Goal state before:
pp: case mpr.inl
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u
x : α
hxs : x ∈ s
hxv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨x, hxs, ⟨h hxs, hxv⟩⟩

Goal state after:
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)
⊢ IsPreconnected (f ⁻¹' t)

Tactic:
isPreconnected_iff_subset_of_fully_disjoint_closed hT

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 α), IsClosed[inst✝¹] u → IsClosed[inst✝¹] v → f ⁻¹' t ⊆ u ∪ v → Disjoint u v → f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen[inst✝] U
⊢ U ⊆ closure[inst✝] (i '' s)

Tactic:
calc
    U ⊆ closure (i '' i ⁻¹' U) := di.dense.subset_closure_image_preimage_of_isOpen hUo
    _ ⊆ closure (i '' s) := closure_mono (image_mono sub)

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map g (comap g (𝓝 d)) ≤ 𝓝 d
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)

Tactic:
replace lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d) := map_mono lim1

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d)
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
Module: Mathlib.Topology.Compactness.Lindelof

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

Tactic:
by
  constructor
  · rintro ⟨h₁, h₂⟩
    obtain ⟨Y, f, rfl, hf⟩ := hb.open_eq_iUnion h₂
    choose f' hf' using hf
    have : b ∘ f' = f := funext hf'
    subst this
    obtain ⟨t, ht⟩ :=
      h₁.elim_countable_subcover (b ∘ f') (fun i => hb.isOpen (Set.mem_range_self _)) Subset.rfl
    refine ⟨t.image f', Countable.image (ht.1) f', le_antisymm ?_ ?_⟩
    · refine Set.Subset.trans ht.2 ?_
      simp only [Set.iUnion_subset_iff]
      intro i hi
      rw [← Set.iUnion_subtype (fun x : ι => x ∈ t.image f') fun i => b i.1]
      exact Set.subset_iUnion (fun i : t.image f' => b i) ⟨_, mem_image_of_mem _ hi⟩
    · apply Set.iUnion₂_subset
      rintro i hi
      obtain ⟨j, -, rfl⟩ := (mem_image ..).mp hi
      exact Set.subset_iUnion (b ∘ f') j
  · rintro ⟨s, hs, rfl⟩
    constructor
    · exact hs.isLindelof_biUnion fun i _ => hb' i
    · exact isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _)

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
hI : I.Countable
f : ι → Set X
hf : ∀ i ∈ I, IsOpen[inst✝] (f i)
⊢ ⋂ i ∈ I, f i = ⋂₀ (f '' I)

Tactic:
rw [sInter_image]

Goal state after:
Module: Mathlib.Data.Rel.Separated

Goal state before:
pp: X : Type u_1
R : SetRel X X
s : Set X
x : X
⊢ R.IsSeparated (insert x s) ↔
    R.IsSeparated s ∧ (∀ (y : X), y ∈ s → (x, y) ∈ R → x = y) ∧ ∀ (y : X), y ∈ s → (y, x) ∈ R → x = y

Tactic:
by
  simp [IsSeparated, pairwise_insert, not_imp_comm (a := _ = _), -not_and, forall_and]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
⊢ CauchySeq (u ∘ f) ↔ CauchySeq u

Tactic:
refine ⟨fun H => ?_, fun H => H.comp_injective hf.injective⟩

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
H : CauchySeq (u ∘ f)
⊢ CauchySeq u
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 univ) (𝓤 β) ↔ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
principal_univ,

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α ⊓ ⊤) (𝓤 β) ↔ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
x y : α
h : Inseparable x y
⊢ 𝓝 (y, y) ≤ 𝓤 α

Tactic:
apply nhds_le_uniformity

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

Goal state before:
pp: α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology α
⊢ 𝓤 α = ⊤

Tactic:
← Filter.ker_eq_univ

Goal state after:
α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology α
⊢ (𝓤 α).ker = univ
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_5
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
x : α
hx : pb x
y : γ
hy : g y = x
⊢ (pb ∘ g) y

Tactic:
simp only [hx, hy, Function.comp_apply]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : Nonempty ι
l : Filter ((i : ι) → α i)
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval i) l)

Tactic:
Pi.uniformSpace_eq,

Goal state after:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : Nonempty ι
l : Filter ((i : ι) → α i)
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval i) l)
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
l : Filter ((i : ι) → α i)
inst✝ : l.NeBot
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval i) l)

Tactic:
Pi.uniformSpace_eq,

Goal state after:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
l : Filter ((i : ι) → α i)
inst✝ : l.NeBot
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval i) l)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ UniformSpace.comap (Prod.fst ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α β) ⊓
      UniformSpace.comap (Prod.snd ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α γ) =
    uniformSpace α (β × γ)

Tactic:
have := (@UniformFun.inf_eq α (β × γ)
      (UniformSpace.comap Prod.fst ‹_›) (UniformSpace.comap Prod.snd ‹_›)).symm

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
this : uniformSpace α (β × γ) ⊓ uniformSpace α (β × γ) = uniformSpace α (β × γ)
⊢ UniformSpace.comap (Prod.fst ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α β) ⊓
      UniformSpace.comap (Prod.snd ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α γ) =
    uniformSpace α (β × γ)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : (𝓤 α).HasBasis p s
⊢ Tendsto (fun x ↦ ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β) (𝓤 (ι →ᵤ α)) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
(UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i → ∀ᶠ (x : β × β) in 𝓤 β, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
S : Set β
hα : (𝓤 α).HasBasis p s
⊢ Tendsto (fun x ↦ ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α)) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
(UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
S : Set β
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i →
        ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S),
          ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun x ↦ f '' x) 𝔗 𝔖
⊢ UniformContinuous fun g ↦ (ofFun 𝔗) ((toFun 𝔖) g ∘ f)

Tactic:
simp_rw [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun x ↦ f '' x) 𝔗 𝔖
⊢ ∀ i ∈ 𝔗,
    ∀ i_2 ∈ 𝓤 β,
      Tendsto (fun x ↦ ((ofFun 𝔗) ((toFun 𝔖) x.1 ∘ f), (ofFun 𝔗) ((toFun 𝔖) x.2 ∘ f)))
        (⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)) (𝓟 (UniformOnFun.gen 𝔗 i i_2))
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ UniformSpace.comap (fun f s ↦ UniformFun.ofFun ((↑s).domRestrict ((toFun 𝔖) f))) (Pi.uniformSpace fun s ↦ ↑↑s →ᵤ β) =
    uniformSpace α β 𝔖

Tactic:
Pi.uniformSpace_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ UniformSpace.comap (fun f s ↦ UniformFun.ofFun ((↑s).domRestrict ((toFun 𝔖) f)))
      (⨅ i, UniformSpace.comap (Function.eval i) (UniformFun.uniformSpace (↑↑i) β)) =
    uniformSpace α β 𝔖
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case mp
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ a • Icc b c → x ∈ Icc (a * b) (a * c)

pp: case mpr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ Icc (a * b) (a * c) → x ∈ a • Icc b c

Tactic:
· rintro ⟨y, ⟨hby, hyc⟩, rfl⟩
    dsimp
    constructor <;> gcongr

Goal state after:
case mpr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ Icc (a * b) (a * c) → x ∈ a • Icc b c
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a * x) ⁻¹' Ioc b c = Ioc (b / a) (c / a)

Tactic:
by
  simp [← Ioi_inter_Iic]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x * a) ⁻¹' Ioc b c = Ioc (b / a) (c / a)

Tactic:
by
  simp [← Ioi_inter_Iic]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
hom : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : UniformSpace G
inst✝³ : UniformSpace H
inst✝² : IsUniformGroup H
inst✝¹ : FunLike hom G H
inst✝ : MonoidHomClass hom G H
f : hom
hf : IsUniformInducing ⇑f
⊢ UniformContinuous fun p ↦ p.1 / p.2

Tactic:
simp_rw [hf.uniformContinuous_iff, Function.comp_def, map_div]
    exact uniformContinuous_div.comp (hf.uniformContinuous.prodMap hf.uniformContinuous)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
hg : Continuous[inst✝², inst✝¹] g
hgf :
  Continuous[inst✝³, inst✝¹] (g ∘ f) ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄, Tendsto (g ∘ f) (↑𝒰) (𝓝 y) → ∃ x, (g ∘ f) x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, ↑𝒰 ≤ 𝓝 x

Tactic:
rcases hgf.2 ((hg.tendsto y).comp h) with ⟨x, -, hx⟩

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
hg : Continuous[inst✝², inst✝¹] g
hgf :
  Continuous[inst✝³, inst✝¹] (g ∘ f) ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄, Tendsto (g ∘ f) (↑𝒰) (𝓝 y) → ∃ x, (g ∘ f) x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰) (𝓝 y)
x : X
hx : ↑𝒰 ≤ 𝓝 x
⊢ ∃ x, ↑𝒰 ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
f : α → M
g : β → M
this✝² : TopologicalSpace α := ⊥
hf : Tendsto f (cocompact α) (𝓝 0)
this✝¹ : DiscreteTopology α
this✝ : TopologicalSpace β := ⊥
hg : Tendsto g (cocompact β) (𝓝 0)
this : DiscreteTopology β
⊢ Tendsto (fun i ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Tactic:
exact tendsto_mul_cocompact_nhds_zero
    continuous_of_discreteTopology continuous_of_discreteTopology hf hg

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

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
⊢ DiscreteTopology (G ⧸ N) ↔ IsOpen[inst✝²] ↑N

Tactic:
by
  rw [← QuotientGroup.preimage_mk_one, MulAction.IsPretransitive.discreteTopology_iff G (mk 1),
      isOpen_coinduced]
  rfl

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:
rw [← 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.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : (𝓝 1).IsCountablyGenerated
⊢ (comap (fun x ↦ x.2 / x.1) (𝓝 1)).IsCountablyGenerated

Tactic:
exact Filter.comap.isCountablyGenerated _ _

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

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
rw [← one_mul 1]

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 (1 * 1))
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ Ioi (x i₀) ∩ Iic m = Iic m ∩ (Ioi (x i₀) ∩ Iic (y i₀))

Tactic:
inter_left_comm,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ Ioi (x i₀) ∩ Iic m = Ioi (x i₀) ∩ (Iic m ∩ Iic (y i₀))