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

Goal state before:
pp: case e_a
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
x : ℕ
hx : x < (n, ⟨u, ⋯⟩).1
⊢ n - 1 - x = n - (x + 1)

Tactic:
lia

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

Goal state before:
pp: case e_a
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
x : ℕ
hx : x < (n, ⟨u, ⋯⟩).1
⊢ n - 1 - x + 1 = n - x

Tactic:
lia

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iic a
⊢ ∑ i ∈ Finset.range ⟨n, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨n, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨n, ⟨u, ⋯⟩⟩.snd i)) ≤
    eVariationOn f (s ∩ Iio a) + edist (f a) l

Tactic:
have : u n ≤ a := (u_mem n (by simp)).2

Goal state after:
case refine_1
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iic a
this : u n ≤ a
⊢ ∑ i ∈ Finset.range ⟨n, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨n, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨n, ⟨u, ⋯⟩⟩.snd i)) ≤
    eVariationOn f (s ∩ Iio a) + edist (f a) l
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
b : α
hb : b ∈ s ∩ Iio a
this✝ : Nonempty ((n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iio a })
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iio a
this :
  Tendsto (fun y ↦ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) l))
⊢ ∀ᶠ (c : α) in 𝓝[s ∩ Iio a] a,
    ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) (f c) ≤ eVariationOn f (s ∩ Iic a)

Tactic:
have : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a :=
      inter_mem_nhdsWithin_inter self_mem_nhdsWithin (Ioo_mem_nhdsLT (by grind [StrictMonoOn]))

Goal state after:
case refine_2
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
b : α
hb : b ∈ s ∩ Iio a
this✝¹ : Nonempty ((n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iio a })
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iio a
this✝ :
  Tendsto (fun y ↦ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
⊢ ∀ᶠ (c : α) in 𝓝[s ∩ Iio a] a,
    ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) (f c) ≤ eVariationOn f (s ∩ Iic a)
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 μ
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
this : Tendsto (ENNReal.toReal ∘ fun a ↦ (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
a : Set α
h'a : μ a < ∞
h''a : IntegrableOn f a μ
A : IntegrableOn (fun y ↦ ↑‖f y - f x‖₊) a μ
⊢ (μ a).toReal⁻¹ * ∫ (a : α) in a, ↑‖f a - f x‖₊ ∂μ = (μ.real a)⁻¹ * ∫ (y : α) in a, ‖f y - f x‖ ∂μ

Tactic:
simp only [coe_nnnorm, measureReal_def]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (fun x ↦ f x + r) a = (algebraMap R A) r + cfc f a

Tactic:
conv_lhs => simp only [add_comm]

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
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (fun x ↦ r + f x) a = (algebraMap R A) r + cfc f a
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
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (fun x ↦ r + f x) a = (algebraMap R A) r + cfc f a

Tactic:
exact cfc_const_add r f a hf ha

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
⊢ (fun x ↦ r) '' spectrum R 0 ⊆ {r}

Tactic:
rintro - ⟨x, -, rfl⟩

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 x : R
⊢ (fun x ↦ r) x ∈ {r}
Module: Mathlib.Topology.Algebra.StarSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : StarRing A
inst✝¹⁰ : StarModule R A
inst✝⁹ : IsSemitopologicalSemiring A
inst✝⁸ : ContinuousStar A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : StarRing B
inst✝³ : T2Space B
F : Type u_4
S : StarSubalgebra R A
inst✝² : FunLike F (↥S.topologicalClosure) B
inst✝¹ : AlgHomClass F R (↥S.topologicalClosure) B
inst✝ : StarHomClass F (↥S.topologicalClosure) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst✝⁷] ⇑φ
hψ : Continuous[instTopologicalSpaceSubtype, inst✝⁷] ⇑ψ
h : ∀ (x : ↥S), φ ((inclusion ⋯) x) = ψ ((inclusion ⋯) x)
this : ↑φ = ↑ψ
⊢ ⇑↑φ = ⇑ψ

Tactic:
apply congrArg _ this

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

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

Tactic:
cfcₙ_apply_of_not_map_zero _ h

Goal state after:
case neg.inr.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 : ¬f 0 = 0
⊢ P 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁴ : CommRing R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalRing 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
f g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum R a, f x ≤ g x

Tactic:
rw [cfc_apply f a, cfc_apply g a, cfcHom_le_iff (show p a from ha), ContinuousMap.le_def]
  simp

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

Goal state before:
pp: case neg.inr.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
h0 : ¬g 0 = 0
⊢ cfcₙ f a = cfcₙ g a

Tactic:
rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero]

Goal state after:
case neg.inr.inr.hf
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
hfg : Set.EqOn f g (σₙ R a)
h0 : ¬g 0 = 0
⊢ ¬f 0 = 0
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : 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:
apply iSup_le _

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
a b : α
hf : MonotoneOn f s
as : a ∈ s
bs : b ∈ s
hab : a ≤ b
⊢ ∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Set.Icc a b }),
    ∑ i_1 ∈ Finset.range i.1, edist (f (↑i.2 (i_1 + 1))) (f (↑i.2 i_1)) ≤ ENNReal.ofReal (f b - f a)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
F : Type u_3
inst✝ : PseudoEMetricSpace F
f : E → F
C : ℝ≥0
t : Set E
h : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
⊢ eVariationOn (f ∘ g) s ≤ ↑C * eVariationOn g s

Tactic:
apply iSup_le _

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
F : Type u_3
inst✝ : PseudoEMetricSpace F
f : E → F
C : ℝ≥0
t : Set E
h : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
⊢ ∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }),
    ∑ i_1 ∈ Finset.range i.1, edist ((f ∘ g) (↑i.2 (i_1 + 1))) ((f ∘ g) (↑i.2 i_1)) ≤ ↑C * eVariationOn g s
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
inst✝ : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
⊢ cfcₙ (g ∘ f) a = cfcₙ g (cfcₙ f a)

Tactic:
have sp_eq :
      σₙ R (cfcₙHom (show p a from ha) ⟨ContinuousMap.mk _ hf.domRestrict, hf0⟩) =
        f '' (σₙ R a) := by
    rw [cfcₙHom_map_quasispectrum (by exact ha) _]
    ext
    simp

Goal state after:
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
inst✝ : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq : σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a
⊢ cfcₙ (g ∘ f) a = cfcₙ g (cfcₙ f a)
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
h'' : ν > 0
⊢ n - 1 - (ν - 1) = n - ν

Tactic:
lia

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)

Tactic:
induction ν generalizing n with
    | zero => simp [eval_at_0]
    | succ ν ih =>
      have h' : ν ≤ n - 1 := le_tsub_of_add_le_right h
      simp only [derivative_succ, ih (n - 1) h', iterate_derivative_succ_at_0_eq_zero,
        Nat.succ_sub_succ_eq_sub, sub_zero, iterate_derivative_sub,
        iterate_derivative_natCast_mul, eval_one, eval_mul, eval_add, eval_sub, eval_X, eval_comp,
        eval_natCast, Function.comp_apply, Function.iterate_succ, ascPochhammer_succ_left]
      obtain rfl | h'' := ν.eq_zero_or_pos
      · simp
      · have : n - 1 - (ν - 1) = n - ν := by lia
        rw [this, ascPochhammer_eval_succ, Nat.sub_zero]
        rw_mod_cast [tsub_add_cancel_of_le (h'.trans n.pred_le)]

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

Goal state before:
pp: case inr.e_a.e_x
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ n - (n - ν - 1) = ν + 1

Tactic:
lia

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

Goal state before:
pp: f : C(↑I, ℝ)
⊢ f ∈ (polynomialFunctions I).topologicalClosure

Tactic:
refine mem_closure_of_tendsto (bernsteinApproximation_uniform f) <| .of_forall fun n ↦ ?_

Goal state after:
f : C(↑I, ℝ)
n : ℕ
⊢ bernsteinApproximation n f ∈ ↑(polynomialFunctions I).toSubsemiring
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 g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
ha : p a
⊢ cfcₙ (fun x ↦ f x - g x) a = cfcₙ f a - cfcₙ g a

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

Tactic:
· rw [cfcₙ_apply f a, cfcₙ_apply g a, ← map_sub, cfcₙ_apply ..]
    congr

Goal state after:
case neg
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 g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
ha : ¬p a
⊢ cfcₙ (fun x ↦ f x - g x) a = cfcₙ f a - cfcₙ g a
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✝¹⁸ : 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
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
⊢ 0 ≤ a ↔ ∀ x ∈ σₙ R a, 0 ≤ x

Tactic:
by
  have := cfcₙ_nonneg_iff (id : R → R) a (by fun_prop)
  simpa [cfcₙ_id _ a ha] using this

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

Goal state before:
pp: 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
hφ : Continuous[_, inst✝¹] ⇑φ
⊢ Continuous[_, inst✝¹] ⇑φ.realContinuousMapOfNNReal

Tactic:
by
  dsimp [realContinuousMapOfNNReal]
  fun_prop

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

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
A : Type u_2
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra ℝ A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
f : C(X, ℝ≥0)
⊢ φ.realContinuousMapOfNNReal ({ toFun := toReal, continuous_toFun := continuous_coe }.comp f) = φ f

Tactic:
simp only [realContinuousMapOfNNReal_apply]
  convert_to φ f - φ 0 = φ f using 2
  on_goal -1 => rw [map_zero, sub_zero]
  all_goals
    congr
    ext x
    simp

Goal state after:
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:
rw [NNReal.smul_def, ← smul_neg, ← NNReal.smul_def, toNNReal_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
⊢ _root_.toContinuousMap ⁻¹' closure ↑(adjoin 𝕜 {↑(ContinuousMapZero.id s)}) = Set.univ

Tactic:
toContinuousMap_id,

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
⊢ _root_.toContinuousMap ⁻¹' closure ↑(adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)}) = Set.univ
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
U₁ : SetRel α α
U₂ : SetRel β β
s₁ t₁ : Set α
s₂ t₂ : Set β
h₁ : (s₁, t₁) ∈ hausdorffEntourage U₁
h₂ : (s₂, t₂) ∈ hausdorffEntourage U₂
⊢ (s₁ ×ˢ s₂, t₁ ×ˢ t₂) ∈ hausdorffEntourage (entourageProd U₁ U₂)

Tactic:
simp only [mem_hausdorffEntourage] at *

Goal state after:
α : Type u_1
β : Type u_2
U₁ : SetRel α α
U₂ : SetRel β β
s₁ t₁ : Set α
s₂ t₂ : Set β
h₁ : s₁ ⊆ U₁.preimage t₁ ∧ t₁ ⊆ U₁.image s₁
h₂ : s₂ ⊆ U₂.preimage t₂ ∧ t₂ ⊆ U₂.image s₂
⊢ s₁ ×ˢ s₂ ⊆ (entourageProd U₁ U₂).preimage (t₁ ×ˢ t₂) ∧ t₁ ×ˢ t₂ ⊆ (entourageProd U₁ U₂).image (s₁ ×ˢ s₂)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball x V ⊆ U
⊢ {s | (s ∩ U).Nonempty} ∈ 𝓝 s

Tactic:
rw [mem_nhds_iff]

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball x V ⊆ U
⊢ ∃ V ∈ 𝓤 (Set α), ball s V ⊆ {s | (s ∩ U).Nonempty}
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ :
  (s, t) ∈
    (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹' hausdorffEntourage V
hst :
  ((fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) (s, t)).1 ⊆
    V.preimage ((fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) (s, t)).2
hts :
  ((fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) (s, t)).2 ⊆
    V.image ((fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) (s, t)).1
⊢ (s, t) ∈ hausdorffEntourage U

Tactic:
simp only [mem_hausdorffEntourage] at *

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ :
  (s, t) ∈
    (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹' hausdorffEntourage V
hst : closure[inst✝.toTopologicalSpace] s ⊆ V.preimage (closure[inst✝.toTopologicalSpace] t)
hts : closure[inst✝.toTopologicalSpace] t ⊆ V.image (closure[inst✝.toTopologicalSpace] s)
⊢ s ⊆ SetRel.preimage U t ∧ t ⊆ SetRel.image U s
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ↑‖1‖₊ ^ (1 / ↑b) ≤ ε⁻¹
n : ℕ
⊢ N ≤ n + N + 1

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
x✝ : CompactSpace (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst✝.toTopologicalSpace] (F i)
hF₂ : ⋂ i, F i = ∅
this : {x | ↑x ⊆ ⋂ i, F i} ⊆ {⊥} → ∃ u, {x | ↑x ⊆ ⋂ i ∈ u, F i} ⊆ {⊥}
⊢ ∃ u, ⋂ i ∈ u, F i = ∅

Tactic:
hF₂,

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
x✝ : CompactSpace (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst✝.toTopologicalSpace] (F i)
hF₂ : ⋂ i, F i = ∅
this : {x | ↑x ⊆ ∅} ⊆ {⊥} → ∃ u, {x | ↑x ⊆ ⋂ i ∈ u, F i} ⊆ {⊥}
⊢ ∃ u, ⋂ i ∈ u, F i = ∅