mathlib-initiative/mathlib-tactics huggingface dataset:
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
a b : α
h : (𝓝[>] a).NeBot
h' : ContinuousWithinAt f (Ici a) a
hab : a < b
this : (𝓝[Iic b ∩ Ioi a] a).NeBot
⊢ Ioc a b = Iic b ∩ Ioi a

pp: case e'_3
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
a b : α
h : (𝓝[>] a).NeBot
h' : ContinuousWithinAt f (Ici a) a
hab : a < b
this : (𝓝[Iic b ∩ Ioi a] a).NeBot
⊢ Icc a b = Iic b ∩ Ici a

Tactic:
<;>

Goal state after:
case e'_2
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
a b : α
h : (𝓝[>] a).NeBot
h' : ContinuousWithinAt f (Ici a) a
hab : a < b
this : (𝓝[Iic b ∩ Ioi a] a).NeBot
⊢ Ioc a b = Iic b ∩ Ioi a

case e'_3
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
a b : α
h : (𝓝[>] a).NeBot
h' : ContinuousWithinAt f (Ici a) a
hab : a < b
this : (𝓝[Iic b ∩ Ioi a] a).NeBot
⊢ Icc a b = Iic b ∩ Ici a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case pos
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
a : A
f g : R → R
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
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✝⁸ : 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
a : A
f g : R → R
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
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_add, cfc_apply _ a]
    congr

Goal state after:
case neg
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
a : A
f g : R → R
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : ¬p a
⊢ cfc (fun x ↦ f x + g x) a = cfc f a + cfc g 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
this : (fun z ↦ r + f z) = fun z ↦ (fun x ↦ r) z + f z
⊢ cfc (fun x ↦ r) a + cfc f a = (algebraMap R A) r + cfc f a

Tactic:
cfc_const r a ha

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
this : (fun z ↦ r + f z) = fun z ↦ (fun x ↦ r) z + f z
⊢ (algebraMap R A) r + cfc f a = (algebraMap R A) r + cfc f a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case pos
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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun z ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i, f ↑i) (spectrum R a)
⊢ cfc (∑ i, f ↑i) a = ∑ i, (cfcHom ha) { toFun := (spectrum R a).domRestrict (f ↑i), continuous_toFun := ⋯ }

Tactic:
← map_sum,

Goal state after:
case pos
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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun z ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i, f ↑i) (spectrum R a)
⊢ cfc (∑ i, f ↑i) a = (cfcHom ha) (∑ x, { toFun := (spectrum R a).domRestrict (f ↑x), continuous_toFun := ⋯ })
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inl.hs
α : 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 : x ≤ y
⊢ (s ∩ Icc y x).Subsingleton

pp: case inl.hs
α : 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 : x ≤ y
⊢ (s ∩ Ico y x).Subsingleton

Tactic:
<;>

Goal state after:
case inl.hs
α : 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 : x ≤ y
⊢ (s ∩ Icc y x).Subsingleton

case inl.hs
α : 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 : x ≤ y
⊢ (s ∩ Ico y x).Subsingleton
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

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

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

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
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
⊢ c < eVariationOn f s

Tactic:
obtain ⟨J, J_fin, k, k_mem, hk⟩ : ∃ (J : Set ℕ), J.Finite ∧ ∃ k, (∀ (i : ℕ), k i ∈ 𝓝 (u i)) ∧
    J.pi k ⊆ _ := mem_pi.1 this

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}
⊢ c < eVariationOn f s
Module: Mathlib.Topology.Algebra.StarSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Semiring A
inst✝⁴ : StarRing A
inst✝³ : IsSemitopologicalSemiring A
inst✝² : ContinuousStar A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
x y✝ : A
hy✝¹ : y✝ ∈ elemental R x
P : (u : A) → u ∈ elemental R x → Prop
self : P x ⋯
star_self : P (star x) ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A) r) ⋯
add : ∀ (u : A) (hu : u ∈ elemental R x) (v : A) (hv : v ∈ elemental R x), P u hu → P v hv → P (u + v) ⋯
mul : ∀ (u : A) (hu : u ∈ elemental R x) (v : A) (hv : v ∈ elemental R x), P u hu → P v hv → P (u * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ ↑(elemental R x)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst✝⁶] s), P v ⋯
y : A
hy✝ : y ∈ ↑(adjoin R {x})
hy : y ∈ adjoin R {x}
⊢ P y ⋯

Tactic:
← mem_toSubalgebra,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Semiring A
inst✝⁴ : StarRing A
inst✝³ : IsSemitopologicalSemiring A
inst✝² : ContinuousStar A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
x y✝ : A
hy✝¹ : y✝ ∈ elemental R x
P : (u : A) → u ∈ elemental R x → Prop
self : P x ⋯
star_self : P (star x) ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A) r) ⋯
add : ∀ (u : A) (hu : u ∈ elemental R x) (v : A) (hv : v ∈ elemental R x), P u hu → P v hv → P (u + v) ⋯
mul : ∀ (u : A) (hu : u ∈ elemental R x) (v : A) (hv : v ∈ elemental R x), P u hu → P v hv → P (u * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ ↑(elemental R x)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst✝⁶] s), P v ⋯
y : A
hy✝ : y ∈ ↑(adjoin R {x})
hy : y ∈ (adjoin R {x}).toSubalgebra
⊢ P y ⋯
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 : R → R
r : R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc f a ≤ cfc (fun x ↦ r) a ↔ ∀ x ∈ spectrum R a, f x ≤ r

Tactic:
cfc_le_iff ..

Goal state after:
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 : R → R
r : R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ (∀ x ∈ spectrum R a, f x ≤ r) ↔ ∀ x ∈ spectrum R a, f x ≤ r
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 : R → R
r : R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (fun x ↦ r) a ≤ cfc f a ↔ ∀ x ∈ spectrum R a, r ≤ f x

Tactic:
cfc_le_iff ..

Goal state after:
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 : R → R
r : R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ (∀ x ∈ spectrum R a, r ≤ f x) ↔ ∀ x ∈ spectrum R a, r ≤ f x
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
hle : eVariationOn f (s ∩ Set.Icc a b) ≤ ENNReal.ofReal (f b - f a)
h : BoundedVariationOn f (s ∩ Set.Icc a b)
⊢ f b - f a ≤ dist (f a) (f b)

pp: case hx
α : 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)
h : BoundedVariationOn f (s ∩ Set.Icc a b)
⊢ a ∈ s ∩ Set.Icc a b

pp: case hy
α : 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)
h : BoundedVariationOn f (s ∩ Set.Icc a b)
⊢ b ∈ s ∩ Set.Icc a b

Tactic:
<;>

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
hle : eVariationOn f (s ∩ Set.Icc a b) ≤ ENNReal.ofReal (f b - f a)
h : BoundedVariationOn f (s ∩ Set.Icc a b)
⊢ f b - f a ≤ dist (f a) (f b)

case hx
α : 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)
h : BoundedVariationOn f (s ∩ Set.Icc a b)
⊢ a ∈ s ∩ Set.Icc a b

case hy
α : 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)
h : BoundedVariationOn f (s ∩ Set.Icc a b)
⊢ b ∈ s ∩ Set.Icc a b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun z ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i, f ↑i) (σₙ R a)
⊢ cfcₙ (∑ i, f ↑i) a = ∑ i, (cfcₙHom ha) { toFun := (σₙ R a).domRestrict (f ↑i), continuous_toFun := ⋯, map_zero' := ⋯ }

Tactic:
← map_sum,

Goal state after:
case pos
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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun z ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i, f ↑i) (σₙ R a)
⊢ cfcₙ (∑ i, f ↑i) a =
    (cfcₙHom ha) (∑ x, { toFun := (σₙ R a).domRestrict (f ↑x), continuous_toFun := ⋯, map_zero' := ⋯ })
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case e'_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n - ν) * (n + 1).choose (ν + 1) = (n + 1).choose (ν + 1) * (n + 1 - (ν + 1))

pp: case e'_3
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n + 1) * n.choose (ν + 1) = n.choose (ν + 1) * (n + 1)

Tactic:
· convert! mul_comm _ _ using 2
      simp

Goal state after:
case e'_3
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n + 1) * n.choose (ν + 1) = n.choose (ν + 1) * (n + 1)
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
S : Type u_3
inst✝⁴ : SMulZeroClass S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f ((fun x ↦ s • x) '' σₙ R a)
hf0 : f 0 = 0
ha : p a
⊢ cfcₙ (fun x ↦ f (s • x)) a = cfcₙ f (s • a)

Tactic:
by
  rw [cfcₙ_comp' f (s • ·) a, cfcₙ_smul_id s a]

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

Goal state before:
pp: case mpr
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
f : C(↑(σₙ R a), R)₀
⊢ 0 ≤ f → 0 ≤ (cfcₙHom ha) f

Tactic:
· simpa using (cfcₙHom_mono ha (f := 0) (g := f) ·)

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

Goal state before:
pp: case e'_2.e'_3
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✝¹ : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this✝ :
  inferInstance =
    UniformSpace.comap (fun x ↦ x.comp f) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp 0) inferInstance
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
u v : C(↑(σₙ R a), R)₀
⊢ (((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (u, v)).1 = 0

pp: case e'_2.e'_4
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✝¹ : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this✝ :
  inferInstance =
    UniformSpace.comap (fun x ↦ x.comp f) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp 0) inferInstance
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
u v : C(↑(σₙ R a), R)₀
⊢ (((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (u, v)).2 = 0

Tactic:
<;>

Goal state after:
case e'_2.e'_3
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✝¹ : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this✝ :
  inferInstance =
    UniformSpace.comap (fun x ↦ x.comp f) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp 0) inferInstance
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
u v : C(↑(σₙ R a), R)₀
⊢ (((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (u, v)).1 = 0

case e'_2.e'_4
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✝¹ : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this✝ :
  inferInstance =
    UniformSpace.comap (fun x ↦ x.comp f) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp 0) inferInstance
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
u v : C(↑(σₙ R a), R)₀
⊢ (((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (u, v)).2 = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

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✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
a : A
h_cpct : CompactSpace ↑(spectrum R a)
⊢ CompactSpace ↑(σₙ R a)

Tactic:
simp only [← isCompact_iff_compactSpace, quasispectrum_eq_spectrum_union_zero] at h_cpct ⊢

Goal state after:
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
h_cpct : IsCompact (spectrum R a)
⊢ IsCompact (spectrum R a ∪ {0})