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

Goal state before:
pp: case e_a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : ℕ → α := fun i ↦ if i ≤ n then u i else v (i - (n + 1))
⊢ ∑ i ∈ Finset.range m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i))) =
    ∑ i ∈ Finset.Ico (n + 1) (n + 1 + m), edist (f (w (i + 1))) (f (w i))

Tactic:
Finset.range_eq_Ico

Goal state after:
case e_a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : ℕ → α := fun i ↦ if i ≤ n then u i else v (i - (n + 1))
⊢ ∑ i ∈ Finset.Ico 0 m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i))) =
    ∑ i ∈ Finset.Ico (n + 1) (n + 1 + m), edist (f (w (i + 1))) (f (w i))
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : ¬p a
⊢ cfc f a = 0

Tactic:
by
  rw [cfc_def, dif_neg (not_and_of_not_left _ ha)]

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
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(spectrum R a), R)
⊢ p ((starAlgHom (cfcHom ⋯) ⋯) g)

Tactic:
h

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✝¹⁴ : 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
ha : p a
g : C(↑(spectrum R a), R)
⊢ q ((starAlgHom (cfcHom ⋯) ⋯) g) ∧ SpectrumRestricts ((starAlgHom (cfcHom ⋯) ⋯) g) ⇑f
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)
halg : IsClosedEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
g : R → R
hg : ¬ContinuousOn g (spectrum R a)
⊢ ¬ContinuousOn (fun x ↦ (algebraMap R S) (g (f x))) (spectrum S a)

Tactic:
refine fun hg' ↦ hg ?_

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✝¹⁶ : 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)
halg : IsClosedEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
g : R → R
hg : ¬ContinuousOn g (spectrum R a)
hg' : ContinuousOn (fun x ↦ (algebraMap R S) (g (f x))) (spectrum S a)
⊢ ContinuousOn g (spectrum R a)
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✝¹⁸ : 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
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(σₙ R a), R)₀
⊢ p ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) g)

Tactic:
h

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
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(σₙ R a), R)₀
⊢ q ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) g) ∧ QuasispectrumRestricts ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) g) ⇑f
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

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

Tactic:
by
  rw [← Ring.inverse_unit]
  convert! cfc_inv (id : R → R) (a : A) ?_
  · exact (cfc_id R (a : A)).symm
  · rintro x hx rfl
    exact spectrum.zero_notMem R a.isUnit hx

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✝²⁰ : 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)
⊢ ¬ContinuousOn (fun x ↦ (algebraMap R S) (g (f x))) (σₙ S a)

Tactic:
refine fun hg' ↦ hg ?_

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)
hg' : ContinuousOn (fun x ↦ (algebraMap R S) (g (f x))) (σₙ S a)
⊢ ContinuousOn g (σₙ R a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: 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
a : A
ha : p a
f_cont : ContinuousOn f (σₙ R a)
f_zero : f 0 = 0
⊢ cfcₙ f a = (cfcₙHom ha) (mkD ((σₙ R a).domRestrict f) 0)

Tactic:
rw [cfcₙ_apply f a, mkD_of_continuousOn f_cont f_zero]

Goal state after:
Module: Mathlib.Topology.Algebra.StarSubalgebra

Goal state before:
pp: case algebraMap
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 : A
r : R
hy : (Algebra.algebraMap R A) r ∈ ↑(adjoin R {x})
⊢ P ((Algebra.algebraMap R A) r) ⋯

Tactic:
| algebraMap r =>

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
⊢ ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) =
    ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i)))

Tactic:
ofReal_sum_of_nonneg

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
⊢ ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) =
    ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i))

α : 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
⊢ ∀ i ∈ Finset.range n, 0 ≤ f (u (i + 1)) - f (u i)
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
⊢ cfcₙ (fun x ↦ star x) a = star a

Tactic:
rw [cfcₙ_star _ a, cfcₙ_id' R a]

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

Goal state before:
pp: case refine_4
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
a : ℚ
x : ℚ[X]
hx✝ : x ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
⊢ eval 1 ((⇑derivative)^[n - k] x) = 0 → eval 1 ((⇑derivative)^[n - k] (a • x)) = 0

Tactic:
h

Goal state after:
case refine_4
n k : ℕ
h✝ : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
a : ℚ
x : ℚ[X]
hx✝ : x ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
h : eval 1 ((⇑derivative)^[n - k] x) = 0
⊢ eval 1 ((⇑derivative)^[n - k] (a • x)) = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case mp.inr
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✝ : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ 0 ∈ range ⇑f

Tactic:
exact ⟨0, map_zero f⟩

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

Goal state before:

Tactic:
∑ k ∈ S, bernstein n k x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ S, bernstein n k x * (1 / 2) := by
        gcongr with k hk
        refine (hδ _ _ ?_).le
        simpa [S] using hk
      _ = 1 / 2 * ∑ k ∈ S, bernstein n k x := by rw [mul_comm, Finset.sum_mul]
      -- In this step we increase the sum over `S` back to a sum over all of `Fin (n+1)`,
      -- so that we can use `bernstein.probability`.
      _ ≤ 1 / 2 * ∑ k : Fin (n + 1), bernstein n k x := by gcongr; exact S.subset_univ
      _ = 1 / 2 := by rw [bernstein.probability, mul_one]

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

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

Tactic:
calc
      ∑ k ∈ S, bernstein n k x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ S, bernstein n k x * (1 / 2) := by
        gcongr with k hk
        refine (hδ _ _ ?_).le
        simpa [S] using hk
      _ = 1 / 2 * ∑ k ∈ S, bernstein n k x := by rw [mul_comm, Finset.sum_mul]
      -- In this step we increase the sum over `S` back to a sum over all of `Fin (n+1)`,
      -- so that we can use `bernstein.probability`.
      _ ≤ 1 / 2 * ∑ k : Fin (n + 1), bernstein n k x := by gcongr; exact S.subset_univ
      _ = 1 / 2 := by rw [bernstein.probability, mul_one]

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

Goal state before:
pp: 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, ⋯⟩
x : X
⊢ ∀ (z : X), f z - ε < ↑(h x) z

Tactic:
z

Goal state after:
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, ⋯⟩
x z : X
⊢ f z - ε < ↑(h x) z
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
φ ψ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
⊢ φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal → φ = ψ

Tactic:
h

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
A : Type u_2
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra ℝ A
φ ψ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
h : φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal
⊢ φ = ψ
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case pos.left
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
xs_w : ⋃ x ∈ xs, W x = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhds)
xs_nonempty : xs.Nonempty
k : ↑L := ⟨xs.inf' xs_nonempty fun x ↦ ↑(h x), ⋯⟩
z : X
⊢ ∃ b ∈ xs, ↑(h b) z < f z + ε

Tactic:
exact Set.exists_set_mem_of_union_eq_top _ _ xs_w z

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
φ ψ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
⊢ φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal → φ = ψ

Tactic:
h

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
φ ψ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
h : φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal
⊢ φ = ψ
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case algebraMap
𝕜 : 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, 𝕜)
r : 𝕜
⊢ p ((algebraMap 𝕜 C(↑s, 𝕜)) r)

Tactic:
| algebraMap r =>

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, 𝕜)
⊢ p f

Tactic:
refine f.induction_on const id star_id add mul fun h f ↦ frequently f ?_
  have := polynomialFunctions.starClosure_topologicalClosure s ▸ mem_top (x := f)
  rw [← SetLike.mem_coe, topologicalClosure_coe, mem_closure_iff_frequently] at this
  exact this.mp <| .of_forall h

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ x ∈ StarAlgebra.adjoin 𝕜 ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ↔
    x ∈ span 𝕜 ({1} ∪ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}))

Tactic:
← StarSubalgebra.mem_toSubalgebra,

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ x ∈ (StarAlgebra.adjoin 𝕜 ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})).toSubalgebra ↔
    x ∈ span 𝕜 ({1} ∪ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}))
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ x ∈ StarAlgebra.adjoin 𝕜 ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ↔
    x ∈ ↑(𝕜 ∙ 1) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})

Tactic:
← StarSubalgebra.mem_toSubalgebra,

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ x ∈ (StarAlgebra.adjoin 𝕜 ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})).toSubalgebra ↔
    x ∈ ↑(𝕜 ∙ 1) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})