mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ ∃ p q,
    MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q ∧ ∀ x ∈ s, ∀ y ∈ s, p y - p x + (q y - q x) = variationOnFromTo f s x y

Tactic:
refine ⟨fun x ↦ (variationOnFromTo f s c x + f x) / 2,
    fun x ↦ (variationOnFromTo f s c x - f x) / 2, ?_, ?_, ?_, ?_⟩

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ MonotoneOn (fun x ↦ (variationOnFromTo f s c x + f x) / 2) s

case inr.refine_2
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ MonotoneOn (fun x ↦ (variationOnFromTo f s c x - f x) / 2) s

case inr.refine_3
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ f = (fun x ↦ (variationOnFromTo f s c x + f x) / 2) - fun x ↦ (variationOnFromTo f s c x - f x) / 2

case inr.refine_4
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ ∀ x ∈ s,
    ∀ y ∈ s,
      (fun x ↦ (variationOnFromTo f s c x + f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x + f x) / 2) x +
          ((fun x ↦ (variationOnFromTo f s c x - f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x - f x) / 2) x) =
        variationOnFromTo f s x y
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: α : Type u_2
inst✝⁶ : LinearOrder α
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set α
f : α → E
g : α → F
C D : ℝ≥0∞
hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C
hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D
B : E →L[ℝ] F →L[ℝ] G
n : ℕ
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1,
      edist ((fun x ↦ (B (f x)) (g x)) (↑(n, ⟨u, ⋯⟩).2 (i + 1))) ((fun x ↦ (B (f x)) (g x)) (↑(n, ⟨u, ⋯⟩).2 i)) ≤
    ‖B‖ₑ * (C * eVariationOn g s + D * eVariationOn f s)

Tactic:
calc ∑ i ∈ range n, edist (B (f (u (i + 1))) (g (u (i + 1)))) (B (f (u i)) (g (u i)))
  _ ≤ ∑ i ∈ range n, edist (B (f (u (i + 1))) (g (u (i + 1)))) (B (f (u i)) (g (u (i + 1)))) +
      ∑ i ∈ range n, edist (B (f (u i)) (g (u (i + 1)))) (B (f (u i)) (g (u i))) := by
    rw [← Finset.sum_add_distrib]
    gcongr with i hi
    apply edist_triangle
  _ = ∑ i ∈ range n, ‖B (f (u (i + 1)) - f (u i)) (g (u (i + 1)))‖ₑ +
      ∑ i ∈ range n, ‖B (f (u i)) (g (u (i + 1)) - g (u i))‖ₑ := by simp [edist_eq_enorm_sub]
  _ ≤ ∑ i ∈ range n, ‖B‖ₑ * ‖f (u (i + 1)) - f (u i)‖ₑ * ‖g (u (i + 1))‖ₑ +
      ∑ i ∈ range n, ‖B‖ₑ * ‖f (u i)‖ₑ * ‖g (u (i + 1)) - g (u i)‖ₑ := by
    gcongr with i hi i hi
    · apply ContinuousLinearMap.le_opENorm₂
    · apply ContinuousLinearMap.le_opENorm₂
  _ ≤ ∑ i ∈ range n, ‖B‖ₑ * ‖f (u (i + 1)) - f (u i)‖ₑ * D +
      ∑ i ∈ range n, ‖B‖ₑ * C * ‖g (u (i + 1)) - g (u i)‖ₑ := by
    gcongr with i hi i hi
    · apply hg _ (u_mem _)
    · apply hf _ (u_mem _)
  _ = ‖B‖ₑ * D * ∑ i ∈ range n, ‖f (u (i + 1)) - f (u i)‖ₑ +
      ‖B‖ₑ * C * ∑ i ∈ range n, ‖g (u (i + 1)) - g (u i)‖ₑ := by
    simp only [← sum_mul, ← mul_sum]
    ring
  _ ≤ ‖B‖ₑ * D * eVariationOn f s + ‖B‖ₑ * C * eVariationOn g s := by
    simp only [← edist_eq_enorm_sub]
    gcongr
    · exact eVariationOn.sum_le_of_monotoneOn_Iic (u_mono.monotoneOn _) (fun i hi ↦ u_mem i)
    · exact eVariationOn.sum_le_of_monotoneOn_Iic (u_mono.monotoneOn _) (fun i hi ↦ u_mem i)
  _ = ‖B‖ₑ * (C * eVariationOn g s + D * eVariationOn f s) := by ring

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 α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a ↦ μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
⊢ ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1

Tactic:
refine ae_restrict_of_ae_restrict_of_subset (subset_toMeasurable μ s) ?_

Goal state after:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a ↦ μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
⊢ ∀ᵐ (x : α) ∂μ.restrict (toMeasurable μ s), t.indicator 1 x = 1
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K} :=
  μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x ↦ c) x‖ₑ)
x : α
hx :
  ∀ (n : ℕ),
    ∀ c ∈ t,
      Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
        (𝓝 ‖f x - (A.set n).indicator (fun x ↦ c) x‖ₑ)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
c : E
hc : c ∈ t
⊢ ∃ n, x ∈ A.set n

Tactic:
simpa [← A.spanning] using mem_univ x

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✝ : 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
x : ↑(spectrum R a)
⊢ (spectrum R a).domRestrict f x ∈ f '' spectrum R a

Tactic:
use x.1

Goal state after:
case h
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
x : ↑(spectrum R a)
⊢ ↑x ∈ spectrum R a ∧ f ↑x = (spectrum R a).domRestrict f x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
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✝ : CompleteSpace R
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
hφ : IsClosedEmbedding ⇑φ
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
halg : IsUniformEmbedding ⇑(algebraMap R S)
⊢ IsClosedEmbedding ⇑(nonUnitalStarAlgHom φ h)

Tactic:
by
  have : h.homeomorph.symm 0 = 0 := Subtype.ext (map_zero <| algebraMap _ _)
  refine hφ.comp <| IsUniformEmbedding.isClosedEmbedding <| .comp
    (ContinuousMapZero.isUniformEmbedding_comp _ halg)
    (UniformEquiv.arrowCongrLeft₀ h.homeomorph.symm this |>.isUniformEmbedding)

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

Goal state before:
pp: case refine_1
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
f : C(↑(σₙ R a), R)₀
f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀
hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)
g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀
ψ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] C(↑(σₙ R a), R)₀ :=
  { toFun := fun x ↦ x.comp f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ
⊢ Continuous[_, inst✝⁴] ⇑φ

Tactic:
refine (cfcₙHom_continuous ha).comp <| continuous_induced_rng.mpr ?_

Goal state after:
case refine_1
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
f : C(↑(σₙ R a), R)₀
f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀
hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)
g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀
ψ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] C(↑(σₙ R a), R)₀ :=
  { toFun := fun x ↦ x.comp f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ
⊢ Continuous (_root_.toContinuousMap ∘ ⇑↑ψ.toNonUnitalAlgHom)
Module: Mathlib.Topology.Algebra.StarSubalgebra

Goal state before:
pp: case mem.inr
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})
hu : star u = x
⊢ P u ⋯

Tactic:
· simp_rw [← hu, star_star] at star_self
      exact star_self

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
a b : α
hf : MonotoneOn f s
as : a ∈ s
bs : b ∈ s
hab : a ≤ b
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Set.Icc a b
⊢ ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) = ENNReal.ofReal (f (u n) - f (u 0))

Tactic:
sum_range_sub (f <| u ·)

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
a b : α
hf : MonotoneOn f s
as : a ∈ s
bs : b ∈ s
hab : a ≤ b
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Set.Icc a b
⊢ ENNReal.ofReal (f (u n) - f (u 0)) = ENNReal.ofReal (f (u n) - f (u 0))
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
x : ↑(σₙ R a)
⊢ (σₙ R a).domRestrict f x ∈ f '' σₙ R a

Tactic:
use x.1

Goal state after:
case h
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
x : ↑(σₙ R a)
⊢ ↑x ∈ σₙ R a ∧ f ↑x = (σₙ R a).domRestrict f x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

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✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this :
  inferInstance =
    UniformSpace.comap (fun x ↦ x.comp f) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp 0) inferInstance
⊢ Filter.comap
      (fun x ↦
        (↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
                  toContinuousMapHom).toNonUnitalAlgHom
            x.1,
          ↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
                  toContinuousMapHom).toNonUnitalAlgHom
            x.2))
      (𝓤 C(↑(spectrum R a), R)) =
    𝓤 C(↑(σₙ R a), R)₀

Tactic:
simp_rw +instances [← isUniformEmbedding_toContinuousMap.comap_uniformity, this,
    @inf_uniformity _ (.comap _ _) (.comap _ _), uniformity_comap, Filter.comap_inf,
    Filter.comap_comap]

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✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this :
  inferInstance =
    UniformSpace.comap (fun x ↦ x.comp f) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp 0) inferInstance
⊢ Filter.comap
      (fun x ↦
        (↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
                  toContinuousMapHom).toNonUnitalAlgHom
            x.1,
          ↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
                  toContinuousMapHom).toNonUnitalAlgHom
            x.2))
      (𝓤 C(↑(spectrum R a), R)) =
    Filter.comap ((Prod.map (fun x ↦ x.comp f) fun x ↦ x.comp f) ∘ fun x ↦ (↑x.1, ↑x.2)) (𝓤 C(↑(spectrum R a), R)) ⊓
      Filter.comap ((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (𝓤 C(Unit, R))
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: case hbc
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 := ⋯
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 : Fin (n + 1)
hk : k ∈ Sᶜ
⊢ 1 ≤ (↑x - ↑k/ₙ) ^ 2 / δ ^ 2

Tactic:
simpa [one_le_div₀, hδ₀, sq_le_sq, S, abs_of_pos, ← Real.dist_eq, dist_comm (x : ℝ)]
          using! hk

Goal state after:
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
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
f g : C(X, ℝ)
this :
  φ (f * g).toNNReal + φ (-f).toNNReal * φ g.toNNReal + φ f.toNNReal * φ (-g).toNNReal -
      (φ (-(f * g)).toNNReal + φ f.toNNReal * φ g.toNNReal + φ (-f).toNNReal * φ (-g).toNNReal) =
    0
⊢ φ (f * g).toNNReal - φ (-(f * g)).toNNReal -
      (φ f.toNNReal * φ g.toNNReal - φ (-f).toNNReal * φ g.toNNReal -
        (φ f.toNNReal * φ (-g).toNNReal - φ (-f).toNNReal * φ (-g).toNNReal)) =
    0

Tactic:
convert! this using 1

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
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
f g : C(X, ℝ)
this :
  φ (f * g).toNNReal + φ (-f).toNNReal * φ g.toNNReal + φ f.toNNReal * φ (-g).toNNReal -
      (φ (-(f * g)).toNNReal + φ f.toNNReal * φ g.toNNReal + φ (-f).toNNReal * φ (-g).toNNReal) =
    0
⊢ φ (f * g).toNNReal - φ (-(f * g)).toNNReal -
      (φ f.toNNReal * φ g.toNNReal - φ (-f).toNNReal * φ g.toNNReal -
        (φ f.toNNReal * φ (-g).toNNReal - φ (-f).toNNReal * φ (-g).toNNReal)) =
    φ (f * g).toNNReal + φ (-f).toNNReal * φ g.toNNReal + φ f.toNNReal * φ (-g).toNNReal -
      (φ (-(f * g)).toNNReal + φ f.toNNReal * φ g.toNNReal + φ (-f).toNNReal * φ (-g).toNNReal)
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
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
f g : C(X, ℝ)
this :
  φ (f + g).toNNReal + φ (-f).toNNReal + φ (-g).toNNReal - (φ (-(f + g)).toNNReal + φ f.toNNReal + φ g.toNNReal) = 0
⊢ φ (f + g).toNNReal - φ (-(f + g)).toNNReal - (φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)) = 0

Tactic:
convert! this using 1

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
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
f g : C(X, ℝ)
this :
  φ (f + g).toNNReal + φ (-f).toNNReal + φ (-g).toNNReal - (φ (-(f + g)).toNNReal + φ f.toNNReal + φ g.toNNReal) = 0
⊢ φ (f + g).toNNReal - φ (-(f + g)).toNNReal - (φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)) =
    φ (f + g).toNNReal + φ (-f).toNNReal + φ (-g).toNNReal - (φ (-(f + g)).toNNReal + φ f.toNNReal + φ g.toNNReal)
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
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝¹] ⇑φ
⊢ Continuous[_, inst✝¹] ⇑φ.realContinuousMapZeroOfNNReal

Tactic:
dsimp [realContinuousMapZeroOfNNReal]
  fun_prop

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

Goal state before:
pp: case refine_2
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst✝¹³ : CommRing K
inst✝¹² : Ring A
inst✝¹¹ : Algebra K A
inst✝¹⁰ : TopologicalSpace K
inst✝⁹ : T1Space K
inst✝⁸ : TopologicalSpace A
inst✝⁷ : ContinuousSub A
inst✝⁶ : ContinuousSMul K A
inst✝⁵ : FunLike F A K
inst✝⁴ : AlgHomClass F K A K
inst✝³ : SetLike S A
inst✝² : OneMemClass S A
inst✝¹ : AddSubgroupClass S A
inst✝ : SMulMemClass S K A
φ : F
hφ : Continuous[inst✝⁸, inst✝¹⁰] ⇑φ
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 ↑s).NeBot
hxφ : φ x = 0
this : Tendsto (fun y ↦ y - φ y • 1) (𝓝 x ⊓ 𝓟 ↑s) (𝓝 x)
⊢ ∀ᶠ (x : A) in 𝓝 x, x ∈ ↑s → x - φ x • 1 ∈ ↑s ∩ ↑(RingHom.ker φ)

Tactic:
filter_upwards [] with g hg using
      ⟨sub_mem hg (SMulMemClass.smul_mem _ <| one_mem _), by simp [RingHom.mem_ker]⟩

Goal state after:
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}
⊢ ∃ t_1 ⊆ {x | (f x ∩ g x ∩ t).Nonempty}, IsOpen[inst✝¹] t_1 ∧ x ∈ t_1

Tactic:
refine ⟨U ∩ {x' | (f x' ∩ (t ∩ V)).Nonempty}, ?_, hU.inter (hf _ (ht.inter hV)),
      ⟨hxU, y, hyf, hyt, hyV⟩⟩

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}
⊢ U ∩ {x' | (f x' ∩ (t ∩ V)).Nonempty} ⊆ {x | (f x ∩ g x ∩ t).Nonempty}
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
⊢ UniformContinuous fun x ↦ x.1 ∪ x.2

Tactic:
by
  refine Filter.tendsto_lift'.mpr fun U hU => ?_
  filter_upwards [entourageProd_mem_uniformity (Filter.mem_lift' hU) (Filter.mem_lift' hU)]
    with _ ⟨h₁, h₂⟩ using union_mem_hausdorffEntourage U h₁ h₂

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

Goal state before:
pp: case inr.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}
x : α
hs : {x} ∈ (range fun x ↦ {x})ᶜ
h : {x}.Nonempty
⊢ (range fun x ↦ {x})ᶜ ∈ 𝓝 {x}

Tactic:
cases hs <| Set.mem_range_self x

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 γ
K : Compacts α
⊢ 𝓝 K = 𝓝 K

Tactic:
simp_rw [nhds_induced, K.isCompact.nhds_hausdorff_eq_nhds_vietoris]

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

Goal state before:
pp: case refine_2.inl
α : 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 ∈ 𝒫 U
x : α
hx : x ∈ s
y : α
hyt : y ∈ t
hxy : x ⤳ y
⊢ x ∈ U

Tactic:
exact hxy.mem_open hU <| hs hyt

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 γ
K : NonemptyCompacts α
⊢ 𝓝 K = 𝓝 K

Tactic:
simp_rw [nhds_induced, K.isCompact.nhds_hausdorff_eq_nhds_vietoris]

Goal state after: