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

Goal state before:
pp: case pos
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
ha : p a
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
⊢ cfcₙ (fun x ↦ -f x) a = -cfcₙ f a

Tactic:
rw [cfcₙ_apply f a, ← map_neg, cfcₙ_apply ..]

Goal state after:
case pos
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
ha : p a
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
⊢ (cfcₙHom ha) { toFun := (σₙ R a).domRestrict fun x ↦ -f x, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ha) (-{ toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ })
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:
obtain (hf | hf) := hf

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

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.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:
obtain (hf | hf) := hf

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

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

Goal state before:
pp: case mpr.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)₀
x : ↑(σₙ R a)
hx : ↑x ∈ {0}
⊢ f x ∈ range ⇑((compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }) (toContinuousMapHom f)) ∪ {0}

Tactic:
apply Or.inr

Goal state after:
case mpr.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)₀
x : ↑(σₙ R a)
hx : ↑x ∈ {0}
⊢ f x ∈ {0}
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 < δ}
⊢ 1 / 2 * ∑ k ∈ S, (bernstein n ↑k) x ≤ 1 / 2 * ∑ k, (bernstein n ↑k) x

Tactic:
gcongr

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

Tactic:
gcongr

Goal state after:
case hbc
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)) := ⋯
x : Fin (n + 1)
a✝ : x ∈ Sᶜ
⊢ gauge U (f x/ₙ - f x✝) ≤ C
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 := 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 : Fin (n + 1)
hk : k ∈ Sᶜ
⊢ 1 * (bernstein n ↑k) x ≤ (↑x - ↑k/ₙ) ^ 2 / δ ^ 2 * (bernstein n ↑k) x

Tactic:
gcongr

Goal state after:
case hbc
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)) := ⋯
k : Fin (n + 1)
hk : k ∈ Sᶜ
⊢ 1 ≤ (↑x - ↑k/ₙ) ^ 2 / δ ^ 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 < δ}
⊢ C * ∑ k ∈ Sᶜ, (↑x - ↑k/ₙ) ^ 2 / δ ^ 2 * (bernstein n ↑k) x ≤ C * ∑ k, (↑x - ↑k/ₙ) ^ 2 / δ ^ 2 * (bernstein n ↑k) x

Tactic:
gcongr

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 / δ ^ 2 * ↑x * (1 - ↑x) / ↑n ≤ C / δ ^ 2 * 1 * 1 / ↑n

Tactic:
gcongr

Goal state after:
case c0
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)) := ⋯
⊢ 0 ≤ 1 - ↑x

case hbc
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)) := ⋯
⊢ ↑x ≤ 1

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)) := ⋯
⊢ 1 - ↑x ≤ 1
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:
cases k <;> · simp; ring

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 z y : X
ym : y ∈ ↑(ys x)
zm : z ∈ U x y
⊢ f z - ε < ((ys x).sup' ⋯ fun y ↦ g x y) z

Tactic:
simp only [coe_sup', Finset.sup'_apply, Finset.lt_sup'_iff]

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 y : X
ym : y ∈ ↑(ys x)
zm : z ∈ U x y
⊢ ∃ b ∈ ys x, f z - ε < (g x b) z
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
⊢ (-(r • f)).toNNReal = r • (-f).toNNReal

Tactic:
NNReal.smul_def,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
⊢ (-(↑r • f)).toNNReal = r • (-f).toNNReal
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: case neg
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
r : ℝ
f : C(X, ℝ)₀
hr : 0 < -r
⊢ φ (- -r • f).toNNReal - φ (-r • f).toNNReal = - -r • (φ f.toNNReal - φ (-f).toNNReal)

Tactic:
lift -r to ℝ≥0 using hr.le with r

Goal state after:
case neg
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
r✝ : ℝ
f : C(X, ℝ)₀
r : ℝ≥0
hr : 0 < ↑r
⊢ φ (-↑r • f).toNNReal - φ (↑r • f).toNNReal = -↑r • (φ f.toNNReal - φ (-f).toNNReal)
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖b⋆ * x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + b⋆ * (x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b))‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1 + (mul 𝕜 E) (x⋆ * x).toProd.2‖

Tactic:
← mul_add,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖b⋆ * (x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b))‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1 + (mul 𝕜 E) (x⋆ * x).toProd.2‖
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖b⋆‖ * ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖ ≤
    1 * ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖

Tactic:
gcongr

Goal state after:
case hbc
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖b⋆‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case calc_1
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
y : E
hy : y ∈ Metric.closedBall 0 1
⊢ ‖↑((algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1) y‖ + ‖↑((mul 𝕜 E) (x⋆ * x).toProd.2) y‖ ≤
    ‖(x⋆ * x).toProd.1‖ + ‖(x⋆ * x).toProd.2‖

Tactic:
gcongr

Goal state after:
case h₁
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
y : E
hy : y ∈ Metric.closedBall 0 1
⊢ ‖↑((algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1) y‖ ≤ ‖(x⋆ * x).toProd.1‖

case h₂
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
y : E
hy : y ∈ Metric.closedBall 0 1
⊢ ‖↑((mul 𝕜 E) (x⋆ * x).toProd.2) y‖ ≤ ‖(x⋆ * x).toProd.2‖
Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.1 * y.ofLp.toProd.1‖ + ‖(x.ofLp * y.ofLp).toProd.2‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
      (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)

Tactic:
snd_mul

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.1 * y.ofLp.toProd.1‖ +
      ‖x.ofLp.toProd.1 • y.ofLp.toProd.2 + y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
      (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)
Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.1 * y.ofLp.toProd.1‖ +
      ‖x.ofLp.toProd.1 • y.ofLp.toProd.2 + (y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2)‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.1‖ +
      (‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
        (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖))

Tactic:
gcongr

Goal state after:
case h₁
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.1 * y.ofLp.toProd.1‖ ≤ ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.1‖

case h₂
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.1 • y.ofLp.toProd.2 + (y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2)‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
      (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)