mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : CompleteSpace A
a : A
⊢ ∃ i, True ∧ ∀ ⦃x : 𝕜⦄, x ∈ norm ⁻¹' Set.Ioi i → IsUnit (resolvent a x)

Tactic:
]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
⊢ ∃ i, True ∧ ∀ ⦃x : 𝕜⦄, x ∈ norm ⁻¹' Set.Ioi i → IsUnit (resolvent a x)
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 : ι), UpperHemicontinuous (F n)
hf_compact : ∀ (x : α), IsCompact (f x)
⊢ UpperHemicontinuousOn 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 : ι), UpperHemicontinuous (F n)
hf_compact : ∀ (x : α), IsCompact (f x)
⊢ UpperHemicontinuousOn f univ
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) ∈
    (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.image (V.image s) ⊆ V.image (V.image s)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : ∀ i ∈ 𝓤 α, ∃ x ∈ Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i, x ∈ {s | TotallyBounded s}
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : ∀ i ∈ 𝓤 α, ∃ x ∈ Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i, x ∈ {s | TotallyBounded s}
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}
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
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a ^ n‖₊ * r ^ n ≤ max 1 ‖1‖₊

Tactic:
]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a ^ n‖₊ * r ^ n ≤ max 1 ‖1‖₊
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case succ
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1

Tactic:
]

Goal state after:
case succ
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst✝¹] U → IsOpen[t] {s | (s ∩ U).Nonempty}
⊢ ∀ x ∈ (range fun x ↦ {x})ᶜ, (range fun x ↦ {x})ᶜ ∈ 𝓝 x

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst✝¹] U → IsOpen[t] {s | (s ∩ U).Nonempty}
⊢ ∀ x ∈ (range fun x ↦ {x})ᶜ, (range fun x ↦ {x})ᶜ ∈ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : ∀ i ∈ 𝓤 α, ∃ x ∈ Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i, x ∈ {s | TotallyBounded s}
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
t : Set α
ht : t ∈ {s | TotallyBounded s}
hst : s ⊆ V.preimage t
u : Set α
hu : u.Finite
htu : t ⊆ ⋃ y ∈ u, {x | (x, y) ∈ V}
⊢ V.preimage (⋃ y ∈ u, {x | (x, y) ∈ V}) ⊆ ⋃ y ∈ u, {x | (x, y) ∈ V.comp V}

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : ∀ i ∈ 𝓤 α, ∃ x ∈ Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i, x ∈ {s | TotallyBounded s}
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
t : Set α
ht : t ∈ {s | TotallyBounded s}
hst : s ⊆ V.preimage t
u : Set α
hu : u.Finite
htu : t ⊆ ⋃ y ∈ u, {x | (x, y) ∈ V}
⊢ V.preimage (⋃ y ∈ u, {x | (x, y) ∈ V}) ⊆ ⋃ y ∈ u, {x | (x, y) ∈ V.comp V}
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : r * ‖a‖₊ < 1
n : ℕ
h : ¬‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : r * ‖a‖₊ < 1
n : ℕ
h : ¬‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst✝¹] U → IsOpen[t] {s | (s ∩ U).Nonempty}
hs : ∅ ∈ (range fun x ↦ {x})ᶜ
⊢ ∅ ∈ (range fun x ↦ {x})ᶜ

Tactic:
]

Goal state after:
case inl
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst✝¹] U → IsOpen[t] {s | (s ∩ U).Nonempty}
hs : ∅ ∈ (range fun x ↦ {x})ᶜ
⊢ ∅ ∈ (range fun x ↦ {x})ᶜ
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✝ : DiscreteUniformity α
⊢ SetRel.id ∈ 𝓤 (Set α)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : DiscreteUniformity α
⊢ SetRel.id ∈ 𝓤 (Set α)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : DiscreteUniformity α
⊢ SetRel.id = SetRel.id

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
⊢ (𝓤 β).lift' ((Set.preimage fun x ↦ (f '' x.1, f '' x.2)) ∘ hausdorffEntourage) =
    (𝓤 β).lift' (hausdorffEntourage ∘ Set.preimage fun x ↦ (f x.1, f x.2))

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
⊢ (𝓤 β).lift' ((Set.preimage fun x ↦ (f '' x.1, f '' x.2)) ∘ hausdorffEntourage) =
    (𝓤 β).lift' (hausdorffEntourage ∘ Set.preimage fun x ↦ (f x.1, f x.2))
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case neg
𝕜 : 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‖₊)⁻¹
h : ¬‖a‖₊ = 0
nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹
⊢ ‖y‖₊ < ‖a‖₊⁻¹

Tactic:
]

Goal state after:
case neg
𝕜 : 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‖₊)⁻¹
h : ¬‖a‖₊ = 0
nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹
⊢ ‖y‖₊ < ‖a‖₊⁻¹
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst✝¹] U → IsOpen[t] {s | (s ∩ U).Nonempty}
s : Set α
hs : s ∈ (range fun x ↦ {x})ᶜ
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
U V : Set α
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
hxU : x ∈ U
hyV : y ∈ V
hUV : Disjoint U V
z : α
hzU : z ∈ U
hzV : z ∈ V
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst✝¹] U → IsOpen[t] {s | (s ∩ U).Nonempty}
s : Set α
hs : s ∈ (range fun x ↦ {x})ᶜ
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
U V : Set α
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
hxU : x ∈ U
hyV : y ∈ V
hUV : Disjoint U V
z : α
hzU : z ∈ U
hzV : z ∈ V
⊢ False
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst✝¹] U → IsOpen[t] {s | (s ∩ U).Nonempty}
s : Set α
hs : s ∈ (range fun x ↦ {x})ᶜ
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
U V : Set α
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
hxU : x ∈ U
hyV : y ∈ V
hUV : Disjoint U V
z : α
hzU : (fun x ↦ {x}) z ∈ {s | (s ∩ U).Nonempty}
hzV : (fun x ↦ {x}) z ∈ {s | (s ∩ V).Nonempty}
⊢ False

Tactic:
rw [Set.mem_ofPred, Set.singleton_inter_nonempty] at hzU hzV

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst✝¹] U → IsOpen[t] {s | (s ∩ U).Nonempty}
s : Set α
hs : s ∈ (range fun x ↦ {x})ᶜ
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
U V : Set α
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
hxU : x ∈ U
hyV : y ∈ V
hUV : Disjoint U V
z : α
hzU : z ∈ U
hzV : z ∈ V
⊢ False
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
a : A
z : 𝕜
h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
hu : IsUnit (1 - u • a)
⊢ IsUnit (1 - z • a)

Tactic:
]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
hu : IsUnit (1 - u • a)
⊢ IsUnit (1 - z • a)
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
⊢ ↑u⁻¹ ∈ resolventSet 𝕜 a

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
⊢ ↑u⁻¹ ∈ resolventSet 𝕜 a
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
⊢ ↑‖↑(Units.mk0 z hz)‖₊ < (spectralRadius 𝕜 a)⁻¹

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
⊢ ↑‖↑(Units.mk0 z hz)‖₊ < (spectralRadius 𝕜 a)⁻¹
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsOpen[instTopologicalSpaceProd] U
this✝ : U.IsRefl
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : IsOpen[instTopologicalSpaceProd] V
left✝ : V.IsSymm
hVU : V.comp V ⊆ U
t : Finset α
ht₁ : ↑t ⊆ V.preimage s
ht₂ : s ⊆ V.image ↑t
u : Set α
hu : ↑t ⊆ V.preimage u
⊢ V.preimage (V.preimage u) ⊆ V.preimage (V.preimage u)

Tactic:
]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
⊢ exp a = exp a

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 γ
inst✝ : CompactSpace α
⊢ ∀ (f : Ultrafilter (Set α)), ↑f ≤ 𝓟 Set.univ → ∃ x ∈ Set.univ, ↑f ≤ 𝓝 x

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompactSpace α
⊢ ∀ (f : Ultrafilter (Set α)), ↑f ≤ 𝓟 Set.univ → ∃ x ∈ Set.univ, ↑f ≤ 𝓝 x
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✝ : CompactSpace α
f : Ultrafilter (Set α)
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
⊢ 𝓝 f.lim ≤ 𝓝 f.lim

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
⊢ IsClosed (SetLike.coe ⁻¹' Set.range (SetLike.coe ∘ fun x ↦ {x}))

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
⊢ IsClosed (SetLike.coe ⁻¹' Set.range (SetLike.coe ∘ fun x ↦ {x}))
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F₁ F₂ : Closeds α
h : Inseparable F₁ F₂
x : α
hx₁ : x ∈ F₁
⊢ ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∃ x_1 ∈ U, ∃ a, (x, a) = x_1 ∧ a ∈ ↑F₂

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F₁ F₂ : Closeds α
h : Inseparable F₁ F₂
x : α
hx₁ : x ∈ F₁
⊢ ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∃ x_1 ∈ U, ∃ a, (x, a) = x_1 ∧ a ∈ ↑F₂
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
n : ℕ
hn : n ≠ 0
⊢ ‖(a - ↑ₐ z) ^ n‖ / ↑(n + 1).factorial ≤ ‖a - ↑ₐ z‖ ^ n / ↑n.factorial

Tactic:
]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
n : ℕ
hn : n ≠ 0
⊢ ‖(a - ↑ₐ z) ^ n‖ / ↑(n + 1).factorial ≤ ‖a - ↑ₐ z‖ ^ n / ↑n.factorial
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 : ∀ i' ∈ 𝓤 α, Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id i') ∈ f.curry f
⊢ ∃ x, f ≤ 𝓝 x

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 : ∀ i' ∈ 𝓤 α, Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id i') ∈ f.curry f
⊢ ∃ x, f ≤ 𝓝 x
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
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

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
⊢ ∃ 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
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : ↑K ⊆ V.preimage t
⊢ ∃ t, t.Finite ∧ U.preimage t ∈ 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
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : ↑K ⊆ V.preimage t
⊢ ∃ t, t.Finite ∧ U.preimage t ∈ l
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n ↦ (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
⊢ (fun x ↦ ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b

Tactic:
]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n ↦ (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
⊢ (fun x ↦ ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b
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
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : ↑K ⊆ V.preimage t
⊢ ∀ i ∈ {x | (fun K' ↦ (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}, ↑i ⊆ U.preimage t

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
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : ↑K ⊆ V.preimage t
⊢ ∀ i ∈ {x | (fun K' ↦ (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}, ↑i ⊆ U.preimage t
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} ⊆ {x | (x ∩ L).Nonempty}

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} ⊆ {x | (x ∩ L).Nonempty}
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
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : ↑K ⊆ V.preimage t
⊢ ∀ i ∈ {x | (fun K' ↦ (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}, ↑i ⊆ U.preimage t

Tactic:
intro K' ⟨_, (hK' : ↑K' ⊆ V.preimage K)⟩

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
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : ↑K ⊆ V.preimage t
K' : Compacts α
left✝ : (↑K, ↑K').1 ⊆ SetRel.preimage (Prod.swap ⁻¹' V) (↑K, ↑K').2
hK' : ↑K' ⊆ V.preimage ↑K
⊢ ↑K' ⊆ U.preimage t