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

Goal state before:
pp: case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
ha : ¬p a
⊢ cfcₙ f a ≤ cfcₙ g a

Tactic:
·

Goal state after:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
ha : ¬p a
⊢ cfcₙ f a ≤ cfcₙ g a
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: 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) ((x + y) ^ n)) * X = n • X

Tactic:
·

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] := ⋯
⊢ (MvPolynomial.aeval e) ((pderiv true) ((x + y) ^ n)) * X = n • X
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✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ 0 ≤ cfcₙ f a

pp: case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ 0 ≤ cfcₙ f a

Tactic:
·

Goal state after:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ 0 ≤ cfcₙ f a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ 0 ≤ cfcₙ f a

Tactic:
·

Goal state after:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ 0 ≤ cfcₙ f a
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ Fin.last n/ₙ = 1

Tactic:
simp [z, hn]

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

Goal state before:
pp: case neg.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬ContinuousOn f (σₙ R a)
⊢ 0 ≤ cfcₙ f a

pp: case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬f 0 = 0
⊢ 0 ≤ cfcₙ f a

Tactic:
·

Goal state after:
case neg.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬ContinuousOn f (σₙ R a)
⊢ 0 ≤ cfcₙ f a
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: case e'_2
n : ℕ
hn : n ≠ 0
x : ↑I
⊢ ∑ k, (↑x - ↑(k/ₙ)) ^ 2 * (bernstein n ↑k) x =
    (Polynomial.aeval ↑x) (∑ ν ∈ Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial ℝ n ν) / ↑n ^ 2

pp: case e'_3
n : ℕ
hn : n ≠ 0
x : ↑I
⊢ ↑x * (1 - ↑x) / ↑n = (Polynomial.aeval ↑x) (n • Polynomial.X * (1 - Polynomial.X)) / ↑n ^ 2

Tactic:
·

Goal state after:
case e'_2
n : ℕ
hn : n ≠ 0
x : ↑I
⊢ ∑ k, (↑x - ↑(k/ₙ)) ^ 2 * (bernstein n ↑k) x =
    (Polynomial.aeval ↑x) (∑ ν ∈ Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial ℝ n ν) / ↑n ^ 2
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬f 0 = 0
⊢ 0 ≤ cfcₙ f a

Tactic:
·

Goal state after:
case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬f 0 = 0
⊢ 0 ≤ cfcₙ f a
Module: Mathlib.RingTheory.Polynomial.Bernstein

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

Tactic:
let x : MvPolynomial Bool R := MvPolynomial.X true

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2
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✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ cfcₙ f a ≤ 0

pp: case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ cfcₙ f a ≤ 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ cfcₙ f a ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: case e'_3
n : ℕ
hn : n ≠ 0
x : ↑I
⊢ ↑x * (1 - ↑x) / ↑n = (Polynomial.aeval ↑x) (n • Polynomial.X * (1 - Polynomial.X)) / ↑n ^ 2

Tactic:
·

Goal state after:
case e'_3
n : ℕ
hn : n ≠ 0
x : ↑I
⊢ ↑x * (1 - ↑x) / ↑n = (Polynomial.aeval ↑x) (n • Polynomial.X * (1 - Polynomial.X)) / ↑n ^ 2
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ cfcₙ f a ≤ 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ cfcₙ f a ≤ 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬ContinuousOn f (σₙ R a)
⊢ cfcₙ f a ≤ 0

pp: case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬f 0 = 0
⊢ cfcₙ f a ≤ 0

Tactic:
·

Goal state after:
case neg.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬ContinuousOn f (σₙ R a)
⊢ cfcₙ f a ≤ 0
Module: Mathlib.RingTheory.Polynomial.Bernstein

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

pp: 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

Tactic:
·

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

Goal state before:
pp: case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬f 0 = 0
⊢ cfcₙ f a ≤ 0

Tactic:
·

Goal state after:
case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing 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
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬f 0 = 0
⊢ cfcₙ f a ≤ 0
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case zero
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
⊢ (0 * (0 - 1)) • bernsteinPolynomial R n 0 =
    ↑(n.choose 0) * ((1 - X) ^ (n - 0) * (↑0 * (↑(0 - 1) * X ^ (0 - 1 - 1)))) * X ^ 2

pp: case succ.zero
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
⊢ ((0 + 1) * (0 + 1 - 1)) • bernsteinPolynomial R n (0 + 1) =
    ↑(n.choose (0 + 1)) * ((1 - X) ^ (n - (0 + 1)) * (↑(0 + 1) * (↑(0 + 1 - 1) * X ^ (0 + 1 - 1 - 1)))) * X ^ 2

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 + 1 - 1)) • bernsteinPolynomial R n (k + 1 + 1) =
    ↑(n.choose (k + 1 + 1)) *
        ((1 - X) ^ (n - (k + 1 + 1)) * (↑(k + 1 + 1) * (↑(k + 1 + 1 - 1) * X ^ (k + 1 + 1 - 1 - 1)))) *
      X ^ 2

Tactic:
·

Goal state after:
case zero
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
⊢ (0 * (0 - 1)) • bernsteinPolynomial R n 0 =
    ↑(n.choose 0) * ((1 - X) ^ (n - 0) * (↑0 * (↑(0 - 1) * X ^ (0 - 1 - 1)))) * X ^ 2
Module: Mathlib.RingTheory.Polynomial.Bernstein

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

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 + 1 - 1)) • bernsteinPolynomial R n (k + 1 + 1) =
    ↑(n.choose (k + 1 + 1)) *
        ((1 - X) ^ (n - (k + 1 + 1)) * (↑(k + 1 + 1) * (↑(k + 1 + 1 - 1) * X ^ (k + 1 + 1 - 1 - 1)))) *
      X ^ 2

Tactic:
·

Goal state after:
case succ.zero
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
⊢ ((0 + 1) * (0 + 1 - 1)) • bernsteinPolynomial R n (0 + 1) =
    ↑(n.choose (0 + 1)) * ((1 - X) ^ (n - (0 + 1)) * (↑(0 + 1) * (↑(0 + 1 - 1) * X ^ (0 + 1 - 1 - 1)))) * X ^ 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 + 1 - 1)) • bernsteinPolynomial R n (k + 1 + 1) =
    ↑(n.choose (k + 1 + 1)) *
        ((1 - X) ^ (n - (k + 1 + 1)) * (↑(k + 1 + 1) * (↑(k + 1 + 1 - 1) * X ^ (k + 1 + 1 - 1 - 1)))) *
      X ^ 2

Tactic:
·

Goal state after:
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 + 1 - 1)) • bernsteinPolynomial R n (k + 1 + 1) =
    ↑(n.choose (k + 1 + 1)) *
        ((1 - X) ^ (n - (k + 1 + 1)) * (↑(k + 1 + 1) * (↑(k + 1 + 1 - 1) * X ^ (k + 1 + 1 - 1 - 1)))) *
      X ^ 2