mathlib-initiative/mathlib-tactics huggingface dataset:
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)
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)

Tactic:
rw [Topology.IsInducing.subtypeVal.isOpen_iff] at hU hV

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 : ∃ t, IsOpen[inst✝] t ∧ Subtype.val ⁻¹' t = U
hV : ∃ t, IsOpen[inst✝] t ∧ Subtype.val ⁻¹' t = 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.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))
hy : ¬ClusterPt y l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
simp only [clusterPt_iff_nonempty, not_forall, ← not_disjoint_iff_nonempty_inter, not_not] at hy

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))
hy : ∃ x, ∃ (_ : x ∈ 𝓝 y), ∃ x_1, ∃ (_ : x_1 ∈ l), Disjoint x x_1
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : LindelofSpace X
hf : Continuous[inst✝², inst✝¹] f
hsur : Function.Surjective f
⊢ IsLindelof (f '' univ)

Tactic:
exact IsLindelof.image (isLindelof_univ_iff.mpr ‹_›) hf

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
H : ∀ (s : Set X), IsOpen[inst✝] s → IsLindelof s
s : Set X
x✝ : s ⊆ univ
ι✝ : Type u
U : ι✝ → Set X
U_open : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hU : s ⊆ ⋃ i, U i
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i

Tactic:
obtain ⟨t, t_count, ht⟩ := H (⋃ i, U i) (isOpen_iUnion U_open)
    |>.elim_countable_subcover U U_open subset_rfl

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
H : ∀ (s : Set X), IsOpen[inst✝] s → IsLindelof s
s : Set X
x✝ : s ⊆ univ
ι✝ : Type u
U : ι✝ → Set X
U_open : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hU : s ⊆ ⋃ i, U i
t : Set ι✝
t_count : t.Countable
ht : ⋃ i, U i ⊆ ⋃ i ∈ t, U i
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∅ᶜ ∈ residual X

Tactic:
compl_empty

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ univ ∈ residual X
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
⊢ ⇑h '' connectedComponentIn s x = connectedComponentIn (⇑h '' s) (h x)

Tactic:
refine (h.continuous.continuousOn.image_connectedComponentIn_subset hx).antisymm ?_

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
⊢ connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: case neg
X : Type u_1
Y✝ : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y✝
inst✝⁵ : TopologicalSpace W
inst✝⁴ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
ι : Type u_7
inst✝¹ : DecidableEq ι
i : ι
Y : ι → Type u_8
inst✝ : (j : ι) → TopologicalSpace (Y j)
j : ι
h : ¬j = i
⊢ Continuous[instTopologicalSpaceProd, inst✝ j] fun a ↦ a.2 ⟨j, h⟩

Tactic:
exact (continuous_apply _).comp continuous_snd

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun x ↦ (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun x ↦ (f₂ x, f₃ x)) l (𝓤 α)
s : Set (α × α)
hs : s ∈ 𝓤 α
x : β
hx₁₂ : x ∈ (fun x ↦ (f₁ x, f₂ x)) ⁻¹' s
⊢ x ∈ (fun x ↦ (f₂ x, f₃ x)) ⁻¹' s → x ∈ (fun x ↦ (f₁ x, f₃ x)) ⁻¹' (s ○ s)

Tactic:
hx₂₃

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun x ↦ (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun x ↦ (f₂ x, f₃ x)) l (𝓤 α)
s : Set (α × α)
hs : s ∈ 𝓤 α
x : β
hx₁₂ : x ∈ (fun x ↦ (f₁ x, f₂ x)) ⁻¹' s
hx₂₃ : x ∈ (fun x ↦ (f₂ x, f₃ x)) ⁻¹' s
⊢ x ∈ (fun x ↦ (f₁ x, f₃ x)) ⁻¹' (s ○ s)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
⊢ f ≤ 𝓝 x

Tactic:
by
  -- Consider a neighborhood `s` of `x`
  intro s hs
  -- Take an entourage twice smaller than `s`
  rcases comp_mem_uniformity_sets (mem_nhds_uniformity_iff_right.1 hs) with ⟨U, U_mem, hU⟩
  -- Take a set `t ∈ f`, `t × t ⊆ U`, and a point `y ∈ t` such that `(x, y) ∈ U`
  rcases adhs U U_mem with ⟨t, t_mem, ht, y, hxy, hy⟩
  apply mem_of_superset t_mem
  -- Given a point `z ∈ t`, we have `(x, y) ∈ U` and `(y, z) ∈ t × t ⊆ U`, hence `z ∈ s`
  exact fun z hz => hU (SetRel.prodMk_mem_comp hxy (ht <| mk_mem_prod hy hz)) rfl

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

Goal state before:
pp: α : Type ua
β : Type ub
f : α → β
U : SetRel β β
x x✝ : α
⊢ x✝ ∈ UniformSpace.ball x (Prod.map f f ⁻¹' U) ↔ x✝ ∈ f ⁻¹' UniformSpace.ball (f x) U

Tactic:
simp only [UniformSpace.ball, mem_preimage, Prod.map_apply]

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

Goal state before:
pp: α : Type u_2
x✝ : UniformSpace α
⊢ comap (Prod.map id id) (𝓤 α) = 𝓤 α

Tactic:
Prod.map_id,

Goal state after:
α : Type u_2
x✝ : UniformSpace α
⊢ comap id (𝓤 α) = 𝓤 α
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ 𝓤 (α × β) = map (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β)

Tactic:
rw [map_swap4_eq_comap, uniformity_prod_eq_comap_prod]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
x : α
⊢ Filter.comap mk (𝓝 (mk x)) = Filter.comap mk (Filter.comap (Prod.mk (mk x)) (map (Prod.map mk mk) (𝓤 α)))

Tactic:
by
    conv_lhs => rw [comap_mk_nhds_mk, nhds_eq_comap_uniformity, ← comap_map_mk_uniformity]
    simp only [Filter.comap_comap, Function.comp_def, Prod.map_apply]

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ comap (Prod.map _root_.id _root_.id) (𝓤 α) = 𝓤 α

Tactic:
Prod.map_id,

Goal state after:
α : Type u
inst✝ : UniformSpace α
⊢ comap _root_.id (𝓤 α) = 𝓤 α
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
hf : IsUniformInducing f
⊢ comap (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) = 𝓤 α

Tactic:
← hf.1,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
hf : IsUniformInducing f
⊢ comap (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) = comap (fun x ↦ (f x.1, f x.2)) (𝓤 β)
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 ∈ 𝓝 x
⊢ ∃ i, p i ∧ ∀ x ∈ K, ∃ y, ball x (V i) ⊆ U y

Tactic:
refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhds 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 ∈ 𝓝 x
⊢ ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ y, ball x t ⊆ U y) → ∀ x ∈ K, ∃ y, ball x s ⊆ U y
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Tactic:
have p2 : ∀ᶠ i in p, ∀ᶠ x in p', (F i x, L i) ∈ t := by
    filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝² : One α
inst✝¹ : TopologicalSpace X
Y : Type u_9
inst✝ : TopologicalSpace Y
g : Y → α
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ mulTSupport (g ∘ f) ⊆ f ⁻¹' mulTSupport g

Tactic:
by
  rw [mulTSupport, mulTSupport, mulSupport_comp_eq_preimage]
  exact hf.closure_preimage_subset _

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

Goal state before:
pp: ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
ht : ∃ t, T2Space X ∧ ∀ (i : ι), (u i).toTopologicalSpace ≤ t
⊢ CompleteSpace X

Tactic:
nontriviality X
  rcases ht with ⟨t, ht, hut⟩
  -- The diagonal map `(X, ⨅ i, u i) → ∀ i, (X, u i)` is a uniform embedding.
  have : @IsUniformInducing X (ι → X) (⨅ i, u i) (Pi.uniformSpace (U := u)) (const ι) := by
    simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf,
      Filter.comap_comap, comp_def, const, Prod.eta, comap_id']
  -- Hence, it suffices to show that its range, the diagonal, is closed in `Π i, (X, u i)`.
  simp_rw [@completeSpace_iff_isComplete_range _ _ (_) (_) _ this, range_const_eq_diagonal,
    ofPred_forall]
  -- The separation of `t` ensures that this is the case in `Π i, (X, t)`, hence the result
  -- since the topology associated to each `u i` is finer than `t`.
  have : Pi.topologicalSpace (t₂ := fun i ↦ (u i).toTopologicalSpace) ≤
         Pi.topologicalSpace (t₂ := fun _ ↦ t) :=
    iInf_mono fun i ↦ induced_mono <| hut i
  refine IsClosed.isComplete <| .mono ?_ this
  exact isClosed_iInter fun i ↦ isClosed_iInter fun j ↦
    isClosed_eq (continuous_apply _) (continuous_apply _)

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : IsUniformInducing u
⊢ UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x ↦ u ∘ x) ∘ F)

Tactic:
have := UniformFun.postcomp_isUniformInducing (α := ι) hu

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : IsUniformInducing u
this : IsUniformInducing (⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun)
⊢ UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x ↦ u ∘ x) ∘ F)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
S : Set β
u : α → γ
hu : IsUniformInducing u
⊢ UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((fun x ↦ u ∘ x) ∘ F) S

Tactic:
have := UniformFun.postcomp_isUniformInducing (α := ι) hu

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
S : Set β
u : α → γ
hu : IsUniformInducing u
this : IsUniformInducing (⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun)
⊢ UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((fun x ↦ u ∘ x) ∘ F) S
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
⊢ Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)

Tactic:
have := mulLeftMono_of_mulLeftStrictMono α
  have := mulRightMono_of_mulRightStrictMono α
  rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩
  exact ⟨mul_lt_mul_of_lt_of_le hya hzc, mul_lt_mul_of_le_of_lt hyb hzd⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
⊢ (fun x ↦ x / a) '' [[b, c]] = [[b / a, c / a]]

Tactic:
by
  simp only [div_eq_mul_inv, image_mul_const_uIcc]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.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 : C(X, Y)
hf : IsQuotientMap ⇑f
⊢ Continuous[inst✝¹, instTopologicalSpaceQuotient] (Setoid.quotientKerEquivOfSurjective ⇑f ⋯).invFun

Tactic:
by
    rw [hf.continuous_iff]
    convert! continuous_quotient_mk'
    ext
    simp only [Equiv.invFun_as_coe, Function.comp_apply,
      (Setoid.quotientKerEquivOfSurjective f hf.surjective).symm_apply_eq]
    rfl

Goal state after:
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
⊢ ∃ U ∈ 𝓝 x, ∀ (γ : Γ), γ • x ≠ x → Disjoint ((fun x ↦ γ • x) '' U) U

Tactic:
convert! exists_nhds_image_smul_eq_self Γ x using 4
  rw [← not_imp_not]
  simp [Set.not_disjoint_iff_nonempty_inter]

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

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

Tactic:
(hY : (Ultrafilter.map f 𝒰 : Filter Y) ≤ _)

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

Goal state before:
pp: case refine_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ ⦃s t : Set M⦄, s ⊆ t → (∃ V ∈ 𝓝 0, t * V ⊆ U) → ∃ V ∈ 𝓝 0, s * V ⊆ U

Tactic:
rintro s t hst ⟨V, hV, hV'⟩

Goal state after:
case refine_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
s t : Set M
hst : s ⊆ t
V : Set M
hV : V ∈ 𝓝 0
hV' : t * V ⊆ U
⊢ ∃ V ∈ 𝓝 0, s * V ⊆ U
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f✝ : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ i ∈ f :: l, Tendsto (f✝ i) x (𝓝 (a i))
⊢ Tendsto (fun b ↦ f✝ f b * (List.map (fun c ↦ f✝ c b) l).prod) x (𝓝 (a f * (List.map a l).prod))

Tactic:
exact
      (h f List.mem_cons_self).mul
        (tendsto_list_prod l fun c hc => h c (List.mem_cons_of_mem _ hc))

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

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : TopologicalSpace G
inst✝² : MulDistribMulAction H G
inst✝¹ : ContinuousConstSMul H G
𝒢 : Subgroup G
h : H
inst✝ : IsDiscrete ↑𝒢
⊢ IsDiscrete ↑(h • 𝒢)

Tactic:
refine IsDiscrete.image_of_isOpenMap ‹_› ?_ fun x y ↦ by simp

Goal state after:
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : TopologicalSpace G
inst✝² : MulDistribMulAction H G
inst✝¹ : ContinuousConstSMul H G
𝒢 : Subgroup G
h : H
inst✝ : IsDiscrete ↑𝒢
⊢ IsOpenMap ⇑((MulDistribMulAction.toMonoidEnd H G) h)
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 * h ∈ connectedComponent g

Tactic:
have hmul : g ∈ connectedComponent (g * h) := by
    apply Continuous.image_connectedComponent_subset (continuous_const_mul g)
    rw [← connectedComponent_eq hh]
    exact ⟨(1 : G), mem_connectedComponent, by simp only [mul_one]⟩

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
hmul : g ∈ connectedComponent (g * h)
⊢ g * h ∈ connectedComponent g
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
conj_φ : conj ∘ ⇑φ = dr
⊢ comap (fun gx ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1) = comap snd (𝓝 1)

Tactic:
have snd_φ : snd ∘ φ = dl := by
    ext; simp [φ, dl]

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
conj_φ : conj ∘ ⇑φ = dr
snd_φ : snd ∘ ⇑φ = dl
⊢ comap (fun gx ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1) = comap snd (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x ↦ True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
⊢ ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n

Tactic:
refine atTop_basis.eventually_iff.mpr ⟨max j k, True.intro, fun m hm => ?_⟩

Goal state after:
G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x ↦ True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
m : ℕ
hm : m ∈ Ici (max j k)
⊢ u m * u m ⊆ u n
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, s ⊆ t → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, s * V ⊆ U

Tactic:
rintro s t hst ⟨V, hV, hV'⟩

Goal state after:
case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
s t : Set G
hst : s ⊆ t
V : Set G
hV : V ∈ 𝓝 1
hV' : t * V ⊆ U
⊢ ∃ V ∈ 𝓝 1, s * V ⊆ U
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_2
u : UniformSpace G
inst✝¹ : Group G
inst✝ : IsUniformGroup G
⊢ 𝓤 G = 𝓤 G

Tactic:
uniformity_eq_comap_nhds_one' G,

Goal state after:
G : Type u_2
u : UniformSpace G
inst✝¹ : Group G
inst✝ : IsUniformGroup G
⊢ comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1) = 𝓤 G
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : ContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
⊢ Tendsto (fun n ↦ f n * g n) l (𝓝 (x * y)) ↔ Tendsto f l (𝓝 x)

Tactic:
refine ⟨fun hfg => ?_, fun hf => hf.mul hg⟩
  rw [← mul_div_cancel_right₀ x hy]
  refine Tendsto.congr' ?_ (hfg.div hg hy)
  exact (hg.eventually_ne hy).mono fun n hn => mul_div_cancel_right₀ _ hn

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : ContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
⊢ ContinuousAt (fun x ↦ h x (f x / g x)) a

Tactic:
change ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a

Goal state after:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : ContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
⊢ ContinuousAt (↿h ∘ fun x ↦ (x, f x / g x)) a
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : DiscreteTopology ↥H
hd : IsDiscrete ↑H
V : Set G
V_in : V ∈ 𝓝 1
VH : V ∩ ↑H = {1}
⊢ IsClosed[inst✝³] ↑H

Tactic:
have : (fun p : G × G => p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G := preimage_mem_comap V_in

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : DiscreteTopology ↥H
hd : IsDiscrete ↑H
V : Set G
V_in : V ∈ 𝓝 1
VH : V ∩ ↑H = {1}
this : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
⊢ IsClosed[inst✝³] ↑H
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ G ≃ᵤ Gᵐᵒᵖ

Tactic:
letI : UniformSpace G := IsTopologicalGroup.leftUniformSpace G
  letI : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.rightUniformSpace Gᵐᵒᵖ
  refine ⟨MulOpposite.opEquiv, ?_, ?_⟩
  · simp [uniformContinuous_iff_le_comap, ← comap_op_rightUniformSpace]
  · simp [uniformContinuous_iff_le_comap, ← comap_op_rightUniformSpace, ← UniformSpace.comap_comap]

Goal state after: