mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
⊢ ν Sᶜ + ν Tᶜ ≤ 0

Tactic:
rw [hT₃, hS₃, add_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
⊢ ∀ᵐ (x : α) ∂μ, ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)

Tactic:
have I : ∀ x ∈ w, x ≠ ∞ := fun x xs hx => w_top (hx ▸ xs)

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case hd
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : ↑c ∈ w
d : ℝ≥0
hd : ↑d ∈ w
hcd : ↑c < ↑d
x : α
a✝ : ∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < ↑c
h2x : ∃ᶠ (x : Set α) in v.filterAt x, ↑d < ρ x / μ x
⊢ ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a

Tactic:
apply h2x.mono fun a ha => ?_

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : ↑c ∈ w
d : ℝ≥0
hd : ↑d ∈ w
hcd : ↑c < ↑d
x : α
a✝ : ∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < ↑c
h2x : ∃ᶠ (x : Set α) in v.filterAt x, ↑d < ρ x / μ x
a : Set α
ha : ↑d < ρ a / μ a
⊢ ↑d * μ a ≤ ρ a
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))

Tactic:
by
  filter_upwards [v.ae_tendsto_div hρ]
  intro x hx
  exact tendsto_nhds_limUnder hx

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ ∃ a ∈ s, ∃ b ∈ s, a < b ∧ ε < eVariationOn f (s ∩ Icc a b)

Tactic:
have A : ε < eVariationOn f (s ∩ Icc (u 0) (u n)) := by
    apply hu.trans_le
    simp only [Monotone] at u_mono
    let v (i : ℕ) := min (u i) (u n)
    calc ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
    _ = ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) := by grind [Finset.sum_congr]
    _ ≤ eVariationOn f (s ∩ Icc (u 0) (u n)) :=
      sum_le_of_monotoneOn_Iic (by grind [MonotoneOn]) (by grind)

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
A : ε < eVariationOn f (s ∩ Icc (u 0) (u n))
⊢ ∃ a ∈ s, ∃ b ∈ s, a < b ∧ ε < eVariationOn f (s ∩ Icc a b)
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁶ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SecondCountableTopology α
inst✝³ : BorelSpace α
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
⊢ Tendsto (fun a ↦ ⨍ (y : α) in a, f y ∂μ) (v.filterAt x) (𝓝 (f x))

Tactic:
tendsto_iff_norm_sub_tendsto_zero

Goal state after:
α : Type u_1
inst✝⁶ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SecondCountableTopology α
inst✝³ : BorelSpace α
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
⊢ Tendsto (fun e ↦ ‖⨍ (y : α) in e, f y ∂μ - f x‖) (v.filterAt x) (𝓝 0)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
inst✝ : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ y ∈ s, eVariationOn f (s ∩ Ici y) < ε

Tactic:
have W := hf.tendsto_eVariationOn_Ici_zero_of_filter L hL

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
inst✝ : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
ε : ℝ≥0∞
εpos : ε > 0
W : Tendsto (fun y ↦ eVariationOn f (s ∩ Ici y)) L (𝓝 0)
⊢ ∃ y ∈ s, eVariationOn f (s ∩ Ici y) < ε
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
inst✝ : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ t ∈ map f L, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

Tactic:
obtain ⟨y, y_mem, hy⟩ : ∃ y ∈ s, eVariationOn f (s ∩ Ici y) < ε := by
    have W := hf.tendsto_eVariationOn_Ici_zero_of_filter L hL
    rcases (((tendsto_order.1 W).2 ε εpos).and (hL x₀ hx₀)).exists with ⟨y, hy, h'y⟩
    exact ⟨y, h'y.1, hy⟩

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
inst✝ : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
ε : ℝ≥0∞
εpos : ε > 0
y : α
y_mem : y ∈ s
hy : eVariationOn f (s ∩ Ici y) < ε
⊢ ∃ t ∈ map f L, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
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
inst✝ : Nontrivial A
⊢ spectrum R 0 = {0}

Tactic:
have : (0 : A) = algebraMap R A 0 := Eq.symm (map_zero (algebraMap R A))

Goal state after:
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
inst✝ : Nontrivial A
this : 0 = (algebraMap R A) 0
⊢ spectrum R 0 = {0}
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
r : R
f : R → R
h₁ : ContinuousOn f (spectrum R ((algebraMap R A) r))
⊢ cfc f ((algebraMap R A) r) = (algebraMap R A) (f r)

Tactic:
rw [cfc_apply f (algebraMap R A r) (cfc_predicate_algebraMap r),
    ← AlgHomClass.commutes (cfcHom (p := p) (cfc_predicate_algebraMap r)) (f r)]

Goal state after:
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
r : R
f : R → R
h₁ : ContinuousOn f (spectrum R ((algebraMap R A) r))
⊢ (cfcHom ⋯) { toFun := (spectrum R ((algebraMap R A) r)).domRestrict f, continuous_toFun := ⋯ } =
    (cfcHom ⋯) ((algebraMap R C(↑(spectrum R ((algebraMap R A) r)), R)) (f r))
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
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
⊢ IsStrictlyPositive a ↔ ∀ x ∈ spectrum R a, 0 < x

Tactic:
have := cfc_isStrictlyPositive_iff (id : R → R) a (by fun_prop) ha

Goal state after:
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
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
this : IsStrictlyPositive (cfc id a) ↔ ∀ x ∈ spectrum R a, 0 < id x
⊢ IsStrictlyPositive a ↔ ∀ x ∈ spectrum R a, 0 < x
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))
⊢ c < eVariationOn f s

Tactic:
apply this.trans_le

Goal state after:
α : 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))
⊢ ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) ≤ eVariationOn f s
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
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
w : ∀ (k : ℕ), k • bernsteinPolynomial R n k = ↑k * X ^ (k - 1) * (1 - X) ^ (n - k) * ↑(n.choose k) * X
⊢ ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν =
    (MvPolynomial.aeval e) ((pderiv true) (∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m))) * X

Tactic:
map_sum (pderiv true),

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
w : ∀ (k : ℕ), k • bernsteinPolynomial R n k = ↑k * X ^ (k - 1) * (1 - X) ^ (n - k) * ↑(n.choose k) * X
⊢ ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν =
    (MvPolynomial.aeval e) (∑ x_1 ∈ Finset.range (n + 1), (pderiv true) (x ^ x_1 * y ^ (n - x_1) * ↑(n.choose x_1))) * X
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
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
w :
  ∀ (k : ℕ),
    (k * (k - 1)) • bernsteinPolynomial R n k =
      ↑(n.choose k) * ((1 - X) ^ (n - k) * (↑k * (↑(k - 1) * X ^ (k - 1 - 1)))) * X ^ 2
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν =
    (MvPolynomial.aeval e)
        ((pderiv true) ((pderiv true) (∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)))) *
      X ^ 2

Tactic:
map_sum (pderiv true),

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
w :
  ∀ (k : ℕ),
    (k * (k - 1)) • bernsteinPolynomial R n k =
      ↑(n.choose k) * ((1 - X) ^ (n - k) * (↑k * (↑(k - 1) * X ^ (k - 1 - 1)))) * X ^ 2
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν =
    (MvPolynomial.aeval e)
        ((pderiv true) (∑ x_1 ∈ Finset.range (n + 1), (pderiv true) (x ^ x_1 * y ^ (n - x_1) * ↑(n.choose x_1)))) *
      X ^ 2
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
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
w :
  ∀ (k : ℕ),
    (k * (k - 1)) • bernsteinPolynomial R n k =
      ↑(n.choose k) * ((1 - X) ^ (n - k) * (↑k * (↑(k - 1) * X ^ (k - 1 - 1)))) * X ^ 2
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν =
    (MvPolynomial.aeval e)
        ((pderiv true) (∑ x_1 ∈ Finset.range (n + 1), (pderiv true) (x ^ x_1 * y ^ (n - x_1) * ↑(n.choose x_1)))) *
      X ^ 2

Tactic:
map_sum (pderiv true),

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
w :
  ∀ (k : ℕ),
    (k * (k - 1)) • bernsteinPolynomial R n k =
      ↑(n.choose k) * ((1 - X) ^ (n - k) * (↑k * (↑(k - 1) * X ^ (k - 1 - 1)))) * X ^ 2
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν =
    (MvPolynomial.aeval e)
        (∑ x_1 ∈ Finset.range (n + 1), (pderiv true) ((pderiv true) (x ^ x_1 * y ^ (n - x_1) * ↑(n.choose x_1)))) *
      X ^ 2
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case refine_2
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}
x y : X
⊢ y ∈ U x y

Tactic:
· rw [Set.mem_ofPred_eq, w₂]
      exact sub_lt_self _ pos

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

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

Tactic:
exact norm_mul_le _ _

Goal state after:
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
inst✝ : CStarRing 𝕜
x✝ x : Unitization 𝕜 E
h : ¬(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2 = 0
⊢ ‖((splitMul 𝕜 E) x⋆).2 * ((splitMul 𝕜 E) x).2‖ ≤ ‖((splitMul 𝕜 E) x⋆).2‖ * ‖((splitMul 𝕜 E) x).2‖

Tactic:
exact norm_mul_le _ _

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

Goal state before:
pp: 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.2 * y.ofLp.toProd.2‖ ≤ ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖

Tactic:
exact norm_mul_le _ _

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f✝ f : C(↑s, 𝕜)
hf : f ∈ StarAlgebra.adjoin 𝕜 {(toContinuousMapOnAlgHom s) X}
⊢ p f

Tactic:
induction hf using Algebra.adjoin_induction with
  | mem f hf =>
    push _ ∈ _ at hf
    rw [star_eq_iff_star_eq, eq_comm (b := f)] at hf
    obtain (rfl | rfl) := hf
    all_goals simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]
  | algebraMap r => exact const r
  | add _ _ _ _ hf hg => exact add _ _ hf hg
  | mul _ _ _ _ hf hg => exact mul _ _ hf hg

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

Goal state before:
pp: case smul
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Fact (0 ∈ 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)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id s}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f : C(↑s, 𝕜)₀
r✝ : 𝕜
x✝ : C(↑s, 𝕜)₀
hx✝ : x✝ ∈ NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})
hf : p x✝
⊢ p (r✝ • x✝)

Tactic:
exact smul _ _ hf

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁴ : CommSemiring 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✝¹⁵ : Ring B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Algebra R B
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : ContinuousFunctionalCalculus R A p
inst✝⁴ : ContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMap.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst✝¹⁷, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
ψ : A →⋆ₐ[R] B := ⋯
this : Continuous[inst✝¹⁷, inst✝¹³] ⇑ψ
h_spec : spectrum R (ψ a) ⊆ spectrum R a
hψa : q (ψ a)
ι : C(↑(spectrum R (ψ a)), ↑(spectrum R a)) := ⋯
⊢ (ψ.comp (cfcHom ha)) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) =
    (cfcHom hψa) (ContinuousMap.restrict (spectrum R (ψ a)) (ContinuousMap.id R))

Tactic:
simp [cfcHom_id]

Goal state after:
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 ∈ {x | (f x ∩ g x ∩ t).Nonempty}, ∃ t_1 ⊆ {x | (f x ∩ g x ∩ t).Nonempty}, IsOpen[inst✝¹] t_1 ∧ x ∈ t_1

Tactic:
intro x ⟨y, ⟨hyf, hyg⟩, hyt⟩

Goal state after:
α : 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
⊢ ∃ t_1 ⊆ {x | (f x ∩ g x ∩ t).Nonempty}, IsOpen[inst✝¹] t_1 ∧ x ∈ t_1
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), UpperHemicontinuousOn (F n) s
hf_compact : ∀ x ∈ s, IsCompact (f x)
x₀ : α
hx₀s : x₀ ∈ s
u : Set β
hu : IsOpen[inst✝.toTopologicalSpace] u
hx₀u : f x₀ ⊆ u
⊢ ∀ᶠ (x' : α) in 𝓝[s] x₀, f x' ⊆ u

Tactic:
obtain ⟨W, hW, _, hWu⟩ := lebesgue_number_of_compact_open (hf_compact x₀ hx₀s) hu hx₀u

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), UpperHemicontinuousOn (F n) s
hf_compact : ∀ x ∈ s, IsCompact (f x)
x₀ : α
hx₀s : x₀ ∈ s
u : Set β
hu : IsOpen[inst✝.toTopologicalSpace] u
hx₀u : f x₀ ⊆ u
W : Set (β × β)
hW : W ∈ uniformity β
left✝ : IsOpen[instTopologicalSpaceProd] W
hWu : ∀ x ∈ f x₀, ball x W ⊆ u
⊢ ∀ᶠ (x' : α) in 𝓝[s] x₀, f x' ⊆ u