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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : LocallyBoundedVariationOn f s
x : α
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
y : α
h'f : Tendsto f (𝓝[s ∩ Icc y x ∩ Iio x] x) (𝓝 l)
hy : y ∈ s ∩ Iio x
this✝ : 𝓝[s ∩ Iio x] x = 𝓝[s ∩ Icc y x ∩ Iio x] x
this : BoundedVariationOn f (s ∩ Icc y x)
⊢ x ∈ Icc y x

Tactic:
grind

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

Goal state before:
pp: case e_s
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : LocallyBoundedVariationOn f s
x : α
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
y : α
h'f : Tendsto f (𝓝[s ∩ Icc y x ∩ Iio x] x) (𝓝 l)
hy : y ∈ s ∩ Iio x
this✝ : 𝓝[s ∩ Iio x] x = 𝓝[s ∩ Icc y x ∩ Iio x] x
this : BoundedVariationOn f (s ∩ Icc y x)
z : α
hz : z ∈ s ∩ Icc y x ∩ Iio x
⊢ s ∩ Icc y x ∩ Icc z x = s ∩ Icc z x

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : 𝓝[s ∩ Iio x] x = ⊥
⊢ s = s ∩ Iio x ∪ s ∩ Ici x

Tactic:
grind

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✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
n : ℕ
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfcUnits f a hf' hf ha ^ n = cfcUnits (fun i ↦ f i ^ n) a ⋯ ⋯ ha

Tactic:
by
  ext
  cases n with
  | zero => simp [cfc_const_one R a]
  | succ n => simp [cfc_pow f _ a]

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

Goal state before:
pp: case e'_2
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
W : eVariationOn f (s ∩ Icc y x ∩ Iio x) = eVariationOn f (s ∩ Icc y x ∩ Iic x)
⊢ s ∩ Ico y x = s ∩ Icc y x ∩ Iio x

Tactic:
grind

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

Goal state before:
pp: case e'_3
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
W : eVariationOn f (s ∩ Icc y x ∩ Iio x) = eVariationOn f (s ∩ Icc y x ∩ Iic x)
⊢ s ∩ Icc y x = s ∩ Icc y x ∩ Iic x

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
⊢ s ∩ Icc y x ∩ Iio x = s ∩ Iio x ∩ Ici y

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
⊢ s ∩ Icc y x ∩ Iic x ⊆ s ∩ Iic x

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this✝¹ : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this✝ : ∀ᶠ (b : ℕ → E) in Filter.pi fun i ↦ 𝓝 (g (u i)), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : ℕ → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi t ⊆ {b | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
this : ∀ᶠ (b : ℕ → α) in Filter.pi fun i ↦ 𝓝 (u i), ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2
J : Set ℕ
J_fin : J.Finite
k : ℕ → Set α
k_mem : ∀ (i : ℕ), k i ∈ 𝓝 (u i)
hk : J.pi k ⊆ {x | (fun b ↦ ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2) x}
v : ℕ → α
hv : ∀ i ∈ Iic n, f (v i) ∈ t i ∧ v i ∈ k i
h'v : ∀ i ∈ Iic n, v i ∈ s
f' : ℕ → E := fun i ↦ if i ∈ Iic n then f (v i) else g (u i)
i : ℕ
hi : i ∈ Finset.range n
⊢ edist (f (v (i + 1))) (f (v i)) = edist (f' (i + 1)) (f' i)

Tactic:
grind

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

Goal state before:
pp: case e'_2
R : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed[inst✝⁴] ↑S₁
⊢ ↑S₁ = {x | x ∈ S₁}

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this✝² : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this✝¹ : ∀ᶠ (b : ℕ → E) in Filter.pi fun i ↦ 𝓝 (g (u i)), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : ℕ → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi t ⊆ {b | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
this✝ : ∀ᶠ (b : ℕ → α) in Filter.pi fun i ↦ 𝓝 (u i), ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2
J : Set ℕ
J_fin : J.Finite
k : ℕ → Set α
k_mem : ∀ (i : ℕ), k i ∈ 𝓝 (u i)
hk : J.pi k ⊆ {x | (fun b ↦ ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2) x}
v : ℕ → α
hv : ∀ i ∈ Iic n, f (v i) ∈ t i ∧ v i ∈ k i
h'v : ∀ i ∈ Iic n, v i ∈ s
f' : ℕ → E := fun i ↦ if i ∈ Iic n then f (v i) else g (u i)
this : ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) = ∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i)
A : ∀ (i : ℕ), g (u i) ∈ t i
⊢ f' ∈ I.pi t

Tactic:
grind

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✝¹⁰ : 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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a)) (h0 : { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯ } 0 = 0) (ha : p a),
    P ((cfcₙHom ha) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := h0 })
h : ¬ContinuousOn f (σₙ R a)
⊢ P (cfcₙ f a)

Tactic:
cfcₙ_apply_of_not_continuousOn _ h

Goal state after:
case neg.inl
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a)) (h0 : { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯ } 0 = 0) (ha : p a),
    P ((cfcₙHom ha) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := h0 })
h : ¬ContinuousOn f (σₙ R a)
⊢ P 0
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this✝² : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this✝¹ : ∀ᶠ (b : ℕ → E) in Filter.pi fun i ↦ 𝓝 (g (u i)), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : ℕ → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi t ⊆ {b | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
this✝ : ∀ᶠ (b : ℕ → α) in Filter.pi fun i ↦ 𝓝 (u i), ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2
J : Set ℕ
J_fin : J.Finite
k : ℕ → Set α
k_mem : ∀ (i : ℕ), k i ∈ 𝓝 (u i)
hk : J.pi k ⊆ {x | (fun b ↦ ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2) x}
v : ℕ → α
hv : ∀ i ∈ Iic n, f (v i) ∈ t i ∧ v i ∈ k i
h'v : ∀ i ∈ Iic n, v i ∈ s
this : c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))
w : ℕ → α := fun i ↦ if i ∈ Iic n then v i else u i
A : ∀ (i : ℕ), u i ∈ k i
⊢ w ∈ J.pi k

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this✝² : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this✝¹ : ∀ᶠ (b : ℕ → E) in Filter.pi fun i ↦ 𝓝 (g (u i)), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : ℕ → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi t ⊆ {b | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
this✝ : ∀ᶠ (b : ℕ → α) in Filter.pi fun i ↦ 𝓝 (u i), ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2
J : Set ℕ
J_fin : J.Finite
k : ℕ → Set α
k_mem : ∀ (i : ℕ), k i ∈ 𝓝 (u i)
hk : J.pi k ⊆ {x | (fun b ↦ ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2) x}
v : ℕ → α
hv : ∀ i ∈ Iic n, f (v i) ∈ t i ∧ v i ∈ k i
h'v : ∀ i ∈ Iic n, v i ∈ s
this : c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))
v_mono : StrictMonoOn v (Iic n)
⊢ ∀ i ≤ n, v i ∈ s

Tactic:
grind

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 g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
⊢ cfcₙ (fun x ↦ f x * g x) a = cfcₙ f a * cfcₙ g a

Tactic:
by_cases ha : p a
  · rw [cfcₙ_apply f a, cfcₙ_apply g a, ← map_mul, cfcₙ_apply _ a]
    congr
  · simp [cfcₙ_apply_of_not_predicate a ha]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
a b : α
hf : MonotoneOn f s
as : a ∈ s
bs : b ∈ s
hab : a ≤ b
⊢ eVariationOn f (s ∩ Set.Icc a b) = ENNReal.ofReal (f b - f a)

Tactic:
have hle : eVariationOn f (s ∩ Icc a b) ≤ .ofReal (f b - f a) := by
      apply iSup_le _
      rintro ⟨n, ⟨u, hu, us⟩⟩
      calc
        _ = ∑ i ∈ range n, .ofReal (f (u (i + 1)) - f (u i)) := by
          refine sum_congr rfl fun i hi => ?_
          simp only [Finset.mem_range] at hi
          rw [edist_dist, Real.dist_eq, abs_of_nonneg]
          exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
        _ = .ofReal (∑ i ∈ range n, (f (u (i + 1)) - f (u i))) := by
          rw [ofReal_sum_of_nonneg]
          exact fun i _ ↦ sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
        _ = .ofReal (f (u n) - f (u 0)) := by rw [sum_range_sub (f <| u ·)]
        _ ≤ _ :=
          ofReal_le_ofReal (sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1))

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
a b : α
hf : MonotoneOn f s
as : a ∈ s
bs : b ∈ s
hab : a ≤ b
hle : eVariationOn f (s ∩ Set.Icc a b) ≤ ENNReal.ofReal (f b - f a)
⊢ eVariationOn f (s ∩ Set.Icc a b) = ENNReal.ofReal (f b - f a)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
C : ℝ
hf : MonotoneOn f s
h : ∀ x ∈ s, |f x| ≤ C
a b : α
as : a ∈ s
bs : b ∈ s
hab : a ≤ b
⊢ f b - f a ≤ 2 * C

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 0 (bernsteinPolynomial R n ν) = if ν = 0 then 1 else 0

Tactic:
bernsteinPolynomial

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 1 (bernsteinPolynomial R n ν) = if ν = n then 1 else 0

Tactic:
bernsteinPolynomial

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

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

Tactic:
bernsteinPolynomial

Goal state after:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.derivative (↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n + 1 - (ν + 1))) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))
Module: Mathlib.Topology.ContinuousMap.Weierstrass

Goal state before:
pp: case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
exact p

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

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

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

Tactic:
bernsteinPolynomial

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

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)) • (↑(n.choose (k + 1 + 1)) * X ^ (k + 1 + 1) * (1 - X) ^ (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
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) ((pderiv true) ((x + y) ^ n))) * X ^ 2 = (n * (n - 1)) • X ^ 2

Tactic:
simp only [x, y, e, (pderiv _).leibniz_pow,
      (pderiv true).map_add, pderiv_true_x, pderiv_true_y, smul_eq_mul, add_zero,
      mul_one, map_nsmul, map_pow, map_add, Bool.cond_true,
      Bool.cond_false, MvPolynomial.aeval_X, add_sub_cancel, one_pow, smul_smul,
      smul_one_mul]

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

Goal state before:
pp: case inl
X : Type u_1
inst✝⁵ : TopologicalSpace X
A : Type u_2
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
r : ℝ
hr : 0 ≤ r
⊢ φ ((algebraMap ℝ C(X, ℝ)) r).toNNReal - φ (-(algebraMap ℝ C(X, ℝ)) r).toNNReal = (algebraMap ℝ A) r

pp: case inr
X : Type u_1
inst✝⁵ : TopologicalSpace X
A : Type u_2
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
r : ℝ
hr : r ≤ 0
⊢ φ ((algebraMap ℝ C(X, ℝ)) r).toNNReal - φ (-(algebraMap ℝ C(X, ℝ)) r).toNNReal = (algebraMap ℝ A) r

Tactic:
· lift r to ℝ≥0 using hr
      simpa only [ContinuousMap.toNNReal_algebraMap, ContinuousMap.toNNReal_neg_algebraMap,
        map_zero, sub_zero] using! AlgHomClass.commutes φ r

Goal state after:
case inr
X : Type u_1
inst✝⁵ : TopologicalSpace X
A : Type u_2
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
r : ℝ
hr : r ≤ 0
⊢ φ ((algebraMap ℝ C(X, ℝ)) r).toNNReal - φ (-(algebraMap ℝ C(X, ℝ)) r).toNNReal = (algebraMap ℝ A) r
Module: Mathlib.Analysis.Normed.Algebra.Unitization

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x : Unitization 𝕜 A
⊢ (x.toProd.1, (lift (NonUnitalAlgHom.Lmul 𝕜 A)).toRingHom x) =
    (x.toProd.1, (algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2)

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Unitization

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
key : IsUniformInducing ⇑(addEquiv 𝕜 A)
⊢ 𝓤 (Unitization 𝕜 A) = comap (fun x ↦ ((addEquiv 𝕜 A) x.1, (addEquiv 𝕜 A) x.2)) (𝓤 (𝕜 × A))

Tactic:
rfl

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖g x - f x‖ < ε

Tactic:
let AK : Subalgebra ℝ C(K, ℝ) := Subalgebra.map restrict_on_K A

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖g x - f x‖ < ε
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
hsep : AK.SeparatesPoints
gK : C(↑K, ℝ)
hgKAK✝ : gK ∈ AK
hgapprox : ∀ (x : ↑K), ‖↑⟨gK, hgKAK✝⟩ x - K.domRestrict (⇑f) x‖ < ε
g : C(X, ℝ)
hgA : g ∈ A
hgKAK : ↑restrict_on_K g = gK
x : X
hxK : x ∈ K
⊢ g x = (↑restrict_on_K g) ⟨x, hxK⟩

Tactic:
rfl

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

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f ↦ ⇑f) f x₁ ≠ (fun f ↦ ⇑f) f x₂
⊢ ∃ f ∈ (fun f ↦ ⇑f) '' ↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)),
    f x₁ ≠ f x₂

Tactic:
let F : C(X, 𝕜) := f - const _ (f x₂)

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f ↦ ⇑f) f x₁ ≠ (fun f ↦ ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
⊢ ∃ f ∈ (fun f ↦ ⇑f) '' ↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)),
    f x₁ ≠ f x₂