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

Goal state before:
pp: case a
α : Type u_1
U V : SetRel α α
s₁ s₃ s₂ : Set α
h₁₂ : s₁ ⊆ U.preimage s₂
h₂₁ : s₂ ⊆ U.image s₁
h₂₃ : s₂ ⊆ V.preimage s₃
h₃₂ : s₃ ⊆ V.image s₂
⊢ s₁ ⊆ s₁ ∧ s₃ ⊆ s₃

Tactic:
]

Goal state after:
case a
α : Type u_1
U V : SetRel α α
s₁ s₃ s₂ : Set α
h₁₂ : s₁ ⊆ U.preimage s₂
h₂₁ : s₂ ⊆ U.image s₁
h₂₃ : s₂ ⊆ V.preimage s₃
h₃₂ : s₃ ⊆ V.image s₂
⊢ s₁ ⊆ s₁ ∧ s₃ ⊆ s₃
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
U : SetRel α α
inst✝ : U.IsTrans
⊢ hausdorffEntourage U ⊆ hausdorffEntourage U

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ ↑t, {x | (x, y) ∈ Prod.swap ⁻¹' U}
⊢ ({x | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s) ∈ hausdorffEntourage U

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ ↑t, {x | (x, y) ∈ Prod.swap ⁻¹' U}
⊢ ({x | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s) ∈ hausdorffEntourage U
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ 𝓟 SetRel.id ≤ (𝓤 α).lift' hausdorffEntourage

Tactic:
simp_rw [Filter.principal_le_lift', SetRel.id_subset_iff]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ ∀ s ∈ 𝓤 α, (hausdorffEntourage s).IsRefl
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ ∀ s ∈ 𝓤 α, hausdorffEntourage s ∈ ((𝓤 α).lift' hausdorffEntourage).lift' fun s ↦ SetRel.comp s s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ ∀ s ∈ 𝓤 α, hausdorffEntourage s ∈ ((𝓤 α).lift' hausdorffEntourage).lift' fun s ↦ SetRel.comp s s
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : SetRel.comp V V ⊆ U
⊢ hausdorffEntourage U ⊆ hausdorffEntourage U

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ (((𝓤 α).lift' hausdorffEntourage).lift' fun s ↦ SetRel.comp s s) ≤ (𝓤 α).lift' hausdorffEntourage

Tactic:
rw [Filter.le_lift']
      intro U hU
      obtain ⟨V, hV, hVU⟩ := comp_mem_uniformity_sets hU
      refine Filter.mem_of_superset (Filter.mem_lift' (Filter.mem_lift' hV)) ?_
      grw [← hausdorffEntourage_comp, hVU]

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
⊢ ∀ x ∈ {s | (s ∩ U).Nonempty}, {s | (s ∩ U).Nonempty} ∈ 𝓝 x

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
⊢ ∀ x ∈ {s | (s ∩ U).Nonempty}, {s | (s ∩ U).Nonempty} ∈ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
hx₂ : ∃ V ∈ 𝓤 α, ball x V ⊆ U
⊢ {s | (s ∩ U).Nonempty} ∈ 𝓝 s

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
hx₂ : ∃ V ∈ 𝓤 α, ball x V ⊆ U
⊢ {s | (s ∩ U).Nonempty} ∈ 𝓝 s
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball x V ⊆ U
⊢ ∃ V ∈ 𝓤 (Set α), ball s V ⊆ {s | (s ∩ U).Nonempty}

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball x V ⊆ U
⊢ ∃ V ∈ 𝓤 (Set α), ball s V ⊆ {s | (s ∩ U).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : Set α → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
⊢ ∃ x ∈ {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1},
    s ∈ {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty} ∧
      {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty} ⊆ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : Set α → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
⊢ ∃ x ∈ {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1},
    s ∈ {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty} ∧
      {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty} ⊆ {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
F : Set α
hF : IsClosed[inst✝.toTopologicalSpace] F
⊢ IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {a | ¬a ⊆ F}

Tactic:
← Set.inter_compl_nonempty_iff

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
F : Set α
hF : IsClosed[inst✝.toTopologicalSpace] F
⊢ IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {a | (a ∩ Fᶜ).Nonempty}
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case left
α : Type u_1
inst✝ : UniformSpace α
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] (𝒫 ∅)

Tactic:
]

Goal state after:
case left
α : Type u_1
inst✝ : UniformSpace α
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] (𝒫 ∅)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case right
α : Type u_1
inst✝ : UniformSpace α
⊢ {∅} ∈ (𝓤 (Set α)).lift' (ball ∅)

Tactic:
filter_upwards [Filter.mem_lift' <| Filter.mem_lift' Filter.univ_mem] with F ⟨_, hF⟩

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
F : Set α
left✝ : (∅, F).1 ⊆ SetRel.preimage Set.univ (∅, F).2
hF : (∅, F).2 ⊆ SetRel.image Set.univ (∅, F).1
⊢ F ∈ {∅}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : Set α → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
t : Set α
x✝ : t ∈ {s | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty}
ht₁ : t ⊆ (⋃₀ u, f '' u).1
ht₂ : ∀ ⦃x : Set α⦄, x ∈ u → (t ∩ f x).Nonempty
U : Set α
hU : U ∈ u
⊢ (t ∩ U).Nonempty

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : Set α → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
t : Set α
x✝ : t ∈ {s | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty}
ht₁ : t ⊆ (⋃₀ u, f '' u).1
ht₂ : ∀ ⦃x : Set α⦄, x ∈ u → (t ∩ f x).Nonempty
U : Set α
hU : U ∈ u
⊢ (t ∩ U).Nonempty
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), UpperHemicontinuousOn (F n) s
hf_compact : ∀ x ∈ s, IsCompact (f x)
⊢ ∀ x ∈ s, ∀ (u : Set β), IsOpen[inst✝.toTopologicalSpace] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), UpperHemicontinuousOn (F n) s
hf_compact : ∀ x ∈ s, IsCompact (f x)
⊢ ∀ x ∈ s, ∀ (u : Set β), IsOpen[inst✝.toTopologicalSpace] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
h : ‖a‖ * ‖1‖ < ‖k‖
⊢ IsUnit (k • 1 - a)

Tactic:
]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
h : ‖a‖ * ‖1‖ < ‖k‖
⊢ IsUnit (k • 1 - a)
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
h : ‖a‖ < ‖1‖⁻¹ * ‖k‖
a✝ : Nontrivial A
hk : k ≠ 0
ku : Aˣ := (Units.map ↑↑ₐ) (Units.mk0 k hk)
⊢ IsUnit (k • 1 - a)

Tactic:
]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
h : ‖a‖ < ‖1‖⁻¹ * ‖k‖
a✝ : Nontrivial A
hk : k ≠ 0
ku : Aˣ := (Units.map ↑↑ₐ) (Units.mk0 k hk)
⊢ IsUnit (k • 1 - a)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : Set α → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
t : Set α
x✝ : t ∈ {s | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty}
ht₁ : t ⊆ (⋃₀ u, f '' u).1
ht₂ : ∀ ⦃x : Set α⦄, x ∈ u → (t ∩ f x).Nonempty
U : Set α
hU : U ∈ u
⊢ (t ∩ f U).Nonempty

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : Set α → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
t : Set α
x✝ : t ∈ {s | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty}
ht₁ : t ⊆ (⋃₀ u, f '' u).1
ht₂ : ∀ ⦃x : Set α⦄, x ∈ u → (t ∩ f x).Nonempty
U : Set α
hU : U ∈ u
⊢ (t ∩ f U).Nonempty
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : NormOneClass A
a : A
k : 𝕜
h : ‖a‖ < ‖k‖
⊢ ‖a‖ < ‖k‖

Tactic:
]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : NormOneClass A
a : A
k : 𝕜
h : ‖a‖ < ‖k‖
⊢ ‖a‖ < ‖k‖
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A✝ : Type u_2
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing A✝
inst✝⁴ : NormedAlgebra 𝕜 A✝
inst✝³ : CompleteSpace A✝
A : Type u_3
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : A
inst✝ : IsCompact (spectrum ℝ a)
⊢ IsCompact (spectrum ℝ≥0 a)

Tactic:
]

Goal state after:
𝕜 : Type u_1
A✝ : Type u_2
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing A✝
inst✝⁴ : NormedAlgebra 𝕜 A✝
inst✝³ : CompleteSpace A✝
A : Type u_3
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : A
inst✝ : IsCompact (spectrum ℝ a)
⊢ IsCompact (spectrum ℝ≥0 a)
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A✝ : Type u_2
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing A✝
inst✝⁴ : NormedAlgebra 𝕜 A✝
inst✝³ : CompleteSpace A✝
A : Type u_3
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : A
inst✝ : IsCompact (spectrum ℝ a)
⊢ IsCompact (⇑(algebraMap ℝ≥0 ℝ) ⁻¹' spectrum ℝ a)

Tactic:
]

Goal state after:
𝕜 : Type u_1
A✝ : Type u_2
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing A✝
inst✝⁴ : NormedAlgebra 𝕜 A✝
inst✝³ : CompleteSpace A✝
A : Type u_3
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : A
inst✝ : IsCompact (spectrum ℝ a)
⊢ IsCompact (⇑(algebraMap ℝ≥0 ℝ) ⁻¹' spectrum ℝ a)
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: A : Type u_3
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : A
inst✝ : CompactSpace ↑(spectrum ℝ a)
⊢ CompactSpace ↑(spectrum ℝ≥0 a)

Tactic:
]

Goal state after:
A : Type u_3
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : A
inst✝ : CompactSpace ↑(spectrum ℝ a)
⊢ CompactSpace ↑(spectrum ℝ≥0 a)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case left
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ : (s, t) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
⊢ V.preimage (V.preimage t) ⊆ V.preimage (V.preimage t)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NormedField 𝕜
B : Type u_3
inst✝⁵ : NonUnitalNormedRing B
inst✝⁴ : NormedSpace 𝕜 B
inst✝³ : CompleteSpace B
inst✝² : IsScalarTower 𝕜 B B
inst✝¹ : SMulCommClass 𝕜 B B
inst✝ : ProperSpace 𝕜
a : B
⊢ IsCompact (σ ((WithLp.unitizationAlgEquiv 𝕜).symm ↑a))

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NormedField 𝕜
B : Type u_3
inst✝⁵ : NonUnitalNormedRing B
inst✝⁴ : NormedSpace 𝕜 B
inst✝³ : CompleteSpace B
inst✝² : IsScalarTower 𝕜 B B
inst✝¹ : SMulCommClass 𝕜 B B
inst✝ : ProperSpace 𝕜
a : B
⊢ IsCompact (σ ((WithLp.unitizationAlgEquiv 𝕜).symm ↑a))
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝¹³ : NormedField 𝕜
inst✝¹² : NormedRing A
inst✝¹¹ : NormedAlgebra 𝕜 A
inst✝¹⁰ : CompleteSpace A
B : Type u_3
inst✝⁹ : NonUnitalNormedRing B
inst✝⁸ : NormedSpace 𝕜 B
inst✝⁷ : CompleteSpace B
inst✝⁶ : IsScalarTower 𝕜 B B
inst✝⁵ : SMulCommClass 𝕜 B B
inst✝⁴ : ProperSpace 𝕜
inst✝³ : NormedSpace ℝ B
inst✝² : IsScalarTower ℝ B B
inst✝¹ : SMulCommClass ℝ B B
a : B
inst✝ : IsCompact (quasispectrum ℝ a)
⊢ IsCompact (quasispectrum ℝ≥0 a)

Tactic:
]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝¹³ : NormedField 𝕜
inst✝¹² : NormedRing A
inst✝¹¹ : NormedAlgebra 𝕜 A
inst✝¹⁰ : CompleteSpace A
B : Type u_3
inst✝⁹ : NonUnitalNormedRing B
inst✝⁸ : NormedSpace 𝕜 B
inst✝⁷ : CompleteSpace B
inst✝⁶ : IsScalarTower 𝕜 B B
inst✝⁵ : SMulCommClass 𝕜 B B
inst✝⁴ : ProperSpace 𝕜
inst✝³ : NormedSpace ℝ B
inst✝² : IsScalarTower ℝ B B
inst✝¹ : SMulCommClass ℝ B B
a : B
inst✝ : IsCompact (quasispectrum ℝ a)
⊢ IsCompact (quasispectrum ℝ≥0 a)
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝¹³ : NormedField 𝕜
inst✝¹² : NormedRing A
inst✝¹¹ : NormedAlgebra 𝕜 A
inst✝¹⁰ : CompleteSpace A
B : Type u_3
inst✝⁹ : NonUnitalNormedRing B
inst✝⁸ : NormedSpace 𝕜 B
inst✝⁷ : CompleteSpace B
inst✝⁶ : IsScalarTower 𝕜 B B
inst✝⁵ : SMulCommClass 𝕜 B B
inst✝⁴ : ProperSpace 𝕜
inst✝³ : NormedSpace ℝ B
inst✝² : IsScalarTower ℝ B B
inst✝¹ : SMulCommClass ℝ B B
a : B
inst✝ : IsCompact (quasispectrum ℝ a)
⊢ IsCompact (⇑(algebraMap ℝ≥0 ℝ) ⁻¹' quasispectrum ℝ a)

Tactic:
]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝¹³ : NormedField 𝕜
inst✝¹² : NormedRing A
inst✝¹¹ : NormedAlgebra 𝕜 A
inst✝¹⁰ : CompleteSpace A
B : Type u_3
inst✝⁹ : NonUnitalNormedRing B
inst✝⁸ : NormedSpace 𝕜 B
inst✝⁷ : CompleteSpace B
inst✝⁶ : IsScalarTower 𝕜 B B
inst✝⁵ : SMulCommClass 𝕜 B B
inst✝⁴ : ProperSpace 𝕜
inst✝³ : NormedSpace ℝ B
inst✝² : IsScalarTower ℝ B B
inst✝¹ : SMulCommClass ℝ B B
a : B
inst✝ : IsCompact (quasispectrum ℝ a)
⊢ IsCompact (⇑(algebraMap ℝ≥0 ℝ) ⁻¹' quasispectrum ℝ a)
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: B : Type u_3
inst✝⁴ : NonUnitalNormedRing B
inst✝³ : NormedSpace ℝ B
inst✝² : IsScalarTower ℝ B B
inst✝¹ : SMulCommClass ℝ B B
a : B
inst✝ : CompactSpace ↑(quasispectrum ℝ a)
⊢ CompactSpace ↑(quasispectrum ℝ≥0 a)

Tactic:
]

Goal state after:
B : Type u_3
inst✝⁴ : NonUnitalNormedRing B
inst✝³ : NormedSpace ℝ B
inst✝² : IsScalarTower ℝ B B
inst✝¹ : SMulCommClass ℝ B B
a : B
inst✝ : CompactSpace ↑(quasispectrum ℝ a)
⊢ CompactSpace ↑(quasispectrum ℝ≥0 a)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case right
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ : (s, t) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
⊢ V.image (V.image s) ⊆ V.image (V.image s)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ {t | t.Finite ∧ t ⊆ s} ⊆ 𝒫 closure[inst✝] s

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ {t | t.Finite ∧ t ⊆ s} ⊆ 𝒫 closure[inst✝] s
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
⊢ ∀ i' ∈ 𝓤 α,
    ∃ i ∈ 𝓤 α,
      (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹'
          hausdorffEntourage i ⊆
        hausdorffEntourage i'

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
⊢ ∀ i' ∈ 𝓤 α,
    ∃ i ∈ 𝓤 α,
      (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹'
          hausdorffEntourage i ⊆
        hausdorffEntourage i'
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s K : Set α
hKs : K ∈ 𝒫 closure[inst✝] s
⊢ ∀ ⦃x : Set (Set α)⦄,
    x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U} →
      K ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} →
        ({s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∩ {t | t.Finite ∧ t ⊆ s}).Nonempty

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s K : Set α
hKs : K ∈ 𝒫 closure[inst✝] s
⊢ ∀ ⦃x : Set (Set α)⦄,
    x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U} →
      K ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} →
        ({s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∩ {t | t.Finite ∧ t ⊆ s}).Nonempty
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case e'_3
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊
hn : 0 < ↑(n + 1)
⊢ ↑‖k‖₊ = ↑‖k‖₊

pp: case e'_3.hn
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊
hn : 0 < ↑(n + 1)
⊢ n + 1 ≠ 0

Tactic:
]

Goal state after:
case e'_3.hn
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊
hn : 0 < ↑(n + 1)
⊢ n + 1 ≠ 0
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case e'_4
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊
hn : 0 < ↑(n + 1)
⊢ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1)) = ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1))

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
⊢ spectralRadius 𝕜 a ≤ ⨆ i, ⨅ i_1, ↑‖a ^ (i_1 + i)‖₊ ^ (1 / ↑(i_1 + i)) * ε⁻¹

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
⊢ spectralRadius 𝕜 a ≤ ⨆ i, ⨅ i_1, ↑‖a ^ (i_1 + i)‖₊ ^ (1 / ↑(i_1 + i)) * ε⁻¹
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case left
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ :
  (s, t) ∈
    (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹' hausdorffEntourage V
hst : closure[inst✝.toTopologicalSpace] s ⊆ V.preimage (closure[inst✝.toTopologicalSpace] t)
hts : closure[inst✝.toTopologicalSpace] t ⊆ V.image (closure[inst✝.toTopologicalSpace] s)
⊢ V.preimage (V.preimage t) ⊆ V.preimage (V.preimage t)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s K : Set α
hKs : K ∈ 𝒫 closure[inst✝] s
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
ht₁ : K ⊆ ⋃₀ u
ht₂ : ∀ U ∈ u, (K ∩ U).Nonempty
x : ↑u → α
hxU : ∀ (U : ↑u), x U ∈ ↑U
hxs : ∀ (U : ↑u), x U ∈ s
this : Finite ↑u
⊢ ({s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty} ∩ {t | t.Finite ∧ t ⊆ s}).Nonempty

Tactic:
exact ⟨range x, ⟨range_subset_iff.mpr fun V => mem_sUnion_of_mem (hxU V) V.prop,
      fun U hU => ⟨x ⟨U, hU⟩, mem_range_self _, hxU ⟨U, hU⟩⟩⟩,
      finite_range _, range_subset_iff.mpr hxs⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ↑‖1‖₊ ^ (1 / ↑b) ≤ ε⁻¹
n : ℕ
⊢ ↑‖a ^ (n + N + 1)‖₊ ^ (1 / ↑(n + N + 1)) * ε⁻¹ ≤ ↑‖a ^ (n + N + 1)‖₊ ^ (1 / ↑(n + N + 1)) * ε⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformly F f l
hF : ∀ (n : ι), LowerHemicontinuous (F n)
⊢ LowerHemicontinuousOn f univ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformly F f l
hF : ∀ (n : ι), LowerHemicontinuous (F n)
⊢ LowerHemicontinuousOn f univ
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x✝ :
  (∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
⊢ ∀ s ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V},
    IsOpen[inst✝¹] (f ⁻¹' s)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x✝ :
  (∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
⊢ ∀ s ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V},
    IsOpen[inst✝¹] (f ⁻¹' s)