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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ν (s ∩ f ⁻¹' {0}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {0})
⊢ (μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ρ s

Tactic:
have B : ν (s ∩ f ⁻¹' {∞}) ≤ ((t : ℝ≥0∞) ^ 2 • ρ :) (s ∩ f ⁻¹' {∞}) := by
    rw [withDensity_absolutelyContinuous μ]
    · exact zero_le
    · rw [← nonpos_iff_eq_zero]
      exact (measure_mono inter_subset_right).trans (v.measure_limRatioMeas_top hρ).le

Goal state after:
α : 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
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ν (s ∩ f ⁻¹' {0}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {0})
B : ν (s ∩ f ⁻¹' {∞}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {∞})
⊢ (μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ρ s
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
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ν (s ∩ f ⁻¹' {0}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {0})
B : ν (s ∩ f ⁻¹' {∞}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {∞})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ ∫⁻ (x : α) in s ∩ f ⁻¹' I, ↑t ^ (n + 1) ∂μ = ↑t ^ (n + 1) * μ (s ∩ f ⁻¹' I)

Tactic:
by
        simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]

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 α
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)) (f (w (N - 1))) + (edist (f (w (N + 1))) (f (w N)) + 0)

Tactic:
add_zero,

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)) (f (w (N - 1))) + edist (f (w (N + 1))) (f (w N))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inr.inr
α : 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
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j))

Tactic:
calc
      (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
          ((∑ i ∈ Finset.Ico 0 (N - 1), edist (f (u (i + 1))) (f (u i))) +
              ∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i))) +
            ∑ i ∈ Finset.Ico N n, edist (f (u (i + 1))) (f (u i)) := by
        rw [Finset.sum_Ico_consecutive, Finset.sum_Ico_consecutive, Finset.range_eq_Ico] <;> grind
      _ = (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i))) +
              edist (f (u N)) (f (u (N - 1))) +
            ∑ i ∈ Finset.Ico N n, edist (f (w (1 + i + 1))) (f (w (1 + i))) := by
        congr 1
        · congr 1
          · grind [Finset.sum_congr]
          · have A : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
            have : Finset.Ico (N - 1) N = {N - 1} := by rw [← Nat.Ico_succ_singleton, A]
            simp only [this, A, Finset.sum_singleton]
        · grind [Finset.sum_congr]
      _ = (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i))) +
              edist (f (w (N + 1))) (f (w (N - 1))) +
            ∑ i ∈ Finset.Ico (N + 1) (n + 1), edist (f (w (i + 1))) (f (w i)) := by
        congr 1
        · grind
        · exact Finset.sum_Ico_add (fun i => edist (f (w (i + 1))) (f (w i))) N n 1
      _ ≤ ((∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i))) +
              ∑ i ∈ Finset.Ico (N - 1) (N + 1), edist (f (w (i + 1))) (f (w i))) +
            ∑ i ∈ Finset.Ico (N + 1) (n + 1), edist (f (w (i + 1))) (f (w i)) := by
        refine add_le_add (add_le_add le_rfl ?_) le_rfl
        have A : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
        have B : N - 1 + 1 < N + 1 := A.symm ▸ N.lt_succ_self
        have C : N - 1 < N + 1 := lt_of_le_of_lt N.pred_le N.lt_succ_self
        rw [Finset.sum_eq_sum_Ico_succ_bot C, Finset.sum_eq_sum_Ico_succ_bot B, A, Finset.Ico_self,
          Finset.sum_empty, add_zero, add_comm (edist _ _)]
        exact edist_triangle _ _ _
      _ = ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)) := by
        rw [Finset.sum_Ico_consecutive, Finset.sum_Ico_consecutive, Finset.range_eq_Ico] <;> grind

Goal state after:
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
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {∞}) ≤ (t • ν) (s ∩ f ⁻¹' {∞})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ ↑t ^ (n + 1) * μ (s ∩ f ⁻¹' I) = ∫⁻ (x : α) in s ∩ f ⁻¹' I, ↑t ^ (n + 1) ∂μ

Tactic:
by
        simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case h'f
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K} := ⋯
t : Set E
t_count : t.Countable
ht : range f ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
n : ℕ
c : E
hi✝ : c ∈ t
⊢ ∫⁻ (y : α), ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ ∂μ ≠ ∞

Tactic:
apply ne_of_lt
      calc
        ∫⁻ y, ‖f y - (A.set n).indicator (fun _ : α => c) y‖ₑ ∂μ
          ≤ ∫⁻ y, ‖f y‖ₑ + ‖(A.set n).indicator (fun _ : α => c) y‖ₑ ∂μ :=
          lintegral_mono fun x ↦ enorm_sub_le
        _ = ∫⁻ y, ‖f y‖ₑ ∂μ + ∫⁻ y, ‖(A.set n).indicator (fun _ : α => c) y‖ₑ ∂μ :=
          lintegral_add_left h'f.enorm _
        _ < ∞ + ∞ :=
          haveI I : Integrable ((A.set n).indicator fun _ : α => c) μ := by
            simp only [integrable_indicator_iff (IsOpen.measurableSet (A.set_mem n)),
              integrableOn_const_iff (C := c), A.finite n, or_true]
          ENNReal.add_lt_add hf.2 I.2

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

Goal state before:
pp: case 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 : y ≤ x
⊢ 0 = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))

pp: case inr.hs
α : 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 : y ≤ x
⊢ (t ∩ Icc x y).Subsingleton

Tactic:
eVariationOn.subsingleton

Goal state after:
case 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 : y ≤ x
⊢ 0 = 0

case inr.hs
α : 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 : y ≤ x
⊢ (φ '' t ∩ Icc (φ x) (φ y)).Subsingleton

case inr.hs
α : 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 : y ≤ x
⊢ (t ∩ Icc x y).Subsingleton
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
a : A
ha : p a
⊢ cfc f a = (cfcHom ha) (mkD ((spectrum R a).domRestrict f) 0)

Tactic:
by_cases hf : ContinuousOn f (spectrum R a)
  · rw [cfc_apply f a, mkD_of_continuousOn hf]
  · rw [cfc_apply_of_not_continuousOn a hf, mkD_of_not_continuousOn hf,
      map_zero]

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

Goal state before:
pp: case inl
α : 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
⊢ 0 = eVariationOn f (s ∩ Icc y x)

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:
eVariationOn.subsingleton

Goal state after:
case inl
α : 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
⊢ 0 = 0

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.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 u : A
hu : u ∈ {x} ∪ star {x}
hy : u ∈ ↑(adjoin R {x})
⊢ ?m.230

Tactic:
simpa using hu

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
C : ℝ
hf : MonotoneOn f s
h : ∀ x ∈ s, |f x| ≤ C
⊢ ⨆ p ∈ {p | p.1 ∈ s ∧ p.2 ∈ s ∧ p.1 ≤ p.2}, eVariationOn f (s ∩ Set.Icc p.1 p.2) ≤ ENNReal.ofReal (2 * C)

Tactic:
simp only [mem_ofPred_eq, iSup_le_iff, and_imp, Prod.forall]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
C : ℝ
hf : MonotoneOn f s
h : ∀ x ∈ s, |f x| ≤ C
⊢ ∀ (a b : α), a ∈ s → b ∈ s → a ≤ b → eVariationOn f (s ∩ Set.Icc a b) ≤ ENNReal.ofReal (2 * C)
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ X.toContinuousMap = ContinuousMap.id R

Tactic:
by
  ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
⊢ X.toContinuousMapOn s = restrict s (ContinuousMap.id R)

Tactic:
by
  ext; simp

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

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

Tactic:
apply Or.inr
      push _ ∈ _ at hx ⊢
      rw [show x = 0 from Subtype.val_injective hx, map_zero]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
⊢ ((algebraMap ℝ C(X, ℝ)) ↑r).toNNReal = (algebraMap ℝ≥0 C(X, ℝ≥0)) r

Tactic:
by
  ext; simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
⊢ (-(algebraMap ℝ C(X, ℝ)) ↑r).toNNReal = 0

Tactic:
by
  ext; simp

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
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
φ ψ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst✝²] ⇑φ
hψ : Continuous[_, inst✝²] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) = ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
ξ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A
hξ : Continuous[_, inst✝²] ⇑ξ
ξ' : C(↑s', ℝ) →⋆ₐ[ℝ] A := ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e)
⊢ Continuous[_, inst✝²] ⇑ξ' ∧
    ξ' (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) = ξ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))

Tactic:
refine ⟨ξ.continuous_realContinuousMapOfNNReal hξ |>.comp <|
        ContinuousMap.continuous_precomp _, ?_⟩

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
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
φ ψ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst✝²] ⇑φ
hψ : Continuous[_, inst✝²] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) = ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
ξ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A
hξ : Continuous[_, inst✝²] ⇑ξ
ξ' : C(↑s', ℝ) →⋆ₐ[ℝ] A := ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e)
⊢ ξ' (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) = ξ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
Module: Mathlib.Analysis.Real.Spectrum

Goal state before:
pp: case refine_1
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
h : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ≥0
hx : (algebraMap ℝ≥0 ℝ) x ∈ spectrum ℝ a
⊢ 0 ≤ (algebraMap ℝ≥0 ℝ) x

Tactic:
exact coe_nonneg x

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
⊢ f ∈ A.topologicalClosure

Tactic:
subalgebra_topologicalClosure_eq_top_of_separatesPoints A w

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
⊢ f ∈ ⊤
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case right
X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
hsep : AK.SeparatesPoints
gK : C(↑K, ℝ)
hgKAK✝ : gK ∈ AK
hgapprox : ∀ (x : ↑K), ‖↑⟨gK, hgKAK✝⟩ x - K.domRestrict (⇑f) x‖ < ε
g : C(X, ℝ)
hgA : g ∈ A
hgKAK : ↑restrict_on_K g = gK
x : X
hxK : x ∈ K
eqg : g x = gK ⟨x, hxK⟩
⊢ ‖g x - f x‖ < ε

Tactic:
eqg

Goal state after:
case right
X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
hsep : AK.SeparatesPoints
gK : C(↑K, ℝ)
hgKAK✝ : gK ∈ AK
hgapprox : ∀ (x : ↑K), ‖↑⟨gK, hgKAK✝⟩ x - K.domRestrict (⇑f) x‖ < ε
g : C(X, ℝ)
hgA : g ∈ A
hgKAK : ↑restrict_on_K g = gK
x : X
hxK : x ∈ K
eqg : g x = gK ⟨x, hxK⟩
⊢ ‖gK ⟨x, hxK⟩ - f x‖ < ε
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
⊢ ∀ (x : C(X, 𝕜)), x ∈ A.topologicalClosure

Tactic:
have key : I.range ≤ (A.toSubmodule.restrictScalars ℝ).topologicalClosure := by
    -- Let `A₀` be the subalgebra of `C(X, ℝ)` consisting of `A`'s purely real elements; it is the
    -- preimage of `A` under `I`.  In this argument we only need its submodule structure.
    let A₀ : Submodule ℝ C(X, ℝ) := (A.toSubmodule.restrictScalars ℝ).comap I.toLinearMap
    -- By `Subalgebra.SeparatesPoints.rclike_to_real`, this subalgebra also separates points, so
    -- we may apply the real Stone-Weierstrass result to it.
    have SW : A₀.topologicalClosure = ⊤ :=
      haveI := subalgebra_topologicalClosure_eq_top_of_separatesPoints _ hA.rclike_to_real
      congr_arg Subalgebra.toSubmodule this
    rw [← Submodule.map_top, ← SW]
    -- So it suffices to prove that the image under `I` of the closure of `A₀` is contained in the
    -- closure of `A`, which follows by abstract nonsense
    have h₁ := A₀.topologicalClosure_map I
    have h₂ := (A.toSubmodule.restrictScalars ℝ).map_comap_le I.toLinearMap
    exact h₁.trans (Submodule.topologicalClosure_mono h₂)

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : (↑I).range ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
⊢ ∀ (x : C(X, 𝕜)), x ∈ A.topologicalClosure
Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖

Tactic:
by
    simp_rw [unitization_norm_def, add_mul, mul_add, unitization_mul, fst_mul, snd_mul]
    rw [add_assoc, add_assoc]
    gcongr
    · exact norm_mul_le _ _
    · apply (norm_add_le _ _).trans
      gcongr
      · simp [norm_smul]
      · apply (norm_add_le _ _).trans
        gcongr
        · simp [norm_smul, mul_comm]
        · exact norm_mul_le _ _

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
⊢ characterSpace 𝕜 A ∪ {0} ⊆ {φ | ∀ (x y : A), φ (x * y) = φ x * φ y}

Tactic:
by
      rintro φ (hφ | rfl)
      · exact hφ.2
      · exact fun _ _ => by exact (zero_mul (0 : 𝕜)).symm

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ x ∈ 𝕜 ∙ 1 ⊔ (adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}).toSubmodule ↔
    x ∈ 𝕜 ∙ 1 ⊔ span 𝕜 ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})

Tactic:
span_eq_toSubmodule

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ x ∈ 𝕜 ∙ 1 ⊔ (adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}).toSubmodule ↔
    x ∈ 𝕜 ∙ 1 ⊔ (adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}).toSubmodule
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: 𝕜 : 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 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed (characterSpace 𝕜 A)

Tactic:
by
  rw [eq_set_map_one_map_mul, Set.ofPred_and]
  refine IsClosed.inter (isClosed_eq (eval_continuous _) continuous_const) ?_
  simpa only [(union_zero 𝕜 A).symm] using union_zero_isClosed _ _

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 • 1) ⟨0, h0⟩ + 0 = 0
this : f ⟨0, h0⟩ = 0
⊢ r • 1 + f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

Tactic:
add_zero,

Goal state after:
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 • 1) ⟨0, h0⟩ = 0
this : f ⟨0, h0⟩ = 0
⊢ r • 1 + f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}