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
inst✝ : UniqueHom R A
f : R → R
a : A
hf : ContinuousOn f (star '' spectrum R a)
ha : p a
⊢ cfc (fun x ↦ f (star x)) a = cfc f (star a)

Tactic:
by
  rw [cfc_comp' .., cfc_star_id ..]

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
inst✝ : Nontrivial A
⊢ spectrum R 1 = {1}

Tactic:
have : (1 : A) = algebraMap R A 1 := Eq.symm (map_one (algebraMap R A))
  rw [this, spectrum_algebraMap_eq]

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
ι : Type u_3
f : ι → R → R
a : A
ha : p a
hf : ∀ (i : ι), ContinuousOn (f i) (σₙ R a)
hf0 : ∀ (i : ι), f i 0 = 0
⊢ (fun i ↦ cfcₙ (f i) a) = fun i ↦
    (cfcₙHom ha) { toFun := (σₙ R a).domRestrict (f i), continuous_toFun := ⋯, map_zero' := ⋯ }

Tactic:
ext i
  simp only [cfcₙ_apply (f i) a (hf i) (hf0 i)]

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
f : R → R
a : A
⊢ cfcₙ (fun x ↦ star (f x)) a = star (cfcₙ f a)

Tactic:
by
  by_cases h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0
  · obtain ⟨ha, hf, h0⟩ := h
    rw [cfcₙ_apply f a, ← map_star, cfcₙ_apply _ a]
    congr
  · simp only [not_and_or] at h
    obtain (ha | hf | h0) := h
    · simp [cfcₙ_apply_of_not_predicate a ha]
    · rw [cfcₙ_apply_of_not_continuousOn a hf, cfcₙ_apply_of_not_continuousOn, star_zero]
      exact fun hf_star ↦ hf <| by simpa using hf_star.star
    · rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero, star_zero]
      exact fun hf0 ↦ h0 <| by simpa using congr(star $(hf0))

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

Goal state before:
pp: f : C(↑I, ℝ)
n : ℕ
i : Fin (n + 1)
⊢ bernstein n ↑i • const (↑I) (f (bernstein.z i)) ∈ polynomialFunctions I

Tactic:
← SetLike.mem_coe,

Goal state after:
f : C(↑I, ℝ)
n : ℕ
i : Fin (n + 1)
⊢ bernstein n ↑i • const (↑I) (f (bernstein.z i)) ∈ ↑(polynomialFunctions I)
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
⊢ |↑f| ∈ A.topologicalClosure

Tactic:
let f' := attachBound (f : C(X, ℝ))

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := (↑f).attachBound
⊢ |↑f| ∈ A.topologicalClosure
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ ↑A.topologicalClosure = ↑A

Tactic:
rw [Subalgebra.topologicalClosure_coe, closure_eq_iff_isClosed]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ IsClosed ↑A
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L

Tactic:
choose g hg w₁ w₂ using sep f

Goal state after:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
⊢ ∃ x, dist x f < ε ∧ x ∈ L
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := fun x ↦ {z | ↑(h x) z < f z + ε}
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
⊢ ∃ x, dist x f < ε ∧ x ∈ L

Tactic:
let xs : Finset X := (CompactSpace.elim_nhds_subcover W W_nhds).choose

Goal state after:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := fun x ↦ {z | ↑(h x) z < f z + ε}
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯.choose
⊢ ∃ x, dist x f < ε ∧ x ∈ L
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case pos.right
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := ⋯
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := ⋯
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := ⋯
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := ⋯
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯
xs_w : ⋃ x ∈ xs, W x = ⊤ := ⋯
xs_nonempty : xs.Nonempty
k : ↑L := ⋯
z : X
⊢ f z - ε < ↑k z

Tactic:
simp only [k, Finset.lt_inf'_iff, ContinuousMap.inf'_apply]
    rintro x -
    apply lt_h

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

Goal state before:
pp: case mem.inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f✝ f : C(↑s, 𝕜)
⊢ p ((toContinuousMapOnAlgHom s) X)

Tactic:
simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]

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

Goal state before:
pp: case mem.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f✝ f : C(↑s, 𝕜)
⊢ p (star ((toContinuousMapOnAlgHom s) X))

Tactic:
simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
frequently : ∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)
h : ∀ f ∈ (polynomialFunctions s).starClosure, p f
f : C(↑s, 𝕜)
this : f ∈ (polynomialFunctions s).starClosure.topologicalClosure
⊢ ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g

Tactic:
← SetLike.mem_coe,

Goal state after:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
frequently : ∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)
h : ∀ f ∈ (polynomialFunctions s).starClosure, p f
f : C(↑s, 𝕜)
this : f ∈ ↑(polynomialFunctions s).starClosure.topologicalClosure
⊢ ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
hf₁ : f ∈ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
hf₂ : f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
⊢ f ∈ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})

Tactic:
rw [SetLike.mem_coe] at hf₂ ⊢

Goal state after:
case mp
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
hf₁ : f ∈ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
hf₂ : f ∈ RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)
⊢ f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ IsOpenMap f ↔ LowerHemicontinuous fun x ↦ f ⁻¹' {x}

Tactic:
rw [isOpenMap_iff_kernImage, lowerHemicontinuous_iff_isClosed_preimage_Iic]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ (∀ {u : Set α}, IsClosed[inst✝¹] u → IsClosed[inst✝] (kernImage f u)) ↔
    ∀ (u : Set α), IsClosed[inst✝¹] u → IsClosed[inst✝] ((fun x ↦ f ⁻¹' {x}) ⁻¹' Iic u)
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hg : HasOpenCGraph g
hf : ∀ (u : Set β), IsOpen[inst✝] u → IsOpen[inst✝¹] {x | (f x ∩ u).Nonempty}
t : Set β
ht : IsOpen[inst✝] t
x : α
y : β
hyf : y ∈ f x
hyg : y ∈ g x
hyt : y ∈ t
U : Set α
V : Set β
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝] V
hxU : x ∈ U
hyV : y ∈ V
hUV : U ×ˢ V ⊆ {x | x.2 ∈ g x.1}
x' : α
⊢ x' ∈ U ∩ {x' | (f x' ∩ (t ∩ V)).Nonempty} → x' ∈ {x | (f x ∩ g x ∩ t).Nonempty}

Tactic:
⟨hx'U, z, hzf, hzt, hzV⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hg : HasOpenCGraph g
hf : ∀ (u : Set β), IsOpen[inst✝] u → IsOpen[inst✝¹] {x | (f x ∩ u).Nonempty}
t : Set β
ht : IsOpen[inst✝] t
x : α
y : β
hyf : y ∈ f x
hyg : y ∈ g x
hyt : y ∈ t
U : Set α
V : Set β
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝] V
hxU : x ∈ U
hyV : y ∈ V
hUV : U ×ˢ V ⊆ {x | x.2 ∈ g x.1}
x' : α
hx'U : x' ∈ U
z : β
hzf : z ∈ f x'
hzt : z ∈ t
hzV : z ∈ V
⊢ x' ∈ {x | (f x ∩ g x ∩ t).Nonempty}
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
V : Set β
hV : IsOpen[inst✝.toTopologicalSpace] V
y₀ : β
hy₀f : y₀ ∈ f x₀
hy₀V : y₀ ∈ V
W : Set (β × β)
hW : W ∈ uniformity β
hWsub : ball y₀ W ⊆ V
U₁ : Set (β × β)
hU₁ : U₁ ∈ uniformity β
hU₁sym : SetRel.IsSymm U₁
hU₁comp : SetRel.comp U₁ U₁ ⊆ W
U : Set (β × β)
hU : U ∈ uniformity β
hUsym : SetRel.IsSymm U
hUcomp : SetRel.comp U U ⊆ U₁
⊢ ∀ᶠ (x' : α) in 𝓝[s] x₀, (f x' ∩ V).Nonempty

Tactic:
have hU_le_U₁ : U ⊆ U₁ := fun _p hp => hUcomp ⟨_, refl_mem_uniformity hU, hp⟩

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
V : Set β
hV : IsOpen[inst✝.toTopologicalSpace] V
y₀ : β
hy₀f : y₀ ∈ f x₀
hy₀V : y₀ ∈ V
W : Set (β × β)
hW : W ∈ uniformity β
hWsub : ball y₀ W ⊆ V
U₁ : Set (β × β)
hU₁ : U₁ ∈ uniformity β
hU₁sym : SetRel.IsSymm U₁
hU₁comp : SetRel.comp U₁ U₁ ⊆ W
U : Set (β × β)
hU : U ∈ uniformity β
hUsym : SetRel.IsSymm U
hUcomp : SetRel.comp U U ⊆ U₁
hU_le_U₁ : U ⊆ U₁
⊢ ∀ᶠ (x' : α) in 𝓝[s] x₀, (f x' ∩ V).Nonempty
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_4
inst✝ : Finite ι
⊢ Continuous[Pi.topologicalSpace, TopologicalSpace.vietoris α] range

Tactic:
simp_rw [continuous_iff, powerset, preimage_ofPred_eq, range_subset_iff, ofPred_forall]
  exact ⟨
    fun U hU => isOpen_iInter_of_finite fun i => hU.preimage <| continuous_apply i,
    fun F hF => isClosed_iInter fun i => hF.preimage <| continuous_apply i⟩

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

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

Tactic:
← TopologicalSpace.vietoris.specializes_closure.nhds_le_nhds,

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 ≤ 𝓝 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 = ∅
⊢ ∃ u, ⋂ i ∈ u, F i = ∅

Tactic:
have := isClopen_singleton_bot.compl.isClosed.isCompact.elim_finite_subfamily_closed
    (fun i => {C : Closeds α | ↑C ⊆ F i})
    (fun i => isClosed_subsets_of_isClosed (hF₁ i))

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 : {⊥}ᶜ ∩ ⋂ i, {C | ↑C ⊆ F i} = ∅ → ∃ u, {⊥}ᶜ ∩ ⋂ i ∈ u, {C | ↑C ⊆ F i} = ∅
⊢ ∃ u, ⋂ i ∈ u, F i = ∅
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case left
α : 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 α := ⋯
hl : l.TotallyBounded
L : Compacts α := ⋯
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
⊢ ↑K ⊆ U.preimage ↑L

pp: case right
α : 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 α := ⋯
hl : l.TotallyBounded
L : Compacts α := ⋯
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
⊢ ↑L ⊆ U.image ↑K

Tactic:
· intro x hx
    set lx := l ⊓ 𝓟 (UniformSpace.ball x U) with le_def
    have hlx : lx.TotallyBounded := hl.mono inf_le_left
    have : lx.NeBot := by
      rw [le_def, Filter.lift'_inf_principal_eq, Filter.lift'_neBot_iff fun _ _ h =>
        Set.inter_subset_inter_left _ <| Set.biUnion_subset_biUnion_left h]
      intro s hs
      obtain ⟨K', ⟨h₁, -⟩, h₂⟩ := Filter.nonempty_of_mem <| Filter.inter_mem hK hs
      obtain ⟨y, hy, hxy⟩ := h₁ hx
      exact ⟨y, Set.mem_iUnion₂_of_mem h₂ hy, hxy⟩
    obtain ⟨y, hy⟩ := hlx.exists_clusterPt
    have hy₁ : ClusterPt y l := .of_inf_left hy
    have hy₂ : ClusterPt y (𝓟 (UniformSpace.ball x U)) := .of_inf_right hy
    rw [← mem_closure_iff_clusterPt, (UniformSpace.isClosed_ball x hU₂).closure_eq] at hy₂
    exact ⟨y, hy₁, hy₂⟩

Goal state after:
case right
α : 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 α := ⋯
hl : l.TotallyBounded
L : Compacts α := ⋯
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
⊢ ↑L ⊆ U.image ↑K
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case right
α : 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
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
x : α
hx : ClusterPt x l
⊢ U.image ↑K ∈ l

Tactic:
refine Filter.mem_of_superset (Filter.mem_lift' hK) ?_

Goal state after:
case right
α : 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
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
x : α
hx : ClusterPt x l
⊢ ⋃ K_1 ∈ {x | (fun K' ↦ (↑K, ↑K') ∈ hausdorffEntourage U) x}, ↑K_1 ⊆ U.image ↑K
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
⊢ dist p₁ (midpoint 𝕜 p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂

Tactic:
dist_left_midpoint

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.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₂ = dist p₂ (midpoint 𝕜 p₁ p₂)

Tactic:
dist_right_midpoint p₁ p₂

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.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
x y : E
⊢ edist (k • x +ᵥ c) (k • y +ᵥ c) = ↑‖k‖₊ * edist x y

Tactic:
show edist (k • x +ᵥ c) (k • y +ᵥ c) = _ from (IsometryEquiv.vaddConst c).isometry ..

Goal state after:
𝕜 : 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
x y : E
⊢ edist (k • x) (k • y) = ↑‖k‖₊ * edist x y
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.lim a✝) (c.lim x) ≤ (3 / 4) ^ (n + 1)

Tactic:
pow_succ',

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.lim a✝) (c.lim x) ≤ 3 / 4 * (3 / 4) ^ n