mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : T2Space A
f : ℂ → ℂ
a : A
hf_real : ∀ x ∈ σ ℂ a, star (f x) = f x
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σ ℂ a
⊢ f x = ↑(f ↑x.re).re

Tactic:
[

Goal state after:
A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : T2Space A
f : ℂ → ℂ
a : A
hf_real : ∀ x ∈ σ ℂ a, star (f x) = f x
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σ ℂ a
⊢ f x = ↑(f ↑x.re).re
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
f : ℂ → ℂ
a : A
hf_real : ∀ x ∈ σₙ ℂ a, star (f x) = f x
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σₙ ℂ a
⊢ f x = ↑(f ↑x.re).re

Tactic:
[

Goal state after:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
f : ℂ → ℂ
a : A
hf_real : ∀ x ∈ σₙ ℂ a, star (f x) = f x
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σₙ ℂ a
⊢ f x = ↑(f ↑x.re).re
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: r : ℝ
s : Set ℂ
hs₁ : {z | z.im < r} ⊆ s
hs₂ : s ⊆ {z | z.im ≤ r}
⊢ IsConnected {z | z.im < r}

Tactic:
exact (convex_halfSpace_im_lt r).isConnected ⟨(r - 1) * I, by simp⟩

Goal state after:
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: z w : ℂ
⊢ z.Rectangle w = (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}

Tactic:
[

Goal state after:
z w : ℂ
⊢ z.Rectangle w = (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}
Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula

Goal state before:
pp: A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
⊢ ↑r ≤ (limsup (fun n ↦ ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop)⁻¹

Tactic:
[

Goal state after:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
⊢ ↑r ≤ (limsup (fun n ↦ ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop)⁻¹
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, (↑K ∩ U).Nonempty
w : Set (Set α)
hKV : ↑K ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, (↑K ∩ W).Nonempty
hw : w.Finite
huw : u ⊆ w
⊢ ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
    K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
rw [exists_mem_image]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, (↑K ∩ U).Nonempty
w : Set (Set α)
hKV : ↑K ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, (↑K ∩ W).Nonempty
hw : w.Finite
huw : u ⊆ w
⊢ ∃ x ∈ {u | u.Finite ∧ u ⊆ B},
    K ∈ {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty} ∧
      {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty} ⊆ SetLike.coe ⁻¹' {s | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
⊢ Continuous fun p ↦ p.1 ⊔ p.2

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
⊢ Continuous fun p ↦ p.1 ⊔ p.2
Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula

Goal state before:
pp: A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
n : ℕ
⊢ spectrum ℂ (a ^ n) = (fun x ↦ x ^ n) '' spectrum ℂ a

Tactic:
by
  simpa only [aeval_X_pow, eval_X_pow] using map_polynomial_aeval a (X ^ n)

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x : Unitization ℂ A
this : ∀ {s : Unitization ℂ A}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊
⊢ ‖ψ x‖₊ * ‖ψ x‖₊ ≤ ‖x‖₊ * ‖x‖₊

Tactic:
[

Goal state after:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x : Unitization ℂ A
this : ∀ {s : Unitization ℂ A}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊
⊢ ‖ψ x‖₊ * ‖ψ x‖₊ ≤ ‖x‖₊ * ‖x‖₊
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {V | IsOpen[instTopologicalSpaceProd] V}
K : Compacts α
L : Compacts β
x : α
y : β
hx : x ∈ K
hy : y ∈ L
hxy : (x, y) ∈ U
V : Set α
W : Set β
hV : IsOpen[inst✝¹] V
hW : IsOpen[inst✝] W
hxV : x ∈ V
hyW : y ∈ W
hVW : V ×ˢ W ⊆ U
⊢ ∃ t ⊆ {a | ((SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) a ∩ V ×ˢ W).Nonempty}, IsOpen t ∧ (K, L) ∈ t

Tactic:
[

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {V | IsOpen[instTopologicalSpaceProd] V}
K : Compacts α
L : Compacts β
x : α
y : β
hx : x ∈ K
hy : y ∈ L
hxy : (x, y) ∈ U
V : Set α
W : Set β
hV : IsOpen[inst✝¹] V
hW : IsOpen[inst✝] W
hxV : x ∈ V
hyW : y ∈ W
hVW : V ×ˢ W ⊆ U
⊢ ∃ t ⊆ {a | ((SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) a ∩ V ×ˢ W).Nonempty}, IsOpen t ∧ (K, L) ∈ t
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : DiscreteTopology α
K : Compacts α
⊢ {K} = {K_1 | ↑K_1 ⊆ ↑K} ∩ ⋂ i ∈ ↑K, {K | (↑K ∩ {i}).Nonempty}

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : DiscreteTopology α
K : Compacts α
⊢ {K} = {K_1 | ↑K_1 ⊆ ↑K} ∩ ⋂ i ∈ ↑K, {K | (↑K ∩ {i}).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
h' : ∃ x ∈ K₁, x ∉ K₂
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := h'

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
x : α
hx₁ : x ∈ K₁
hx₂ : x ∉ K₂
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
⊢ RegularSpace (Compacts α)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
⊢ RegularSpace (Compacts α)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
hK : K ∈ (fun a ↦ {a_1 | ↑a_1 ⊆ a}) U
V W : Set α
hV : IsOpen[inst✝³] V
hW : IsOpen[inst✝³] W
hKV : ↑K ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ {K | (↑K ∩ W).Nonempty} ∈ 𝓝ˢ {a | ↑a ⊆ U}ᶜ

Tactic:
[

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
hK : K ∈ (fun a ↦ {a_1 | ↑a_1 ⊆ a}) U
V W : Set α
hV : IsOpen[inst✝³] V
hW : IsOpen[inst✝³] W
hKV : ↑K ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ {K | (↑K ∩ W).Nonempty} ∈ 𝓝ˢ {a | ↑a ⊆ U}ᶜ
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
x : α
hx₁ : x ∈ ↑K
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst✝³] V
hW : IsOpen[inst✝³] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ {K | ↑K ⊆ W} ∈ 𝓝ˢ {a | (↑a ∩ U).Nonempty}ᶜ

Tactic:
[

Goal state after:
case inr.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
x : α
hx₁ : x ∈ ↑K
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst✝³] V
hW : IsOpen[inst✝³] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ {K | ↑K ⊆ W} ∈ 𝓝ˢ {a | (↑a ∩ U).Nonempty}ᶜ
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
h : ∀ i ∈ S, ↑i ⊆ ⋃ i, U i
s : Finset (Finset ι)
hs : S ⊆ ⋃ i ∈ s, {K | ↑K ⊆ ⋃ i_1 ∈ i, U i_1}
⊢ ⋃ x ∈ ⋃ i ∈ s, {K | ↑K ⊆ ⋃ i_1 ∈ i, U i_1}, ↑x ⊆ ⋃ i ∈ s.biUnion id, U i

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
h : ∀ i ∈ S, ↑i ⊆ ⋃ i, U i
s : Finset (Finset ι)
hs : S ⊆ ⋃ i ∈ s, {K | ↑K ⊆ ⋃ i_1 ∈ i, U i_1}
⊢ ⋃ x ∈ ⋃ i ∈ s, {K | ↑K ⊆ ⋃ i_1 ∈ i, U i_1}, ↑x ⊆ ⋃ i ∈ s.biUnion id, U i
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
h : CompactSpace (Compacts α)
⊢ ⋃ K ∈ univ, ↑K = univ

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
h : CompactSpace (Compacts α)
⊢ ⋃ K ∈ univ, ↑K = univ
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ NoncompactSpace (Compacts α) ↔ NoncompactSpace α

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ NoncompactSpace (Compacts α) ↔ NoncompactSpace α
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ {a | (↑a).Nonempty} ∩ {a | ↑a ⊆ s} ⊆ closure ({a | (↑a).Nonempty} ∩ {a | (↑a).Finite ∧ ↑a ⊆ s})

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ {a | (↑a).Nonempty} ∩ {a | ↑a ⊆ s} ⊆ closure ({a | (↑a).Nonempty} ∩ {a | (↑a).Finite ∧ ↑a ⊆ s})
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = ⇑f
⊢ Tendsto f' (cocompact α) (𝓝 0)

Tactic:
[

Goal state after:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = ⇑f
⊢ Tendsto f' (cocompact α) (𝓝 0)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
⊢ IsPreconnected ({K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty} ∩ {K | (↑K).Finite})

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
⊢ IsPreconnected ({K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty} ∩ {K | (↑K).Finite})
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this✝ : Fintype ↑u := hu'.fintype
this :
  {K | ↑K ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑K ∩ U).Nonempty) ∧ (↑K).Finite} =
    Finset.univ.sup '' univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}
⊢ IsPreconnected {a | ↑a ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑a ∩ U).Nonempty) ∧ (↑a).Finite}

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this✝ : Fintype ↑u := hu'.fintype
this :
  {K | ↑K ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑K ∩ U).Nonempty) ∧ (↑K).Finite} =
    Finset.univ.sup '' univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}
⊢ IsPreconnected (Finset.univ.sup '' univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U})
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp (z • star b) * (NormedSpace.exp (-(star z • b)) * x * NormedSpace.exp (star z • a)) *
      NormedSpace.exp (z • star (-a)) =
    ↑(expUnitary (2 • ℑ (z • star b))) * x * ↑(expUnitary (2 • ℑ (star z • a)))

Tactic:
[

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp (z • star b) * (NormedSpace.exp (-(star z • b)) * x * NormedSpace.exp (star z • a)) *
      NormedSpace.exp (z • star (-a)) =
    ↑(expUnitary (2 • ℑ (z • star b))) * x * ↑(expUnitary (2 • ℑ (star z • a)))
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this : Fintype ↑u := ⋯
⊢ (Finset.univ.sup '' univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}) ⊆
    {K | ↑K ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑K ∩ U).Nonempty) ∧ (↑K).Finite}

Tactic:
[

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this : Fintype ↑u := ⋯
⊢ (Finset.univ.sup '' univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}) ⊆
    {K | ↑K ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑K ∩ U).Nonempty) ∧ (↑K).Finite}
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : IsStarNormal a
x : ℝ
hcomm : Commute (x • a) (-x • star a)
⊢ NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) = ↑(expUnitary (x • 2 • ℑ a))

Tactic:
rw [← exp_add_of_commute hcomm]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : IsStarNormal a
x : ℝ
hcomm : Commute (x • a) (-x • star a)
⊢ NormedSpace.exp (x • a + -x • star a) = ↑(expUnitary (x • 2 • ℑ a))
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
x : E
⊢ x ∈ (absConvexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → AbsConvex 𝕜 t → x ∈ t

Tactic:
[

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
x : E
⊢ x ∈ (absConvexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → AbsConvex 𝕜 t → x ∈ t
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: case e'_3
A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A
x : ℝ
u : ↥(unitary A) := ⟨NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a), ⋯⟩
⊢ NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a) = ↑u⁻¹

Tactic:
[

Goal state after:
case e'_3
A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A
x : ℝ
u : ↥(unitary A) := ⟨NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a), ⋯⟩
⊢ NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a) = ↑u⁻¹
Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ {y | (gaugeSeminorm ⋯ ⋯ ⋯) y < 1} = ↑s

Tactic:
[

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ {y | (gaugeSeminorm ⋯ ⋯ ⋯) y < 1} = ↑s
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.Nonempty ∧ 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.Nonempty ∧ 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 toCompacts '' (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
    ∀ x ∈ u,
      ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u.Nonempty ∧ 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 toCompacts '' (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
    ∀ x ∈ u,
      ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u.Nonempty ∧ u ⊆ B}, x ∈ v ∧ v ⊆ u
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a✝ : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a✝) * NormedSpace.exp (-x • star a✝) ∈ unitary A
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a✝) * NormedSpace.exp (x • star a✝) =
      NormedSpace.exp (x • star a✝) * NormedSpace.exp (-x • a✝)
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
a b : A
⊢ deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • a) * 1 * NormedSpace.exp (x • b)) y) 0 =
    a ^ 2 + 2 • (a * b) + b ^ 2

Tactic:
[

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a✝ : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a✝) * NormedSpace.exp (-x • star a✝) ∈ unitary A
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a✝) * NormedSpace.exp (x • star a✝) =
      NormedSpace.exp (x • star a✝) * NormedSpace.exp (-x • a✝)
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
a b : A
⊢ deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • a) * 1 * NormedSpace.exp (x • b)) y) 0 =
    a ^ 2 + 2 • (a * b) + b ^ 2
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
K : NonemptyCompacts α
hK₁ : ↑K.toCompacts ⊆ ⋃₀ u
hK₂ : ∀ U ∈ u, (↑K.toCompacts ∩ U).Nonempty
hu' : u.Nonempty
⊢ ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u.Nonempty ∧ u ⊆ B},
    K ∈ v ∧ v ⊆ toCompacts ⁻¹' {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}

Tactic:
rw [exists_mem_image]

Goal state after:
case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
K : NonemptyCompacts α
hK₁ : ↑K.toCompacts ⊆ ⋃₀ u
hK₂ : ∀ U ∈ u, (↑K.toCompacts ∩ U).Nonempty
hu' : u.Nonempty
⊢ ∃ x ∈ {u | u.Finite ∧ u.Nonempty ∧ u ⊆ B},
    K ∈ {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty} ∧
      {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty} ⊆ toCompacts ⁻¹' {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ Continuous fun p ↦ p.1 ×ˢ p.2

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ Continuous fun p ↦ p.1 ×ˢ p.2