mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
A : ∀ a ∈ t', r a ≤ 1
⊢ ∃ u ⊆ t', u.PairwiseDisjoint B ∧ ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b

Tactic:
have A' : ∀ a ∈ t', (B a).Nonempty :=
      fun a hat' => Set.Nonempty.mono interior_subset (ht a hat'.1)

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
A : ∀ a ∈ t', r a ≤ 1
A' : ∀ a ∈ t', (B a).Nonempty
⊢ ∃ u ⊆ t', u.PairwiseDisjoint B ∧ ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
x✝ : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
H : R x ≤ R0
R0pos : 0 < R0
⊢ ∃ K, μ (closedBall x K) < ∞ ∧ ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K

Tactic:
have vnonempty : v.Nonempty := by
        by_contra h
        rw [nonempty_iff_ne_empty, Classical.not_not] at h
        rw [h, image_empty, Real.sSup_empty] at R0_def
        exact lt_irrefl _ (R0pos.trans_le (le_of_eq R0_def))

Goal state after:
case inr
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
x✝ : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
H : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
⊢ ∃ K, μ (closedBall x K) < ∞ ∧ ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ∞
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : ν U ≤ ν s + ↑ε
f : α → Set (Set α) := fun x ↦ {a | ρ a ≤ ν a ∧ a ⊆ U}
x : α
hx : x ∈ s
this : ∃ᶠ (x_1 : Set α) in v.filterAt x, ρ x_1 ≤ ν x_1 ∧ x_1 ∈ v.setsAt x ∧ x_1 ⊆ U
a : Set α
ρa : ρ a ≤ ν a
left✝ : a ∈ v.setsAt x
aU : a ⊆ U
⊢ a ∈ f x

Tactic:
exact ⟨ρa, aU⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
n : ℕ
⊢ ∃ s,
    MeasurableSet s ∧
      (∀ (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ s) ≤ μ (t ∩ s)) ∧
        ∀ (t : Set α), MeasurableSet t → μ (t ∩ sᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ sᶜ)

Tactic:
obtain ⟨s, hs, hs_le, hs_ge⟩ := hahn_decomposition μ ((1 / (n + 1) : ℝ≥0) • ν)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
n : ℕ
s : Set α
hs : MeasurableSet s
hs_le : ∀ (t : Set α), MeasurableSet t → t ⊆ s → ((1 / (↑n + 1)) • ν) t ≤ μ t
hs_ge : ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ((1 / (↑n + 1)) • ν) t
⊢ ∃ s,
    MeasurableSet s ∧
      (∀ (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ s) ≤ μ (t ∩ s)) ∧
        ∀ (t : Set α), MeasurableSet t → μ (t ∩ sᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ sᶜ)
Module: Mathlib.MeasureTheory.Covering.OneDim

Goal state before:
pp: x y : ℝ
hxy : x < y
⊢ Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ (vitaliFamily volume 1).setsAt x

Tactic:
refine closedBall_mem_vitaliFamily_of_dist_le_mul _ ?_ (by linarith)

Goal state after:
x y : ℝ
hxy : x < y
⊢ dist x ((x + y) / 2) ≤ 1 * ((y - x) / 2)
Module: Mathlib.MeasureTheory.Covering.OneDim

Goal state before:
pp: x y : ℝ
hxy : x < y
⊢ Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ (vitaliFamily volume 1).setsAt y

Tactic:
refine closedBall_mem_vitaliFamily_of_dist_le_mul _ ?_ (by linarith)

Goal state after:
x y : ℝ
hxy : x < y
⊢ dist y ((x + y) / 2) ≤ 1 * ((y - x) / 2)
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : StieltjesFunction ℝ
x : ℝ
hx : Tendsto (fun a ↦ f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y ↦ (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y ↦ (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L3 :
  Tendsto (fun y ↦ (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[<] x)
    (𝓝 (f.measure.rnDeriv volume x).toReal)
y : ℝ
hy : y < x
⊢ (↑f y - ↑f x) / (y - x) ≤ (leftLim (↑f) y - ↑f x) / (y - x)

Tactic:
refine div_le_div_of_nonpos_of_le (by linarith) ?_

Goal state after:
f : StieltjesFunction ℝ
x : ℝ
hx : Tendsto (fun a ↦ f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y ↦ (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y ↦ (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L3 :
  Tendsto (fun y ↦ (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[<] x)
    (𝓝 (f.measure.rnDeriv volume x).toReal)
y : ℝ
hy : y < x
⊢ leftLim (↑f) y - ↑f x ≤ ↑f y - ↑f x
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 α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Tactic:
by
  rcases le_total n m with hnm | hmn
  · simp [Finset.Ico_eq_empty_of_le hnm]
  let π := projIcc m n hmn
  let v i := u (π i)
  calc
    ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i))
        = ∑ i ∈ Finset.Ico m n, edist (f (v (i + 1))) (f (v i)) :=
      Finset.sum_congr rfl fun i hi ↦ by
        rw [Finset.mem_Ico] at hi
        simp only [v, π, projIcc_of_mem hmn ⟨hi.1, hi.2.le⟩,
          projIcc_of_mem hmn ⟨hi.1.trans i.le_succ, hi.2⟩]
    _ ≤ ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) :=
      Finset.sum_mono_set _ (Nat.Iio_eq_range n ▸ Finset.Ico_subset_Iio_self)
    _ ≤ eVariationOn f s :=
      sum_le (fun i j h ↦ hu (π i).2 (π j).2 (monotone_projIcc hmn h)) fun i ↦ us _ (π i).2

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
⊢ ∃ a ∈ s, ∃ b ∈ s, a < b ∧ ε < eVariationOn f (s ∩ Icc a b)

Tactic:
obtain ⟨n, u, ⟨u_mono, u_mem⟩, hu⟩ : ∃ n u, (Monotone u ∧ ∀ (i : ℕ), u i ∈ s) ∧
      ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) := by
    simpa [eVariationOn, lt_iSup_iff] using h

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ ∃ a ∈ s, ∃ b ∈ s, a < b ∧ ε < eVariationOn f (s ∩ Icc a b)
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
⊢ spectrum R ((algebraMap R A) r) ⊆ {r}

Tactic:
← cfc_const r 0 (cfc_predicate_zero R),

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
⊢ spectrum R (cfc (fun x ↦ r) 0) ⊆ {r}
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
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ (cfcₙHom ha) f = cfcₙ (Function.extend Subtype.val (⇑f) g) a

Tactic:
by
  have h : f = (σₙ R a).domRestrict (Function.extend Subtype.val f g) := by
    ext; simp
  have hg : ContinuousOn (Function.extend Subtype.val f g) (σₙ R a) :=
    continuousOn_iff_continuous_domRestrict.mpr <| h ▸ map_continuous f
  have hg0 : (Function.extend Subtype.val f g) 0 = 0 := by
    rw [← quasispectrum.coe_zero (R := R) a, Subtype.val_injective.extend_apply]
    exact map_zero f
  generalize Function.extend Subtype.val f g = f' at *
  rw [cfcₙ_apply ..]
  congr!

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✝¹² : PartialOrder R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ContinuousSqrt R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, 0 ≤ f x
⊢ 0 ≤ cfc f a

Tactic:
by_cases hf : ContinuousOn f (spectrum R a)
  · simpa using cfc_mono h
  · simp only [cfc_apply_of_not_continuousOn _ hf, le_rfl]

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✝¹² : PartialOrder R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ContinuousSqrt R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ 0
⊢ cfc f a ≤ 0

Tactic:
by_cases hf : ContinuousOn f (spectrum R a)
  · simpa using cfc_mono h
  · simp only [cfc_apply_of_not_continuousOn _ hf, le_rfl]

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✝¹⁴ : 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
⊢ cfc f a ≤ 0 ↔ ∀ x ∈ spectrum R a, f x ≤ 0

Tactic:
simp_rw [← neg_nonneg, ← cfc_neg]
  exact cfc_nonneg_iff (fun x ↦ -f x) a

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 α
hs : IsOpen[inst✝¹] s
⊢ eVariationOn (Function.rightLim f) s ≤ eVariationOn f s

Tactic:
apply eVariationOn_le_of_mapClusterPt (fun x hx ↦ ?_)
  rw [IsOpen.nhdsWithin_eq hs hx]
  exact (mapClusterPt_rightLim f x).mono nhdsWithin_le_nhds

Goal state after:
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
f : R → R
a : A
h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ cfcₙ (fun x ↦ star (f x)) a = star (cfcₙ f a)

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
h : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ cfcₙ (fun x ↦ star (f x)) a = star (cfcₙ f a)

Tactic:
· obtain ⟨ha, hf, h0⟩ := h
    rw [cfcₙ_apply f a, ← map_star, cfcₙ_apply _ a]
    congr

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
h : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ cfcₙ (fun x ↦ star (f x)) a = star (cfcₙ f a)
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: case mpr.refine_2
a b : ℝ
h : a < b
p : ℝ[X]
q : ℝ[X] := p.comp ((b - a) • X + Polynomial.C a)
⊢ ↑(toContinuousMapOnAlgHom I) q =
    ↑(compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (↑(toContinuousMapOnAlgHom (Set.Icc a b)) p)

Tactic:
ext x
      simp [q, mul_comm]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
n : ℕ
f : C(↑I, E)
x : ↑I
⊢ (bernsteinApproximation n f) x = ∑ k, (bernstein n ↑k) x • f k/ₙ

Tactic:
simp [bernsteinApproximation]

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

Goal state before:
pp: case mpr.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 : ↑(σₙ R a)
hx : ↑x ∈ spectrum R a
⊢ f x ∈ range ⇑((compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }) (toContinuousMapHom f)) ∪ {0}

Tactic:
exact Or.inl ⟨⟨x.1, hx⟩, rfl⟩

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

Goal state before:
pp: case inl_add_inr
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
r✝ : 𝕜
a✝ : A
hx : (splitMul 𝕜 A) (inl r✝ + ↑a✝) = 0
⊢ inl r✝ + ↑a✝ = 0

Tactic:
rw [map_add] at hx

Goal state after:
case inl_add_inr
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ⇑(mul 𝕜 A)
r✝ : 𝕜
a✝ : A
hx : (splitMul 𝕜 A) (inl r✝) + (splitMul 𝕜 A) ↑a✝ = 0
⊢ inl r✝ + ↑a✝ = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : TopologicalSpace A
inst✝⁵ : T2Space A
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst✝⁶] ⇑φ
hψ : Continuous[_, inst✝⁶] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
⊢ φ = ψ

Tactic:
by
    rw [DFunLike.ext'_iff, ← Set.eqOn_univ, ← (ContinuousMapZero.adjoin_id_dense _).closure_eq]
    refine Set.EqOn.closure (fun f hf ↦ ?_) hφ hψ
    rw [← NonUnitalStarAlgHom.mem_equalizer]
    apply adjoin_le ?_ hf
    rw [Set.singleton_subset_iff]
    exact h

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
frequently : ∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g) → p f
f : C(↑s, 𝕜)
⊢ p f

Tactic:
refine f.induction_on const id star_id add mul fun h f ↦ frequently f ?_

Goal state after:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
frequently : ∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)
h : ∀ f ∈ (polynomialFunctions s).starClosure, p f
f : C(↑s, 𝕜)
⊢ ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
⊢ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) = ↑(𝕜 ∙ 1) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})

Tactic:
ext x
  rw [SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra,
    ← StarSubalgebra.mem_toSubalgebra, ← Subalgebra.mem_toSubmodule,
    StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, mem_sup]
  simp [Set.mem_add]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: case refine_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
⊢ φ ∈ {φ | φ 1 = 1 ∧ ∀ (x y : A), φ (x * y) = φ x * φ y} → φ ∈ characterSpace 𝕜 A

Tactic:
· rintro ⟨hφ₁, hφ₂⟩
    refine ⟨?_, hφ₂⟩
    rintro rfl
    exact zero_ne_one hφ₁

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

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C(↑s, 𝕜)
hf : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf₂ : r = 0
this : f ⟨0, h0⟩ = 0
⊢ r • 1 + f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

Tactic:
rwa [hf₂, zero_smul, zero_add]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
x₀ : α
hx₀s : x₀ ∈ s
V : Set β
hV : IsOpen[inst✝.toTopologicalSpace] V
y₀ : β
hy₀f : y₀ ∈ f x₀
hy₀V : y₀ ∈ V
W : Set (β × β)
hW : W ∈ uniformity β
hWsub : ball y₀ W ⊆ V
U₁ : Set (β × β)
hU₁ : U₁ ∈ uniformity β
hU₁sym : SetRel.IsSymm U₁
hU₁comp : SetRel.comp U₁ U₁ ⊆ W
U : Set (β × β)
hU : U ∈ uniformity β
hUsym : SetRel.IsSymm U
hUcomp : SetRel.comp U U ⊆ U₁
hU_le_U₁ : U ⊆ U₁
hHU : hausdorffEntourage U ∈ uniformity (Set β)
⊢ ∀ᶠ (x' : α) in 𝓝[s] x₀, (f x' ∩ V).Nonempty

Tactic:
obtain ⟨N, hN⟩ := (htendsto (hausdorffEntourage U) hHU).exists

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
x₀ : α
hx₀s : x₀ ∈ s
V : Set β
hV : IsOpen[inst✝.toTopologicalSpace] V
y₀ : β
hy₀f : y₀ ∈ f x₀
hy₀V : y₀ ∈ V
W : Set (β × β)
hW : W ∈ uniformity β
hWsub : ball y₀ W ⊆ V
U₁ : Set (β × β)
hU₁ : U₁ ∈ uniformity β
hU₁sym : SetRel.IsSymm U₁
hU₁comp : SetRel.comp U₁ U₁ ⊆ W
U : Set (β × β)
hU : U ∈ uniformity β
hUsym : SetRel.IsSymm U
hUcomp : SetRel.comp U U ⊆ U₁
hU_le_U₁ : U ⊆ U₁
hHU : hausdorffEntourage U ∈ uniformity (Set β)
N : ι
hN : ∀ x ∈ s, (f x, F N x) ∈ hausdorffEntourage U
⊢ ∀ᶠ (x' : α) in 𝓝[s] x₀, (f x' ∩ V).Nonempty