mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ v.limRatioMeas hρ ⁻¹' {0}
⊢ ∃ u ∈ 𝓝[v.limRatioMeas hρ ⁻¹' {0}] x, ρ u = 0

Tactic:
obtain ⟨o, xo, o_open, μo⟩ : ∃ o : Set α, x ∈ o ∧ IsOpen o ∧ μ o < ∞ :=
    Measure.exists_isOpen_measure_lt_top μ x

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : μ o < ∞
⊢ ∃ u ∈ 𝓝[v.limRatioMeas hρ ⁻¹' {0}] x, ρ u = 0
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
E✝ : Type u_2
inst✝ : PseudoEMetricSpace E✝
f : α → E✝
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : n = 0
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))

Tactic:
simp [hn₀]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 (s.indicator 1 x))

Tactic:
have : IsLocallyFiniteMeasure (μ.restrict s) :=
    isLocallyFiniteMeasure_of_le restrict_le_self

Goal state after:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
hs : MeasurableSet s
this : IsLocallyFiniteMeasure (μ.restrict s)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 (s.indicator 1 x))
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
a : A
ha : p a
inst✝ : UniqueHom R A
φ : C(↑(spectrum R a), R) →⋆ₐ[R] A
hφ₁ : Continuous[_, inst✝⁴] ⇑φ
hφ₂ : φ (restrict (spectrum R a) (ContinuousMap.id R)) = a
⊢ a = φ (restrict (spectrum R a) (ContinuousMap.id R))

Tactic:
hφ₂

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
a : A
ha : p a
inst✝ : UniqueHom R A
φ : C(↑(spectrum R a), R) →⋆ₐ[R] A
hφ₁ : Continuous[_, inst✝⁴] ⇑φ
hφ₂ : φ (restrict (spectrum R a) (ContinuousMap.id R)) = a
⊢ a = 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
r : R
a : A
ha : p a
⊢ cfc (fun x ↦ r) a = (algebraMap R A) r

Tactic:
rw [cfc_apply (fun _ : R ↦ r) a, ← AlgHomClass.commutes (cfcHom ha (p := p)) r]

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
a : A
ha : p a
⊢ (cfcHom ha) { toFun := (spectrum R a).domRestrict fun x ↦ r, continuous_toFun := ⋯ } =
    (cfcHom ha) ((algebraMap R C(↑(spectrum R a), R)) r)
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 α
hf : BoundedVariationOn f s
x : α
this :
  (fun y ↦ eVariationOn f (s ∩ Ioc x y)) = fun y ↦
    eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Ico (toDual y) (toDual x))
⊢ Tendsto (fun y ↦ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Ico (toDual y) (toDual x))) (𝓝[s] x) (𝓝 0)

Tactic:
exact hf.ofDual.tendsto_eVariationOn_Ico_zero (toDual x)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Semifield S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalSemiring S
inst✝¹² : ContinuousStar S
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus S A q
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
⊢ cfcHom hpa = starAlgHom (cfcHom hqa) h

Tactic:
apply cfcHom_eq_of_continuous_of_map_id

Goal state after:
case hφ₁
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Semifield S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalSemiring S
inst✝¹² : ContinuousStar S
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus S A q
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
⊢ Continuous[_, inst✝³] ⇑(starAlgHom (cfcHom hqa) h)

case hφ₂
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Semifield S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalSemiring S
inst✝¹² : ContinuousStar S
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus S A q
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
⊢ (starAlgHom (cfcHom hqa) h) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a
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
f g : R → R
a : A
hg' : ∀ x ∈ spectrum R a, g x ≠ 0
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ cfc (fun x ↦ f x / g x) a = cfc f a * (cfc g a)⁻¹ʳ

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
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
f g : R → R
a : A
hg' : ∀ x ∈ spectrum R a, g x ≠ 0
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ cfc (fun x ↦ f x * (g x)⁻¹) a = cfc f a * (cfc g a)⁻¹ʳ
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
a : A
ha : p a
inst✝ : UniqueHom R A
φ : C(↑(σₙ R a), R)₀ →⋆ₙₐ[R] A
hφ₁ : Continuous[_, inst✝⁴] ⇑φ
hφ₂ : φ (ContinuousMapZero.id (σₙ R a)) = a
⊢ a = φ (ContinuousMapZero.id (σₙ R a))

Tactic:
hφ₂

Goal state after:
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
a : A
ha : p a
inst✝ : UniqueHom R A
φ : C(↑(σₙ R a), R)₀ →⋆ₙₐ[R] A
hφ₁ : Continuous[_, inst✝⁴] ⇑φ
hφ₂ : φ (ContinuousMapZero.id (σₙ R a)) = a
⊢ a = a
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
inst✝ : UniqueHom R A
f : R → R
n : ℤ
a : Aˣ
hf : ContinuousOn f ((fun x ↦ x ^ n) '' spectrum R ↑a)
ha : p ↑a
⊢ cfc (fun x ↦ f (x ^ n)) ↑a = cfc f ↑(a ^ n)

Tactic:
rw [cfc_comp' .., cfc_zpow a]

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

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁵ : Semifield R
inst✝²⁴ : StarRing R
inst✝²³ : MetricSpace R
inst✝²² : IsTopologicalSemiring R
inst✝²¹ : ContinuousStar R
inst✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : TopologicalSpace A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus S A q
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts a ⇑f
g : R → R
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
⊢ cfcₙ
      (Function.extend Subtype.val
        (⇑({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
            ({ toFun := (σₙ R a).domRestrict g, continuous_toFun := ⋯, map_zero' := ⋯ }.comp
              { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })))
        0)
      a =
    cfcₙ (fun x ↦ (algebraMap R S) (g (f x))) a

Tactic:
apply cfcₙ_congr fun x hx ↦ ?_

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁵ : Semifield R
inst✝²⁴ : StarRing R
inst✝²³ : MetricSpace R
inst✝²² : IsTopologicalSemiring R
inst✝²¹ : ContinuousStar R
inst✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : TopologicalSpace A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus S A q
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts a ⇑f
g : R → R
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
x : S
hx : x ∈ σₙ S a
⊢ Function.extend Subtype.val
      (⇑({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
          ({ toFun := (σₙ R a).domRestrict g, continuous_toFun := ⋯, map_zero' := ⋯ }.comp
            { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })))
      0 x =
    (algebraMap R S) (g (f x))
Module: Mathlib.Topology.Algebra.StarSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Semiring A
inst✝⁴ : StarRing A
inst✝³ : IsSemitopologicalSemiring A
inst✝² : ContinuousStar A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
x y✝ : A
hy✝ : y✝ ∈ elemental R x
P : (u : A) → u ∈ elemental R x → Prop
self : P x ⋯
star_self : P (star x) ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A) r) ⋯
add : ∀ (u : A) (hu : u ∈ elemental R x) (v : A) (hv : v ∈ elemental R x), P u hu → P v hv → P (u + v) ⋯
mul : ∀ (u : A) (hu : u ∈ elemental R x) (v : A) (hv : v ∈ elemental R x), P u hu → P v hv → P (u * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ ↑(elemental R x)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst✝⁶] s), P v ⋯
y u : A
hu : u ∈ {x} ∪ star {x}
hy : u ∈ ↑(adjoin R {x})
⊢ ?m.230

Tactic:
by simpa using hu

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

Goal state before:
pp: case refine_2.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * ↑(n - ν) = ↑(n + 1) * (↑(n.choose (ν + 1)) * X ^ (ν + 1))

Tactic:
rw [mul_comm, ← mul_assoc, ← mul_assoc]

Goal state after:
case refine_2.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(n - ν) * ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) = ↑(n + 1) * ↑(n.choose (ν + 1)) * X ^ (ν + 1)
Module: Mathlib.Topology.ContinuousMap.Weierstrass

Goal state before:
pp: a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∃ᶠ (x : C(↑(Set.Icc a b), ℝ)) in nhds f, x ∈ ↑(polynomialFunctions (Set.Icc a b)).toSubsemiring
⊢ ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

Tactic:
Metric.nhds_basis_ball.frequently_iff

Goal state after:
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑(polynomialFunctions (Set.Icc a b)).toSubsemiring
⊢ ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε
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
h : Function.Injective ⇑(mul 𝕜 A)
⊢ Function.Injective ⇑(splitMul 𝕜 A)

Tactic:
injective_iff_map_eq_zero

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
h : Function.Injective ⇑(mul 𝕜 A)
⊢ ∀ (a : Unitization 𝕜 A), (splitMul 𝕜 A) a = 0 → a = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
A : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
φ ψ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst✝²] ⇑φ
hψ : Continuous[_, inst✝²] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) = ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
⊢ φ = ψ

Tactic:
let s' : Set ℝ := (↑) '' s

Goal state after:
X : Type u_1
inst✝⁶ : TopologicalSpace X
A : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
φ ψ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst✝²] ⇑φ
hψ : Continuous[_, inst✝²] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) = ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
s' : Set ℝ := toReal '' s
⊢ φ = ψ
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∃ᶠ (x : C(X, ℝ)) in 𝓝 f, x ∈ ↑A.toSubsemiring
⊢ ∃ g, ‖↑g - f‖ < ε

Tactic:
Metric.nhds_basis_ball.frequently_iff

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑A.toSubsemiring
⊢ ∃ g, ‖↑g - f‖ < ε
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ g, ‖↑g - f‖ < ε

Tactic:
by
  have w :=
    mem_closure_iff_frequently.mp (continuousMap_mem_subalgebra_closure_of_separatesPoints A w f)
  rw [Metric.nhds_basis_ball.frequently_iff] at w
  obtain ⟨g, H, m⟩ := w ε pos
  rw [Metric.mem_ball, dist_eq_norm] at H
  exact ⟨⟨g, m⟩, H⟩

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

Goal state before:
pp: X : Type u_1
inst✝⁹ : TopologicalSpace X
inst✝⁸ : Zero X
A : Type u_2
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsSemitopologicalRing A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
⊢ φ = ψ

Tactic:
let s' : Set ℝ := (↑) '' s

Goal state after:
X : Type u_1
inst✝⁹ : TopologicalSpace X
inst✝⁸ : Zero X
A : Type u_2
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsSemitopologicalRing A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
s' : Set ℝ := toReal '' s
⊢ φ = ψ
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 ∈ RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)
hf₁ : f ∈ ↑(𝕜 ∙ 1) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
⊢ f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

Tactic:
Set.mem_add,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
this : ∀ (u : Set β), (f ⁻¹' Iic uᶜ)ᶜ = {x | (f x ∩ u).Nonempty}
⊢ LowerHemicontinuous f ↔ ∀ (u : Set β), IsOpen[inst✝] u → IsOpen[inst✝¹] (f ⁻¹' Iic uᶜ)ᶜ

Tactic:
simpa [this] using lowerHemicontinuous_iff_isOpen_inter_nonempty

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 α
hf : UpperHemicontinuousOn f s
u : Set β
hu : IsClosed[inst✝] u
⊢ UpperHemicontinuousOn (fun x ↦ f x ∩ u) s

Tactic:
rw [upperHemicontinuousOn_iff] at hf ⊢
  exact (hf · · |>.inter hu)

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s K : Set α
hKs : K ∈ 𝒫 closure[inst✝] s
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
ht₁ : K ⊆ ⋃₀ u
ht₂ : ∀ U ∈ u, (K ∩ U).Nonempty
⊢ ({s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty} ∩ {t | t.Finite ∧ t ⊆ s}).Nonempty

Tactic:
choose x hxU hxs using fun U : u => show (↑U ∩ s).Nonempty by
      obtain ⟨x, hxK, hxV⟩ := ht₂ U U.prop
      exact mem_closure_iff.mp (hKs hxK) _ (hu₂ _ U.prop) hxV

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s K : Set α
hKs : K ∈ 𝒫 closure[inst✝] s
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
ht₁ : K ⊆ ⋃₀ u
ht₂ : ∀ U ∈ u, (K ∩ U).Nonempty
x : ↑u → α
hxU : ∀ (U : ↑u), x U ∈ ↑U
hxs : ∀ (U : ↑u), x U ∈ s
⊢ ({s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty} ∩ {t | t.Finite ∧ t ⊆ s}).Nonempty
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ inst✝ =
    induced (fun x ↦ {x})
      (generateFrom (powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}))

Tactic:
induced_generateFrom_eq,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ inst✝ =
    generateFrom
      ((preimage fun x ↦ {x}) ''
        (powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}))
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
⊢ 𝓝 s ≤ 𝓝 s

Tactic:
nhds_eq_comap_uniformity,

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
⊢ 𝓝 s ≤ Filter.comap (Prod.mk s) (𝓤 (Set α))
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F₁ F₂ : Closeds α
h : Inseparable F₁ F₂
x : α
hx₁ : x ∈ F₁
⊢ ∃ᶠ (y : α) in 𝓝 x, y ∈ ↑F₂

Tactic:
nhds_eq_comap_uniformity,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F₁ F₂ : Closeds α
h : Inseparable F₁ F₂
x : α
hx₁ : x ∈ F₁
⊢ ∃ᶠ (y : α) in Filter.comap (Prod.mk x) (𝓤 α), y ∈ ↑F₂
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 α
⊢ IsCompact Set.univ

Tactic:
simpa [gi.l_surjective.range_eq]
    using isCompact_univ.image continuous_closure

Goal state after: