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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this✝ : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ (μ - ν.withDensity ξ) (A ∩ E)
hε₂ : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν ≤ μ (A ∩ E)
A : Set α
hA : MeasurableSet A
this :
  ∫⁻ (a : α) in A, (ξ + E.indicator fun x ↦ ↑ε) a ∂ν = ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν + ∫⁻ (a : α) in A \ E, ξ a ∂ν
⊢ ∫⁻ (x : α) in A, (ξ + E.indicator fun x ↦ ↑ε) x ∂ν ≤ μ A

Tactic:
this,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this✝ : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ (μ - ν.withDensity ξ) (A ∩ E)
hε₂ : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν ≤ μ (A ∩ E)
A : Set α
hA : MeasurableSet A
this :
  ∫⁻ (a : α) in A, (ξ + E.indicator fun x ↦ ↑ε) a ∂ν = ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν + ∫⁻ (a : α) in A \ E, ξ a ∂ν
⊢ ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν + ∫⁻ (a : α) in A \ E, ξ a ∂ν ≤ μ A
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ dist (f x) (f y) ≤ (eVariationOn f s).toReal

Tactic:
exact h.dist_le hx hy

Goal state after:
Module: Mathlib.Analysis.Complex.Spectrum

Goal state before:
pp: A : Type u_1
inst✝³ : NonUnitalRing A
inst✝² : Module ℂ A
inst✝¹ : IsScalarTower ℂ A A
inst✝ : SMulCommClass ℂ A A
a : A
⊢ QuasispectrumRestricts a ⇑Complex.reCLM ↔ ∀ x ∈ σₙ ℂ a, x = ↑x.re

Tactic:
quasispectrumRestricts_iff_spectrumRestricts_inr,

Goal state after:
A : Type u_1
inst✝³ : NonUnitalRing A
inst✝² : Module ℂ A
inst✝¹ : IsScalarTower ℂ A A
inst✝ : SMulCommClass ℂ A A
a : A
⊢ SpectrumRestricts ↑a ⇑Complex.reCLM ↔ ∀ x ∈ σₙ ℂ a, x = ↑x.re
Module: Mathlib.Topology.ContinuousMap.StarOrdered

Goal state before:
pp: case mp.add_left
α : Type u_1
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : Zero α
R : Type u_2
inst✝⁸ : TopologicalSpace R
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : NoZeroDivisors R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : IsTopologicalSemiring R
inst✝¹ : ContinuousStar R
inst✝ : StarOrderedRing C(α, R)
p✝ s : C(α, R)
s_mem : s ∈ Set.range fun s ↦ star s * s
p : C(α, R)
p_mem : p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hp' : ∀ (f g : C(α, R)₀), ↑g = ↑f + p → ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p
f g : C(α, R)₀
hp : ↑g = ↑f + (s + p)
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p

Tactic:
| add_left s s_mem p p_mem hp' =>

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
s : Set α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hb : b ∈ s
⊢ eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)

Tactic:
have A : IsGreatest (s ∩ Icc a b) b :=
    ⟨⟨hb, hab, le_rfl⟩, inter_subset_right.trans Icc_subset_Iic_self⟩
  have B : IsLeast (s ∩ Icc b c) b :=
    ⟨⟨hb, le_rfl, hbc⟩, inter_subset_right.trans Icc_subset_Ici_self⟩
  rw [← eVariationOn.union f A B, ← inter_union_distrib_left, Icc_union_Icc_eq_Icc hab hbc]

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 α
inst✝ : DenselyOrdered α
f : α → E
a b : α
h' : ContinuousWithinAt f (Iic a) a
⊢ eVariationOn f (Ico b a) = eVariationOn f (Icc b a)

Tactic:
by
  rw [← comp_ofDual f, ← comp_ofDual f, ← Ioc_toDual, ← Icc_toDual]
  exact eVariationOn_Ioc_eq_Icc_of_continuousWithinAt h'

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 : ∀ ⦃a b : ℕ⦄, a ≤ b → u a ≤ u b
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) ≤ eVariationOn f (s ∩ Icc (u 0) (u n))

Tactic:
let v (i : ℕ) := min (u i) (u n)

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 : ∀ ⦃a b : ℕ⦄, a ≤ b → u a ≤ u b
u_mem : ∀ (i : ℕ), u i ∈ s
v : ℕ → α := fun i ↦ min (u i) (u n)
⊢ ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) ≤ eVariationOn f (s ∩ Icc (u 0) (u n))
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 + f x) a = (algebraMap R A) r + cfc f a

Tactic:
this,

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
⊢ cfc (fun z ↦ (fun x ↦ r) z + f z) 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
a : A
n : ℕ
ha : p a
⊢ cfc (fun x ↦ x) a ^ n = a ^ n

Tactic:
cfc_id' ..

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
a : A
n : ℕ
ha : p a
⊢ a ^ n = a ^ n
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
S : Type u_3
inst✝⁴ : SMul S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
a : A
ha : p a
⊢ s • cfc (fun x ↦ x) a = s • a

Tactic:
cfc_id' ..

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
S : Type u_3
inst✝⁴ : SMul S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
a : A
ha : p a
⊢ s • a = s • 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
a : A
ha : p a
⊢ star (cfc (fun x ↦ x) a) = star a

Tactic:
cfc_id' ..

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
a : A
ha : p a
⊢ star a = star 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
q : R[X]
a : A
ha : p a
⊢ (aeval (cfc (fun x ↦ x) a)) q = (aeval a) q

Tactic:
cfc_id' ..

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
q : R[X]
a : A
ha : p a
⊢ (aeval a) q = (aeval a) q
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
this : 0 = (algebraMap R A) 0
⊢ spectrum R 0 = {0}

Tactic:
this,

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 ((algebraMap R A) 0) = {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 : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Ioi x] x) (𝓝 l)
hx : x ∈ s
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Icc x y)) (𝓝[s ∩ Ioi x] x) (𝓝 (edist (f x) l))

Tactic:
by
  have : (fun y ↦ eVariationOn f (s ∩ Icc x y)) =
      (fun y ↦ eVariationOn (f ∘ ofDual) (ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))) := by
    ext y
    rw [Icc_toDual, ← preimage_inter, comp_ofDual]
  rw [this]
  exact hf.ofDual.tendsto_eVariationOn_Icc_left h'f hx

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
inst✝ : Nontrivial A
this : 1 = (algebraMap R A) 1
⊢ spectrum R 1 = {1}

Tactic:
this,

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 : 1 = (algebraMap R A) 1
⊢ spectrum R ((algebraMap R A) 1) = {1}
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 : α
h'f : Tendsto f (𝓝[s ∩ Ioi x] x) (𝓝 l)
hx : x ∈ s
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Icc x y)) (𝓝[s ∩ Ioi x] x) (𝓝 (edist (f x) l))

Tactic:
by
  have : (fun y ↦ eVariationOn f (s ∩ Icc x y)) =
      (fun y ↦ eVariationOn (f ∘ ofDual) (ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))) := by
    ext y
    rw [Icc_toDual, ← preimage_inter, comp_ofDual]
  rw [this]
  exact hf.ofDual.tendsto_eVariationOn_Icc_left h'f hx

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

Goal state before:
pp: case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : 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 : R → R
a : A
ha : p a
f_cont : ContinuousOn f (σₙ R a)
f_zero : ¬f 0 = 0
⊢ cfcₙ f a = (cfcₙHom ha) (mkD ((σₙ R a).domRestrict f) 0)

Tactic:
cfcₙ_apply_of_not_map_zero a f_zero,

Goal state after:
case neg
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 : R → R
a : A
ha : p a
f_cont : ContinuousOn f (σₙ R a)
f_zero : ¬f 0 = 0
⊢ 0 = (cfcₙHom ha) (mkD ((σₙ R a).domRestrict f) 0)
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
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)

Tactic:
have h : BoundedVariationOn f (s ∩ Icc a b) := (hle.trans_lt ofReal_lt_top).ne

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)
h : BoundedVariationOn f (s ∩ Set.Icc a b)
⊢ eVariationOn f (s ∩ Set.Icc a b) = ENNReal.ofReal (f b - f a)
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case pos.succ.inr
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
this : n - 1 - (ν - 1) = n - ν
⊢ ↑n * eval (↑(n - 1 - (ν - 1))) (ascPochhammer R ν) = ↑(n - (ν - 0)) * eval (↑(n - (ν - 0)) + 1) (ascPochhammer R ν)

Tactic:
this,

Goal state after:
case pos.succ.inr
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
this : n - 1 - (ν - 1) = n - ν
⊢ ↑n * eval (↑(n - ν)) (ascPochhammer R ν) = ↑(n - (ν - 0)) * eval (↑(n - (ν - 0)) + 1) (ascPochhammer R ν)
Module: Mathlib.Topology.ContinuousMap.Weierstrass

Goal state before:
pp: f : C(↑I, ℝ)
n : ℕ
i : Fin (n + 1)
⊢ bernstein n ↑i • const (↑I) (f (bernstein.z i)) ∈ ↑(polynomialFunctions I)

Tactic:
polynomialFunctions_coe

Goal state after:
f : C(↑I, ℝ)
n : ℕ
i : Fin (n + 1)
⊢ bernstein n ↑i • const (↑I) (f (bernstein.z i)) ∈ Set.range ⇑(Polynomial.toContinuousMapOnAlgHom I)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommRing R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalRing 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
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
ha : p a
⊢ cfcₙ f a ≤ cfcₙ g a ↔ ∀ x ∈ σₙ R a, f x ≤ g x

Tactic:
rw [cfcₙ_apply f a, cfcₙ_apply g a, cfcₙHom_le_iff (show p a from ha), ContinuousMapZero.le_def]

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommRing R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalRing 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
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
ha : p a
⊢ (∀ (x : ↑(σₙ R a)),
      { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ } x ≤
        { toFun := (σₙ R a).domRestrict g, continuous_toFun := ⋯, map_zero' := ⋯ } x) ↔
    ∀ x ∈ σₙ R a, f x ≤ g x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case mp
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
x : R
⊢ x ∈ range ⇑((compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }) (toContinuousMapHom f)) ∪ {0} →
    x ∈ range ⇑f

Tactic:
rintro (⟨x, rfl⟩ | rfl)

Goal state after:
case mp.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
x : ↑(spectrum R a)
⊢ ((compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }) (toContinuousMapHom f)) x ∈ range ⇑f

case mp.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ 0 ∈ range ⇑f
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✝¹ : 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
⊢ Filter.comap
      (fun x ↦
        (↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
                  toContinuousMapHom).toNonUnitalAlgHom
            x.1,
          ↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
                  toContinuousMapHom).toNonUnitalAlgHom
            x.2))
      (𝓤 C(↑(spectrum R a), R)) =
    Filter.comap (fun x ↦ (↑x.1, ↑x.2)) (𝓤 C(↑(σₙ R a), R))

Tactic:
this,

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✝¹ : 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
⊢ Filter.comap
      (fun x ↦
        (↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
                  toContinuousMapHom).toNonUnitalAlgHom
            x.1,
          ↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
                  toContinuousMapHom).toNonUnitalAlgHom
            x.2))
      (𝓤 C(↑(spectrum R a), R)) =
    Filter.comap (fun x ↦ (↑x.1, ↑x.2)) (𝓤 C(↑(σₙ R a), R))
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
x z y : X
ym : y ∈ ↑(ys x)
zm : z ∈ U x y
⊢ ∃ b ∈ ys x, f z - ε < (g x b) z

Tactic:
exact ⟨y, ym, zm⟩

Goal state after:
Module: Mathlib.Analysis.Real.Spectrum

Goal state before:
pp: A : Type u_1
inst✝³ : NonUnitalRing A
inst✝² : Module ℝ A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : SMulCommClass ℝ A A
a : A
⊢ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ σₙ ℝ a, 0 ≤ x

Tactic:
quasispectrumRestricts_iff_spectrumRestricts_inr,

Goal state after:
A : Type u_1
inst✝³ : NonUnitalRing A
inst✝² : Module ℝ A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : SMulCommClass ℝ A A
a : A
⊢ SpectrumRestricts ↑a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ σₙ ℝ a, 0 ≤ x