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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
n : ℕ
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (fun x ↦ f x ^ n) a = cfc f a ^ n

Tactic:
rw [cfc_apply f a, ← map_pow, cfc_apply _ a]
  congr

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
this : (fun z ↦ r + f z) = fun z ↦ (fun x ↦ r) z + f z
⊢ cfc (fun z ↦ (fun x ↦ r) z + f z) a = (algebraMap R A) r + cfc f a

Tactic:
cfc_add a _ _ (continuousOn_const (c := r)) hf,

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
this : (fun z ↦ r + f z) = fun z ↦ (fun x ↦ r) z + f z
⊢ cfc (fun x ↦ r) a + cfc f a = (algebraMap R A) r + cfc f a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
⊢ ContinuousOn g (spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }))

Tactic:
convert! hg

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : LocallyBoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y ∈ s ∩ Iio x
⊢ 𝓝[s ∩ Iio x] x = 𝓝[s ∩ Icc y x ∩ Iio x] x

Tactic:
rw [show (s ∩ Icc y x) ∩ Iio x = (s ∩ Iio x) ∩ Icc y x by grind, eq_comm]

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : LocallyBoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y ∈ s ∩ Iio x
⊢ 𝓝[s ∩ Iio x ∩ Icc y x] x = 𝓝[s ∩ Iio x] x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousInv₀ R
a : Aˣ
n : ℤ
ha : p ↑a
⊢ cfc (fun x ↦ x ^ n) ↑a = ↑(a ^ n)

Tactic:
by
  cases n with
  | ofNat n => simpa using cfc_pow_id (a : A) n
  | negSucc n =>
    simp only [zpow_negSucc, ← inv_pow, Units.val_pow_eq_pow_val]
    have := cfc_pow (fun x ↦ x⁻¹ : R → R) (n + 1) (a : A)
    exact this.trans <| congr($(cfc_inv_id a) ^ (n + 1))

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
⊢ eVariationOn g s ≤ eVariationOn f s

Tactic:
by
  rw [eVariationOn_eq_strictMonoOn]
  apply iSup_le
  rintro ⟨n, u, u_mono, u_mem⟩
  simp only
  have : Nonempty α := ⟨u 0⟩
  apply le_of_forall_lt (fun c hc ↦ ?_)
  have : ∀ᶠ (b : ℕ → E) in 𝓝 (fun i ↦ g (u i)),
      c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i) := by
    have : Continuous (fun (v : ℕ → E) ↦ ∑ i ∈ Finset.range n, edist (v (i + 1)) (v i)) := by
      fun_prop
    exact (tendsto_order.1 (this.continuousAt (x := fun i ↦ g (u i))).tendsto).1 c hc
  rw [nhds_pi] at this
  obtain ⟨I, I_fin, t, t_mem, ht⟩ : ∃ (I : Set ℕ), I.Finite ∧ ∃ t, (∀ (i : ℕ), t i ∈ 𝓝 (g (u i))) ∧
      I.pi t ⊆ {b : ℕ → E | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)} := mem_pi.1 this
  have : ∀ᶠ b in 𝓝 u, ∀ i ∈ ((Finset.Iic n) ×ˢ (Finset.Iic n)).filter
      (fun i ↦ i.1 < i.2), b i.1 < b i.2 := by
    rw [Filter.eventually_all_finset]
    intro i hi
    apply IsOpen.mem_nhds ?_ (by grind [StrictMonoOn])
    exact isOpen_lt (by fun_prop) (by fun_prop)
  rw [nhds_pi] at this
  obtain ⟨J, J_fin, k, k_mem, hk⟩ : ∃ (J : Set ℕ), J.Finite ∧ ∃ k, (∀ (i : ℕ), k i ∈ 𝓝 (u i)) ∧
    J.pi k ⊆ _ := mem_pi.1 this
  have A i (hi : i ∈ Iic n) : ∃ x, (f x ∈ t i ∧ x ∈ k i) ∧ x ∈ s :=
    ((((mapClusterPt_iff_frequently.1 (hg (u i) (u_mem i hi)) (t i) (t_mem i))).and_eventually
      (mem_nhdsWithin_of_mem_nhds (k_mem i))).and_eventually self_mem_nhdsWithin).exists
  choose! v hv h'v using A
  have : c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) := by
    let f' i := if i ∈ Iic n then f (v i) else g (u i)
    have : ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) =
        ∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i) :=
      Finset.sum_congr rfl (fun i hi ↦ by grind)
    rw [this]
    suffices H : f' ∈ I.pi t from ht H
    have A i : g (u i) ∈ t i := mem_of_mem_nhds (t_mem i)
    grind
  apply this.trans_le
  have v_mono : StrictMonoOn v (Iic n) := by
    let w i := if i ∈ Iic n then v i else u i
    suffices w ∈ J.pi k by
      simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_Iic, and_imp, Prod.forall] at hk
      grind [StrictMonoOn]
    have A i : u i ∈ k i := mem_of_mem_nhds (k_mem i)
    grind
  exact sum_le_of_monotoneOn_Iic v_mono.monotoneOn (by grind)

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✝¹² : 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
inst✝ : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq : σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a
⊢ ContinuousOn g (σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ }))

Tactic:
convert! hg

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬(-1) ^ (n - ν) * eval (↑ν + 1) (ascPochhammer R (n - ν)) = 0

Tactic:
neg_one_pow_mul_eq_zero_iff,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (↑ν + 1) (ascPochhammer R (n - ν)) = 0
Module: Mathlib.Topology.ContinuousMap.Weierstrass

Goal state before:
pp: case h
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x ↦ f ↑x, continuous_toFun := ⋯ }
p : ℝ[X]
b : ∀ (x : ↑(Set.Icc a b✝)), ‖(p.toContinuousMapOn (Set.Icc a b✝) - f') x‖ < ε
x : ℝ
m : x ∈ Set.Icc a b✝
⊢ |Polynomial.eval x p - f x| < ε

Tactic:
exact b ⟨x, m⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
C : ℝ
hC : ∀ (x y : ↑I), gauge U (f x - f y) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ : ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2
nhds_zero : Tendsto (fun n ↦ C / δ ^ 2 / ↑n) atTop (𝓝 0)
n : ℕ
nh : C / δ ^ 2 / ↑n < 1 / 2
hn₀ : n ≠ 0
x : ↑I
S : Finset (Fin (n + 1)) := {k | dist k/ₙ x < δ}
⊢ ∑ k ∈ S, (bernstein n ↑k) x * (1 / 2) = 1 / 2 * ∑ k ∈ S, (bernstein n ↑k) x

Tactic:
by rw [mul_comm, Finset.sum_mul]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
k : 𝕜
x : Unitization 𝕜 A
⊢ ‖k • (splitMul 𝕜 A) x‖ ≤ ‖k‖ * ‖x‖

Tactic:
norm_smul,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
k : 𝕜
x : Unitization 𝕜 A
⊢ ‖k‖ * ‖(splitMul 𝕜 A) x‖ ≤ ‖k‖ * ‖x‖
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case refine_3.refine_2
𝕜 : 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
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r < (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) (k • a⋆)

Tactic:
simp only [map_smul, nnnorm_smul, mul_apply', CStarRing.nnnorm_self_mul_star]
        rwa [← div_lt_iff₀ (mul_pos ha ha), div_eq_mul_inv, mul_inv, ← mul_assoc]

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

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f ↦ ⇑f) f x₁ ≠ (fun f ↦ ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
hFA : F ∈ A
a✝ : X
⊢ ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯) { toFun := fun x ↦ ‖F x‖ ^ 2, continuous_toFun := ⋯ }) a✝ = (F * star F) a✝

Tactic:
simp [← RCLike.mul_conj]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
r : 𝕜
x : WithLp 1 (Unitization 𝕜 A)
⊢ ‖r • x.ofLp.toProd.1‖ + ‖r • x.ofLp.toProd.2‖ ≤ ‖r‖ * (‖x.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖)

Tactic:
norm_smul,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
r : 𝕜
x : WithLp 1 (Unitization 𝕜 A)
⊢ ‖r‖ * ‖x.ofLp.toProd.1‖ + ‖r‖ * ‖x.ofLp.toProd.2‖ ≤ ‖r‖ * (‖x.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖)
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case mul
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id s) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id s)) = 0
hφ : Continuous ⇑φ
f✝ g✝ : C(↑s, 𝕜)₀
h : a * φ f✝ = 0
a✝ : a * φ g✝ = 0
⊢ a * φ (f✝ * g✝) = 0

Tactic:
| mul _ _ h _ =>

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
hf : UpperHemicontinuousAt f x
u : Set β
hu : IsClosed[inst✝] u
⊢ UpperHemicontinuousAt (fun x ↦ f x ∩ u) x

Tactic:
rw [← upperHemicontinuousWithinAt_univ_iff] at hf ⊢
  exact hf.inter hu

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

Goal state before:
pp: α : Type u_1
⊢ hausdorffEntourage SetRel.id = SetRel.id

Tactic:
simp_rw [hausdorffEntourage, preimage_id, image_id, ← subset_antisymm_iff, SetRel.id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
x₀ : α
hx₀s : x₀ ∈ s
⊢ LowerHemicontinuousWithinAt f s x₀

Tactic:
lowerHemicontinuousWithinAt_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
x₀ : α
hx₀s : x₀ ∈ s
⊢ ∀ (u : Set β), IsOpen[inst✝.toTopologicalSpace] u → (f x₀ ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x₀, (f x' ∩ u).Nonempty
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case left
α : 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) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
⊢ V.preimage (V.preimage t) ⊆ SetRel.preimage U t

Tactic:
← hVU,

Goal state after:
case left
α : 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) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
⊢ V.preimage (V.preimage t) ⊆ (V.comp V).preimage t
Module: Mathlib.Topology.Sets.VietorisTopology

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

Tactic:
· intro u ⟨hu₁, hu₂⟩ s ⟨hs₁, hs₂⟩
    choose! f hfB hfU hfs using show ∀ U ∈ u, ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty by
      intro U hU
      obtain ⟨x, hxs, hxU⟩ := hs₂ U hU
      obtain ⟨W, hWB, hxW, hW⟩ := hB.exists_subset_of_mem_open hxU <| hu₂ U hU
      exact ⟨W, hWB, hW, x, hxs, hxW⟩
    rw [exists_mem_image]
    refine ⟨⟨⋃₀ u, f '' u⟩, ⟨isOpen_sUnion hu₂, hu₁.image _, by grind⟩, by grind,
      fun t ⟨ht₁, ht₂⟩ => ⟨ht₁, fun U hU => ?_⟩⟩
    rw [forall_mem_image] at ht₂
    grw [← hfU U hU]
    exact ht₂ hU

Goal state after:
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) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
⊢ V.image (V.image s) ⊆ SetRel.image U s

Tactic:
← hVU,

Goal state after:
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) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
⊢ V.image (V.image s) ⊆ (V.comp V).image s
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case e'_3
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊
hn : 0 < ↑(n + 1)
⊢ ↑‖k‖₊ = (↑‖k‖₊ ^ (n + 1)) ^ (1 / ↑(n + 1))

Tactic:
rw [one_div, pow_rpow_inv_natCast]
    positivity

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

Goal state before:
pp: case left
α : 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.preimage (V.preimage t) ⊆ SetRel.preimage U t

Tactic:
← hVU,

Goal state after:
case left
α : 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.preimage (V.preimage t) ⊆ (V.comp V).preimage t
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) ⊆ SetRel.image U s

Tactic:
← hVU,

Goal state after:
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.comp V).image s
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})ᶜ
⊢ (range fun x ↦ {x})ᶜ ∈ 𝓝 s

Tactic:
rcases Set.eq_empty_or_nonempty s with rfl | h

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})ᶜ ∈ 𝓝 ∅

case inr
α : 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
⊢ (range fun x ↦ {x})ᶜ ∈ 𝓝 s
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) ⊆ U.preimage u

Tactic:
← hVU,

Goal state after:
α : 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.comp V).preimage u
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
⊢ ‖(↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n‖ ≤ ‖a - ↑ₐ z‖ ^ n / ↑n.factorial

Tactic:
norm_smul,

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
⊢ ‖(↑(n + 1).factorial)⁻¹‖ * ‖(a - ↑ₐ z) ^ n‖ ≤ ‖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 : ∀ {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

Tactic:
← hVU,

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' ⊆ (V.comp V).preimage t
Module: Mathlib.Topology.Sets.VietorisTopology

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

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

Goal state after: