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 μ
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 μ
⊢ ‖∫ (y : α), f y ∂(μ a)⁻¹ • μ.restrict a - ∫ (x_1 : α), f x ∂(μ a)⁻¹ • μ.restrict a‖ ≤
    ∫ (y : α), ‖f y - f x‖ ∂(μ a)⁻¹ • μ.restrict a

Tactic:
← integral_sub

Goal state after:
α : 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 μ
⊢ ‖∫ (a : α), f a - f x ∂(μ a)⁻¹ • μ.restrict a‖ ≤ ∫ (y : α), ‖f y - f x‖ ∂(μ a)⁻¹ • μ.restrict a

case hf
α : 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 f ((μ a)⁻¹ • μ.restrict a)

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)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case C
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
hf : ContinuousOn f (spectrum R a)
r : R
⊢ cfc (fun x ↦ Polynomial.eval (f x) (Polynomial.C r)) a = (aeval (cfc f a)) (Polynomial.C r)

Tactic:
| C r =>

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
q : R[X]
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ cfc (fun x ↦ Polynomial.eval (f x) q) a = (aeval (cfc f a)) q

Tactic:
by
  induction q using Polynomial.induction_on with
  | C r => simp [cfc_const r a]
  | add q₁ q₂ hq₁ hq₂ =>
    simp only [eval_add, map_add, ← hq₁, ← hq₂, cfc_add a (q₁.eval <| f ·) (q₂.eval <| f ·)]
  | monomial n r _ =>
    simp only [eval_mul, eval_C, eval_X_pow, map_mul, aeval_C, map_pow, aeval_X]
    rw [cfc_const_mul .., cfc_pow _ (n + 1) _, ← smul_eq_mul, algebraMap_smul]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
⊢ p a

Tactic:
by exact ha

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 α
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
H : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))
⊢ (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) =ᶠ[𝓝[s ∩ Iio x] x] fun y ↦ eVariationOn f (s ∩ Icc y x)

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy

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
H : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))
y : α
hy : y ∈ s ∩ Iio x
⊢ eVariationOn f (s ∩ Ico y x) + edist (f x) l = eVariationOn f (s ∩ Icc y x)
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 = ⊥
this : s = s ∩ Iio x ∪ s ∩ Ici x
⊢ (fun x ↦ 0) =ᶠ[𝓝[s ∩ Ici x] x] fun y ↦ eVariationOn f (s ∩ Icc y x)

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy

Goal state after:
α : 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 = ⊥
this : s = s ∩ Iio x ∪ s ∩ Ici x
y : α
hy : y ∈ s ∩ Ici x
⊢ 0 = eVariationOn f (s ∩ Icc y x)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

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✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
n : ℕ
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfcUnits f a hf' hf ha ^ n = cfcUnits (fun i ↦ f i ^ n) a ⋯ ⋯ ha

Tactic:
ext
  cases n with
  | zero => simp [cfc_const_one R a]
  | succ n => simp [cfc_pow f _ a]

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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a)) (h0 : { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯ } 0 = 0) (ha : p a),
    P ((cfcₙHom ha) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := h0 })
h : ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a
⊢ P (cfcₙ f a)

Tactic:
cfcₙ_apply f a h.1 h.2.1 h.2.2

Goal state after:
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a)) (h0 : { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯ } 0 = 0) (ha : p a),
    P ((cfcₙHom ha) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := h0 })
h : ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a
⊢ P ((cfcₙHom ⋯) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ })
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a)) (h0 : { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯ } 0 = 0) (ha : p a),
    P ((cfcₙHom ha) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := h0 })
h : ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a
⊢ P (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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a)) (h0 : { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯ } 0 = 0) (ha : p a),
    P ((cfcₙHom ha) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := h0 })
h : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a)
⊢ P (cfcₙ f a)

Tactic:
· rw [cfcₙ_apply f a h.1 h.2.1 h.2.2]
    exact haf h.1 h.2.1 h.2.2

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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a)) (h0 : { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯ } 0 = 0) (ha : p a),
    P ((cfcₙHom ha) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := h0 })
h : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a)
⊢ P (cfcₙ f a)
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
f g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
⊢ cfcₙ f a = cfcₙ g a

Tactic:
by_cases h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0

Goal state after:
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 g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0
⊢ cfcₙ f a = cfcₙ g a

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 g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
h : ¬(p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0)
⊢ cfcₙ f a = cfcₙ g a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg.inr.inr.hf
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 g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
h0 : ¬g 0 = 0
⊢ ¬f 0 = 0

Tactic:
exact fun hf ↦ h0 (hfg (quasispectrum.zero_mem R a) ▸ hf)

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
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
⊢ p a

Tactic:
by exact ha

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
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
⊢ σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a

Tactic:
cfcₙHom_map_quasispectrum (by exact ha) _

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
inst✝ : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
⊢ Set.range ⇑{ toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 } = f '' σₙ R a
Module: Mathlib.RingTheory.Polynomial.Bernstein

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

Tactic:
simp only [← add_mul]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ x ∈ Finset.range (n + 1), (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

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

Tactic:
refine ⟨k.1, ?_, k.2⟩

Goal state after:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := fun x ↦ {z | ↑(h x) z < f z + ε}
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯.choose
xs_w : ⋃ x ∈ xs, W x = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhds)
xs_nonempty : xs.Nonempty
k : ↑L := ⟨xs.inf' xs_nonempty fun x ↦ ↑(h x), ⋯⟩
⊢ dist (↑k) f < ε
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: case inr
𝕜 : 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
φ : ↑(characterSpace 𝕜 A)
h₁ : φ 1 * (1 - φ 1) = 0
h₂ : 1 - φ 1 = 0
⊢ φ 1 = 1

Tactic:
· exact (sub_eq_zero.mp h₂).symm

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁴ : CommSemiring 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✝¹⁵ : Ring B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Algebra R B
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : ContinuousFunctionalCalculus R A p
inst✝⁴ : ContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMap.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst✝¹⁷, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
⊢ φ (cfc f a) = cfc f (φ a)

Tactic:
let ψ : A →⋆ₐ[R] B := (φ : A →⋆ₐ[S] B).restrictScalars R
  have : Continuous ψ := hφ
  have h_spec := AlgHom.spectrum_apply_subset ψ a
  have hψa : q (ψ a) := hφa
  let ι : C(spectrum R (ψ a), spectrum R a) :=
    ⟨Set.inclusion h_spec, continuous_id.subtype_map h_spec⟩
  suffices ψ.comp (cfcHom ha) = (cfcHom hψa).comp (ContinuousMap.compStarAlgHom' R R ι) by
    have hf' : ContinuousOn f (spectrum R (ψ a)) := hf.mono h_spec
    rw [cfc_apply .., cfc_apply ..]
    congrm($(this) ⟨_, hf.domRestrict⟩)
  refine ContinuousMap.UniqueHom.eq_of_continuous_of_map_id _ _ _ ?_ ?_ ?apply_id
  case apply_id =>
    trans cfcHom hψa (.restrict (spectrum R (ψ a)) (.id R))
    · simp [cfcHom_id]
    · congr
  all_goals
    dsimp [ContinuousMap.compStarAlgHom']
    fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
⊢ UpperHemicontinuousWithinAt (fun x ↦ {f x}) s x ↔ ContinuousWithinAt f s x

Tactic:
by
  refine ⟨?_, fun hf ↦ upperHemicontinuous_singleton_id.upperHemicontinuousWithinAt _ _ |>.comp hf
    (mapsTo_image _ _)⟩
  simp only [upperHemicontinuousWithinAt_iff, nhdsSet_singleton, ContinuousWithinAt,
    tendsto_iff_forall_eventually_mem]
  intro h t ht
  filter_upwards [h t ht] with x
  exact mem_of_mem_nhds

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
⊢ ∀ (u : Set β), IsOpen[inst✝.toTopologicalSpace] u → (f x₀ ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x₀, (f x' ∩ u).Nonempty

Tactic:
intro V

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 β
⊢ IsOpen[inst✝.toTopologicalSpace] V → (f x₀ ∩ V).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x₀, (f x' ∩ V).Nonempty