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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
S : Type u_3
inst✝⁴ : SMulZeroClass S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
⊢ cfcₙ (fun x ↦ s • f x) a = s • cfcₙ f a

Tactic:
by_cases ha : p a
  · rw [cfcₙ_apply f a, cfcₙ_apply _ a]
    simp_rw [← Pi.smul_def, ← smul_one_smul R s _]
    rw [← map_smul]
    congr
  · simp [cfcₙ_apply_of_not_predicate a ha]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ toContinuousMap 1 = 1

Tactic:
by
    ext
    simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
x✝¹ x✝ : R[X]
⊢ (x✝¹ * x✝).toContinuousMap = x✝¹.toContinuousMap * x✝.toContinuousMap

Tactic:
by
    ext
    simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ toContinuousMap 0 = 0

Tactic:
by
    ext
    simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
x✝¹ x✝ : R[X]
⊢ (x✝¹ + x✝).toContinuousMap = x✝¹.toContinuousMap + x✝.toContinuousMap

Tactic:
by
    ext
    simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
⊢ toContinuousMapOn 1 X = 1

Tactic:
by
    ext
    simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
x✝¹ x✝ : R[X]
⊢ (x✝¹ * x✝).toContinuousMapOn X = x✝¹.toContinuousMapOn X * x✝.toContinuousMapOn X

Tactic:
by
    ext
    simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
⊢ toContinuousMapOn 0 X = 0

Tactic:
by
    ext
    simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
x✝¹ x✝ : R[X]
⊢ (x✝¹ + x✝).toContinuousMapOn X = x✝¹.toContinuousMapOn X + x✝.toContinuousMapOn X

Tactic:
by
    ext
    simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
⊢ cfcₙ (-f) = -cfcₙ f

Tactic:
by ext1 a; exact (cfcₙ_neg f a)

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

Goal state before:
pp: case mp
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : ContinuousSqrt R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NoZeroDivisors R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ 0 ≤ (cfcₙHom ha) f → 0 ≤ f

pp: case mpr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : ContinuousSqrt R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NoZeroDivisors R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ 0 ≤ f → 0 ≤ (cfcₙHom ha) f

Tactic:
· exact fun hf x ↦
      (cfcₙHom_map_quasispectrum ha (R := R) _ ▸ quasispectrum_nonneg_of_nonneg (cfcₙHom ha f) hf)
      _ ⟨x, rfl⟩

Goal state after:
case mpr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : ContinuousSqrt R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NoZeroDivisors R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ 0 ≤ f → 0 ≤ (cfcₙHom ha) f
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x : Unitization 𝕜 E
⊢ ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖

Tactic:
simp only [Unitization.norm_def, Prod.norm_def]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x : Unitization 𝕜 E
⊢ max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ * max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ ≤
    max ‖((splitMul 𝕜 E) (x⋆ * x)).1‖ ‖((splitMul 𝕜 E) (x⋆ * x)).2‖
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
hf : LowerHemicontinuousAt f x₀
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y₀ : β
hy₀ : y₀ ∈ f x₀
inst✝ : (𝓝 y₀).IsCountablyGenerated
U : ℕ → Set β
hU : ∀ (i : ℕ), y₀ ∈ U i ∧ IsOpen[inst✝¹] (U i)
hUbasis : (𝓝 y₀).HasAntitoneBasis fun i ↦ U i
hev : ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, (f (x n) ∩ U k).Nonempty
g : ℕ → ℕ := fun n ↦ Nat.findGreatest (fun k ↦ (f (x n) ∩ U k).Nonempty) n
key : ∀ (n k : ℕ), k ≤ n → (f (x n) ∩ U k).Nonempty → (f (x n) ∩ U (g n)).Nonempty
⊢ ∃ y, (∀ᶠ (n : ℕ) in atTop, y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)

Tactic:
let y : ℕ → β := fun n ↦ if h : (f (x n) ∩ U (g n)).Nonempty then h.some else y₀

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
hf : LowerHemicontinuousAt f x₀
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y₀ : β
hy₀ : y₀ ∈ f x₀
inst✝ : (𝓝 y₀).IsCountablyGenerated
U : ℕ → Set β
hU : ∀ (i : ℕ), y₀ ∈ U i ∧ IsOpen[inst✝¹] (U i)
hUbasis : (𝓝 y₀).HasAntitoneBasis fun i ↦ U i
hev : ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, (f (x n) ∩ U k).Nonempty
g : ℕ → ℕ := fun n ↦ Nat.findGreatest (fun k ↦ (f (x n) ∩ U k).Nonempty) n
key : ∀ (n k : ℕ), k ≤ n → (f (x n) ∩ U k).Nonempty → (f (x n) ∩ U (g n)).Nonempty
y : ℕ → β := fun n ↦ if h : (f (x n) ∩ U (g n)).Nonempty then h.some else y₀
⊢ ∃ y, (∀ᶠ (n : ℕ) in atTop, y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : LowerHemicontinuous f
hg : HasOpenCGraph g
⊢ LowerHemicontinuous fun x ↦ f x ∩ g x

Tactic:
simp_rw [lowerHemicontinuous_iff_isOpen_inter_nonempty] at ⊢ hf
  intro t ht
  rw [isOpen_iff_forall_mem_open]
  intro x ⟨y, ⟨hyf, hyg⟩, hyt⟩
  obtain ⟨U, V, hU, hV, hxU, hyV, hUV⟩ := (isOpen_prod_iff.mp hg) x y hyg
  refine ⟨U ∩ {x' | (f x' ∩ (t ∩ V)).Nonempty}, ?_, hU.inter (hf _ (ht.inter hV)),
      ⟨hxU, y, hyf, hyt, hyV⟩⟩
  intro x' ⟨hx'U, z, hzf, hzt, hzV⟩
  exact ⟨z, ⟨hzf, hUV (Set.mk_mem_prod hx'U hzV)⟩, hzt⟩

Goal state after:
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
x : α
hxs : x ∈ s
hxU : x ∈ U
⊢ ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty

Tactic:
obtain ⟨W, hWB, hxW, hW⟩ := hB.exists_subset_of_mem_open hxU <| hu₂ 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 : Set α
hWB : W ∈ B
hxW : x ∈ W
hW : W ⊆ U
⊢ ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
a : A
ha : (σ a).Nonempty
r : ℝ≥0
hr : ∀ k ∈ σ a, ‖k‖₊ < r
⊢ ∀ x ∈ σ a, ‖x‖ₑ < ↑r

Tactic:
by simpa using hr

Goal state after:
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✝¹] {a | (f a ∩ U).Nonempty}

Tactic:
← not_disjoint_iff_nonempty_inter,

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✝¹] {a | ¬Disjoint (f a) U}
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompactSpace α
f : Ultrafilter (Set α)
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
⊢ ↑f ≤ 𝓝 f.lim

Tactic:
f.le_nhds_lim

Goal state after:
α : 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
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 : {x | ↑x ⊆ ∅} ⊆ {⊥} → ∃ u, {x | ↑x ⊆ ⋂ i ∈ u, F i} ⊆ {⊥}
⊢ ∃ u, ⋂ i ∈ u, F i = ∅

Tactic:
Set.subset_empty_iff,

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 : {x | ↑x = ∅} ⊆ {⊥} → ∃ u, {x | ↑x ⊆ ⋂ i ∈ u, F i} ⊆ {⊥}
⊢ ∃ u, ⋂ i ∈ u, F i = ∅
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, (K \ ⋃₀ u ∩ L).Nonempty
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
obtain ⟨_, hUS, hUu⟩ := mem_sUnion.mp <| hKS ⟨sdiff_subset, hsu⟩

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, (K \ ⋃₀ u ∩ L).Nonempty
w✝ : Set (Set α)
hUS : w✝ ∈ S
hUu : K \ ⋃₀ u ∈ w✝
⊢ ∃ 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
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
have hl : l.TotallyBounded := by
    intro U hU
    obtain ⟨V : SetRel α α, hV, hVU⟩ := comp_mem_uniformity_sets hU
    obtain ⟨K, hK⟩ := hf (symm_le_uniformity hV) |>.exists
    obtain ⟨t, ht₁, ht₂⟩ := K.isCompact.totallyBounded V hV
    rw [← SetRel.preimage_eq_biUnion] at ht₂
    refine ⟨t, ht₁, Filter.mem_of_superset (Filter.mem_lift' hK) ?_⟩
    rw [Set.iUnion₂_subset_iff]
    intro K' ⟨_, (hK' : ↑K' ⊆ V.preimage K)⟩
    grw [← hVU, SetRel.preimage_comp, ← ht₂, hK']

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
⊢ ∃ x, f ≤ 𝓝 x
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ SetLike.coe ⁻¹' closure[TopologicalSpace.vietoris α] {K | K.Finite ∧ K ⊆ s} = SetLike.coe ⁻¹' 𝒫 closure[inst✝] s

pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ {K | K.Finite ∧ K ⊆ s} ⊆ range SetLike.coe

Tactic:
vietoris.closure_finite_subsets

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ SetLike.coe ⁻¹' 𝒫 closure[inst✝] s = SetLike.coe ⁻¹' 𝒫 closure[inst✝] s

α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ {K | K.Finite ∧ K ⊆ s} ⊆ range SetLike.coe
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case refine_1
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
x : ℝ
hx : x ∈ spectrum ℝ ((algebraMap ℝ A) ↑t - a)
⊢ ↑‖x‖₊ ≤ ↑t

pp: case refine_2
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 : spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
· rw [← spectrum.singleton_sub_eq] at hx
    obtain ⟨y, hy, rfl⟩ : ∃ y ∈ spectrum ℝ a, ↑t - y = x := by simpa using hx
    obtain ⟨hty, hyt⟩ := Set.mem_Icc.mp <| this hy
    lift y to ℝ≥0 using h y hy
    rw [← NNReal.coe_sub (by exact_mod_cast hyt)]
    simp

Goal state after:
case refine_2
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 : spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: U : Set ℂ
U_convex : Convex ℝ U
z w : ℂ
hz : z ∈ U
hw : w ∈ U
hzw : ↑z.re + ↑w.im * I ∈ U
hwz : ↑w.re + ↑z.im * I ∈ U
⊢ z.Rectangle w ⊆ U

Tactic:
simpa only [rectangle_eq_convexHull] using convexHull_min (by grind) U_convex

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
heq : (fun n ↦ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x ↦ x ^ 2) ∘ fun n ↦ ↑‖a ^ n‖₊ ^ (1 / ↑n)
h₂ : Tendsto ((fun a ↦ a ^ 2) ∘ fun n ↦ ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop (𝓝 (spectralRadius ℂ a ^ 2))
⊢ spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2

Tactic:
rw [← heq] at h₂

Goal state after:
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
heq : (fun n ↦ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x ↦ x ^ 2) ∘ fun n ↦ ↑‖a ^ n‖₊ ^ (1 / ↑n)
h₂ : Tendsto (fun n ↦ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) atTop (𝓝 (spectralRadius ℂ a ^ 2))
⊢ spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})
⊢ IsConnected (σ ℂ a)ᶜ

Tactic:
rw [← Set.inter_union_distrib_left, ← Set.ofPred_or] at this

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {a | 0 ≤ a.im ∨ a.im ≤ 0})
⊢ IsConnected (σ ℂ a)ᶜ
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {U | IsOpen[instTopologicalSpaceProd] U}
K : Compacts α
L : Compacts β
hKL : ↑K ×ˢ ↑L ⊆ U
V : Set α
W : Set β
hV : IsOpen[inst✝¹] V
hW : IsOpen[inst✝] W
hK : ↑K ⊆ V
hL : ↑L ⊆ W
hVW : V ×ˢ W ⊆ U
⊢ ∃ t ⊆ (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' 𝒫 U, IsOpen t ∧ (K, L) ∈ t

Tactic:
exact ⟨_, fun ⟨K', L'⟩ ⟨hK', hL'⟩ => (Set.prod_mono hK' hL').trans hVW,
      (isOpen_subsets_of_isOpen hV).prod (isOpen_subsets_of_isOpen hW), hK, hL⟩

Goal state after:
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
⊢ (absConvexHull 𝕜) s = ⋂ t, ⋂ (_ : s ⊆ t), ⋂ (_ : AbsConvex 𝕜 t), t

Tactic:
by
  simp [absConvexHull, iInter_subtype, iInter_and]

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ closure {K | (↑K).Finite ∧ ↑K ⊆ s} = {K | ↑K ⊆ closure[inst✝] s}

Tactic:
by
  simpa [isOpenEmbedding_toCompacts.isOpenMap.preimage_closure_eq_closure_preimage
    continuous_toCompacts] using congr(toCompacts ⁻¹' $(Compacts.closure_finite_subsets s))

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

Goal state before:
pp: E : Type u_3
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : QuasiCompleteSpace ℝ E
s : Set E
ht : TotallyBounded s
⊢ IsCompact ((closedAbsConvexHull ℝ) s)

Tactic:
rw [closedAbsConvexHull_eq_closure_absConvexHull]
  exact isCompact_closure_of_totallyBounded_quasiComplete (𝕜 := ℝ) ht.absConvexHull

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖x' z‖ ≤ 1
hcr : 0 < ‖c‖ / r
⊢ ‖x'‖ ≤ ‖c‖ / r

Tactic:
refine ContinuousLinearMap.opNorm_le_of_shell hr hcr.le hc fun x h₁ h₂ => ?_

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖x' z‖ ≤ 1
hcr : 0 < ‖c‖ / r
x : E
h₁ : r / ‖c‖ ≤ ‖x‖
h₂ : ‖x‖ < r
⊢ ‖x' x‖ ≤ ‖c‖ / r * ‖x‖
Module: Mathlib.Topology.ContinuousMap.Units

Goal state before:
pp: X : Type u_1
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ ⇑(algebraMap 𝕜 𝕜) ⁻¹' Set.range ⇑f = Set.range ⇑f

Tactic:
Algebra.algebraMap_self

Goal state after:
X : Type u_1
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ ⇑(RingHom.id 𝕜) ⁻¹' Set.range ⇑f = Set.range ⇑f
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ : P
⊢ ‖2⁻¹‖ * dist p₁ p₂ = ‖2‖⁻¹ * dist p₁ p₂

Tactic:
← norm_inv

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ : P
⊢ ‖2⁻¹‖ * dist p₁ p₂ = ‖2⁻¹‖ * dist p₁ p₂
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (⇑g) 0 s
hgt : EqOn (⇑g) 1 t
hicc : ∀ (x : X), 0 ≤ g x ∧ g x ≤ 1
x : X
hx : x ∈ s
⊢ (1 - g) x = 1 x

Tactic:
simp only [ContinuousMap.sub_apply, ContinuousMap.one_apply, Pi.one_apply, sub_eq_self]

Goal state after:
case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (⇑g) 0 s
hgt : EqOn (⇑g) 1 t
hicc : ∀ (x : X), 0 ≤ g x ∧ g x ≤ 1
x : X
hx : x ∈ s
⊢ g x = 0
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
⊢ x ∈ setOfIdeal (idealOfSet 𝕜 s)

Tactic:
mem_setOfIdeal,

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
⊢ ∃ f ∈ idealOfSet 𝕜 s, f x ≠ 0
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
⊢ x ∈ setOfIdeal (idealOfSet 𝕜 s)

Tactic:
simp_rw [mem_setOfIdeal, mem_idealOfSet]

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
⊢ ∃ f, (∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0) ∧ f x ≠ 0
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
⊢ ∀ (x : α →ᵤ β), edist x x = 0

Tactic:
simp [edist_def]

Goal state after:
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
f g : α →ᵤ β
h✝ : IsEmpty α
⊢ edist f g = ENNReal.ofReal (⨆ x, dist (toFun f x) (toFun g x))

Tactic:
simp [edist_def]

Goal state after: