mathlib-initiative/mathlib-tactics huggingface dataset:
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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n ↦ s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n ↦ s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n
m n : ℕ
I : (ρ + μ) (u m) ≠ ∞
J : (ρ + μ) (w n) ≠ ∞
A :
  ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
H : (ρ + μ) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ∞
⊢ μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ∞

Tactic:
simp only [not_or, ENNReal.add_eq_top, Pi.add_apply, Ne, coe_add] at H

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n ↦ s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n ↦ s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n
m n : ℕ
I : (ρ + μ) (u m) ≠ ∞
J : (ρ + μ) (w n) ≠ ∞
A :
  ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
H :
  ¬ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = ∞ ∧
    ¬μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = ∞
⊢ μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ∞
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f g : α → E
s : Set α
h : EqOn f g s
⊢ eVariationOn f s = eVariationOn g s

Tactic:
by
  grind [eVariationOn]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (↑r.toNNReal • μ) =ᵐ[μ] r.toNNReal⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ

Tactic:
ENNReal.coe_toNNReal hr_ne_top,

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r • μ) =ᵐ[μ] r.toNNReal⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ
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
⊢ SpectrumRestricts ↑a ⇑Complex.reCLM ↔ ∀ x ∈ spectrum ℂ ↑a, x = ↑x.re

Tactic:
SpectrumRestricts.real_iff

Goal state after:
A : Type u_1
inst✝³ : NonUnitalRing A
inst✝² : Module ℂ A
inst✝¹ : IsScalarTower ℂ A A
inst✝ : SMulCommClass ℂ A A
a : A
⊢ (∀ x ∈ spectrum ℂ ↑a, x = ↑x.re) ↔ ∀ x ∈ spectrum ℂ ↑a, x = ↑x.re
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 α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
A : N - 1 + 1 = N
B : N - 1 + 1 < N + 1
C : N - 1 < N + 1
⊢ edist (f (w (N + 1))) (f (w (N - 1))) ≤
    edist (f (w (N - 1 + 1))) (f (w (N - 1))) + ∑ k ∈ Finset.Ico (N - 1 + 1) (N + 1), edist (f (w (k + 1))) (f (w k))

Tactic:
Finset.sum_eq_sum_Ico_succ_bot B,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
A : N - 1 + 1 = N
B : N - 1 + 1 < N + 1
C : N - 1 < N + 1
⊢ edist (f (w (N + 1))) (f (w (N - 1))) ≤
    edist (f (w (N - 1 + 1))) (f (w (N - 1))) +
      (edist (f (w (N - 1 + 1 + 1))) (f (w (N - 1 + 1))) +
        ∑ k ∈ Finset.Ico (N - 1 + 1 + 1) (N + 1), edist (f (w (k + 1))) (f (w k)))
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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (v.limRatioMeas hρ)) s = ρ s

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (v.limRatioMeas hρ)) s ≤ ρ s

case refine_2
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ ρ s ≤ (μ.withDensity (v.limRatioMeas hρ)) s
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this : Tendsto (fun t ↦ ↑t ^ 2 * ρ s) (𝓝[>] 1) (𝓝 (1 ^ 2 * ρ s))
⊢ (μ.withDensity (v.limRatioMeas hρ)) s ≤ ρ s

Tactic:
simp only [one_pow, one_mul] at this

Goal state after:
case refine_1
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this : Tendsto (fun t ↦ ↑t ^ 2 * ρ s) (𝓝[>] 1) (𝓝 (ρ s))
⊢ (μ.withDensity (v.limRatioMeas hρ)) s ≤ ρ s
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case e'_3.a.inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
ux : u ≤ x
⊢ φ x ∈ φ '' (t ∩ Icc x y)

Tactic:
exact ⟨x, ⟨hx, ⟨le_rfl, h⟩⟩, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
⊢ eVariationOn f (s ∩ Iic a) = eVariationOn f (s ∩ Iio a) + edist (f a) l

Tactic:
refine le_antisymm ?_ ?_

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)
⊢ eVariationOn f (s ∩ Iic a) ≤ eVariationOn f (s ∩ Iio a) + edist (f a) l

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)
⊢ eVariationOn f (s ∩ Iio a) + edist (f a) l ≤ eVariationOn f (s ∩ Iic 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 ↦ f x + r) a

Tactic:
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
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case hg
α : 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
a : Set α
ha : 0 < μ a
h'a : μ a < ∞
h''a : IntegrableOn f a μ
⊢ Integrable (fun x_1 ↦ f x) ((μ a)⁻¹ • μ.restrict a)

Tactic:
· exact (integrable_inv_smul_measure ha.ne' h'a.ne).2 (integrableOn_const h'a.ne)

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
a : A
h_spec : spectrum R a ⊆ {1}
ha : p a
⊢ a = 1

Tactic:
by
  simpa using eq_algebraMap_of_spectrum_subset_singleton a 1 h_spec

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

Goal state before:
pp: case e_6
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))
x : R
hx : x ∈ spectrum R ((algebraMap R A) r)
⊢ (spectrum R ((algebraMap R A) r)).domRestrict f ⟨x, hx⟩ = (algebraMap R R) (f r)

Tactic:
apply CFC.spectrum_algebraMap_subset r at hx

Goal state after:
case e_6
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))
x : R
hx✝ : x ∈ spectrum R ((algebraMap R A) r)
hx : x ∈ {r}
⊢ (spectrum R ((algebraMap R A) r)).domRestrict f ⟨x, hx✝⟩ = (algebraMap 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✝⁷ : 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
f : R → R
⊢ cfc f 1 = (algebraMap R A) (f 1)

Tactic:
by
  simpa using cfc_algebraMap (A := A) 1 f

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

Goal state before:
pp: case hφ₂
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁵ : Semifield R
inst✝²⁴ : StarRing R
inst✝²³ : MetricSpace R
inst✝²² : IsTopologicalSemiring R
inst✝²¹ : ContinuousStar R
inst✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : TopologicalSpace A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus S A q
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
f : C(S, R)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts a ⇑f
⊢ (nonUnitalStarAlgHom (cfcₙHom hqa) h) (ContinuousMapZero.id (σₙ R a)) = a

Tactic:
exact h.nonUnitalStarAlgHom_id (cfcₙHom_id hqa)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
inst✝ : UniqueHom R A
f : C(↑(σₙ R a), R)₀
f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀
hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)
g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀
ψ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] C(↑(σₙ R a), R)₀ :=
  { toFun := fun x ↦ x.comp f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ
⊢ (cfcₙHom ha) (g.comp f') = (cfcₙHom ⋯) g

Tactic:
suffices cfcₙHom (cfcₙHom_predicate ha f) = φ from DFunLike.congr_fun this.symm g

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
a : A
ha : p a
inst✝ : UniqueHom R A
f : C(↑(σₙ R a), R)₀
f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀
hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)
g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀
ψ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] C(↑(σₙ R a), R)₀ :=
  { toFun := fun x ↦ x.comp f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ
⊢ cfcₙHom ⋯ = φ
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
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ 0 ≤ -cfc f a ↔ ∀ x ∈ spectrum R a, 0 ≤ -f x

Tactic:
← cfc_neg

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
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ 0 ≤ cfc (fun x ↦ -f x) a ↔ ∀ x ∈ spectrum R a, 0 ≤ -f 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 α
inst✝¹ : CompleteSpace E
inst✝ : T3Space E
f : α → E
hf : BoundedVariationOn f univ
x : α
⊢ ContinuousWithinAt (Function.leftLim f) (Iic x) x

Tactic:
have : Tendsto f.leftLim (𝓝[<] x) (𝓝 (f.leftLim.leftLim x)) := hf.leftLim.tendsto_leftLim x
  rw [leftLim_leftLim (hf.tendsto_leftLim x)] at this
  exact continuousWithinAt_Iio_iff_Iic.1 this

Goal state after:
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
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Set.Icc a b
⊢ ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i)) ≤
    ENNReal.ofReal (f b - f a)

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

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

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

Tactic:
simp [hab, hf bs as hab.le]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
r : R
f : R → R
a : A
hf : ContinuousOn f ((fun x ↦ r * x) '' σₙ R a)
hf0 : f 0 = 0
ha : p a
⊢ cfcₙ (fun x ↦ f (r * x)) a = cfcₙ f (r • a)

Tactic:
rw [cfcₙ_comp' f (r * ·) a, cfcₙ_const_mul_id r a]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
r : R
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r) ∈ R[(toContinuousMapOnAlgHom s) X]

Tactic:
rw [Polynomial.C_eq_algebraMap, AlgHomClass.commutes]

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
r : R
⊢ (algebraMap R C(↑s, R)) r ∈ R[(toContinuousMapOnAlgHom s) X]
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✝¹² : 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 : R → R
a : A
inst✝ : UniqueHom R A
hf : ContinuousOn f ((fun x ↦ -x) '' σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ cfcₙ f (cfcₙ Neg.neg a) = cfcₙ f (-a)

Tactic:
cfcₙ_neg_id _

Goal state after:
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 : R → R
a : A
inst✝ : UniqueHom R A
hf : ContinuousOn f ((fun x ↦ -x) '' σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ cfcₙ f (-a) = cfcₙ f (-a)
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν ∈ Finset.range (n + 1), (n • X - ↑ν) ^ 2 * bernsteinPolynomial R n ν = n • X * (1 - X)

Tactic:
by
  have p : ((((Finset.range (n + 1)).sum fun ν => (ν * (ν - 1)) • bernsteinPolynomial R n ν) +
      (1 - (2 * n) • Polynomial.X) * (Finset.range (n + 1)).sum fun ν =>
        ν • bernsteinPolynomial R n ν) + n ^ 2 • X ^ 2 *
          (Finset.range (n + 1)).sum fun ν => bernsteinPolynomial R n ν) = _ :=
    rfl
  conv at p =>
    lhs
    rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
    simp only [← natCast_mul]
    simp only [← mul_assoc]
    simp only [← add_mul]
  conv at p =>
    rhs
    rw [sum, sum_smul, sum_mul_smul, ← natCast_mul]
  calc
    _ = _ := Finset.sum_congr rfl fun k m => ?_
    _ = _ := p
    _ = _ := ?_
  · congr 1; simp only [← natCast_mul, push_cast]
    cases k <;> · simp; ring
  · simp only [← natCast_mul, push_cast]
    cases n
    · simp
    · simp; ring

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
f g : C(X, ℝ)
⊢ φ (f + g).toNNReal - φ (-(f + g)).toNNReal = φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)

Tactic:
have := congr(φ $(f.toNNReal_add_add_neg_add_neg_eq g))

Goal state after:
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
f g : C(X, ℝ)
this : φ ((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) = φ ((-(f + g)).toNNReal + f.toNNReal + g.toNNReal)
⊢ φ (f + g).toNNReal - φ (-(f + g)).toNNReal = φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)
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
⊢ ∀ ⦃a₂ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A⦄, φ.realContinuousMapOfNNReal = a₂.realContinuousMapOfNNReal → φ = a₂

Tactic:
ψ

Goal state after:
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
⊢ φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal → φ = ψ