mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
x✝ : R
⊢ s.sum f x✝ = ∑ i ∈ s, f i x✝

Tactic:
;

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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
x✝ : R
⊢ s.sum f x✝ = ∑ i ∈ s, f i x✝
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ Polynomial.eval 0 (↑(n.choose 0) * X ^ 0 * (1 - X) ^ (n - 0)) = 1

Tactic:
;

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ Polynomial.eval 0 (↑(n.choose 0) * X ^ 0 * (1 - X) ^ (n - 0)) = 1
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
ν : ℕ
⊢ Polynomial.eval 1 (↑(ν.choose ν) * X ^ ν * (1 - X) ^ (ν - ν)) = 1

Tactic:
;

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
ν : ℕ
⊢ Polynomial.eval 1 (↑(ν.choose ν) * X ^ ν * (1 - X) ^ (ν - ν)) = 1
Module: Mathlib.RingTheory.Polynomial.Bernstein

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

Tactic:
;

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

Goal state before:
pp: 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)

Tactic:
;

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.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
ν n✝ : ℕ
⊢ Polynomial.derivative (bernsteinPolynomial R (n✝ + 1) (ν + 1)) =
    (↑n✝ + 1) * (bernsteinPolynomial R (n✝ + 1 - 1) ν - bernsteinPolynomial R (n✝ + 1 - 1) (ν + 1))

Tactic:
;

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
ν n✝ : ℕ
⊢ Polynomial.derivative (bernsteinPolynomial R (n✝ + 1) (ν + 1)) =
    (↑n✝ + 1) * (bernsteinPolynomial R (n✝ + 1 - 1) ν - bernsteinPolynomial R (n✝ + 1 - 1) (ν + 1))
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:
;

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
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
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: 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

Tactic:
;

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.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
a✝ : R
⊢ X.toContinuousMap a✝ = (ContinuousMap.id R) a✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
a✝ : R
⊢ X.toContinuousMap a✝ = (ContinuousMap.id R) a✝
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
a✝ : ↑s
⊢ (X.toContinuousMapOn s) a✝ = (restrict s (ContinuousMap.id R)) a✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
a✝ : ↑s
⊢ (X.toContinuousMapOn s) a✝ = (restrict s (ContinuousMap.id R)) a✝
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ¬eval (↑x) Polynomial.X = eval (↑y) Polynomial.X

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ¬eval (↑x) Polynomial.X = eval (↑y) Polynomial.X
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case refine_1
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
a : ℕ
w : a < k
⊢ eval 1 ((⇑derivative)^[n - k] (bernsteinPolynomial ℚ n ↑⟨a, w⟩)) = 0

Tactic:
;

Goal state after:
case refine_1
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
a : ℕ
w : a < k
⊢ eval 1 ((⇑derivative)^[n - k] (bernsteinPolynomial ℚ n ↑⟨a, w⟩)) = 0
Module: Mathlib.RingTheory.Polynomial.Bernstein

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

Tactic:
;

Goal state after:
case refine_3
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
x y : ℚ[X]
hx✝ : x ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
hy✝ : y ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
hx : eval 1 ((⇑derivative)^[n - k] x) = 0
hy : eval 1 ((⇑derivative)^[n - k] y) = 0
⊢ eval 1 ((⇑derivative)^[n - k] (x + y)) = 0
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)
h : eval 1 ((⇑derivative)^[n - k] x) = 0
⊢ eval 1 ((⇑derivative)^[n - k] (a • x)) = 0

Tactic:
;

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.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
⊢ Pi.single true 1 true = 1

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
⊢ Pi.single true 1 true = 1
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
⊢ Pi.single true 1 false = 0

Tactic:
;

Goal state after:
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
⊢ Pi.single true 1 false = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: 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
⊢ cfcₙ (-f) a = (-cfcₙ f) a

Tactic:
;

Goal state after:
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
⊢ cfcₙ (-f) a = (-cfcₙ f) a
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: case h
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)) := ⋯
⊢ S ⊆ Finset.univ

Tactic:
;

Goal state after:
case h
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)) := ⋯
⊢ S ⊆ Finset.univ
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: case h
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)) := ⋯
⊢ Sᶜ ⊆ Finset.univ

Tactic:
;

Goal state after:
case h
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)) := ⋯
⊢ Sᶜ ⊆ Finset.univ
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: 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 < δ}
⊢ C * (↑x * (1 - ↑x) / ↑n) / δ ^ 2 = C / δ ^ 2 * ↑x * (1 - ↑x) / ↑n

Tactic:
;

Goal state after:
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 < δ}
⊢ C * (↑x * (1 - ↑x) / ↑n) / δ ^ 2 = C / δ ^ 2 * ↑x * (1 - ↑x) / ↑n
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: 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 < δ}
⊢ (C * ∑ k, (↑x - ↑k/ₙ) ^ 2 * (bernstein n ↑k) x) / δ ^ 2 = C / δ ^ 2 * ↑x * (1 - ↑x) / ↑n

Tactic:
rw [variance hn₀]; ring

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

Goal state before:
pp: case calc_1.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
k : ℕ
m : k ∈ Finset.range (n + 1)
⊢ (n • X - ↑k) ^ 2 = ↑(k * (k - 1)) + (1 - ↑(2 * n) * X) * ↑k + ↑(n ^ 2) * X ^ 2

Tactic:
;

Goal state after:
case calc_1.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
k : ℕ
m : k ∈ Finset.range (n + 1)
⊢ (n • X - ↑k) ^ 2 = ↑(k * (k - 1)) + (1 - ↑(2 * n) * X) * ↑k + ↑(n ^ 2) * X ^ 2
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case calc_1.e_a.zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
m : 0 ∈ Finset.range (n + 1)
⊢ (↑n * X) ^ 2 = ↑n ^ 2 * X ^ 2

Tactic:
;

Goal state after:
case calc_1.e_a.zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
m : 0 ∈ Finset.range (n + 1)
⊢ (↑n * X) ^ 2 = ↑n ^ 2 * X ^ 2
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case calc_1.e_a.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
n✝ : ℕ
m : n✝ + 1 ∈ Finset.range (n + 1)
⊢ (↑n * X - (↑n✝ + 1)) ^ 2 = (↑n✝ + 1) * ↑n✝ + (1 - 2 * ↑n * X) * (↑n✝ + 1) + ↑n ^ 2 * X ^ 2

Tactic:
;

Goal state after:
case calc_1.e_a.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
n✝ : ℕ
m : n✝ + 1 ∈ Finset.range (n + 1)
⊢ (↑n * X - (↑n✝ + 1)) ^ 2 = (↑n✝ + 1) * ↑n✝ + (1 - 2 * ↑n * X) * (↑n✝ + 1) + ↑n ^ 2 * X ^ 2
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : TopologicalSpace A
inst✝³ : T2Space A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra 𝕜 A
s : Set 𝕜
x✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) = ψ (ContinuousMap.restrict s (ContinuousMap.id 𝕜))
a✝ : ↑s
⊢ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) a✝ = (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) a✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : TopologicalSpace A
inst✝³ : T2Space A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra 𝕜 A
s : Set 𝕜
x✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) = ψ (ContinuousMap.restrict s (ContinuousMap.id 𝕜))
a✝ : ↑s
⊢ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) a✝ = (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) a✝
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case calc_2.succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
p :
  ∑ x ∈ Finset.range (n✝ + 1 + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * (n✝ + 1)) * X) * ↑x + ↑((n✝ + 1) ^ 2) * X ^ 2) * bernsteinPolynomial R (n✝ + 1) x =
    ↑((n✝ + 1) * (n✝ + 1 - 1)) * X ^ 2 + (1 - (2 * (n✝ + 1)) • X) * (n✝ + 1) • X + (n✝ + 1) ^ 2 • X ^ 2 * 1
⊢ (↑n✝ + 1) * ↑n✝ * X ^ 2 + (1 - 2 * (↑n✝ + 1) * X) * ((↑n✝ + 1) * X) + (↑n✝ + 1) ^ 2 * X ^ 2 = (↑n✝ + 1) * X * (1 - X)

Tactic:
;

Goal state after:
case calc_2.succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
p :
  ∑ x ∈ Finset.range (n✝ + 1 + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * (n✝ + 1)) * X) * ↑x + ↑((n✝ + 1) ^ 2) * X ^ 2) * bernsteinPolynomial R (n✝ + 1) x =
    ↑((n✝ + 1) * (n✝ + 1 - 1)) * X ^ 2 + (1 - (2 * (n✝ + 1)) • X) * (n✝ + 1) • X + (n✝ + 1) ^ 2 • X ^ 2 * 1
⊢ (↑n✝ + 1) * ↑n✝ * X ^ 2 + (1 - 2 * (↑n✝ + 1) * X) * ((↑n✝ + 1) * X) + (↑n✝ + 1) ^ 2 * X ^ 2 = (↑n✝ + 1) * X * (1 - X)
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, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
x : X
⊢ ↑(h x) x = f x

Tactic:
;

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, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
x : X
⊢ ↑(h x) x = f x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
a✝ : X
⊢ ↑(((algebraMap ℝ C(X, ℝ)) ↑r).toNNReal a✝) = ↑(((algebraMap ℝ≥0 C(X, ℝ≥0)) r) a✝)

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
a✝ : X
⊢ ↑(((algebraMap ℝ C(X, ℝ)) ↑r).toNNReal a✝) = ↑(((algebraMap ℝ≥0 C(X, ℝ≥0)) r) a✝)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
a✝ : X
⊢ ↑((-(algebraMap ℝ C(X, ℝ)) ↑r).toNNReal a✝) = ↑(0 a✝)

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
a✝ : X
⊢ ↑((-(algebraMap ℝ C(X, ℝ)) ↑r).toNNReal a✝) = ↑(0 a✝)