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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
h : inst✝ = generateFrom s
⊢ RegularSpace X ↔ ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
by
  refine ⟨fun _ t ht a ha => RegularSpace.regular
    (h ▸ isOpen_generateFrom_of_mem ht).isClosed_compl
    (Set.notMem_compl_iff.mpr ha), fun h' => ⟨fun {t a} ht ha => ?_⟩⟩
  obtain ⟨t, rfl⟩ := compl_involutive.surjective t
  rw [isClosed_compl_iff, h] at ht
  rw [Set.notMem_compl_iff] at ha
  induction ht with
  | basic t ht => exact h' t ht a ha
  | univ => simp
  | inter t₁ t₂ _ _ ih₁ ih₂ => grind [compl_inter, nhdsSet_union, disjoint_sup_left]
  | sUnion S _ ih =>
    obtain ⟨t, ht, ha⟩ := ha
    grw [compl_sUnion, sInter_image, iInter₂_subset t ht]
    exact ih t ht ha

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed[inst✝²] s
t_cl : IsClosed[inst✝²] t
st_dis : Disjoint s t
⊢ _root_.HasSeparatingCover s t

Tactic:
by
  -- `IsLindelof.indexed_countable_subcover` requires the space be Nonempty
  rcases isEmpty_or_nonempty X with empty_X | nonempty_X
  · rw [subset_eq_empty (t := s) (fun ⦃_⦄ _ ↦ trivial) (univ_eq_empty_iff.mpr empty_X)]
    exact hasSeparatingCovers_iff_separatedNhds.mpr (SeparatedNhds.empty_left t) |>.1
  -- This is almost `HasSeparatingCover`, but is not countable. We define for all `a : X` for use
  -- with `IsLindelof.indexed_countable_subcover` momentarily.
  have (a : X) : ∃ n : Set X, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n) := by
    wlog ains : a ∈ s
    · exact ⟨∅, isOpen_empty, SeparatedNhds.empty_left t |>.disjoint_closure_left, fun a ↦ ains a⟩
    obtain ⟨n, nna, ncl, nsubkc⟩ := ((regularSpace_TFAE X).out 0 3 :).mp ‹RegularSpace X› a tᶜ <|
      t_cl.compl_mem_nhds (disjoint_left.mp st_dis ains)
    exact
      ⟨interior n,
       isOpen_interior,
       disjoint_left.mpr fun ⦃_⦄ ain ↦
         nsubkc <| (IsClosed.closure_subset_iff ncl).mpr interior_subset ain,
       fun _ ↦ mem_interior_iff_mem_nhds.mpr nna⟩
  -- By Lindelöf, we may obtain a countable subcover witnessing `HasSeparatingCover`
  choose u u_open u_dis u_nhds using this
  obtain ⟨f, f_cov⟩ := s_cl.isLindelof.indexed_countable_subcover
    u u_open (fun a ainh ↦ mem_iUnion.mpr ⟨a, u_nhds a ainh⟩)
  exact ⟨u ∘ f, f_cov, fun n ↦ ⟨u_open (f n), u_dis (f n)⟩⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed[inst✝¹] s
ht : IsOpen[inst✝¹] t
hst : s ⊆ t
⊢ ∃ u, IsOpen[inst✝¹] u ∧ s ⊆ u ∧ closure[inst✝¹] u ⊆ t

Tactic:
have : Disjoint s tᶜ := Set.disjoint_left.mpr fun x hxs hxt => hxt (hst hxs)
  rcases normal_separation hs (isClosed_compl_iff.2 ht) this with
    ⟨s', t', hs', ht', hss', htt', hs't'⟩
  refine ⟨s', hs', hss', Subset.trans (closure_minimal ?_ (isClosed_compl_iff.2 ht'))
    (compl_subset_comm.1 htt')⟩
  exact fun x hxs hxt => hs't'.le_bot ⟨hxs, hxt⟩

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
⊢ ∀ V' ∈ 𝓝 (φ b), IsClosed[inst✝¹] V' → φ ⁻¹' V' ∈ 𝓝 b

Tactic:
intro V'

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
⊢ V' ∈ 𝓝 (φ b) → IsClosed[inst✝¹] V' → φ ⁻¹' V' ∈ 𝓝 b
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: case refine_1.inr
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen[inst✝] t
T_count : T.Countable
hT : T.Nonempty
⊢ ∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ ⋂₀ T = ⋂ n, f n

Tactic:
· obtain ⟨f, hf⟩ : ∃ (f : ℕ → Set X), T = range f := Countable.exists_eq_range T_count hT
      exact ⟨f, by simp_all, by simp [hf]⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ interior ∅ = ∅

Tactic:
interior_empty

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∅ = ∅
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case refine_1
α : Type u_3
inst✝ : TopologicalSpace α
x y : α
x✝¹ : x ≠ y
x✝ : ∃ u v, IsOpen[inst✝] u ∧ IsOpen[inst✝] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : Disjoint U V
⊢ (fun x1 x2 ↦ ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y

pp: case refine_2
α : Type u_3
inst✝ : TopologicalSpace α
x y : α
x✝¹ : x ≠ y
x✝ : (fun x1 x2 ↦ ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y
U : Set α
hU : IsClopen U
Ux : x ∈ U
Ucy : y ∈ Uᶜ
⊢ ∃ u v, IsOpen[inst✝] u ∧ IsOpen[inst✝] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
· exact ⟨U, isClopen_of_disjoint_cover_open f hU hV disj,
      Ux, fun Uy ↦ Set.disjoint_iff.mp disj ⟨Uy, Vy⟩⟩

Goal state after:
case refine_2
α : Type u_3
inst✝ : TopologicalSpace α
x y : α
x✝¹ : x ≠ y
x✝ : (fun x1 x2 ↦ ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y
U : Set α
hU : IsClopen U
Ux : x ∈ U
Ucy : y ∈ Uᶜ
⊢ ∃ u v, IsOpen[inst✝] u ∧ IsOpen[inst✝] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ map (⇑h) (cocompact X) = cocompact Y

Tactic:
by
  rw [← h.comap_cocompact, map_comap_of_surjective h.surjective]

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
n : ℕ
hn : 0 < n
⊢ ∃ U, (∀ (i : Fin n), IsClopen (U i)) ∧ (∀ (i : Fin n), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ

Tactic:
cases isEmpty_or_nonempty α
  · exact (not_finite (ConnectedComponents α)).elim
  obtain (_ | n) := n
  · simp at hn
  clear hn
  induction n with
  | zero => exact ⟨![.univ], by simp [isClopen_univ, Set.iUnion_fin_add_one_eq_iUnion_succ]⟩
  | succ n IH =>
    obtain ⟨U, h₁, h₂, h₃, h₄⟩ := IH
    obtain ⟨i, hi⟩ : ∃ i, ¬ IsConnected (U i) := by
      simp_rw [isConnected_iff_connectedSpace, ← not_forall]
      exact fun _ ↦ not_finite_iff_infinite.mpr ‹_› (.of_equiv _ (equivOfIsClopen h₁ h₃ h₄).symm)
    obtain ⟨U, rfl⟩ := (Equiv.piCongrLeft (fun _ ↦ Set α) (Equiv.swap 0 i)).symm.surjective U
    cases U using Fin.consCases with | cons s U =>
    simp only [Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero] at *
    obtain ⟨a, b, ha, hb, ha', hb', hab, rfl⟩ := (show IsClopen s by simpa using h₁ i)
      |>.not_isPreconnected_iff.mp (mt (⟨by simpa using h₂ i, ·⟩) hi)
    refine ⟨Fin.cons a (Fin.cons b U), ?_, ?_, ?_, ?_⟩
    · simpa [Fin.forall_iff_succ, *] using fun x ↦ h₁ (Equiv.swap 0 i (.succ x))
    · simpa [Fin.forall_iff_succ, *] using fun x ↦ h₂ (Equiv.swap 0 i (.succ x))
    · have h₃' (j : _) : Disjoint (U j) a ∧ Disjoint (U j) b := by
        simpa [onFun] using h₃ ((Equiv.swap 0 i).injective.ne (Fin.succ_ne_zero j))
      simpa [Pairwise, Fin.forall_iff_succ, onFun, hab, disjoint_comm (a := a),
        disjoint_comm (a := b), h₃'] using
        h₃.comp_of_injective ((Equiv.swap 0 i).injective.comp (Fin.succ_injective _))
    · simpa [← union_assoc, (Equiv.surjective _).iUnion_comp] using h₄

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

Goal state before:
pp: case hopen
α : Type u
u : Core α
x : α
⊢ ∀ (a : α),
    ∀ i ∈ u.uniformity,
      ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id i ∈ comap (Prod.mk x) u.uniformity

Tactic:
· intro a U hU
    rcases u.comp_mem_uniformity_sets hU with ⟨V, hV, hVU⟩
    filter_upwards [preimage_mem_comap hV] with b hb
    filter_upwards [preimage_mem_comap hV] with c hc
    exact hVU ⟨b, hb, hc⟩

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}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ cl_d ∈ 𝓝 (x, y)

Tactic:
rw [nhds_eq_uniformity_prod, mem_lift'_sets]
        · exact ⟨d, hd, fun ⟨a, b⟩ ⟨ha, hb⟩ => ⟨x, y, ha, hp, hb⟩⟩
        · exact fun _ _ h _ h' => ⟨h h'.1, h h'.2⟩

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

Goal state before:
pp: α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
x : α
h : (comap Prod.swap (𝓤 α)).HasBasis p fun i ↦ Prod.swap ⁻¹' s i
⊢ (𝓝 x).HasBasis p fun i ↦ {y | (y, x) ∈ s i}

Tactic:
rw [comap_swap_uniformity] at h

Goal state after:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
x : α
h : (𝓤 α).HasBasis p fun i ↦ Prod.swap ⁻¹' s i
⊢ (𝓝 x).HasBasis p fun i ↦ {y | (y, x) ∈ s i}
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
⊢ IsComplete (⋃ i, s i)

Tactic:
set S := ⋃ i, s i
  intro l hl hls
  rw [le_principal_iff] at hls
  obtain ⟨hl_ne, hl'⟩ := cauchy_iff.1 hl
  obtain ⟨t, htS, htl, htU⟩ : ∃ t, t ⊆ S ∧ t ∈ l ∧ t ×ˢ t ⊆ U := by
    rcases hl' U hU with ⟨t, htl, htU⟩
    refine ⟨t ∩ S, inter_subset_right, inter_mem htl hls, Subset.trans ?_ htU⟩
    gcongr <;> apply inter_subset_left
  obtain ⟨i, hi⟩ : ∃ i, t ⊆ s i := by
    rcases Filter.nonempty_of_mem htl with ⟨x, hx⟩
    rcases mem_iUnion.1 (htS hx) with ⟨i, hi⟩
    refine ⟨i, fun y hy => ?_⟩
    rcases mem_iUnion.1 (htS hy) with ⟨j, hj⟩
    rwa [hd i j x hi y hj (htU <| mk_mem_prod hx hy)]
  rcases hs i l hl (le_principal_iff.2 <| mem_of_superset htl hi) with ⟨x, hxs, hlx⟩
  exact ⟨x, mem_iUnion.2 ⟨i, hxs⟩, hlx⟩

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ b ∈ s, Tendsto (fun x ↦ (f x, f b)) (𝓝[s] b) (𝓤 α)

Tactic:
by
  simp [ContinuousOn, continuousWithinAt_iff'_left]

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
s : Set α
⊢ CompleteSpace ↑s ↔ IsComplete s

Tactic:
completeSpace_iff_isComplete_range isUniformEmbedding_subtype_val.isUniformInducing,

Goal state after:
α : Type u
inst✝ : UniformSpace α
s : Set α
⊢ IsComplete (range Subtype.val) ↔ IsComplete s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p ∈ U N

Tactic:
refine (setSeqAux hf U_mem N).2.2 ⟨?_, ?_⟩ <;> apply setSeq_sub_aux

Goal state after:
case refine_1
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.1 ∈ setSeq hf U_mem N

case refine_2
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.2 ∈ setSeq hf U_mem N
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : One α
inst✝ : TopologicalSpace X
f : X → α
⊢ mulTSupport f = ∅ ↔ f = 1

Tactic:
mulTSupport,

Goal state after:
X : Type u_1
α : Type u_2
inst✝¹ : One α
inst✝ : TopologicalSpace X
f : X → α
⊢ closure[inst✝] (mulSupport f) = ∅ ↔ f = 1
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : One α
inst✝ : TopologicalSpace X
⊢ (mulTSupport fun x ↦ 1) = ∅

Tactic:
mulTSupport,

Goal state after:
X : Type u_1
α : Type u_2
inst✝¹ : One α
inst✝ : TopologicalSpace X
⊢ closure[inst✝] (mulSupport fun x ↦ 1) = ∅
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : One α
inst✝ : TopologicalSpace X
⊢ mulTSupport 1 = ∅

Tactic:
mulTSupport,

Goal state after:
X : Type u_1
α : Type u_2
inst✝¹ : One α
inst✝ : TopologicalSpace X
⊢ closure[inst✝] (mulSupport 1) = ∅
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
α : Type u_2
β : Type u_4
inst✝² : One α
inst✝¹ : TopologicalSpace X
inst✝ : One β
g : α → β
hg : ∀ {x : α}, g x = 1 ↔ x = 1
f : X → α
⊢ mulTSupport (g ∘ f) = mulTSupport f

Tactic:
mulTSupport,

Goal state after:
X : Type u_1
α : Type u_2
β : Type u_4
inst✝² : One α
inst✝¹ : TopologicalSpace X
inst✝ : One β
g : α → β
hg : ∀ {x : α}, g x = 1 ↔ x = 1
f : X → α
⊢ closure[inst✝¹] (mulSupport (g ∘ f)) = mulTSupport f
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
α : Type u_2
β : Type u_4
inst✝² : One α
inst✝¹ : TopologicalSpace X
inst✝ : One β
g : α → β
hg : ∀ {x : α}, g x = 1 ↔ x = 1
f : X → α
⊢ closure[inst✝¹] (mulSupport (g ∘ f)) = mulTSupport f

Tactic:
mulTSupport,

Goal state after:
X : Type u_1
α : Type u_2
β : Type u_4
inst✝² : One α
inst✝¹ : TopologicalSpace X
inst✝ : One β
g : α → β
hg : ∀ {x : α}, g x = 1 ↔ x = 1
f : X → α
⊢ closure[inst✝¹] (mulSupport (g ∘ f)) = closure[inst✝¹] (mulSupport f)
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
α : Type u_2
β : Type u_4
inst✝² : One α
inst✝¹ : TopologicalSpace X
inst✝ : One β
g : α → β
hg : ∀ {x : α}, g x = 1 ↔ x = 1
f : X → α
⊢ mulTSupport (g ∘ f) = mulTSupport f

Tactic:
rw [mulTSupport, mulTSupport, mulSupport_comp_eq g hg]

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

Goal state before:
pp: X : Type u_1
α : Type u_2
β : Type u_4
inst✝² : One α
inst✝¹ : TopologicalSpace X
inst✝ : One β
g : α → β
f : X → α
hg : ∀ {x : α}, x ∈ range f → (g x = 1 ↔ x = 1)
⊢ mulTSupport (g ∘ f) = mulTSupport f

Tactic:
mulTSupport,

Goal state after:
X : Type u_1
α : Type u_2
β : Type u_4
inst✝² : One α
inst✝¹ : TopologicalSpace X
inst✝ : One β
g : α → β
f : X → α
hg : ∀ {x : α}, x ∈ range f → (g x = 1 ↔ x = 1)
⊢ closure[inst✝¹] (mulSupport (g ∘ f)) = mulTSupport f
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
α : Type u_2
β : Type u_4
inst✝² : One α
inst✝¹ : TopologicalSpace X
inst✝ : One β
g : α → β
f : X → α
hg : ∀ {x : α}, x ∈ range f → (g x = 1 ↔ x = 1)
⊢ closure[inst✝¹] (mulSupport (g ∘ f)) = mulTSupport f

Tactic:
mulTSupport,

Goal state after:
X : Type u_1
α : Type u_2
β : Type u_4
inst✝² : One α
inst✝¹ : TopologicalSpace X
inst✝ : One β
g : α → β
f : X → α
hg : ∀ {x : α}, x ∈ range f → (g x = 1 ↔ x = 1)
⊢ closure[inst✝¹] (mulSupport (g ∘ f)) = closure[inst✝¹] (mulSupport f)
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:
mulTSupport,

Goal state after:
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
⊢ closure[inst✝¹] (mulSupport (g ∘ f)) ⊆ f ⁻¹' mulTSupport g
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
⊢ closure[inst✝¹] (mulSupport (g ∘ f)) ⊆ f ⁻¹' mulTSupport g

Tactic:
mulTSupport,

Goal state after:
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
⊢ closure[inst✝¹] (mulSupport (g ∘ f)) ⊆ f ⁻¹' closure[inst✝] (mulSupport g)
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
⊢ mulTSupport (g ∘ ⇑f) = ⇑f ⁻¹' mulTSupport g

Tactic:
mulTSupport,

Goal state after:
X : Type u_1
α : Type u_2
inst✝² : One α
inst✝¹ : TopologicalSpace X
Y : Type u_9
inst✝ : TopologicalSpace Y
g : Y → α
f : X ≃ₜ Y
⊢ closure[inst✝¹] (mulSupport (g ∘ ⇑f)) = ⇑f ⁻¹' mulTSupport g
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
⊢ closure[inst✝¹] (mulSupport (g ∘ ⇑f)) = ⇑f ⁻¹' mulTSupport g

Tactic:
mulTSupport,

Goal state after:
X : Type u_1
α : Type u_2
inst✝² : One α
inst✝¹ : TopologicalSpace X
Y : Type u_9
inst✝ : TopologicalSpace Y
g : Y → α
f : X ≃ₜ Y
⊢ closure[inst✝¹] (mulSupport (g ∘ ⇑f)) = ⇑f ⁻¹' closure[inst✝] (mulSupport g)
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
x : α
⊢ x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1

Tactic:
mulTSupport,

Goal state after:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
x : α
⊢ x ∉ closure[inst✝¹] (mulSupport f) ↔ f =ᶠ[𝓝 x] 1
Module: Mathlib.Topology.UniformSpace.UniformApproximation

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : α → β
x : α
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∃ F, ContinuousWithinAt F univ x ∧ ∀ y ∈ t, (f y, F y) ∈ u

Tactic:
simpa only [exists_prop, nhdsWithin_univ, continuousWithinAt_univ] using L

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst✝¹.toTopologicalSpace, inst✝.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ SetRel.symmetrize {x | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r}
h₁ : b₁ ∉ s
h₂ : b₂ ∉ s
⊢ (f (b₁, b₂).1, f (b₁, b₂).2) ∈ SetRel.comp t t

Tactic:
exact ⟨x, SetRel.symm t <| hst h₁, hst h₂⟩

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : α' → β' → δ
n₁ : α → α'
n₂ : β → β'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ f) (map n₂ g)

Tactic:
map_map₂,

Goal state after:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : α' → β' → δ
n₁ : α → α'
n₂ : β → β'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)
⊢ map₂ (fun a b ↦ n (m a b)) f g = map₂ m' (map n₁ f) (map n₂ g)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ : Set α
p : Filter ι
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
e : γ ≃ α
he : 𝔗 ⊆ image ⇑e ⁻¹' 𝔖
he' : 𝔖 ⊆ preimage ⇑e ⁻¹' 𝔗
s : Set α
hs : s ∈ 𝔖
⊢ (fun x ↦ ⇑e.symm '' x) s ∈ 𝔗

Tactic:
by
      change e.symm '' s ∈ 𝔗
      rw [Equiv.image_symm_eq_preimage]
      exact he' hs

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
f : Filter γ
⊢ (a • b) • f = a • b • f

Tactic:
simp only [← Filter.map_smul, map_map, smul_assoc]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
f : Filter γ
⊢ map (fun b_1 ↦ a • b • b_1) f = map ((fun b ↦ a • b) ∘ fun b_1 ↦ b • b_1) f
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MulDistribMulAction α β
x✝ : α
⊢ {x✝ • 1} = 1

Tactic:
smul_one,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MulDistribMulAction α β
x✝ : α
⊢ {1} = 1
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
c : G
s : Set α
hs : Dense s
⊢ Dense (c • s)

Tactic:
dense_iff_closure_eq

Goal state after:
α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
c : G
s : Set α
hs : closure[inst✝³] s = univ
⊢ closure[inst✝³] (c • s) = univ
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
s : Set G
⊢ Dense (mk '' s) ↔ Dense (s * ↑N)

Tactic:
← dense_preimage_mk,

Goal state after:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
s : Set G
⊢ Dense (mk ⁻¹' mk '' s) ↔ Dense (s * ↑N)
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 : α
inst✝ : l.NeBot
h : Tendsto f l atTop
hrf : Tendsto (fun x ↦ r * f x) l atTop
hr : r ≤ 0
x : β
hx : 0 ≤ f x
hrx : 0 < r * f x
⊢ False

Tactic:
exact (mul_nonpos_of_nonpos_of_nonneg hr hx).not_gt hrx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : UniformSpace α
inst✝⁷ : Group α
inst✝⁶ : IsUniformGroup α
hom : Type u_3
inst✝⁵ : UniformSpace β
inst✝⁴ : DiscreteTopology β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
⊢ UniformContinuous ⇑f ↔ IsOpen[inst✝⁸.toTopologicalSpace] ↑(↑f).ker

Tactic:
by
  refine ⟨fun hf => ?_, fun hf => ?_⟩
  · apply (isOpen_discrete ({1} : Set β)).preimage hf.continuous
  · apply uniformContinuous_of_continuousAt_one
    rw [ContinuousAt, nhds_discrete β, map_one, tendsto_pure]
    exact hf.mem_nhds (map_one f)

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

Goal state before:
pp: case refine_1
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
⊢ ∀ (n : ℕ), IsCompact ((fun n ↦ (fun x ↦ x * denseSeq G n) ⁻¹' L) n)

Tactic:
intro n
    exact (Homeomorph.mulRight _).isCompact_preimage.mpr hLc

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ map (fun x_1 ↦ x * x_1) (map (fun x ↦ x * y) (map₂ (fun x1 x2 ↦ x1 * x2) (𝓝 1) (𝓝 1))) =
    map₂ (fun a b ↦ x * (a * b * y)) (𝓝 1) (𝓝 1)

Tactic:
map_map₂,

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ map (fun x_1 ↦ x * x_1) (map₂ (fun a b ↦ a * b * y) (𝓝 1) (𝓝 1)) = map₂ (fun a b ↦ x * (a * b * y)) (𝓝 1) (𝓝 1)