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

Goal state before:
pp: case pos
α : 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
⊢ (b₁, b₂) ∈ {x | (f x.1, f x.2) ∈ r}

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
⊢ (b₁, b₂) ∈ {x | (f x.1, f x.2) ∈ r}

Tactic:
;

Goal state after:
case pos
α : 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
⊢ (b₁, b₂) ∈ {x | (f x.1, f x.2) ∈ r}

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
⊢ (b₁, b₂) ∈ {x | (f x.1, f x.2) ∈ r}
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: case pos
α : 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
⊢ (b₁, b₂) ∈ {x | (f x.1, f x.2) ∈ r}

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
⊢ (b₁, b₂) ∈ {x | (f x.1, f x.2) ∈ r}

Tactic:
;

Goal state after:
case pos
α : 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
⊢ (b₁, b₂) ∈ {x | (f x.1, f x.2) ∈ r}

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
⊢ (b₁, b₂) ∈ {x | (f x.1, f x.2) ∈ r}
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
s : Set α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen[inst✝²] s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
⊢ [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v].TFAE

Tactic:
tfae_have 2 → 3
  | h, x, hx => by
    obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp (hs.mem_nhds hx)
    exact ⟨K, nhdsWithin_le_nhds hK1, h K hK3 hK2⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
s : Set α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen[inst✝²] s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 : (∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K) → ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
⊢ [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v].TFAE
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst✝ : Finite ι
F : ι → β → α
⊢ (∀ (b : ι), ∀ a ∈ 𝓤 α, ∀ᶠ (x : β × β) in 𝓤 β, (F b x.1, F b x.2) ∈ a) ↔ ∀ (i : ι), UniformContinuous (F i)

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst✝ : Finite ι
F : ι → β → α
⊢ (∀ (b : ι), ∀ a ∈ 𝓤 α, ∀ᶠ (x : β × β) in 𝓤 β, (F b x.1, F b x.2) ∈ a) ↔ ∀ (i : ι), UniformContinuous (F i)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst✝ : Finite ι
F : ι → β → α
S : Set β
⊢ (∀ (b : ι), ∀ a ∈ 𝓤 α, ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), (F b x.1, F b x.2) ∈ a) ↔
    ∀ (i : ι), UniformContinuousOn (F i) S

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst✝ : Finite ι
F : ι → β → α
S : Set β
⊢ (∀ (b : ι), ∀ a ∈ 𝓤 α, ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), (F b x.1, F b x.2) ∈ a) ↔
    ∀ (i : ι), UniformContinuousOn (F i) S
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 ι
G : ι → α → β
hf : TendstoLocallyUniformly F f p
hg : ∀ᶠ (n : ι) in p, ∀ (x : α), Inseparable (F n x) (G n x)
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ univ, Inseparable (F n x) (G n x)

Tactic:
by simpa using hg

Goal state after:
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 ι
g : α → β
hf : TendstoLocallyUniformly F f p
hg : ∀ (x : α), Inseparable (f x) (g x)
⊢ ∀ x ∈ univ, Inseparable (f x) (g x)

Tactic:
by simpa using hg

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous (F ∘ rangeSplitting F)

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous (F ∘ rangeSplitting F)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
h : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn (F ∘ rangeSplitting F) S

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
h : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn (F ∘ rangeSplitting F) S
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

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

Tactic:
rwa [UniformFun.comap_eq, UniformFun.comap_eq] at this

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_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h : Filter γ
s : Set α
t : Set β
u : Set γ
a : α
b : β
m : α → β → γ
f : Filter α
g : Filter β
x✝ : Set γ
⊢ x✝ ∈ {s | ∃ u ∈ f, ∃ v ∈ g, ∀ x ∈ u, ∀ y ∈ v, m x y ∈ s} ↔
    ∃ t₁ ∈ f, ∃ t₂ ∈ g, ∀ x ∈ t₁, ∀ y ∈ t₂, (x, y) ∈ uncurry m ⁻¹' x✝

Tactic:
;

Goal state after:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h : Filter γ
s : Set α
t : Set β
u : Set γ
a : α
b : β
m : α → β → γ
f : Filter α
g : Filter β
x✝ : Set γ
⊢ x✝ ∈ {s | ∃ u ∈ f, ∃ v ∈ g, ∀ x ∈ u, ∀ y ∈ v, m x y ∈ s} ↔
    ∃ t₁ ∈ f, ∃ t₂ ∈ g, ∀ x ∈ t₁, ∀ y ∈ t₂, (x, y) ∈ uncurry m ⁻¹' x✝
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
⊢ map ((fun p ↦ m p.1 p.2) ∘ Prod.mk a) g = map (m a) g

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
⊢ map ((fun p ↦ m p.1 p.2) ∘ Prod.mk a) g = map (m a) g
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
b : β
⊢ map ((fun p ↦ m p.1 p.2) ∘ fun a ↦ (a, b)) f = map (fun x ↦ m x b) f

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
b : β
⊢ map ((fun p ↦ m p.1 p.2) ∘ fun a ↦ (a, b)) f = map (fun x ↦ m x b) f
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
inst✝ : g.NeBot
⊢ map₂ (fun x x_1 ↦ x) f g = f

Tactic:
by
  rw [← map_prod_eq_map₂, map_fst_prod]

Goal state after:
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 ∘ fun p ↦ m p.1 p.2) (f ×ˢ g) = map (fun p ↦ n (m p.1 p.2)) (f ×ˢ g)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β → γ
n : γ → δ
⊢ map (n ∘ fun p ↦ m p.1 p.2) (f ×ˢ g) = map (fun p ↦ n (m p.1 p.2)) (f ×ˢ g)
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 ((fun p ↦ m p.1 p.2) ∘ fun p ↦ (n p.1, id p.2)) (f ×ˢ g) = map (fun p ↦ m (n p.1) p.2) (f ×ˢ g)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : γ → β → δ
n : α → γ
⊢ map ((fun p ↦ m p.1 p.2) ∘ fun p ↦ (n p.1, id p.2)) (f ×ˢ g) = map (fun p ↦ m (n p.1) p.2) (f ×ˢ g)
Module: Mathlib.Order.Filter.NAry

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

Tactic:
by simp_rw [h_comm]

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x ↦ F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
U : Set α
hU : U ∈ 𝓝 (f x₀)
⊢ U ∈ map f (𝓝[S] x₀)

Tactic:
;

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x ↦ F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
U : Set α
hU : U ∈ 𝓝 (f x₀)
⊢ U ∈ map f (𝓝[S] x₀)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
S : Set β
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F S
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ U ∈ map (fun x ↦ (f x.1, f x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S))

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
S : Set β
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F S
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ U ∈ map (fun x ↦ (f x.1, f x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S))
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
h₁ : Tendsto F l (𝓝 f)
h₂ : UniformEquicontinuous F
⊢ UniformContinuous f

Tactic:
by
  rw [← uniformContinuousOn_univ, ← uniformEquicontinuousOn_univ, tendsto_pi_nhds] at *
  exact uniformContinuousOn_of_uniformEquicontinuousOn (fun x _ ↦ h₁ x) h₂

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
⊢ (fun x y ↦ ∃ u v, IsOpen[topologicalSpace α β 𝔖] u ∧ IsOpen[topologicalSpace α β 𝔖] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v)
    f g

Tactic:
obtain ⟨x, hx⟩ := not_forall.mp (mt funext hfg)

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
⊢ ∃ u v, IsOpen[topologicalSpace α β 𝔖] u ∧ IsOpen[topologicalSpace α β 𝔖] v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ici b = Iic (a / b)

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ici b = Iic (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Iic b = Ici (a / b)

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Iic b = Ici (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioi b = Iio (a / b)

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioi b = Iio (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Iio b = Ioi (a / b)

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Iio b = Ioi (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Icc b c = Icc (a / c) (a / b)

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Icc b c = Icc (a / c) (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ico b c = Ioc (a / c) (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioc b c = Ico (a / c) (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioo b c = Ioo (a / c) (a / b)

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioo b c = Ioo (a / c) (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a + x) ∘ fun x ↦ -x) '' a_1 = (fun x ↦ a + x) '' (fun x ↦ -x) '' a_1
⊢ (fun x ↦ a - x) '' [[b, c]] = [[a - b, a - c]]

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a + x) ∘ fun x ↦ -x) '' a_1 = (fun x ↦ a + x) '' (fun x ↦ -x) '' a_1
⊢ (fun x ↦ a - x) '' [[b, c]] = [[a - b, a - c]]
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 γ
⊢ map (fun b_1 ↦ a • b • b_1) f = map ((fun b ↦ a • b) ∘ fun b_1 ↦ b • b_1) f

Tactic:
;

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.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
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
y x : X
U : Set M := {m' | m' • y = x}
hU' : U ≠ ∅
m : M
hm : m • y = x
x✝ : M
⊢ x✝ ∈ U ↔ x✝ ∈ (fun m' ↦ m' * m⁻¹) ⁻¹' ↑(MulAction.stabilizer M x)

Tactic:
;

Goal state after:
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
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
y x : X
U : Set M := {m' | m' • y = x}
hU' : U ≠ ∅
m : M
hm : m • y = x
x✝ : M
⊢ x✝ ∈ U ↔ x✝ ∈ (fun m' ↦ m' * m⁻¹) ⁻¹' ↑(MulAction.stabilizer M x)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun x ↦ c * x) ⁻¹' Iio a = Ioi (a / c)

Tactic:
by
  simpa only [mul_comm] using preimage_mul_const_Iio_of_neg a h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
f g : C(α, β)
inst✝ : DiscreteTopology α
x✝ : C(α, β)
a✝ : α
⊢ ((fun f ↦ { toFun := f, continuous_toFun := ⋯ }) ((fun f ↦ ⇑f) x✝)) a✝ = x✝ a✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
f g : C(α, β)
inst✝ : DiscreteTopology α
x✝ : C(α, β)
a✝ : α
⊢ ((fun f ↦ { toFun := f, continuous_toFun := ⋯ }) ((fun f ↦ ⇑f) x✝)) a✝ = x✝ a✝
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
f g : C(α, β)
inst✝ : DiscreteTopology α
x✝¹ : α → β
x✝ : α
⊢ (fun f ↦ ⇑f) ((fun f ↦ { toFun := f, continuous_toFun := ⋯ }) x✝¹) x✝ = x✝¹ x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
f g : C(α, β)
inst✝ : DiscreteTopology α
x✝¹ : α → β
x✝ : α
⊢ (fun f ↦ ⇑f) ((fun f ↦ { toFun := f, continuous_toFun := ⋯ }) x✝¹) x✝ = x✝¹ x✝
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case h.inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a < 0
⊢ (fun x ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

Tactic:
;

Goal state after:
case h.inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a < 0
⊢ (fun x ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)