mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : X
⊢ map (⇑h) (𝓝[≠] x) = 𝓝[≠] h x

Tactic:
convert! h.isEmbedding.map_nhdsWithin_eq ({ x }ᶜ) x
  rw [h.image_compl, Set.image_singleton]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf_inj : Function.Injective ⇑f
hf : IsOpenMap ⇑f
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap : IsOpenMap (Prod.map (⇑f) (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm))
⊢ IsOpen[instTopologicalSpaceUnits] (⇑(map f) '' ⇑(embedProduct M) ⁻¹' U)

Tactic:
refine ⟨_, hg_openMap U hU, Set.ext fun y ↦ ?_⟩

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf_inj : Function.Injective ⇑f
hf : IsOpenMap ⇑f
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap : IsOpenMap (Prod.map (⇑f) (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm))
y : Nˣ
⊢ y ∈ ⇑(embedProduct N) ⁻¹' Prod.map (⇑f) (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) '' U ↔
    y ∈ ⇑(map f) '' ⇑(embedProduct M) ⁻¹' U
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

Goal state after:
case hopen
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
⊢ ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id U ∈ comap (Prod.mk x) u.uniformity
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
this✝ : Nonempty β
this : Tendsto (Prod.map u u) (atTop ×ˢ atTop) (𝓤 α)
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Tactic:
simpa [MapsTo] using atTop_basis.prod_self.tendsto_left_iff.1 this V hV

Goal state after:
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 α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', Inseparable (F n.1 n.2) (F' n.1 n.2)
⊢ TendstoUniformlyOnFilter F' f p p'

Tactic:
tendstoUniformlyOnFilter_iff_tendsto,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
F' : ι → α → β
hf : Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', Inseparable (F n.1 n.2) (F' n.1 n.2)
⊢ Tendsto (fun q ↦ (f q.2, F' q.1 q.2)) (p ×ˢ p') (𝓤 β)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ UniformContinuousOn f univ ↔ UniformContinuous f

Tactic:
rw [UniformContinuousOn, UniformContinuous, univ_prod_univ, principal_univ, inf_top_eq]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this✝ : s ⊆ interior d
this : interior d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Tactic:
simp [this]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
l' : Filter α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformlyOnFilter F f l l' ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i

Tactic:
tendstoUniformlyOnFilter_iff_tendsto,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
l' : Filter α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (l ×ˢ l') (𝓤 β) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : t ∈ map (Prod.map mk mk) (𝓤 α)
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen[instTopologicalSpaceProd] U
hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t
x y : α
hxyU : (x, y) ∈ U
y' z : α
hyzU : (y', z) ∈ U
hy : (Prod.map mk mk (y', z)).1 = (Prod.map mk mk (x, y)).2
this : y' ⤳ y
⊢ ((Prod.map mk mk (x, y)).1, (Prod.map mk mk (y', z)).2) ∈ t

Tactic:
exact @hUt (x, z) ⟨y', this.mem_open (UniformSpace.isOpen_ball _ hUo) hxyU, hyzU⟩

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

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

Tactic:
rw [lift', dif_neg hf]

Goal state after:
case neg
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x ↦ f ⋯.some
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen[inst✝.toTopologicalSpace] (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
V : Set β
hV : V ∈ 𝓝 y
x : α
hxV : e x ∈ V
hxU : e x ∈ UniformSpace.ball (e a) U
⊢ (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty

Tactic:
exact ⟨e x, hxV, mem_image_of_mem e hxU⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
⊢ IsComplete (m '' s) ↔ IsComplete s

Tactic:
have fact1 : SurjOn (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := surjOn_image .. |>.filter_map_Iic
  have fact2 : MapsTo (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := mapsTo_image .. |>.filter_map_Iic
  simp_rw [IsComplete, imp.swap (a := Cauchy _), ← mem_Iic (b := 𝓟 _), fact1.forall fact2,
    hm.cauchy_map_iff, exists_mem_image, map_le_iff_le_comap, hm.isInducing.nhds_eq_comap]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst✝ : l.IsCountablyGenerated
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n ↦ F (u n)) f atTop s
u : ℕ → ι × α
hu : Tendsto u atTop (l ×ˢ 𝓟 s)
⊢ Tendsto ((fun q ↦ (f q.2, F q.1 q.2)) ∘ u) atTop (𝓤 β)

Tactic:
rw [tendsto_prod_iff'] at hu

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst✝ : l.IsCountablyGenerated
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n ↦ F (u n)) f atTop s
u : ℕ → ι × α
hu : Tendsto (fun n ↦ (u n).1) atTop l ∧ Tendsto (fun n ↦ (u n).2) atTop (𝓟 s)
⊢ Tendsto ((fun q ↦ (f q.2, F q.1 q.2)) ∘ u) atTop (𝓤 β)
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆ closure (range (SeparationQuotient.mk ∘ f))
⊢ Subtype.val ∘ fwd = Subtype.val ∘ rangeFactorization (SeparationQuotient.mk ∘ hid.extend f)

Tactic:
← val_comp_inclusion hrr,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆ closure (range (SeparationQuotient.mk ∘ f))
⊢ Subtype.val ∘ fwd = (Subtype.val ∘ inclusion hrr) ∘ rangeFactorization (SeparationQuotient.mk ∘ hid.extend f)
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
this : UniformContinuousOn (↿f) (K ×ˢ univ)
⊢ TendstoUniformly f (f x) (𝓝 x)

Tactic:
exact this.tendstoUniformly hxK

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
inst✝ : TopologicalSpace α
f : α →ᵤ β
u : Filter (α →ᵤ β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] (toFun f)}
huf : u ≤ 𝓝 f
⊢ f ∈ {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] (toFun f)}

Tactic:
rw [← tendsto_id', UniformFun.tendsto_iff_tendstoUniformly] at huf

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
inst✝ : TopologicalSpace α
f : α →ᵤ β
u : Filter (α →ᵤ β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] (toFun f)}
huf : TendstoUniformly (⇑toFun ∘ id) (toFun f) u
⊢ f ∈ {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] (toFun f)}
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β → γ
n : γ → δ
⊢ map n (map₂ m f g) = map₂ (fun a b ↦ n (m a b)) f g

Tactic:
by
  rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, map_map]; rfl

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
u : α → β
hu : IsUniformInducing u
⊢ Equicontinuous F ↔ Equicontinuous ((fun x ↦ u ∘ x) ∘ F)

Tactic:
congrm ∀ x, ?_
  rw [hu.equicontinuousAt_iff]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b c d : α
⊢ Icc a b * Icc c d ⊆ Icc (a * c) (b * d)

Tactic:
rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩
  exact ⟨mul_le_mul' hya hzc, mul_le_mul' hyb hzd⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
f : Filter α
ι : Sort u_7
p : ι → Prop
s : ι → Set α
h : f.HasBasis p s
⊢ f⁻¹.HasBasis p fun i ↦ (s i)⁻¹

Tactic:
by
  simpa using h.map Inv.inv

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
s : Set β
hs : s ∈ 0
⊢ (fun x ↦ 0 • x) ⁻¹' s ∈ g

Tactic:
convert! @univ_mem _ g

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
s : Set β
hs : s ∈ 0
⊢ (fun x ↦ 0 • x) ⁻¹' s = univ
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun x ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)

Tactic:
suffices (· + b) '' (a * ·) '' Icc c d = Icc (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this
  rw [image_mul_left_Icc' h, image_add_const_Icc]

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

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : Monoid M
inst✝³ : MulAction M X
inst✝² : ContinuousSMul M X
N : Type u_5
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : N →* M
hf : Continuous[inst✝¹, inst✝⁶] ⇑f
x✝ : MulAction N X := compHom X f
⊢ ContinuousSMul N X

Tactic:
exact ⟨(hf.comp continuous_fst).smul continuous_snd⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
h' : TendstoUniformly F' f p
⊢ TendstoUniformly (fun i x ↦ g (F i x)) (fun x ↦ g (f x)) p

Tactic:
apply (tendstoUniformly_congr _).mpr
    (UniformContinuousOn.comp_tendstoUniformly (by grind) hf hg h')

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := ⋯
hF : F =ᶠ[p] F'
h' : TendstoUniformly F' f p
⊢ (fun i x ↦ g (F i x)) =ᶠ[p] fun i x ↦ g (F' i x)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst✝²] s
t : Set G
⊢ s * closure[inst✝²] t⁻¹ = s * t⁻¹

Tactic:
hs.mul_closure

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

Goal state before:
pp: case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ (y * x⁻¹) • K ∈ 𝓝 y

Tactic:
rw [← preimage_smul_inv]

Goal state after:
case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ (fun x_1 ↦ (y * x⁻¹)⁻¹ • x_1) ⁻¹' K ∈ 𝓝 y
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
⊢ IsOpenMap ⇑f ↔ 𝓝 1 ≤ map (⇑f) (𝓝 1)

Tactic:
refine ⟨fun H ↦ map_one f ▸ H.nhds_le 1, fun h ↦ IsOpenMap.of_nhds_le fun x ↦ ?_⟩

Goal state after:
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
⊢ 𝓝 (f x) ≤ map (⇑f) (𝓝 x)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
⊢ UniformContinuous fun p ↦ p.1 / p.2

Tactic:
by
    let φ : (β × β) × (β × β) → β := fun ⟨⟨x₁, x₂⟩, ⟨y₁, y₂⟩⟩ ↦ x₂ * y₂⁻¹ * y₁ * x₁⁻¹
    let ψ : (β × β) × (β × β) → β := fun ⟨⟨x₁, x₂⟩, ⟨y₁, y₂⟩⟩ ↦ (x₁⁻¹ * x₂) * (y₂⁻¹ * y₁)
    let g : (β × β) × (β × β) → β := fun ⟨⟨x₁, x₂⟩, ⟨y₁, y₂⟩⟩ ↦ x₁
    suffices Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1) by
      rw [UniformContinuous, uniformity_eq_comap_mul_inv_nhds_one β, tendsto_comap_iff,
        uniformity_prod_eq_prod, tendsto_map'_iff]
      simpa [Function.comp_def, div_eq_mul_inv, ← mul_assoc]
    have φ_ψ_conj : φ = g * ψ * g⁻¹ := by
      ext
      simp [φ, ψ, g, mul_assoc]
    have ψ_tendsto : Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 1) := by
      rw [← one_mul 1]
      refine .mul ?_ ?_
      · rw [uniformity_eq_comap_inv_mul_nhds_one]
        exact tendsto_comap.comp tendsto_fst
      · rw [uniformity_eq_comap_inv_mul_nhds_one_swapped]
        exact tendsto_comap.comp tendsto_snd
    exact φ_ψ_conj ▸ ψ_tendsto.conj_nhds_one g

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

Goal state before:
pp: K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
R : Type u_2
inst✝⁵ : DivisionSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : PosMulReflectLT R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousInv₀ R
⊢ ∀ (x : { r // 0 < r }), ContinuousAt (fun x ↦ (↑x)⁻¹) x

Tactic:
exact fun x ↦ ContinuousAt.inv₀ (by fun_prop) x.2.ne'

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

Goal state before:
pp: case inr
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
this : ∀ {a : G}, (DenseRange fun x ↦ a ^ x) → 1 < a → Surjective fun x ↦ a ^ x
ha₀ : a ≤ 1
⊢ Surjective fun x ↦ a ^ x

Tactic:
simp only [← range_eq_univ, DenseRange] at *

Goal state after:
case inr
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x ↦ a ^ x)
ha₀ : a ≤ 1
this : ∀ {a : G}, Dense (range fun x ↦ a ^ x) → 1 < a → (range fun x ↦ a ^ x) = univ
⊢ (range fun x ↦ a ^ x) = univ
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
this : (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
⊢ ∃ a_1, (fun x ↦ a ^ x) a_1 = b

Tactic:
rcases h.exists_mem_open isOpen_Ioo this with ⟨l, hl⟩

Goal state after:
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
this : (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
l : ℤ
hl : a ^ l ∈ Ioo (a ^ m) (a ^ (m + 1))
⊢ ∃ a_1, (fun x ↦ a ^ x) a_1 = b
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case hfh
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0)
⊢ ∀ᶠ (b : α) in l, (abs ∘ fun x ↦ f x * g x) b ≤ |C * g b|

Tactic:
filter_upwards [hf] with x hx

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0)
x : α
hx : |f x| ≤ C
⊢ (abs ∘ fun x ↦ f x * g x) x ≤ |C * g x|
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv α γ
x : α
he : x ∈ e.source
he' : x ∈ e'.source
⊢ ↑e x ∈ ↑e.symm.symm.symm ⁻¹' e'.source

Tactic:
by rwa [mem_preimage, PartialEquiv.symm_symm, e.left_inv he]

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

Goal state before:
pp: case hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (x ∈ e.source ∧ y ∈ e'.source) ∧ ↑e x ∈ f.source ∧ ↑e' y ∈ f'.source ↔
    (x ∈ e.source ∧ ↑e x ∈ f.source) ∧ y ∈ e'.source ∧ ↑e' y ∈ f'.source

Tactic:
tauto

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ induced f inst✝¹ = Preorder.topology α

Tactic:
refine le_antisymm (induced_topology_le_preorder hf) ?_

Goal state after:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ Preorder.topology α ≤ induced f inst✝¹
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
t : Set α
ht : t.OrdConnected
⊢ (range Subtype.val).OrdConnected

Tactic:
by
    rwa [← @Subtype.range_val _ t] at ht

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
y : 𝕜
hy : y ∈ Ico a (a + p)
⊢ ↑((equivIco p a) ↑y) = y

Tactic:
have : equivIco p a y = ⟨y, hy⟩ := (equivIco p a).right_inv ⟨y, hy⟩

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
y : 𝕜
hy : y ∈ Ico a (a + p)
this : (equivIco p a) ↑y = ⟨y, hy⟩
⊢ ↑((equivIco p a) ↑y) = y
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
y : 𝕜
hy : y ∈ Ico a (a + p)
this : (equivIco p a) ↑y = ⟨y, hy⟩
⊢ ↑((equivIco p a) ↑y) = y

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
y : 𝕜
hy : y ∈ Ioc a (a + p)
this : (equivIoc p a) ↑y = ⟨y, hy⟩
⊢ ↑((equivIoc p a) ↑y) = y

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
⊢ x = y → ↑x = ↑y

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ioc a (a + p)
hy : y ∈ Ioc a (a + p)
⊢ x = y → ↑x = ↑y

Tactic:
tauto

Goal state after: