mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case pos
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 g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : p a ∧ ContinuousOn g (spectrum R a)
⊢ cfc f a = cfc g a

pp: case neg
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 g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : ¬(p a ∧ ContinuousOn g (spectrum R a))
⊢ cfc f a = cfc g a

Tactic:
· rw [cfc_apply (ha := h.1) (hf := h.2.congr hfg), cfc_apply (ha := h.1) (hf := h.2)]
    congr 2
    exact Set.domRestrict_eq_iff.mpr hfg

Goal state after:
case neg
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 g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : ¬(p a ∧ ContinuousOn g (spectrum R a))
⊢ cfc f a = cfc g a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict

Goal state before:
pp: case pos
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)
halg : IsClosedEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
g : R → R
hg : ContinuousOn g (spectrum R a)
⊢ cfc g a = cfc (fun x ↦ (algebraMap R S) (g (f x))) a

Tactic:
rw [cfc_apply g a, cfcHom_eq_restrict f hpa hqa h, SpectrumRestricts.starAlgHom_apply,
      cfcHom_eq_cfc_extend 0]

Goal state after:
case pos
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)
halg : IsClosedEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
g : R → R
hg : ContinuousOn g (spectrum R a)
⊢ cfc
      (Function.extend Subtype.val
        (⇑({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
            ({ toFun := (spectrum R a).domRestrict g, continuous_toFun := ⋯ }.comp
              { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ })))
        0)
      a =
    cfc (fun x ↦ (algebraMap R S) (g (f x))) a
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 g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
⊢ Continuous[Pi.topologicalSpace, _] fun v ↦ ∑ i ∈ Finset.range n, edist (v (i + 1)) (v i)

Tactic:
fun_prop

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 g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this✝ : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this : ∀ᶠ (b : ℕ → E) in Filter.pi fun i ↦ 𝓝 (g (u i)), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : ℕ → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi t ⊆ {b | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
i : ℕ × ℕ
hi : i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}
⊢ Continuous[Pi.topologicalSpace, inst✝¹] fun x ↦ x i.1

Tactic:
fun_prop

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 g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this✝ : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this : ∀ᶠ (b : ℕ → E) in Filter.pi fun i ↦ 𝓝 (g (u i)), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : ℕ → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi t ⊆ {b | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
i : ℕ × ℕ
hi : i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}
⊢ Continuous[Pi.topologicalSpace, inst✝¹] fun x ↦ x i.2

Tactic:
fun_prop

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
f : R → R
a : A
ha : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
      (cfcₙHom ⋯) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ }
    else 0) =
    0

Tactic:
dif_neg 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
f : R → R
a : A
ha : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ 0 = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case mpr
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
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
f : C(↑(spectrum R a), R)
⊢ 0 ≤ f → 0 ≤ (cfcHom ha) f

Tactic:
· simpa using (cfcHom_mono ha (f := 0) (g := f) ·)

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
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
⊢ ContinuousOn id (spectrum R a)

Tactic:
fun_prop

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

Goal state before:
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
ha : p a
f_cont : ContinuousOn f (σₙ R a)
f_zero : ¬f 0 = 0
⊢ cfcₙ f a = (cfcₙHom ha) (mkD ((σₙ R a).domRestrict f) 0)

Tactic:
· rw [cfcₙ_apply_of_not_map_zero a f_zero, mkD_of_not_zero, map_zero]
      exact f_zero

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n k ν : ℕ
⊢ k < ν + 1 → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0

Tactic:
rw [Nat.lt_succ_iff]
    induction k generalizing n ν with
    | zero => simp [eval_at_0]
    | succ k ih =>
      simp only [derivative_succ, Function.comp_apply,
        Function.iterate_succ, Polynomial.iterate_derivative_sub,
        Polynomial.iterate_derivative_natCast_mul, Polynomial.eval_mul, Polynomial.eval_natCast,
        Polynomial.eval_sub]
      intro h
      apply mul_eq_zero_of_right
      rw [ih _ _ (Nat.le_of_succ_le h), sub_zero]
      convert! ih _ _ (Nat.pred_le_pred h)
      exact (Nat.succ_pred_eq_of_pos (k.succ_pos.trans_le h)).symm

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

Goal state before:
pp: case pos.succ
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
⊢ eval 0 ((⇑derivative)^[ν + 1] (bernsteinPolynomial R n (ν + 1))) = eval (↑(n - (ν + 1 - 1))) (ascPochhammer R (ν + 1))

Tactic:
have h' : ν ≤ n - 1 := le_tsub_of_add_le_right h

Goal state after:
case pos.succ
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
⊢ eval 0 ((⇑derivative)^[ν + 1] (bernsteinPolynomial R n (ν + 1))) = eval (↑(n - (ν + 1 - 1))) (ascPochhammer R (ν + 1))
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
p : R[X]
⊢ Continuous fun x ↦ eval x p

Tactic:
fun_prop

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
p : R[X]
X : Set R
⊢ Continuous fun x ↦ p.toContinuousMap ↑x

Tactic:
fun_prop

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✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : ContinuousSqrt R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NoZeroDivisors R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
⊢ ContinuousOn id (σₙ R a)

Tactic:
fun_prop

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
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
⊢ Continuous fun x ↦
    match x with
    | (x, y) => gauge U (f x - f y)

Tactic:
fun_prop

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✝⁹ : 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
⊢ Continuous ⇑↑toContinuousMapHom.toNonUnitalAlgHom

Tactic:
fun_prop

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 = 0

Tactic:
show x = 0 from Subtype.val_injective hx,

Goal state after:
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 0 = 0
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case refine_1.hf
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 := ⋯
x y : X
⊢ Continuous[inst✝¹, _] fun b ↦ f b - ε

Tactic:
fun_prop

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

Goal state before:
pp: case refine_1.hg
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 := ⋯
x y : X
⊢ Continuous[inst✝¹, _] ⇑(g x y)

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u_1
inst✝⁵ : TopologicalSpace X
A : Type u_2
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst✝¹] ⇑φ
⊢ Continuous[_, inst✝¹] fun f ↦ φ f.toNNReal - φ (-f).toNNReal

Tactic:
fun_prop

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

Goal state before:
pp: case refine_1.hf
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 := ⋯
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := ⋯
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := ⋯
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := ⋯
x : X
⊢ Continuous[inst✝¹, _] ⇑↑(h x)

Tactic:
fun_prop

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

Goal state before:
pp: case refine_1.hg
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 := ⋯
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := ⋯
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := ⋯
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := ⋯
x : X
⊢ Continuous[inst✝¹, _] fun b ↦ f b + ε

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝¹] ⇑φ
⊢ Continuous[_, inst✝¹] fun f ↦ φ f.toNNReal - φ (-f).toNNReal

Tactic:
fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f ↦ ⇑f) f x₁ ≠ (fun f ↦ ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
hFA : F ∈ A
⊢ Continuous fun x ↦ ‖F x‖ ^ 2

Tactic:
fun_prop

Goal state after:
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
⊢ A.topologicalClosure = ⊤

Tactic:
by
  rw [StarSubalgebra.eq_top_iff]
  -- Let `I` be the natural inclusion of `C(X, ℝ)` into `C(X, 𝕜)`
  let I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ofRealCLM.compLeftContinuous ℝ X
  -- The main point of the proof is that its range (i.e., every real-valued function) is contained
  -- in the closure of `A`
  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₂)
  -- In particular, for a function `f` in `C(X, 𝕜)`, the real and imaginary parts of `f` are in the
  -- closure of `A`
  intro f
  let f_re : C(X, ℝ) := (⟨RCLike.re, RCLike.reCLM.continuous⟩ : C(𝕜, ℝ)).comp f
  let f_im : C(X, ℝ) := (⟨RCLike.im, RCLike.imCLM.continuous⟩ : C(𝕜, ℝ)).comp f
  have h_f_re : I f_re ∈ A.topologicalClosure := key ⟨f_re, rfl⟩
  have h_f_im : I f_im ∈ A.topologicalClosure := key ⟨f_im, rfl⟩
  -- So `f_re + I • f_im` is in the closure of `A`
  have := A.topologicalClosure.add_mem h_f_re (A.topologicalClosure.smul_mem h_f_im RCLike.I)
  rw [StarSubalgebra.mem_toSubalgebra] at this
  convert! this
  -- And this, of course, is just `f`
  ext
  apply Eq.symm
  simp [I, f_re, f_im, mul_comm RCLike.I _]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
f : F
⊢ Continuous[instTopologicalSpace B, inst✝⁷] (B.flip f).toFun

Tactic:
fun_prop

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, 𝕜)
h : ∀ f ∈ (polynomialFunctions s).starClosure, p f
f : C(↑s, 𝕜)
this : f ∈ ↑(polynomialFunctions s).starClosure.topologicalClosure
⊢ ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g

Tactic:
topologicalClosure_coe,

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, 𝕜)
this : f ∈ closure ↑(polynomialFunctions s).starClosure
⊢ ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: case refine_1
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✝²⁸ : Nontrivial R
inst✝²⁷ : StarRing R
inst✝²⁶ : MetricSpace R
inst✝²⁵ : IsTopologicalSemiring R
inst✝²⁴ : ContinuousStar R
inst✝²³ : CommRing S
inst✝²² : Algebra R S
inst✝²¹ : NonUnitalRing A
inst✝²⁰ : StarRing A
inst✝¹⁹ : TopologicalSpace A
inst✝¹⁸ : Module R A
inst✝¹⁷ : IsScalarTower R A A
inst✝¹⁶ : SMulCommClass R A A
inst✝¹⁵ : NonUnitalRing B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Module R B
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : SMulCommClass R B B
inst✝⁹ : Module S A
inst✝⁸ : Module S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus R A p
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMapZero.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst✝¹⁹, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R ↑φ
this : Continuous[inst✝¹⁹, inst✝¹³] ⇑ψ
h_spec : quasispectrum R (φ a) ⊆ quasispectrum R a
hψa : q (ψ a)
ι : C(↑(quasispectrum R (ψ a)), ↑(quasispectrum R a))₀ :=
  { toFun := Set.inclusion h_spec, continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Continuous[_, inst✝¹³] (⇑ψ ∘ ⇑(cfcₙHom ha))

Tactic:
fun_prop

Goal state after: