mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map₂ m (map₂ n f g) h = map₂ m' f (map₂ n' g h)

Tactic:
by

Goal state after:
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

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s
⊢ UniformEquicontinuousOn F S ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)]
  simp only [Prod.forall]
  rfl

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s
⊢ UniformEquicontinuousOn F S ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m' : α → γ → δ'
n' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)
⊢ map₂ m f (map₂ n g h) = map₂ n' g (map₂ m' f h)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
⊢ 𝓝 f = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V i}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m' : α → γ → δ'
n' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b
⊢ map₂ m (map₂ n f g) h = map₂ n' (map₂ m' f h) g

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : (𝓤 α).HasBasis p s
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
by

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:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : α →ᵤ[𝔖] β
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V} ∈ 𝓝 f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ UniformContinuous fun f ↦ (ofFun 𝔖) (UniformFun.toFun f)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
S : Set β
hα : (𝓤 α).HasBasis p s
⊢ UniformEquicontinuousOn F S ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
by

Goal state after:
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 α)
h : univ ∈ 𝔖
⊢ UniformContinuous fun f ↦ UniformFun.ofFun ((toFun 𝔖) f)

Tactic:
by

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

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

Tactic:
by

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 β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ UniformEquicontinuous F ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
by

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
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
⊢ map₂ m (map₂ n f g) h ≤ map₂ n' (map₂ m₁ f h) (map₂ m₂ g h)

Tactic:
by

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 β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ UniformEquicontinuousOn F S ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
by

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_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ b) (n₂ a)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ g) (map n₂ f)

Tactic:
by

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 → α
x₀ : X
u : α → β
hu : IsUniformInducing u
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x ↦ u ∘ x) ∘ F) x₀

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
l : Filter β
⊢ map₂ f (pure a) l = l

Tactic:
by

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 → α
S : Set X
x₀ : X
u : α → β
hu : IsUniformInducing u
⊢ EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((fun x ↦ u ∘ x) ∘ F) S x₀

Tactic:
by

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:
by

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 → α
S : Set X
u : α → β
hu : IsUniformInducing u
⊢ EquicontinuousOn F S ↔ EquicontinuousOn ((fun x ↦ u ∘ x) ∘ F) S

Tactic:
congrm ∀ x ∈ S, ?_
  rw [hu.equicontinuousWithinAt_iff]

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 → α
S : Set X
u : α → β
hu : IsUniformInducing u
⊢ EquicontinuousOn F S ↔ EquicontinuousOn ((fun x ↦ u ∘ x) ∘ F) S

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
l : Filter α
⊢ map₂ f l (pure b) = l

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
⊢ EquicontinuousWithinAt (u ∘ Subtype.val) S x₀

Tactic:
by

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

Goal state before:
pp: X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousAt (u ∘ Subtype.val) x₀
hu : Continuous[tY, Pi.topologicalSpace] u
⊢ EquicontinuousAt (u ∘ Subtype.val) x₀

Tactic:
by

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

Goal state before:
pp: X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
hA : EquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
x : X
hx : x ∈ S
⊢ Continuous[tY, uα.toTopologicalSpace] (eval x ∘ u)

Tactic:
by

Goal state after:
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
⊢ UniformContinuous (⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : 𝔖 ⊆ 𝔗
s : Set α
x✝ : s ∈ 𝔖
⊢ {s} ⊆ 𝔗

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : 𝔖 ⊆ 𝔗
s : Set α
x✝ : s ∈ 𝔖
⊢ {s}.Finite ∧ s ⊆ ⋃₀ {s}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
s : Set α
h : s ∈ 𝔖
⊢ {s} ⊆ 𝔖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ uniformSpace α γ 𝔖 = ⨅ i, uniformSpace α γ 𝔖

Tactic:
by

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

Goal state before:
pp: Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
⊢ UniformEquicontinuousOn (u ∘ Subtype.val) S

Tactic:
by

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

Goal state before:
pp: Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
hA : UniformEquicontinuous (u ∘ Subtype.val)
hu : Continuous[tY, Pi.topologicalSpace] u
⊢ UniformEquicontinuous (u ∘ Subtype.val)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ 𝔖 = uniformSpace α γ 𝔖 ⊓ uniformSpace α γ 𝔖

Tactic:
by

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₀
⊢ ContinuousWithinAt f S x₀

Tactic:
by

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 → α
x₀ : X
h₁ : Tendsto F l (𝓝 f)
h₂ : EquicontinuousAt F x₀
⊢ ContinuousAt f x₀

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ uniformSpace α γ 𝔖 = UniformSpace.comap (fun x ↦ f ∘ x) (uniformSpace α β 𝔖)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ UniformContinuous (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖))

Tactic:
by

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 β
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
⊢ UniformContinuousOn f S

Tactic:
by

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 β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
h₁ : Tendsto F l (𝓝 f)
h₂ : UniformEquicontinuous F
⊢ UniformContinuous f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : IsUniformInducing f
⊢ IsUniformInducing (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun x ↦ f '' x) 𝔗 𝔖
⊢ UniformContinuous fun g ↦ (ofFun 𝔗) ((toFun 𝔖) g ∘ f)

Tactic:
by

Goal state after:
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

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:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ UniformContinuous ((⋃₀ 𝔖).domRestrict ∘ ⇑(toFun 𝔖))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ IsUniformInducing fun f s ↦ UniformFun.ofFun ((↑s).domRestrict ((toFun 𝔖) f))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ UniformContinuous ⇑(toFun 𝔖)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt ((toFun 𝔖) f) x
⊢ ContinuousAt (fun fx ↦ (toFun 𝔖) fx.1 fx.2) (f, x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
p : Filter ι
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
⊢ Tendsto F p (𝓝 f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(toFun 𝔖) ∘ F) ((toFun 𝔖) f) p s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
X : Type u_5
inst✝ : TopologicalSpace X
f : X → α →ᵤ[𝔖] β
⊢ Continuous[inst✝, topologicalSpace α β 𝔖] f ↔
    ∀ s ∈ 𝔖, Continuous[inst✝, UniformFun.topologicalSpace (↑s) β] (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖) ∘ f)

Tactic:
by

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 ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : Tendsto f (𝓝[s] x) (𝓝 z)
hs : ∀ y ∈ s, Tendsto (fun x ↦ F x y) l (𝓝 (f y))
hx : x ∈ closure[tX] s
⊢ Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 z)

Tactic:
by

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:
by

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 : α
⊢ Iic a * Iic b ⊆ Iic (a * b)

Tactic:
by

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 : α
⊢ Ici a * Ici b ⊆ Ici (a * b)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 α)
inst✝ : CompleteSpace β
⊢ CompleteSpace (α →ᵤ[𝔖] β)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
⊢ Iic a * Iio b ⊆ Iio (a * b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
⊢ Iio a * Iic b ⊆ Iio (a * b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
⊢ Ioi a * Ici b ⊆ Ioi (a * b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
⊢ Ici a * Ioi b ⊆ Ioi (a * b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c : α
⊢ a • Icc b c = Icc (a * b) (a * c)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : One α
inst✝² : One β
inst✝¹ : FunLike F α β
inst✝ : OneHomClass F α β
φ : F
⊢ map (⇑φ) 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s⁻¹ ∈ f⁻¹

Tactic:
by

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

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✝ : InvolutiveInv α
f✝ g : Filter α
s : Set α
f : Filter α
⊢ map (Inv.inv ∘ Inv.inv) f = f

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
f g : Filter α
⊢ f⁻¹ ≤ g ↔ f ≤ g⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a b : α
⊢ pure a * pure b = pure (a * b)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : Div α
a b : α
⊢ pure a / pure b = pure (a / b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ Icc a b * Icc c d = Icc (a * c) (b * d)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (Icc a b)⁻¹ = Icc b⁻¹ a⁻¹

Tactic:
by

Goal state after: