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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
⊢ ∀ x ∈ s, ∃ t, IsOpen[inst✝] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r

Tactic:
intro x hx

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
⊢ ∃ t, IsOpen[inst✝] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝¹ : CompleteSpace α
f : Filter α
inst✝ : f.NeBot
hf : f.TotallyBounded
m : Ultrafilter α := Ultrafilter.of f
hmf : ↑m ≤ f
⊢ ∃ x, ClusterPt x f

Tactic:
have hm := m.cauchy_of_totallyBounded' (hf.mono hmf)

Goal state after:
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : CompleteSpace α
f : Filter α
inst✝ : f.NeBot
hf : f.TotallyBounded
m : Ultrafilter α := Ultrafilter.of f
hmf : ↑m ≤ f
hm : Cauchy ↑m
⊢ ∃ x, ClusterPt x f
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : β → Set β
t_open : ∀ x ∈ s, IsOpen[inst✝] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
x : β
hx : x ∈ ⋃ x ∈ s, t x
⊢ (f x, g x) ∈ r

Tactic:
simp only [mem_iUnion, exists_prop] at hx

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : β → Set β
t_open : ∀ x ∈ s, IsOpen[inst✝] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
x : β
hx : ∃ i ∈ s, x ∈ t i
⊢ (f x, g x) ∈ r
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 ⟨?_, ?_⟩

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 ∈ ↑(setSeqAux 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 ∈ ↑(setSeqAux hf U_mem N)
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x ↦ f ↑x
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst✝².toTopologicalSpace] (range e)
hb : closure[inst✝².toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst✝³.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)

Tactic:
by
  have de : IsDenseEmbedding e := he.isDenseEmbedding hd
  have de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e) := de.subtype p
  have ue' : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e) :=
    isUniformEmbedding_subtypeEmb _ he de
  have : b ∈ closure (e '' { x | p x }) :=
    (closure_mono <| monotone_image <| hp) (mem_of_mem_nhds hb)
  let ⟨c, hc⟩ := uniformly_extend_exists ue'.isUniformInducing de'.dense hf ⟨b, this⟩
  replace hc : Tendsto (f ∘ Subtype.val (p := p)) (((𝓝 b).comap e).comap Subtype.val) (𝓝 c) := by
    simpa only [nhds_subtype_eq_comap, comap_comap, IsDenseEmbedding.subtypeEmb_coe] using! hc
  refine ⟨c, (tendsto_comap'_iff ?_).1 hc⟩
  rw [Subtype.range_coe_subtype]
  exact ⟨_, hb, by rwa [← de.isInducing.closure_eq_preimage_closure_image, hs.closure_eq]⟩

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

Goal state before:
pp: γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
this✝ : CompactSpace γ
this : CompactSpace γ
⊢ 𝓤 γ = 𝓤 γ

Tactic:
@compactSpace_uniformity _ u,

Goal state after:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
this✝ : CompactSpace γ
this : CompactSpace γ
⊢ ⨆ x, 𝓝 (x, x) = 𝓤 γ
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
hU : ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Tactic:
refine hU.mono fun i hi x => ?_

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
hU : ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : ↥t), ∀ y ∈ U ↑↑i_1, (f y, F i y) ∈ V
x : α
⊢ (f x, F i x) ∈ V
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
⊢ ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 (β × γ))

Tactic:
intro x hx

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
x : α
hx : x ∈ s
⊢ Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 (β × γ))
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: case hunion
α : 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
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
p : α
hp : p ∈ v ∩ v'
x : β
hx : x ∈ t ∪ t'
⊢ (f p x, f q x) ∈ u

Tactic:
rcases hx with h'x | h'x

Goal state after:
case hunion.inl
α : 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
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
p : α
hp : p ∈ v ∩ v'
x : β
h'x : x ∈ t
⊢ (f p x, f q x) ∈ u

case hunion.inr
α : 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
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
p : α
hp : p ∈ v ∩ v'
x : β
h'x : x ∈ t'
⊢ (f p x, f q x) ∈ u
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 ∈ k, ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u

Tactic:
intro x hx

Goal state after:
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
⊢ ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
T : Set (Set α)
hT𝔗 : T ⊆ 𝔗
hT : T.Finite
hsT : s ⊆ ⋃₀ T
f : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)
hf : ∀ i ∈ T, ∀ x ∈ i, ((toFun 𝔗) f.1 x, (toFun 𝔗) f.2 x) ∈ V
⊢ ∀ x ∈ s, ((toFun 𝔖) ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) f.1) x, (toFun 𝔖) ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) f.2) x) ∈ V

Tactic:
intro x hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
T : Set (Set α)
hT𝔗 : T ⊆ 𝔗
hT : T.Finite
hsT : s ⊆ ⋃₀ T
f : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)
hf : ∀ i ∈ T, ∀ x ∈ i, ((toFun 𝔗) f.1 x, (toFun 𝔗) f.2 x) ∈ V
x : α
hx : x ∈ s
⊢ ((toFun 𝔖) ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) f.1) x, (toFun 𝔖) ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) f.2) x) ∈ V
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : Group α
f g : Filter α
h : 1 ≤ f / g
hfg : Disjoint f g
⊢ False

pp: case refine_2
α : Type u_2
inst✝ : Group α
f g : Filter α
⊢ ¬Disjoint f g → 1 ≤ f / g

Tactic:
· obtain ⟨s, hs, t, ht, hst⟩ := hfg.le_bot (mem_bot : ∅ ∈ ⊥)
    exact Set.one_mem_div_iff.1 (h <| div_mem_div hs ht) (disjoint_iff.2 hst.symm)

Goal state after:
case refine_2
α : Type u_2
inst✝ : Group α
f g : Filter α
⊢ ¬Disjoint f g → 1 ≤ f / g
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

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

Tactic:
inv_eq_iff_eq_inv,

Goal state after:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
⊢ Ioi a = (Ioo 0 a⁻¹)⁻¹
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : IsTopologicalGroup M
inst✝¹ : MulAction M X
inst✝ : DiscreteTopology X
⊢ ContinuousSMul M X ↔ ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)

Tactic:
by
  refine ⟨fun _ _ ↦ stabilizer_isOpen .., fun h ↦ ⟨?_⟩⟩
  rw [continuous_prod_of_discrete_right]
  intro y
  rw [continuous_discrete_rng]
  intro x
  let U := {m' : M | m' • y = x}
  have hU : IsOpen U := by
    by_cases hU' : U ≠ ∅
    · obtain ⟨m, (hm : m • y = x)⟩ := Set.nonempty_iff_empty_ne.mpr hU'.symm
      convert! (h x).preimage (by fun_prop : Continuous fun m' : M ↦ m' * m⁻¹)
      ext; simp [← smul_smul, U, eq_inv_smul_iff.mpr hm]
    simp_all
  simpa using! hU

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
A : Set (Set α)
F : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    (F s hs) ⟨x, hxi⟩ = (F t ht) ⟨x, hxj⟩
hA : ∀ (x : α), ∃ i ∈ A, i ∈ 𝓝 x
s : Set α
hs : s ∈ A
x : ↑s
x' : ↑↑⟨s, hs⟩ := x
⊢ (let F_1 := fun i ↦ F ↑i ⋯;
      liftCover Subtype.val F_1 ⋯ ⋯)
      ↑x =
    (F s hs) x

Tactic:
exact ContinuousMap.liftCover_coe x'

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
⊢ (Iio a)⁻¹ = Ioo a⁻¹ 0

Tactic:
inv_eq_iff_eq_inv,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
⊢ Iio a = (Ioo a⁻¹ 0)⁻¹
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: α : Type u_2
G₀ : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : AddMonoid α
inst✝² : DistribMulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
⊢ c • s ∈ 𝓝 0 ↔ c • s ∈ 𝓝 (c • 0)

Tactic:
rw [smul_zero]

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

Goal state before:
pp: case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Tactic:
intro x hx

Goal state after:
case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
⊢ ContinuousOn (fun a ↦ (List.map (fun i ↦ f i a) l).prod) t

Tactic:
intro x hx

Goal state after:
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousWithinAt (fun a ↦ (List.map (fun i ↦ f i a) l).prod) t x
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x
⊢ ∏ i ∈ s, f i =ᶠ[l] ∏ i ∈ s, g i

Tactic:
filter_upwards [hs] with x hx

Goal state after:
ι : Type u_1
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x
x : X
hx : ∀ i ∈ s, f i x = g i x
⊢ (∏ i ∈ s, f i) x = (∏ i ∈ s, g i) x
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type u_1
inst✝¹ : MulOneClass G
inst✝ : TopologicalSpace G
s : Set G
this : s ⊆ s * {1}
⊢ s ⊆ s * closure[inst✝] {1}

Tactic:
exact this.trans (smul_subset_smul_left subset_closure)

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact s⁻¹

Tactic:
rw [← image_inv_eq_inv]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact ((fun x ↦ x⁻¹) '' s)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
⊢ closure[inst✝²] U ⊆ U * U

Tactic:
intro x hx

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
x : G
hx : x ∈ closure[inst✝²] U
⊢ x ∈ U * U
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ 𝓤 Gᵣ = comap (fun x ↦ x.1 / x.2) (𝓝 1)

Tactic:
rw [← comap_swap_uniformity, uniformity_eq_comap_nhds_one, comap_comap, Function.comp_def]

Goal state after:
Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ comap (fun x ↦ x.swap.2 / x.swap.1) (𝓝 1) = comap (fun x ↦ x.1 / x.2) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_4
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
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
intro x hx

Goal state after:
case refine_4
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
x : G
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
inst✝² : UniformSpace G
inst✝¹ : IsRightUniformGroup G
inst✝ : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
x : G
hx : ∀ᶠ (y : G) in f, y / x ∈ K
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
simp_rw [div_eq_mul_inv, ← op_smul_eq_mul, MulOpposite.op_inv,
      ← mem_smul_set_iff_inv_smul_mem] at hx

Goal state after:
G : Type u_3
inst✝³ : Group G
inst✝² : UniformSpace G
inst✝¹ : IsRightUniformGroup G
inst✝ : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
x : G
hx : ∀ᶠ (y : G) in f, y ∈ MulOpposite.op x • K
⊢ ∃ x, f ≤ 𝓝 x
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update f i '' Icc a b ↔ x ∈ Icc (update f i a) (update f i b)

Tactic:
rw [← Set.pi_univ_Icc]

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update f i '' Icc a b ↔ x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Ioc a (f i) = Ioc (update f i a) f

Tactic:
simpa using image_update_Ioc f i a (f i)

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.2 ≤ p.1
⊢ p ∈ (fun p ↦ [[p.1, p.2]]) ⁻¹' s

Tactic:
rw [mem_preimage, uIcc_of_ge h]

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.2 ≤ p.1
⊢ Icc p.2 p.1 ∈ s
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
⊢ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ⊆ t ∪ {x | IsTop x}

Tactic:
intro x hx

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
x : α
hx : x ∈ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}
⊢ x ∈ t ∪ {x | IsTop x}
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ x_1, x < x_1
u : Set α
hu : u ∈ 𝓝 x
h'u : u ∩ (s ∩ Ioi x) = ∅
y : α
hxy : x < y
hy : Ico x y ⊆ u
⊢ s ∩ Ioo x y = ∅

Tactic:
contrapose! h'u

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ x_1, x < x_1
u : Set α
hu : u ∈ 𝓝 x
y : α
hxy : x < y
hy : Ico x y ⊆ u
h'u : (s ∩ Ioo x y).Nonempty
⊢ (u ∩ (s ∩ Ioi x)).Nonempty
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
x : α
hx : x ∈ e.source
⊢ x ∈ s ↔ ↑e x ∈ t

Tactic:
h hx

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
x : α
hx : x ∈ e.source
⊢ x ∈ s ↔ x ∈ s
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 0)

Tactic:
by
  simp only [div_eq_mul_inv]
  exact bdd_le_mul_tendsto_zero hb hB hg.inv_tendsto_atTop

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝 a = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)

Tactic:
by
  rw [OrderTopology.topology_eq_generate_intervals (α := α), nhds_generateFrom]
  simp_rw [mem_ofPred_eq, @and_comm (a ∈ _), exists_or, or_and_right, iInf_or, iInf_and,
    iInf_exists, iInf_inf_eq, iInf_comm (ι := Set α), iInf_iInf_eq_left, mem_Ioi, mem_Iio]

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

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ EqOn (↑(e.trans f)) (↑(e'.trans f')) (e.trans f).source

Tactic:
intro x hx

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ (e.trans f).source
⊢ ↑(e.trans f) x = ↑(e'.trans f') x
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
⊢ EqOn (↑(e.restr s)) (↑(e'.restr s)) (e.restr s).source

Tactic:
intro x hx

Goal state after:
case right
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
x : α
hx : x ∈ (e.restr s).source
⊢ ↑(e.restr s) x = ↑(e'.restr s) x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a

Tactic:
have : Finite kl := k_fin.subset (by simp [k_eq])

Goal state after:
case refine_2
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this : Finite ↑kl
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a