mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
L1 : Tendsto (fun y ↦ (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
this :
  Tendsto (fun y ↦ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[<] x)
    (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
y : ℝ
hy : y - x < 0
⊢ (↑hf.stieltjesFunction y - f x) / (y - x) ≤ (f y - f x) / (y - x)

Tactic:
apply div_le_div_of_nonpos_of_le hy.le

Goal state after:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
L1 : Tendsto (fun y ↦ (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
this :
  Tendsto (fun y ↦ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[<] x)
    (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
y : ℝ
hy : y - x < 0
⊢ f y - f x ≤ ↑hf.stieltjesFunction y - f x
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
L1 : Tendsto (fun y ↦ (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
this✝ :
  Tendsto (fun y ↦ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[<] x)
    (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
y : ℝ
hy : y - x < 0
this : 0 < (y - x) ^ 2
⊢ (f y - f x) / (y - x) ≤ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)

Tactic:
apply div_le_div_of_nonpos_of_le hy.le

Goal state after:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
L1 : Tendsto (fun y ↦ (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
this✝ :
  Tendsto (fun y ↦ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[<] x)
    (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
y : ℝ
hy : y - x < 0
this : 0 < (y - x) ^ 2
⊢ ↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x ≤ f y - f x
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : u n ≤ x
v : ℕ → α := fun i ↦ if i ≤ n then u i else x
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) = ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))

Tactic:
by grind [Finset.sum_congr]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
⊢ μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ

Tactic:
restrict_sub_eq_restrict_sub_restrict hs.compl,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
⊢ μ.restrict sᶜ + (ν.restrict sᶜ - ξ.restrict sᶜ) = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
⊢ μ + (ν - ξ) = μ + ν - ξ

Tactic:
by
  let s := h.nullSet
  have hs : MeasurableSet s := h.measurableSet_nullSet
  have h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s := by
    rw [h.restrict_nullSet, restrict_sub_eq_restrict_sub_restrict hs]
    simp
  have h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ =
      μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ := by
    rw [restrict_sub_eq_restrict_sub_restrict hs.compl, h.restrict_compl_nullSet]
    simp
  calc μ + (ν - ξ)
  _ = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ := by
    rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]
  _ = μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) := by abel
  _ = (μ.restrict s + ν.restrict s - ξ.restrict s) +
      (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) := by rw [h_le_s, h_le_s_compl]
  _ = (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ := by
      simp [restrict_sub_eq_restrict_sub_restrict hs,
        restrict_sub_eq_restrict_sub_restrict hs.compl]
  _ = μ + ν - ξ := by rw [restrict_add_restrict_compl hs]

Goal state after:
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
⊢ eVariationOn (fun x ↦ (B (f x)) (g x)) s ≤ ‖B‖ₑ * (C * eVariationOn g s + D * eVariationOn f s)

Tactic:
apply iSup_le
  rintro ⟨n, ⟨u, u_mono, u_mem⟩⟩
  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.Topology.ContinuousMap.StarOrdered

Goal state before:
pp: case mp
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : PartialOrder R
inst✝⁶ : NonUnitalSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : TopologicalSpace R
inst✝² : ContinuousStar R
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousSqrt R
f g : C(α, R)
⊢ (∀ (a : α), f a ≤ g a) → ∃ s, g = f + star s * s

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : PartialOrder R
inst✝⁶ : NonUnitalSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : TopologicalSpace R
inst✝² : ContinuousStar R
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousSqrt R
f g : C(α, R)
h : ∀ (a : α), f a ≤ g a
⊢ ∃ s, g = f + star s * s
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : ∀ (i : ι), LipschitzWith 1 fun x ↦ x i
this : ∀ (i : ι), ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (fun x ↦ f x i) s x
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
filter_upwards [ae_all_iff.2 this] with x hx xs

Goal state after:
ι : Type u_2
inst✝ : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : ∀ (i : ι), LipschitzWith 1 fun x ↦ x i
this : ∀ (i : ι), ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (fun x ↦ f x i) s x
x : ℝ
hx : ∀ (i : ι), x ∈ s → DifferentiableWithinAt ℝ (fun x ↦ f x i) s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case neg
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
⊢ P (cfc f a)

Tactic:
· simp only [not_and_or] at h
    obtain (h | h) := h
    · rwa [cfc_apply_of_not_predicate _ h]
    · rwa [cfc_apply_of_not_continuousOn _ h]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : ∀ ⦃a b : ℕ⦄, a ≤ b → u a ≤ u b
u_mem : ∀ (i : ℕ), u i ∈ s
v : ℕ → α := fun i ↦ min (u i) (u n)
⊢ ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) = ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))

Tactic:
by grind [Finset.sum_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
a : A
ha : p a
⊢ cfc (fun x ↦ r) a = (algebraMap R A) r

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

Goal state after:
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 μ
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
a : Set α
ha : 0 < μ a
h'a : μ a < ∞
h''a : IntegrableOn f a μ
⊢ ‖⨍ (y : α) in a, f y ∂μ - f x‖ ≤ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ

Tactic:
nth_rw 1 [← setAverage_const ha.ne' h'a.ne (f x)]

Goal state after:
α : Type u_1
inst✝⁶ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SecondCountableTopology α
inst✝³ : BorelSpace α
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
a : Set α
ha : 0 < μ a
h'a : μ a < ∞
h''a : IntegrableOn f a μ
⊢ ‖⨍ (y : α) in a, f y ∂μ - ⨍ (x_1 : α) in a, f x ∂μ‖ ≤ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
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
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
⊢ CompactSpace ↑(spectrum R a)

Tactic:
have := ContinuousFunctionalCalculus.compactSpace_spectrum (R := S) a
    rw [← isCompact_iff_compactSpace] at this ⊢
    simpa using halg.isCompact_preimage this

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

Goal state before:
pp: case monomial
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
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
n : ℕ
r : R
a✝ : cfc (fun x ↦ Polynomial.eval (f x) (Polynomial.C r * X ^ n)) a = (aeval (cfc f a)) (Polynomial.C r * X ^ n)
⊢ cfc (fun x ↦ r * f x ^ (n + 1)) a = (algebraMap R A) r * cfc f a ^ (n + 1)

Tactic:
rw [cfc_const_mul .., cfc_pow _ (n + 1) _, ← smul_eq_mul, algebraMap_smul]

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 α
hs : IsOpen[inst✝¹] s
x : α
hx : x ∈ s
⊢ MapClusterPt (Function.leftLim f x) (𝓝[s] x) f

Tactic:
rw [IsOpen.nhdsWithin_eq hs hx]

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hs : IsOpen[inst✝¹] s
x : α
hx : x ∈ s
⊢ MapClusterPt (Function.leftLim f x) (𝓝 x) f
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 α
hs : IsOpen[inst✝¹] s
x : α
hx : x ∈ s
⊢ MapClusterPt (Function.rightLim f x) (𝓝[s] x) f

Tactic:
rw [IsOpen.nhdsWithin_eq hs hx]

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hs : IsOpen[inst✝¹] s
x : α
hx : x ∈ s
⊢ MapClusterPt (Function.rightLim f x) (𝓝 x) f
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝ : CommRing R
k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
⊢ k + 1 ≤ ν →
    ↑n *
        (Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) ν)) -
          Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) (ν + 1)))) =
      0

Tactic:
intro h

Goal state after:
case succ.succ
R : Type u_1
inst✝ : CommRing R
k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
⊢ ↑n *
      (Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) ν)) -
        Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) (ν + 1)))) =
    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
f : R → R
⊢ cfcₙ f 0 = 0

Tactic:
by_cases hf0 : f 0 = 0

Goal state after:
case pos
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
hf0 : f 0 = 0
⊢ cfcₙ f 0 = 0

case neg
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
hf0 : ¬f 0 = 0
⊢ cfcₙ f 0 = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg.inr.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
⊢ cfcₙ (fun x ↦ -f x) a = -cfcₙ f a

Tactic:
rw [cfcₙ_apply_of_not_continuousOn a hf, cfcₙ_apply_of_not_continuousOn, neg_zero]
      exact fun hf_neg ↦ hf <| by simpa using hf_neg.fun_neg

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2

Tactic:
trans MvPolynomial.aeval e (pderiv true (pderiv true ((x + y) ^ n))) * X ^ 2

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := ⋯
y : MvPolynomial Bool R := ⋯
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := ⋯
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν =
    (MvPolynomial.aeval e) ((pderiv true) ((pderiv true) ((x + y) ^ n))) * X ^ 2

R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := ⋯
y : MvPolynomial Bool R := ⋯
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := ⋯
⊢ (MvPolynomial.aeval e) ((pderiv true) ((pderiv true) ((x + y) ^ n))) * X ^ 2 = (n * (n - 1)) • X ^ 2
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 := ⋯ }
⊢ 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:
have := uniformSpace_eq_inf_precomp_of_cover (β := R) f (0 : C(Unit, σₙ R a))
    (map_continuous f).isProperMap (map_continuous 0).isProperMap <| by
      simp only [← Subtype.val_injective.image_injective.eq_iff, f, ContinuousMap.coe_mk,
        ContinuousMap.coe_zero, range_zero, image_union, image_singleton,
        quasispectrum.coe_zero, ← range_comp, val_comp_inclusion, image_univ, Subtype.range_coe,
        quasispectrum_eq_spectrum_union_zero]

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)) =
    𝓤 C(↑(σₙ R a), R)₀
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))
⊢ ∃ x, dist x f < ε ∧ x ∈ L

Tactic:
have ys_nonempty : ∀ x, (ys x).Nonempty := fun x =>
    Set.nonempty_of_union_eq_top_of_nonempty _ _ nX (ys_w x)

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
⊢ ∃ x, dist x f < ε ∧ x ∈ L