mathlib-initiative/mathlib-tactics huggingface dataset:
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 ι
h : TendstoUniformly F f p
u : Set (β × β)
hu : u ∈ 𝓤 β
x✝ : α
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ univ, (f y, F n y) ∈ u

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformly F f p
u : Set (β × β)
hu : u ∈ 𝓤 β
x✝ : α
⊢ ∀ᶠ (n : ι) in p, ∀ (y : α), (f y, F n y) ∈ u
Module: Mathlib.Topology.UniformSpace.Equiv

Goal state before:
pp: α : Type u
β✝ : Type u_1
γ : Type u_2
δ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β✝
inst✝² : UniformSpace γ
inst✝¹ : UniformSpace δ
ι : Type u_4
ι' : Type u_5
β : ι' → Type u_6
inst✝ : (j : ι') → UniformSpace (β j)
e : ι ≃ ι'
i : ι
⊢ UniformContinuous fun x ↦ (Equiv.piCongrLeft β e).toFun x (e i)

Tactic:
simpa using

Goal state after:
α : Type u
β✝ : Type u_1
γ : Type u_2
δ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β✝
inst✝² : UniformSpace γ
inst✝¹ : UniformSpace δ
ι : Type u_4
ι' : Type u_5
β : ι' → Type u_6
inst✝ : (j : ι') → UniformSpace (β j)
e : ι ≃ ι'
i : ι
⊢ UniformContinuous fun x ↦ x i
Module: Mathlib.Topology.UniformSpace.UniformApproximation

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

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : α → β
x : α
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
Module: Mathlib.Topology.UniformSpace.Equiv

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
p : α → Prop
q : β → Prop
e : α ≃ᵤ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ UniformContinuous (e.subtypeEquiv h).toFun

Tactic:
simpa using

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
p : α → Prop
q : β → Prop
e : α ≃ᵤ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ UniformContinuous (Subtype.map ⇑e ⋯)
Module: Mathlib.Topology.UniformSpace.UniformApproximation

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : α → β
L : ∀ u ∈ 𝓤 β, ∃ F, Continuous[inst✝¹, inst✝.toTopologicalSpace] F ∧ ∀ (y : α), (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ F, ContinuousOn F univ ∧ ∀ y ∈ univ, (f y, F y) ∈ u

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : α → β
L : ∀ u ∈ 𝓤 β, ∃ F, Continuous[inst✝¹, inst✝.toTopologicalSpace] F ∧ ∀ (y : α), (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ F, Continuous[inst✝¹, inst✝.toTopologicalSpace] F ∧ ∀ (y : α), (f y, F y) ∈ u
Module: Mathlib.Topology.UniformSpace.Equiv

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
p : α → Prop
q : β → Prop
e : α ≃ᵤ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ UniformContinuous (e.subtypeEquiv h).invFun

Tactic:
simpa using

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
p : α → Prop
q : β → Prop
e : α ≃ᵤ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ UniformContinuous (Subtype.map ⇑e.symm ⋯)
Module: Mathlib.Topology.UniformSpace.Equiv

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α ≃ β
hf : IsUniformInducing ⇑f
⊢ UniformContinuous (⇑f ∘ f.invFun)

Tactic:
simpa using

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α ≃ β
hf : IsUniformInducing ⇑f
⊢ UniformContinuous id
Module: Mathlib.Topology.UniformSpace.UniformApproximation

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : ∀ u ∈ 𝓤 β, ∃ F, UniformContinuous F ∧ ∀ (y : α), (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ F, UniformContinuousOn F univ ∧ ∀ y ∈ univ, (f y, F y) ∈ u

Tactic:
simpa using

Goal state after:
α : Type u_4
β : Type u_5
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : ∀ u ∈ 𝓤 β, ∃ F, UniformContinuous F ∧ ∀ (y : α), (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ F, UniformContinuous F ∧ ∀ (y : α), (f y, F y) ∈ u
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 ι
h : ∀ (x : α), ∃ t ∈ 𝓝 x, TendstoUniformlyOn F f p t
⊢ ∀ x ∈ univ, ∃ t ∈ 𝓝[univ] x, TendstoUniformlyOn F f p t

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : ∀ (x : α), ∃ t ∈ 𝓝 x, TendstoUniformlyOn F f p t
⊢ ∀ (x : α), ∃ t ∈ 𝓝 x, TendstoUniformlyOn F f p t
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ min (a / c) (b / c) = min a b / c

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ min (a * c⁻¹) (b * c⁻¹) = min a b * c⁻¹
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ max (a / c) (b / c) = max a b / c

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ max (a * c⁻¹) (b * c⁻¹) = max a b * c⁻¹
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |min a b - min c d| ≤ max |a - c| |b - d|

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |min a b - min c d| ≤ max |a - c| |b - d|
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ |max a c - max b c| ≤ |a - b|

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ |max a c - max b c| ≤ |a - b|
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 ι
⊢ TendstoLocallyUniformly F f p ↔ ∀ (x : α), TendstoUniformlyOnFilter F f p (𝓝 x)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoLocallyUniformlyOn F f p univ ↔ ∀ (x : α), TendstoUniformlyOnFilter F f p (𝓝[univ] 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 : α → β
s : Set α
p : Filter ι
hf : TendstoLocallyUniformlyOn F f p s
a : α
ha : a ∈ s
⊢ 𝓟 {a} ≤ 𝓝[s] a

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hf : TendstoLocallyUniformlyOn F f p s
a : α
ha : a ∈ s
⊢ pure a ≤ 𝓝[s] a
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
⊢ ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
⊢ ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
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:
simpa using

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

Tactic:
simpa using

Goal state after:
α : 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 : α), Inseparable (f x) (g x)
Module: Mathlib.Topology.Algebra.Monoid.Defs

Goal state before:
pp: α : Type u_2
E : Type u_3
inst✝² : CommGroup E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f g : α → E
m : E
x : Filter α
hf : Tendsto f x (𝓝 m)
hfg : Tendsto (g / f) x (𝓝 1)
⊢ Tendsto g x (𝓝 m)

Tactic:
simpa using

Goal state after:
α : Type u_2
E : Type u_3
inst✝² : CommGroup E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f g : α → E
m : E
x : Filter α
hf : Tendsto f x (𝓝 m)
hfg : Tendsto (g / f) x (𝓝 1)
⊢ Tendsto g x (𝓝 m)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), UniformEquicontinuous F

Tactic:
simp_rw [uniformEquicontinuous_iff_uniformContinuous (uα := _)]
  rw [UniformFun.iInf_eq, uniformContinuous_iInf_rng]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
⊢ ∀ (i : ι × ι), True → ∃ i', True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t i.1) (V i.2)

Tactic:
rintro ⟨k, l⟩ -
    rcases directed_of (· ≤ ·) k l with ⟨n, hkn, hln⟩
    exact ⟨n, trivial, UniformOnFun.gen_mono (hmono hkn) (hb.2 <| hln)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : Filter α
g : Filter β
ι : Type u_11
ι' : Type u_12
p : ι → Prop
q : ι' → Prop
s : ι → Set α
t : ι' → Set β
m : α → β → γ
hf : f.HasBasis p s
hg : g.HasBasis q t
⊢ (map₂ m f g).HasBasis (fun i ↦ p i.1 ∧ q i.2) fun i ↦ image2 m (s i.1) (t i.2)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : Filter α
g : Filter β
ι : Type u_11
ι' : Type u_12
p : ι → Prop
q : ι' → Prop
s : ι → Set α
t : ι' → Set β
m : α → β → γ
hf : f.HasBasis p s
hg : g.HasBasis q t
⊢ (Filter.map (fun p ↦ m p.1 p.2) (f ×ˢ g)).HasBasis (fun i ↦ p i.1 ∧ q i.2) fun i ↦
    (fun p ↦ m p.1 p.2) '' s i.1 ×ˢ t i.2
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:
simpa using

Goal state after:
α : 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)⁻¹
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ (fun x ↦ a + x) ⁻¹' [[b, c]] = [[b - a, c - a]]
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Group α
f : Filter α
h : f.NeBot
⊢ 1 ≤ f / f

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Group α
f : Filter α
h : f.NeBot
⊢ ¬f = ⊥
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
⊢ uniformSpace α β 𝔖 =
    UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁) ⊓
      UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂)

Tactic:
set ψ₁ : Π S : Set α, φ₁ ⁻¹' S → S := fun S ↦ S.restrictPreimage φ₁

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
⊢ uniformSpace α β 𝔖 =
    UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁) ⊓
      UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
S : Set α
hS : S ∈ 𝔖
⊢ range (ψ₁ S) ∪ range (ψ₂ S) = univ

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
S : Set α
hS : S ∈ 𝔖
⊢ S ⊆ range φ₁ ∪ range φ₂
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid γ
inst✝ : MulAction γ β
m : α → β
c : γ
f : Filter α
g : Filter β
hc : IsUnit c
d : γ
hd : d * c = 1
H : Tendsto (c • m) f (c • g)
⊢ Tendsto m f g

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid γ
inst✝ : MulAction γ β
m : α → β
c : γ
f : Filter α
g : Filter β
hc : IsUnit c
d : γ
hd : d * c = 1
H : Tendsto (c • m) f (c • g)
⊢ Tendsto m f g
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : SMul M X
inst✝² : ContinuousSMul M X
f : Y → M
g : Y → X
b : Y
s : Set Y
inst✝¹ : SMul Mᵐᵒᵖ X
inst✝ : IsCentralScalar M X
⊢ Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ MulOpposite.op p.1 • p.2

Tactic:
simpa using

Goal state after:
M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : SMul M X
inst✝² : ContinuousSMul M X
f : Y → M
g : Y → X
b : Y
s : Set Y
inst✝¹ : SMul Mᵐᵒᵖ X
inst✝ : IsCentralScalar M X
⊢ Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ p.1 • p.2
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: M : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : SMul M X
inst✝² : ContinuousSMul M X
g : Y → X
N : Type u_5
inst✝¹ : SMul N Y
inst✝ : TopologicalSpace N
f : N → M
hg : IsInducing g
hf : Continuous[inst✝, inst✝⁶] f
hsmul : ∀ {c : N} {x : Y}, g (c • x) = f c • g x
⊢ Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ p.1 • p.2

Tactic:
simpa using

Goal state after:
M : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : SMul M X
inst✝² : ContinuousSMul M X
g : Y → X
N : Type u_5
inst✝¹ : SMul N Y
inst✝ : TopologicalSpace N
f : N → M
hg : IsInducing g
hf : Continuous[inst✝, inst✝⁶] f
hsmul : ∀ {c : N} {x : Y}, g (c • x) = f c • g x
⊢ Continuous[instTopologicalSpaceProd, inst✝⁵] fun x ↦ f x.1 • g x.2
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:
simpa using

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun x ↦ c * x) ⁻¹' Iio a = Ioi (a / c)
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) ⁻¹' Ioi a = Iio (a / c)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun x ↦ c * x) ⁻¹' Ioi a = Iio (a / c)
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) ⁻¹' Iic a = Ici (a / c)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun x ↦ c * x) ⁻¹' Iic a = Ici (a / c)
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) ⁻¹' Ici a = Iic (a / c)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun x ↦ c * x) ⁻¹' Ici a = Iic (a / c)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun x ↦ c * x) ⁻¹' Ioo a b = Ioo (b / c) (a / c)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun x ↦ c * x) ⁻¹' Ioc a b = Ico (b / c) (a / c)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun x ↦ c * x) ⁻¹' Ico a b = Ioc (b / c) (a / c)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun x ↦ c * x) ⁻¹' Icc a b = Icc (b / c) (a / c)
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(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩
hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x
H : ⋃ i, S i = Set.univ
i : ι
⊢ Continuous[instTopologicalSpaceSubtype, inst✝²] ((S i).domRestrict (Set.liftCover S (fun i ↦ ⇑(φ i)) hφ H))

Tactic:
simpa using

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(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩
hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x
H : ⋃ i, S i = Set.univ
i : ι
⊢ Continuous[instTopologicalSpaceSubtype, inst✝²] fun x ↦ (φ i) x
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
⊢ (fun x ↦ a * x) '' [[b, c]] = [[a * b, a * c]]

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
⊢ (fun x ↦ a * x) '' [[b, c]] = [[a * b, a * c]]
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
g : C(X, Z)
h : FactorsThrough ⇑g ⇑f
a✝ : X
⊢ ((hf.lift g h).comp f) a✝ = g a✝

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
g : C(X, Z)
h : FactorsThrough ⇑g ⇑f
a✝ : X
⊢ g (surjInv ⋯ (f a✝)) = g a✝
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
g✝ : C(X, Z)
h : FactorsThrough ⇑g✝ ⇑f
g : C(Y, Z)
a : Y
⊢ ((fun g ↦ hf.lift ↑g ⋯) ((fun g ↦ ⟨g.comp f, ⋯⟩) g)) a = g a

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
g✝ : C(X, Z)
h : FactorsThrough ⇑g✝ ⇑f
g : C(Y, Z)
a : Y
⊢ g (f (surjInv ⋯ a)) = g a