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

Goal state before:
pp: case neg
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : ¬closedBall y r ⊆ closedBall x (R / 4)
⊢ (∃ r_1,
      closedBall y r ⊆ closedBall x r_1 ∧
        μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)

Tactic:
exact Or.inr H

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ρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
⊢ ∀ (a : α),
    (∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt a, ρ a < ↑(u n) * μ a) →
      (∀ᶠ (a : Set α) in v.filterAt a, 0 < μ a) → Tendsto (fun a ↦ ρ a / μ a) (v.filterAt a) (𝓝 0)

Tactic:
intro x hx h'x

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
⊢ Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 0)
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ρ : ρ ≪ μ
⊢ ∀ (a : α),
    Tendsto (fun a ↦ ρ a / μ a) (v.filterAt a) (𝓝 (v.limRatio ρ a)) →
      v.limRatio ρ a = AEMeasurable.mk (v.limRatio ρ) ⋯ a →
        Tendsto (fun a ↦ ρ a / μ a) (v.filterAt a) (𝓝 (v.limRatioMeas hρ a))

Tactic:
intro x hx h'x

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
hx : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
h'x : v.limRatio ρ x = AEMeasurable.mk (v.limRatio ρ) ⋯ x
⊢ Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ eVariationOn f s ≤ ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i))

Tactic:
apply iSup_le
    rintro ⟨n, u, u_mono, u_mem⟩
    have : ∃ p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s },
        (p.2 : ℕ → α) p.1 = u n ∧
        ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) =
        ∑ i ∈ Finset.range p.1, edist (f ((p.2 : ℕ → α) (i + 1))) (f ((p.2 : ℕ → α) i)) := by
      induction n with
      | zero => exact ⟨⟨0, ⟨u, by grind [StrictMonoOn], fun i hi ↦ u_mem _⟩⟩, by simp⟩
      | succ n ih =>
        rcases ih with ⟨⟨m, v, v_mono, v_mem⟩, hv, h'v⟩
        simp only [Finset.sum_range_succ, Sigma.exists, Subtype.exists, mem_Iic, exists_and_left,
          exists_prop]
        rcases (u_mono (Nat.le_add_right n 1)).eq_or_lt with hn | hn
        · simp only [← hn, edist_self, add_zero]
          exact ⟨m, v, hv, ⟨v_mono, v_mem⟩, h'v⟩
        · refine ⟨m + 1, fun i ↦ if i ≤ m then v i else u (n + 1), by simp,
            by grind [StrictMonoOn], ?_⟩
          simp only [h'v, ← hv, Order.add_one_le_iff, Finset.sum_range_succ, lt_self_iff_false,
            ↓reduceIte, le_refl]
          congr 1
          exact Finset.sum_congr rfl (by grind)
    rcases this with ⟨p, -, hp⟩
    rw [hp]
    apply le_iSup _ p

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
⊢ (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)

Tactic:
rw [← (r • ν).haveLebesgueDecomposition_add μ, singularPart_smul, ← smul_add,
      ← ν.haveLebesgueDecomposition_add μ]

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ (variationOnFromTo f s c x + f x) / 2 ≤ (variationOnFromTo f s c y + f y) / 2

Tactic:
gcongr 1

Goal state after:
case hab
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ variationOnFromTo f s c x + f x ≤ variationOnFromTo f s c y + f y
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ (variationOnFromTo f s c x - f x) / 2 ≤ (variationOnFromTo f s c y - f y) / 2

Tactic:
gcongr 1

Goal state after:
case hab
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ variationOnFromTo f s c x - f x ≤ variationOnFromTo f s c y - f y
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr.refine_3
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ f = (fun x ↦ (variationOnFromTo f s c x + f x) / 2) - fun x ↦ (variationOnFromTo f s c x - f x) / 2

pp: case inr.refine_4
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ ∀ x ∈ s,
    ∀ y ∈ s,
      (fun x ↦ (variationOnFromTo f s c x + f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x + f x) / 2) x +
          ((fun x ↦ (variationOnFromTo f s c x - f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x - f x) / 2) x) =
        variationOnFromTo f s x y

Tactic:
· ext
    simp
    ring

Goal state after:
case inr.refine_4
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ ∀ x ∈ s,
    ∀ y ∈ s,
      (fun x ↦ (variationOnFromTo f s c x + f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x + f x) / 2) x +
          ((fun x ↦ (variationOnFromTo f s c x - f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x - f x) / 2) x) =
        variationOnFromTo f s x y
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: α : Type u_2
inst✝⁷ : LinearOrder α
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
𝕜 : Type u_6
f : α → 𝕜
g : α → F
inst✝⁴ : NormedRing 𝕜
inst✝³ : NormedAlgebra ℝ 𝕜
inst✝² : Module 𝕜 F
inst✝¹ : NormSMulClass 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
C D : ℝ≥0∞
s : Set α
hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C
hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D
⊢ ‖ContinuousLinearMap.lsmul ℝ 𝕜‖ₑ * (C * eVariationOn g s + D * eVariationOn f s) ≤
    C * eVariationOn g s + D * eVariationOn f s

Tactic:
ContinuousLinearMap.opENorm_lsmul_le,

Goal state after:
α : Type u_2
inst✝⁷ : LinearOrder α
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
𝕜 : Type u_6
f : α → 𝕜
g : α → F
inst✝⁴ : NormedRing 𝕜
inst✝³ : NormedAlgebra ℝ 𝕜
inst✝² : Module 𝕜 F
inst✝¹ : NormSMulClass 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
C D : ℝ≥0∞
s : Set α
hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C
hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D
⊢ 1 * (C * eVariationOn g s + D * eVariationOn f s) ≤ C * eVariationOn g s + D * eVariationOn f s
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
h : LocallyBoundedVariationOn f univ
x : ℝ
hx : x ∈ univ → DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ f x

Tactic:
exact hx (mem_univ _)

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ρ : ρ ≪ μ
A : (μ.withDensity (v.limRatioMeas hρ)).rnDeriv μ =ᵐ[μ] v.limRatioMeas hρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))

Tactic:
rw [v.withDensity_limRatioMeas_eq hρ] at A

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : ρ.rnDeriv μ =ᵐ[μ] v.limRatioMeas hρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
this : ∀ (a b : α), a ≤ b → eVariationOn f {a, b} = edist (f a) (f b)
hab : ¬a ≤ b
⊢ eVariationOn f {a, b} = edist (f a) (f b)

pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
⊢ eVariationOn f {a, b} = edist (f a) (f b)

Tactic:
· simpa [edist_comm, pair_comm] using this b a (le_of_not_ge hab)

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
⊢ eVariationOn f {a, b} = edist (f a) (f b)
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 μ
s : Set α
hs : MeasurableSet s
this : IsLocallyFiniteMeasure (μ.restrict s)
⊢ ∀ (a : α),
    Tendsto (fun a ↦ (μ.restrict s) a / μ a) (v.filterAt a) (𝓝 ((μ.restrict s).rnDeriv μ a)) →
      (μ.restrict s).rnDeriv μ a = s.indicator 1 a →
        Tendsto (fun a ↦ μ (s ∩ a) / μ a) (v.filterAt a) (𝓝 (s.indicator 1 a))

Tactic:
intro x hx h'x

Goal state after:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
hs : MeasurableSet s
this : IsLocallyFiniteMeasure (μ.restrict s)
x : α
hx : Tendsto (fun a ↦ (μ.restrict s) a / μ a) (v.filterAt x) (𝓝 ((μ.restrict s).rnDeriv μ x))
h'x : (μ.restrict s).rnDeriv μ x = s.indicator 1 x
⊢ Tendsto (fun a ↦ μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 (s.indicator 1 x))
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
a : A
ha : p a
⊢ cfc (fun x ↦ r) a = (algebraMap R A) r

Tactic:
cfc_apply (fun _ : R ↦ r) a,

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
a : A
ha : p a
⊢ (cfcHom ha) { toFun := (spectrum R a).domRestrict fun x ↦ r, continuous_toFun := ⋯ } = (algebraMap R A) r
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : Semifield R
inst✝⁷ : Semifield S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace S
a : A
f : C(S, R)
h : SpectrumRestricts a ⇑f
h_cpct : CompactSpace ↑(spectrum S a)
⊢ CompactSpace ↑(spectrum R a)

Tactic:
by
  rw [← isCompact_iff_compactSpace] at h_cpct ⊢
  exact h.image ▸ h_cpct.image (map_continuous 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✝¹⁶ : Semifield S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalSemiring S
inst✝¹² : ContinuousStar S
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus S A q
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
⊢ (starAlgHom (cfcHom hqa) h) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a

Tactic:
exact h.starAlgHom_id (cfcHom_id hqa)

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
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) (𝓝[s ∩ Iio x] x) (𝓝 (0 + edist (f x) l))

Tactic:
apply Tendsto.add ?_ tendsto_const_nhds

Goal state after:
α : 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 ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
⊢ Tendsto (fun x_1 ↦ eVariationOn f (s ∩ Ico x_1 x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict

Goal state before:
pp: 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
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
⊢ ∀ (f_1 : C(↑(σₙ R a), R)₀) (x : R), (∃ y, f_1 (Subtype.map ⇑f ⋯ y) = x) ↔ ∃ y, f_1 y = x

Tactic:
exact fun _ _ ↦ ((h a).mp ha).2.homeomorph.exists_congr fun b ↦ Iff.rfl

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
ν n✝ : ℕ
⊢ Polynomial.derivative (bernsteinPolynomial R (n✝ + 1) (ν + 1)) =
    ↑(n✝ + 1) * (bernsteinPolynomial R (n✝ + 1 - 1) ν - bernsteinPolynomial R (n✝ + 1 - 1) (ν + 1))

Tactic:
rw [Nat.cast_succ]; apply derivative_succ_aux

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) ≠ 0

Tactic:
simp only [bernsteinPolynomial.iterate_derivative_at_0, Ne]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (↑(n - (ν - 1))) (ascPochhammer R ν) = 0
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: case mp
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
⊢ f ∈ polynomialFunctions (Set.Icc a b)

Tactic:
refine ⟨q, ⟨?_, ?_⟩⟩

Goal state after:
case mp.refine_1
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
⊢ q ∈ ↑⊤.toSubsemiring

case mp.refine_2
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
⊢ ↑(toContinuousMapOnAlgHom (Set.Icc a b)) q = f
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ (-1) ^ (n - ν) * eval (↑(n - (n - ν - 1))) (ascPochhammer R (n - ν)) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (ascPochhammer R (n - ν))

Tactic:
· norm_cast
    congr
    lia

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

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

Tactic:
refine ⟨q, ⟨?_, ?_⟩⟩

Goal state after:
case mpr.refine_1
a b : ℝ
h : a < b
p : ℝ[X]
q : ℝ[X] := p.comp ((b - a) • X + Polynomial.C a)
⊢ q ∈ ↑⊤.toSubsemiring

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)
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
⊢ σₙ R 0 = {0}

Tactic:
by
  refine Set.eq_singleton_iff_unique_mem.mpr ⟨quasispectrum.zero_mem R 0, fun x hx ↦ ?_⟩
  rw [← cfcₙ_zero R (0 : A),
    cfcₙ_map_quasispectrum _ _ (by cfc_cont_tac) (by cfc_zero_tac) (cfcₙ_predicate_zero R)] at hx
  simp_all

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

Goal state before:
pp: case h
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x ↦ f ↑x, continuous_toFun := ⋯ }
p : ℝ[X]
b : ∀ (x : ↑(Set.Icc a b✝)), ‖(p.toContinuousMapOn (Set.Icc a b✝) - f') x‖ < ε
⊢ ∀ x ∈ Set.Icc a b✝, |Polynomial.eval x p - f x| < ε

Tactic:
intro x m

Goal state after:
case h
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x ↦ f ↑x, continuous_toFun := ⋯ }
p : ℝ[X]
b : ∀ (x : ↑(Set.Icc a b✝)), ‖(p.toContinuousMapOn (Set.Icc a b✝) - f') x‖ < ε
x : ℝ
m : x ∈ Set.Icc a b✝
⊢ |Polynomial.eval x p - f x| < ε
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
a✝ : X
⊢ ((g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound) a✝ = ↑((Polynomial.aeval f) g) a✝

Tactic:
simp only [Polynomial.aeval_subalgebra_coe, Polynomial.aeval_continuousMap_apply]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
a✝ : X
⊢ ((g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound) a✝ = Polynomial.eval (↑f a✝) g
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))
        (Filter.comap (Prod.map (fun x ↦ x.comp f) fun x ↦ x.comp f) (𝓤 C(↑(spectrum R a), R))) ⊓
      Filter.comap (fun x ↦ (↑x.1, ↑x.2)) (Filter.comap (Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) (𝓤 C(Unit, R)))

Tactic:
Filter.comap_comap

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 ((Prod.map (fun x ↦ x.comp f) fun x ↦ x.comp f) ∘ fun x ↦ (↑x.1, ↑x.2)) (𝓤 C(↑(spectrum R a), R)) ⊓
      Filter.comap ((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (𝓤 C(Unit, R))
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
⊢ Continuous toNNReal

Tactic:
rw [continuous_induced_rng]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
⊢ Continuous (_root_.toContinuousMap ∘ toNNReal)