mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
x : α
hf : UpperHemicontinuousAt f x
hg : UpperHemicontinuousAt g x
⊢ UpperHemicontinuousAt (fun x ↦ f x ∪ g x) x

Tactic:
by
  rw [← upperHemicontinuousWithinAt_univ_iff] at hf hg ⊢
  exact hf.union hg

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
x : α
hf : ∀ (u : Set β), IsOpen[inst✝] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
u : Set β
hu : IsClosed[inst✝] u
t : Set β
⊢ IsOpen[inst✝] t → f x ∩ u ⊆ t → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ u ⊆ t

Tactic:
ht_open

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
x : α
hf : ∀ (u : Set β), IsOpen[inst✝] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
u : Set β
hu : IsClosed[inst✝] u
t : Set β
ht_open : IsOpen[inst✝] t
⊢ f x ∩ u ⊆ t → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ u ⊆ t
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h✝ : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U | IsOpen[inst✝] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U | IsOpen[inst✝] U}
v : Set (Set α)
hv₁ : v ⊆ {U | IsOpen[inst✝] U}
hv₂ : v.Finite
hv : (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}
ht₁ : (powerset '' u).Finite ∧ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' v).Finite
ht₂ :
  powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hs : s ∈ ⋂₀ (powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v)
U : Set α := ⋂₀ u
⊢ ∃ x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
    s ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∧
      {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ (powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v)

Tactic:
have hU : IsOpen U := hu₂.isOpen_sInter hu₁

Goal state after:
case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h✝ : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U | IsOpen[inst✝] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U | IsOpen[inst✝] U}
v : Set (Set α)
hv₁ : v ⊆ {U | IsOpen[inst✝] U}
hv₂ : v.Finite
hv : (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}
ht₁ : (powerset '' u).Finite ∧ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' v).Finite
ht₂ :
  powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hs : s ∈ ⋂₀ (powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v)
U : Set α := ⋂₀ u
hU : IsOpen[inst✝] U
⊢ ∃ x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
    s ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∧
      {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ (powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : 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
U : Set α
hU : U ∈ u
⊢ ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty

Tactic:
obtain ⟨x, hxs, hxU⟩ := hs₂ U hU

Goal state after:
α : 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
U : Set α
hU : U ∈ u
x : α
hxs : x ∈ s
hxU : x ∈ U
⊢ ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ UniformContinuous fun x ↦ x.1 ×ˢ x.2

Tactic:
refine (𝓤 α).basis_sets.uniformity_prod (𝓤 β).basis_sets |>.lift' monotone_hausdorffEntourage
    |>.tendsto_right_iff.mpr fun ⟨U, V⟩ ⟨hU, hV⟩ => ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
x✝¹ : Set (α × α) × Set (β × β)
U : Set (α × α)
V : Set (β × β)
x✝ : (U, V).1 ∈ 𝓤 α ∧ (U, V).2 ∈ 𝓤 β
hU : (U, V).1 ∈ 𝓤 α
hV : (U, V).2 ∈ 𝓤 β
⊢ ∀ᶠ (x : (Set α × Set β) × Set α × Set β) in 𝓤 (Set α × Set β),
    ((fun x ↦ x.1 ×ˢ x.2) x.1, (fun x ↦ x.1 ×ˢ x.2) x.2) ∈
      (hausdorffEntourage ∘ fun i ↦ entourageProd (id i.1) (id i.2)) (U, V)
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 + 1)‖₊ * r ^ (n + 1) ≤ max 1 ‖1‖₊

Tactic:
grw [nnnorm_pow_le' a n.succ_pos, ← le_max_left]
        by_cases h : ‖a‖₊ = 0
        · simp [h, pow_succ']
        · rw [← coe_inv h, coe_lt_coe, NNReal.lt_inv_iff_mul_lt h] at hr
          simpa only [← mul_pow, mul_comm] using! pow_le_one' hr.le n.succ

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 γ
⊢ T0Space (Closeds α)

Tactic:
suffices ∀ F₁ F₂ : Closeds α, Inseparable F₁ F₂ → F₁ ≤ F₂ from
    ⟨fun F₁ F₂ h => le_antisymm (this F₁ F₂ h) (this F₂ F₁ h.symm)⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ ∀ (F₁ F₂ : Closeds α), Inseparable F₁ F₂ → F₁ ≤ F₂
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 | (⋃ i ∈ T, x ∩ i).Nonempty}

Tactic:
← inter_iUnion

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 ∩ ⋃ i ∈ T, i).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✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
this : CompleteSpace ↥S
μ : 𝕜
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ Tendsto (fun x_1 ↦ (algebraMap 𝕜 ↥S) x_1 - x) (𝓝 μ) (𝓝 ((algebraMap 𝕜 ↥S) μ - x))

Tactic:
← ContinuousAt

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 : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ ContinuousAt (fun x_1 ↦ (algebraMap 𝕜 ↥S) x_1 - x) μ
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case refine_2
𝕜 : 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 : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ ∀ᶠ (x : ↥S) in map (fun x_1 ↦ (algebraMap 𝕜 ↥S) x_1 - x) (𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ), IsUnit x

Tactic:
· rw [eventually_map]
    apply Eventually.filter_mono inf_le_right
    simp [spectrum.notMem_iff]

Goal state after:
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:
by
  simp_rw +singlePass [← compl_compl F, Set.inter_compl_nonempty_iff, ← Set.compl_ofPred]
  exact (isOpen_subsets_of_isOpen h.isOpen_compl).isClosed_compl

Goal state after:
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) ∪ frontier (σ 𝕜 ↑x) ⊆ frontier (σ 𝕜 ↑x)

Tactic:
union_self

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) ⊆ frontier (σ 𝕜 ↑x)
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: case lower
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ {z | z.im < 0}
hz' : z ∈ σ ℂ a
⊢ False

Tactic:
rw [Set.mem_ofPred_eq, ha.im_eq_zero_of_mem_spectrum hz'] at hz

Goal state after:
case lower
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : 0 < 0
hz' : z ∈ σ ℂ a
⊢ False
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: case upper
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ {z | 0 < z.im}
hz' : z ∈ σ ℂ a
⊢ False

Tactic:
rw [Set.mem_ofPred_eq, ha.im_eq_zero_of_mem_spectrum hz'] at hz

Goal state after:
case upper
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : 0 < 0
hz' : z ∈ σ ℂ a
⊢ False
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsUnit a

pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ (a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a * a⋆)

pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ ↑(a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a⋆ * a)

Tactic:
· have h₁ : ha₁.unit⁻¹ * star a * a = 1 := mul_assoc _ _ a ▸ ha₁.val_inv_mul
    have h₂ : a * (star a * ha₂.unit⁻¹) = 1 := (mul_assoc a _ _).symm ▸ ha₂.mul_val_inv
    exact ⟨⟨a, ha₁.unit⁻¹ * star a, left_inv_eq_right_inv h₁ h₂ ▸ h₂, h₁⟩, rfl⟩

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ (a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a * a⋆)

A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ ↑(a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a⋆ * a)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
this :
  ∀ (K₁ K₂ : Compacts α),
    K₁ ≠ K₂ → ¬K₁ ≤ K₂ → (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) K₁ K₂
h' : ¬¬K₁ ≤ K₂
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v

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' : ¬K₁ ≤ K₂
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v

Tactic:
· grind [Disjoint.symm, le_antisymm]

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₂
h' : ¬K₁ ≤ K₂
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
Module: Mathlib.Analysis.LocallyConvex.Polar

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
⊢ B.polar Set.univ = {0}

Tactic:
by
  rw [Set.eq_singleton_iff_unique_mem]
  refine ⟨by simp only [zero_mem_polar], fun y hy => h _ fun x => ?_⟩
  refine norm_le_zero_iff.mp (le_of_forall_gt_imp_ge_of_dense fun ε hε => ?_)
  rcases NormedField.exists_norm_lt 𝕜 hε with ⟨c, hc, hcε⟩
  calc
    ‖B x y‖ = ‖c‖ * ‖B (c⁻¹ • x) y‖ := by
      rw [B.map_smul, LinearMap.smul_apply, smul_eq_mul, norm_mul, norm_inv,
        mul_inv_cancel_left₀ hc.ne']
    _ ≤ ε * 1 := by gcongr; exact hy _ trivial
    _ = ε := mul_one _

Goal state after:
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:
· simp_rw [u, ← Unitary.val_inv_toUnits_apply, neg_smul, ← Units.mul_eq_one_iff_eq_inv,
          Unitary.val_toUnits_apply]
        let _ := invertibleExp (𝔸 := A)
        rw [mul_assoc]
        simp [← invOf_exp]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakDual

Goal state before:
pp: ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
⊢ φ ∈ Submodule.span 𝕜 (Set.range f) ↔ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm

Tactic:
let t := ⨅ i, induced (f i) t𝕜

Goal state after:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
⊢ φ ∈ Submodule.span 𝕜 (Set.range f) ↔ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm
Module: Mathlib.Analysis.LocallyConvex.Barrelled

Goal state before:
pp: α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ⇑p
h₁ : ∀ (n : ℕ), IsClosed[inst✝³] (p.closedBall 0 ↑n)
h₂ : ⋃ n, p.closedBall 0 ↑n = univ
n : ℕ
x : E
hxn : {y | p y ≤ ↑n} ∈ map (fun x_1 ↦ x + x_1) (𝓝 0)
hxn' : p x ≤ ↑n
⊢ {y | p y ≤ ↑n + ↑n} ∈ 𝓝 0

Tactic:
filter_upwards [hxn] with y hy

Goal state after:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ⇑p
h₁ : ∀ (n : ℕ), IsClosed[inst✝³] (p.closedBall 0 ↑n)
h₂ : ⋃ n, p.closedBall 0 ↑n = univ
n : ℕ
x : E
hxn : {y | p y ≤ ↑n} ∈ map (fun x_1 ↦ x + x_1) (𝓝 0)
hxn' : p x ≤ ↑n
y : E
hy : y ∈ (fun x_1 ↦ x + x_1) ⁻¹' {y | p y ≤ ↑n}
⊢ p y ≤ ↑n + ↑n
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ 1
c : CU P
this : approx n c.left x + approx n c.right x ≤ 2
⊢ (approx n c.left x + approx n c.right x) / 2 ≤ 1

Tactic:
exact Iff.mpr (div_le_one zero_lt_two) this

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
P : Type u_3
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
⊢ ⇑(smulTorsor c hk) ⁻¹' Metric.ball c ‖k‖ = Metric.ball 0 1

Tactic:
aesop (add simp norm_smul)

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
⊢ c.lim x = midpoint ℝ (c.left.lim x) (c.right.lim x)

Tactic:
refine tendsto_nhds_unique (c.tendsto_approx_atTop x) ((tendsto_add_atTop_iff_nat 1).1 ?_)

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
⊢ Tendsto (fun n ↦ approx (n + 1) c x) atTop (𝓝 (midpoint ℝ (c.left.lim x) (c.right.lim x)))
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.U
a✝ : X
hyl : a✝ ∈ c.left.U
hyd : dist (c.left.lim a✝) (c.left.lim x) ≤ (3 / 4) ^ n
⊢ (dist (c.left.lim a✝) (c.left.lim x) + 0) / 2 ≤ 3 / 4 * (3 / 4) ^ n

Tactic:
add_zero,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.U
a✝ : X
hyl : a✝ ∈ c.left.U
hyd : dist (c.left.lim a✝) (c.left.lim x) ≤ (3 / 4) ^ n
⊢ dist (c.left.lim a✝) (c.left.lim x) / 2 ≤ 3 / 4 * (3 / 4) ^ n
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt a ^ 2 = a

Tactic:
by
  simp only [nnrpow_sqrt, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, div_self]
  rw [nnrpow_one a]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: case neg
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬0 ≤ a
ha' : ¬0 ≤ ↑a
⊢ CFC.sqrt ↑a = ↑(CFC.sqrt a)

Tactic:
CFC.sqrt,

Goal state after:
case neg
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬0 ≤ a
ha' : ¬0 ≤ ↑a
⊢ cfcₙ ⇑NNReal.sqrt ↑a = ↑(CFC.sqrt a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: case neg
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬0 ≤ a
ha' : ¬0 ≤ ↑a
⊢ cfcₙ ⇑NNReal.sqrt ↑a = ↑(CFC.sqrt a)

Tactic:
CFC.sqrt,

Goal state after:
case neg
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬0 ≤ a
ha' : ¬0 ≤ ↑a
⊢ cfcₙ ⇑NNReal.sqrt ↑a = ↑(cfcₙ (⇑NNReal.sqrt) a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ x ∈ Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖ ≤ 1

Tactic:
simpa only [map_one] using mem_Icc_algebraMap_iff_norm_le zero_le_one (A := A)

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: A : Type u_2
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedAlgebra ℝ A
inst✝⁶ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : ContinuousStar A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
⊢ ContinuousOn (cfc f) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}

Tactic:
have : {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}.EqOn (cfc f) (cfc (fun x : ℝ ↦ f x.toNNReal)) :=
    fun a ha ↦ cfc_nnreal_eq_real _ _ ha.1
  refine ContinuousOn.congr ?_ this
  replace hf : ContinuousOn (fun x ↦ f x.toNNReal : ℝ → ℝ) (NNReal.toReal '' s) := by
    apply hf.ofReal_map_toNNReal
    rw [Set.mapsTo_image_iff]
    intro x hx
    simpa
  refine continuousOn_cfc A (hs.image NNReal.continuous_coe) _ hf |>.mono fun a ha ↦ ?_
  simp only [Set.mem_ofPred_eq, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts] at ha ⊢
  rw [← SpectrumRestricts] at ha
  refine ⟨ha.1.1, ?_⟩
  rw [← ha.1.2.algebraMap_image]
  exact Set.image_mono ha.2

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

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A₁
inst✝⁵ : NonUnitalCStarAlgebra A₂
inst✝⁴ : PartialOrder A₁
inst✝³ : PartialOrder A₂
inst✝² : StarOrderedRing A₁
inst✝¹ : StarOrderedRing A₂
n : Type u_3
inst✝ : Fintype n
φ : A₁ →CP A₂
M : CStarMatrix n n A₁
hM : 0 ≤ M
⊢ 0 ≤ M.map ⇑φ

Tactic:
by
  let k := Fintype.card n
  let e := Fintype.equivFinOfCardEq (rfl : Fintype.card n = k)
  have hmain : 0 ≤ (reindexₐ ℂ A₁ e M).mapₗ (φ : A₁ →ₗ[ℂ] A₂) := by
    simp only [mapₗ, LinearMap.coe_coe, LinearMap.coe_mk, AddHom.coe_mk]
    exact CompletelyPositiveMapClass.map_cstarMatrix_nonneg' _ k _ (map_nonneg _ hM)
  rw [← mapₗ_reindexₐ] at hmain
  simpa [reindexₐ_symm] using map_nonneg (reindexₐ ℂ A₂ e).symm hmain

Goal state after: