mathlib-initiative/mathlib-tactics huggingface dataset:
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₀ : α
hx₀s : x₀ ∈ s
u : Set β
hu : IsOpen[inst✝.toTopologicalSpace] u
hx₀u : f x₀ ⊆ u
W : Set (β × β)
hW : W ∈ uniformity β
left✝ : IsOpen[instTopologicalSpaceProd] W
hWu : ∀ x ∈ f x₀, ball x W ⊆ u
V : Set (β × β)
hV : V ∈ uniformity β
hVsym : SetRel.IsSymm V
hVcomp : SetRel.comp V V ⊆ W
U : SetRel β β
hUsub : id U ⊆ V
hUmem : U ∈ uniformity β
hUopen : IsOpen[instTopologicalSpaceProd] U
hHU : hausdorffEntourage U ∈ uniformity (Set β)
N : ι
hN : ∀ x ∈ s, (f x, F N x) ∈ hausdorffEntourage U
hFN_image : F N x₀ ⊆ U.image (f x₀)
⊢ ∀ᶠ (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₀ : α
hx₀s : x₀ ∈ s
u : Set β
hu : IsOpen[inst✝.toTopologicalSpace] u
hx₀u : f x₀ ⊆ u
W : Set (β × β)
hW : W ∈ uniformity β
left✝ : IsOpen[instTopologicalSpaceProd] W
hWu : ∀ x ∈ f x₀, ball x W ⊆ u
V : Set (β × β)
hV : V ∈ uniformity β
hVsym : SetRel.IsSymm V
hVcomp : SetRel.comp V V ⊆ W
U : SetRel β β
hUsub : id U ⊆ V
hUmem : U ∈ uniformity β
hUopen : IsOpen[instTopologicalSpaceProd] U
hHU : hausdorffEntourage U ∈ uniformity (Set β)
N : ι
hN : ∀ x ∈ s, (f x, F N x) ∈ hausdorffEntourage U
hFN_image : F N x₀ ⊆ U.image (f x₀)
⊢ ∀ᶠ (x' : α) in 𝓝[s] x₀, f x' ⊆ u
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
⊢ 𝓝 (closure[inst✝.toTopologicalSpace] s) = 𝓝 s

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
⊢ 𝓝 (closure[inst✝.toTopologicalSpace] s) = 𝓝 s
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] {s | TotallyBounded s}

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] {s | TotallyBounded s}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inr
α : 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)
U : Set β
hU : U ∈ {V | IsOpen[inst✝] V}
⊢ IsOpen[inst✝¹] (f ⁻¹' {s | (s ∩ U).Nonempty})

Tactic:
[

Goal state after:
case inr
α : 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)
U : Set β
hU : U ∈ {V | IsOpen[inst✝] V}
⊢ IsOpen[inst✝¹] (f ⁻¹' {s | (s ∩ U).Nonempty})
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ inst✝ = induced (fun x ↦ {x}) (TopologicalSpace.vietoris α)

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ inst✝ = induced (fun x ↦ {x}) (TopologicalSpace.vietoris α)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : UniformContinuous f
U : Set (β × β)
hU : U ∈ 𝓤 β
s t : Set α
h₁ : (s, t).1 ⊆ SetRel.preimage ((fun x ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).2
h₂ : (s, t).2 ⊆ SetRel.image ((fun x ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).1
⊢ (f '' s, f '' t) ∈ hausdorffEntourage U

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : UniformContinuous f
U : Set (β × β)
hU : U ∈ 𝓤 β
s t : Set α
h₁ : (s, t).1 ⊆ SetRel.preimage ((fun x ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).2
h₂ : (s, t).2 ⊆ SetRel.image ((fun x ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).1
⊢ (f '' s, f '' t) ∈ hausdorffEntourage U
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
t : Set α
ht : TotallyBounded t
⊢ TotallyBounded (𝒫 t)

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
t : Set α
ht : TotallyBounded t
⊢ TotallyBounded (𝒫 t)
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ Metric.eball 0 (↑‖a‖₊)⁻¹
⊢ HasSum (fun n ↦ (ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) fun x ↦ y) (Ring.inverse (1 - (0 + y) • a))

Tactic:
by
      have norm_lt : ‖y • a‖ < 1 := by
        by_cases h : ‖a‖₊ = 0
        · simp only [nnnorm_eq_zero.mp h, norm_zero, zero_lt_one, smul_zero]
        · have nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹ := by
            simpa only [← coe_inv h, mem_ball_zero_iff, Metric.eball_coe] using! hy
          rwa [← coe_nnnorm, ← Real.lt_toNNReal_iff_coe_lt, Real.toNNReal_one, nnnorm_smul,
            ← NNReal.lt_inv_iff_mul_lt h]
      simpa [← smul_pow, (summable_geometric_of_norm_lt_one norm_lt).hasSum_iff] using!
        (NormedRing.inverse_one_sub _ norm_lt).symm

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
⊢ 𝓝 s ≤ 𝓝 s

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
⊢ 𝓝 s ≤ 𝓝 s
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.vietoris α] fun x ↦ x.1 ∪ x.2

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.vietoris α] fun x ↦ x.1 ∪ x.2
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_4
inst✝ : Finite ι
⊢ Continuous[Pi.topologicalSpace, TopologicalSpace.vietoris α] range

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_4
inst✝ : Finite ι
⊢ Continuous[Pi.topologicalSpace, TopologicalSpace.vietoris α] range
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : IsCompact s
⊢ 𝓝 s ≤ 𝓝 s

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : IsCompact s
⊢ 𝓝 s ≤ 𝓝 s
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
⊢ Continuous[TopologicalSpace.vietoris α, TopologicalSpace.vietoris β] fun x ↦ f '' x

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
⊢ Continuous[TopologicalSpace.vietoris α, TopologicalSpace.vietoris β] fun x ↦ f '' x
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
x✝ : CompactSpace (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst✝.toTopologicalSpace] (F i)
hF₂ : ⋂ i, F i = ∅
this : {⊥}ᶜ ∩ ⋂ i, {C | ↑C ⊆ F i} = ∅ → ∃ u, {⊥}ᶜ ∩ ⋂ i ∈ u, {C | ↑C ⊆ F i} = ∅
⊢ ∃ u, ⋂ i ∈ u, F i = ∅

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
x✝ : CompactSpace (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst✝.toTopologicalSpace] (F i)
hF₂ : ⋂ i, F i = ∅
this : {⊥}ᶜ ∩ ⋂ i, {C | ↑C ⊆ F i} = ∅ → ∃ u, {⊥}ᶜ ∩ ⋂ i ∈ u, {C | ↑C ⊆ F i} = ∅
⊢ ∃ u, ⋂ i ∈ u, F i = ∅
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
x✝ : CompactSpace (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst✝.toTopologicalSpace] (F i)
hF₂ : ⋂ i, F i = ∅
this : Disjoint {⊥}ᶜ (⋂ i, {C | ↑C ⊆ F i}) → ∃ u, Disjoint {⊥}ᶜ (⋂ i ∈ u, {C | ↑C ⊆ F i})
⊢ ∃ u, ⋂ i ∈ u, F i = ∅

Tactic:
Set.disjoint_compl_left_iff_subset,

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
x✝ : CompactSpace (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst✝.toTopologicalSpace] (F i)
hF₂ : ⋂ i, F i = ∅
this : ⋂ i, {C | ↑C ⊆ F i} ⊆ {⊥} → ∃ u, ⋂ i ∈ u, {C | ↑C ⊆ F i} ⊆ {⊥}
⊢ ∃ u, ⋂ i ∈ u, F i = ∅
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
this : {U | IsOpen[inst✝¹] U} = (fun x ↦ f ⁻¹' x) '' {V | IsOpen[inst✝] V}
⊢ TopologicalSpace.vietoris α = induced (fun x ↦ f '' x) (TopologicalSpace.vietoris β)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
this : {U | IsOpen[inst✝¹] U} = (fun x ↦ f ⁻¹' x) '' {V | IsOpen[inst✝] V}
⊢ TopologicalSpace.vietoris α = induced (fun x ↦ f '' x) (TopologicalSpace.vietoris β)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
⊢ NoncompactSpace (Closeds α) ↔ NoncompactSpace α

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
⊢ NoncompactSpace (Closeds α) ↔ NoncompactSpace α
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
K : Compacts α
⊢ 𝓝 K = 𝓝 K

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
K : Compacts α
⊢ 𝓝 K = 𝓝 K
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case pos
α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS : S ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hKS : {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U | IsOpen[inst✝] U ∧ {s | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hLT : L ⊆ ⋃ i ∈ T, i
⊢ {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ ((fun U ↦ {s | (s ∩ U).Nonempty}) '' T)

Tactic:
[

Goal state after:
case pos
α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS : S ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hKS : {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U | IsOpen[inst✝] U ∧ {s | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hLT : L ⊆ ⋃ i ∈ T, i
⊢ {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ ((fun U ↦ {s | (s ∩ U).Nonempty}) '' T)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case neg
α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS : S ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hKS : {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U | IsOpen[inst✝] U ∧ {s | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ L ∈ s, ¬L ⊆ ⋃₀ u
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
[

Goal state after:
case neg
α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS : S ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hKS : {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U | IsOpen[inst✝] U ∧ {s | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ L ∈ s, ¬L ⊆ ⋃₀ u
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
⊢ f ≤ 𝓝 L

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
⊢ f ≤ 𝓝 L
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
⊢ K ∈ (fun y ↦ (y, L)) ⁻¹' Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id U)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
⊢ K ∈ (fun y ↦ (y, L)) ⁻¹' Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id U)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
⊢ s ⤳ t

Tactic:
[

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
⊢ s ⤳ t
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
U : Set α
hU : U ∈ {U | IsOpen[inst✝] U}
hs : t ∈ (fun V ↦ {s | (s ∩ V).Nonempty}) U
⊢ ⨅
      s_1 ∈
        {s_2 |
          s ∈ s_2 ∧
            s_2 ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}},
      Filter.principal s_1 ≤
    Filter.principal ((fun V ↦ {s | (s ∩ V).Nonempty}) U)

Tactic:
· obtain ⟨x, hxt, hxU⟩ := hs
      obtain ⟨y, hyU, hys⟩ := mem_closure_iff.mp (hts hxt) U hU hxU
      exact iInf₂_le {t | (t ∩ U).Nonempty} ⟨⟨y, hys, hyU⟩, .inr <| mem_image_of_mem _ hU⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s t : Set α
inst✝ : T1Space α
⊢ s ⤳ t ↔ s ⊆ t ∧ t ⊆ closure[inst✝¹] s

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
s t : Set α
inst✝ : T1Space α
⊢ s ⤳ t ↔ s ⊆ t ∧ t ⊆ closure[inst✝¹] s
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
x : α
hx : x ∈ s
this : {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s} = ⋃ n, range '' univ.pi fun x ↦ s
⊢ IsPreconnected {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s}

Tactic:
this

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
x : α
hx : x ∈ s
this : {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s} = ⋃ n, range '' univ.pi fun x ↦ s
⊢ IsPreconnected (⋃ n, range '' univ.pi fun x ↦ 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 γ
K : NonemptyCompacts α
⊢ 𝓝 K = 𝓝 K

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
K : NonemptyCompacts α
⊢ 𝓝 K = 𝓝 K
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsClosed {K | ↑K ⊆ F}

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsClosed {K | ↑K ⊆ F}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsClosed {K | (↑K ∩ F).Nonempty}

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsClosed {K | (↑K ∩ F).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ u ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B}, IsOpen u

Tactic:
[

Goal state after:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ u ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B}, IsOpen u
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀
    u ∈
      preimage SetLike.coe ''
        (fun p ↦ {s | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
          {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1},
    ∀ x ∈ u, ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B}, x ∈ v ∧ v ⊆ u

Tactic:
[

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀
    u ∈
      preimage SetLike.coe ''
        (fun p ↦ {s | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
          {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1},
    ∀ x ∈ u, ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B}, x ∈ v ∧ v ⊆ u
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
this : CompleteSpace ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 ↑x)
⊢ frontier (σ 𝕜 ↑x)ᶜ ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∪
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 ↑x)ᶜ ∩ frontier (σ 𝕜 x) ⊆
    frontier (σ 𝕜 ↑x)

Tactic:
inter_subset_left,

Goal state after:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
this : CompleteSpace ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 ↑x)
⊢ frontier (σ 𝕜 ↑x)ᶜ ∪ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 ↑x)ᶜ ∩ frontier (σ 𝕜 x) ⊆
    frontier (σ 𝕜 ↑x)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
⊢ IsOpen {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}

Tactic:
[

Goal state after:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
⊢ IsOpen {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁶ : NormedRing A
inst✝⁵ : CompleteSpace A
inst✝⁴ : SetLike SA A
inst✝³ : SubringClass SA A
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
this : σ 𝕜 x \ σ 𝕜 ↑x = ∅
⊢ σ 𝕜 ↑x ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 ↑x, connectedComponentIn (σ 𝕜 ↑x)ᶜ z = σ 𝕜 ↑x

Tactic:
this

Goal state after:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁶ : NormedRing A
inst✝⁵ : CompleteSpace A
inst✝⁴ : SetLike SA A
inst✝³ : SubringClass SA A
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
this : σ 𝕜 x \ σ 𝕜 ↑x = ∅
⊢ σ 𝕜 ↑x ∪ ⋃ z ∈ ∅, connectedComponentIn (σ 𝕜 ↑x)ᶜ z = σ 𝕜 ↑x
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case a
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst✝⁶ : NormedField 𝕜₁
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜₁ A
inst✝² : NormedAlgebra 𝕜₂ A
inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂
inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊
⊢ ⨆ k ∈ spectrum 𝕜₁ a, ↑‖k‖₊ ≤ ⨆ k ∈ spectrum 𝕜₂ a, ↑‖k‖₊

pp: case a
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst✝⁶ : NormedField 𝕜₁
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜₁ A
inst✝² : NormedAlgebra 𝕜₂ A
inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂
inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊
⊢ ⨆ k ∈ spectrum 𝕜₂ a, ↑‖k‖₊ ≤ ⨆ k ∈ spectrum 𝕜₁ a, ↑‖k‖₊

Tactic:
all_goals apply iSup₂_le fun x hx ↦ ?_

Goal state after:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst✝⁶ : NormedField 𝕜₁
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜₁ A
inst✝² : NormedAlgebra 𝕜₂ A
inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂
inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊
x : 𝕜₁
hx : x ∈ spectrum 𝕜₁ a
⊢ ↑‖x‖₊ ≤ ⨆ k ∈ spectrum 𝕜₂ a, ↑‖k‖₊

𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst✝⁶ : NormedField 𝕜₁
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜₁ A
inst✝² : NormedAlgebra 𝕜₂ A
inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂
inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊
x : 𝕜₂
hx : x ∈ spectrum 𝕜₂ a
⊢ ↑‖x‖₊ ≤ ⨆ k ∈ spectrum 𝕜₁ a, ↑‖k‖₊
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
y : ℝ≥0
hy : ↑y ∈ spectrum ℝ a
hx : ↑t - ↑y ∈ {↑t} - spectrum ℝ a
hty : -↑t ≤ ↑y
hyt : ↑y ≤ ↑t
⊢ y ≤ t

Tactic:
by exact_mod_cast hyt

Goal state after: