mathlib-initiative/mathlib-tactics huggingface dataset:
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
a : A
f g : R → R
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : ¬p a
⊢ cfc (fun x ↦ f x + g x) a = cfc f a + cfc g a

Tactic:
simp [cfc_apply_of_not_predicate a ha]

Goal state after:
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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : ¬p a
⊢ cfc (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (f i) a

Tactic:
simp [cfc_apply_of_not_predicate a ha]

Goal state after:
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
S : Type u_3
inst✝⁴ : SMul S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : ¬p a
⊢ cfc (fun x ↦ s • f x) a = s • cfc f a

Tactic:
simp [cfc_apply_of_not_predicate a ha]

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

Goal state before:
pp: case neg.inl
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
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
ha : ¬p a
⊢ cfc (fun x ↦ star (f x)) a = star (cfc f a)

Tactic:
simp [cfc_apply_of_not_predicate a ha]

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
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
hf_star : ContinuousOn (fun x ↦ star (f x)) (spectrum R a)
⊢ ContinuousOn f (spectrum R a)

Tactic:
by simpa using hf_star.star

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : CompleteSpace E
inst✝ : DenselyOrdered α
f : α → E
a : α
hf : BoundedVariationOn f univ
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
ha : IsBot a
⊢ eVariationOn f (Iic a) = eVariationOn f (Iio a) + edist (f a) (Function.leftLim f a)

Tactic:
have A : Iic a = {a} := by ext x; grind [ha x]

Goal state after:
case pos
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : CompleteSpace E
inst✝ : DenselyOrdered α
f : α → E
a : α
hf : BoundedVariationOn f univ
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
ha : IsBot a
A : Iic a = {a}
⊢ eVariationOn f (Iic a) = eVariationOn f (Iio a) + edist (f a) (Function.leftLim f a)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case h'f
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
H : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))
y : α
hy : y ∈ s ∩ Iio x
N : 𝓝[s ∩ Ici y ∩ Iio x] x = 𝓝[s ∩ Iio x] x
⊢ Tendsto f (𝓝[s ∩ Ici y ∩ Iio x] x) (𝓝 l)

Tactic:
convert h'f

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

Goal state before:
pp: case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : ¬p a
⊢ cfc (fun x ↦ f x - g x) a = cfc f a - cfc g a

Tactic:
simp [cfc_apply_of_not_predicate a ha]

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

Goal state before:
pp: case neg.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
ha : ¬p a
⊢ cfc (fun x ↦ -f x) a = -cfc f a

Tactic:
simp [cfc_apply_of_not_predicate a ha]

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✝¹² : PartialOrder R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ContinuousSqrt R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
a : A
h : ∀ x ∈ spectrum R a, r ≤ x
ha : p a
⊢ (algebraMap R A) r ≤ a

Tactic:
by
  rw [← cfc_id R a]
  exact algebraMap_le_cfc id r a h

Goal state after:
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
a : A
hf : ¬ContinuousOn f (σₙ R a)
hf_star : ContinuousOn (fun x ↦ star (f x)) (σₙ R a)
⊢ ContinuousOn f (σₙ R a)

Tactic:
by simpa using hf_star.star

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

Goal state before:
pp: case neg.inr.inr
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
h0 : ¬f 0 = 0
⊢ cfcₙ (fun x ↦ star (f x)) a = star (cfcₙ f a)

Tactic:
· rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero, star_zero]
      exact fun hf0 ↦ h0 <| by simpa using congr(star $(hf0))

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ 3 * X ^ 2 * (1 - X) = 3 * X ^ 2 - 3 * X ^ 3

Tactic:
ring

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

Goal state before:
pp: case succ
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
k : ℕ
⊢ (↑k + 1) * (↑(n.choose (k + 1)) * (X ^ k * X) * (1 - X) ^ (n - (k + 1))) =
    (↑k + 1) * X ^ k * (1 - X) ^ (n - (k + 1)) * ↑(n.choose (k + 1)) * X

Tactic:
ring

Goal state after:
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
this : UniformContinuous ⇑f
⊢ ∃ δ > 0, ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2

Tactic:
Metric.uniformity_basis_dist.uniformContinuous_iff
      (basis_sets _).uniformity_of_nhds_zero_swapped

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
this : ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (x y : ↑I), (x, y) ∈ {p | dist p.1 p.2 < j} → (f x, f y) ∈ {x | x.1 - x.2 ∈ id i}
⊢ ∃ δ > 0, ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case succ.succ
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
k : ℕ
⊢ (↑k + 1 + 1) * (↑k + 1) * (↑(n.choose (k + 1 + 1)) * (X ^ k * X * X) * (1 - X) ^ (n - (k + 1 + 1))) =
    ↑(n.choose (k + 1 + 1)) * ((1 - X) ^ (n - (k + 1 + 1)) * ((↑k + 1 + 1) * ((↑k + 1) * X ^ k))) * (X ^ 0 * X * X)

Tactic:
ring

Goal state after:
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 < δ}
⊢ gauge U ((bernsteinApproximation n f) x - f x) < 1

Tactic:
calc
    gauge U (bernsteinApproximation n f x - f x)
      = gauge U (∑ k : Fin (n + 1), bernstein n k x • (f k/ₙ - f x)) := by
      simp [bernsteinApproximation.apply, smul_sub, ← Finset.sum_smul]
    _ ≤ ∑ k : Fin (n + 1), gauge U (bernstein n k x • (f k/ₙ - f x)) :=
      gauge_sum_le hUc (absorbent_nhds_zero hU₀) _ _
    _ = ∑ k : Fin (n + 1), bernstein n k x * gauge U (f k/ₙ - f x) := by
      simp only [gauge_smul_of_nonneg, bernstein_nonneg, smul_eq_mul]
    _ = (∑ k ∈ S, bernstein n k x * gauge U (f k/ₙ - f x)) +
          ∑ k ∈ Sᶜ, bernstein n k x * gauge U (f k/ₙ - f x) :=
      (S.sum_add_sum_compl _).symm
    -- We'll now deal with the terms in `S` and the terms in `Sᶜ` in separate calc blocks.
    _ < 1 / 2 + 1 / 2 := add_lt_add_of_le_of_lt ?_ ?_
    _ = 1 := add_halves 1

Goal state after:
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

case calc_2
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
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 < δ}
⊢ ∑ k ∈ Sᶜ, (bernstein n ↑k) x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ Sᶜ, C * (bernstein n ↑k) x

Tactic:
by
        simp only [mul_comm (bernstein n _ x)]
        gcongr
        apply hC

Goal state after:
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:
ring

Goal state after:
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:
ring

Goal state after:
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:
ring

Goal state after:
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:
ring

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f g : C(X, ℝ)
x : X
⊢ ↑(((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) x) =
    ↑(((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal) x)

Tactic:
simp [max_neg_zero, add_mul, mul_add]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
f g : C(X, ℝ)
x : X
⊢ max (f x * g x) 0 + (-(f x * max (g x) 0) + max (f x) 0 * max (g x) 0) +
      (-(max (f x) 0 * g x) + max (f x) 0 * max (g x) 0) =
    -(f x * g x) + max (f x * g x) 0 + max (f x) 0 * max (g x) 0 +
      (-(max (f x) 0 * g x) + f x * g x + (-(f x * max (g x) 0) + max (f x) 0 * max (g x) 0))
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring 𝕜
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : ContinuousAdd 𝕜
inst✝⁵ : ContinuousConstSMul 𝕜 𝕜
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : TopologicalSpace A
inst✝² : Module 𝕜 A
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed (characterSpace 𝕜 A ∪ {0})

Tactic:
by
  simp only [union_zero, Set.ofPred_forall]
  exact
    isClosed_iInter fun x =>
      isClosed_iInter fun y =>
        isClosed_eq (eval_continuous _) <| (eval_continuous _).mul (eval_continuous _)

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : φ 1 * (1 - φ 1) = 0
h₂ : φ 1 = 0
this : ∀ (a : A), φ (a * 1) = 0
⊢ ∀ (x : A), ↑φ x = 0 x

Tactic:
simpa only [mul_one] using! this

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

Goal state before:
pp: case smul
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ : C(↑s, 𝕜)
r : 𝕜
f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f = 0
⊢ r • 0 = 0

Tactic:
smul_zero

Goal state after:
case smul
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ : C(↑s, 𝕜)
r : 𝕜
f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f = 0
⊢ 0 = 0
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
frequently : ∀ (f : C(↑s, 𝕜)₀), (∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f, p g) → p f
f : C(↑s, 𝕜)₀
⊢ p f

Tactic:
refine f.induction_on zero id star_id add mul smul fun h f ↦ frequently f ?_
  have := (ContinuousMapZero.adjoin_id_dense s).closure_eq ▸ Set.mem_univ (x := f)
  exact mem_closure_iff_frequently.mp this |>.mp <| .of_forall h

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

Goal state before:
pp: case smul
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id s) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id s)) * a = 0
hφ : Continuous ⇑φ
r✝ : 𝕜
f✝ : C(↑s, 𝕜)₀
h : φ f✝ * a = 0
⊢ r✝ • 0 = 0

Tactic:
smul_zero

Goal state after:
case smul
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id s) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id s)) * a = 0
hφ : Continuous ⇑φ
r✝ : 𝕜
f✝ : C(↑s, 𝕜)₀
h : φ f✝ * a = 0
⊢ 0 = 0
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case smul
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id s) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id s)) = 0
hφ : Continuous ⇑φ
r✝ : 𝕜
f✝ : C(↑s, 𝕜)₀
h : a * φ f✝ = 0
⊢ r✝ • 0 = 0

Tactic:
smul_zero

Goal state after:
case smul
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id s) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id s)) = 0
hφ : Continuous ⇑φ
r✝ : 𝕜
f✝ : C(↑s, 𝕜)₀
h : a * φ f✝ = 0
⊢ 0 = 0
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}
x' : α
hx'U : x' ∈ U
z : β
hzf : z ∈ f x'
hzt : z ∈ t
hzV : z ∈ V
⊢ x' ∈ {x | (f x ∩ g x ∩ t).Nonempty}

Tactic:
exact ⟨z, ⟨hzf, hUV (Set.mk_mem_prod hx'U hzV)⟩, hzt⟩

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

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

Tactic:
TopologicalSpace.nhds_generateFrom,

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : IsCompact s
⊢ 𝓝 s ≤
    ⨅
      s_1 ∈
        {s_2 |
          s ∈ s_2 ∧
            s_2 ∈
              Set.powerset '' {U | IsOpen[inst✝.toTopologicalSpace] U} ∪
                (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝.toTopologicalSpace] V}},
      𝓟 s_1
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_4
inst✝ : Finite ι
⊢ (∀ (U : Set α), IsOpen[inst✝¹] U → IsOpen[Pi.topologicalSpace] (⋂ i, {x | x i ∈ U})) ∧
    ∀ (F : Set α), IsClosed[inst✝¹] F → IsClosed[Pi.topologicalSpace] (⋂ i, {x | x i ∈ F})

Tactic:
exact ⟨
    fun U hU => isOpen_iInter_of_finite fun i => hU.preimage <| continuous_apply i,
    fun F hF => isClosed_iInter fun i => hF.preimage <| continuous_apply i⟩

Goal state after: