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

Goal state before:
pp: case neg.inr
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
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ cfc (fun x ↦ star (f x)) a = star (cfc f a)

Tactic:
rw [cfc_apply_of_not_continuousOn a hf, cfc_apply_of_not_continuousOn, star_zero]

Goal state after:
case neg.inr.hf
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
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ ¬ContinuousOn (fun x ↦ star (f x)) (spectrum R a)
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
a : A
ha : p a
⊢ cfc (fun x ↦ star x) a = star a

Tactic:
by
  rw [cfc_star .., cfc_id' ..]

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

Goal state before:
pp: case negSucc
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
hf : ContinuousOn f (spectrum R a)
ha : p a
n : ℕ
⊢ cfcUnits f a hf' hf ha ^ Int.negSucc n = cfcUnits (f ^ Int.negSucc n) a ⋯ ⋯ ha

Tactic:
simp only [zpow_negSucc, ← inv_pow]
    ext
    exact cfc_pow (hf := hf.inv₀ hf') .. |>.symm

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✝¹¹ : 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
inst✝ : UniqueHom R A
f : R → R
n : ℤ
a : Aˣ
hf : ContinuousOn f ((fun x ↦ x ^ n) '' spectrum R ↑a)
ha : p ↑a
⊢ cfc f (cfc (fun x ↦ x ^ n) ↑a) = cfc f ↑(a ^ n)

Tactic:
cfc_zpow a

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✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousInv₀ R
inst✝ : UniqueHom R A
f : R → R
n : ℤ
a : Aˣ
hf : ContinuousOn f ((fun x ↦ x ^ n) '' spectrum R ↑a)
ha : p ↑a
⊢ cfc f ↑(a ^ n) = cfc f ↑(a ^ n)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
inst✝ : UniqueHom R A
f : C(↑(σₙ R a), R)₀
f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀
hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)
g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀
ψ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] C(↑(σₙ R a), R)₀ :=
  { toFun := fun x ↦ x.comp f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ
⊢ Continuous[_, inst✝⁴] ⇑φ

Tactic:
refine (cfcₙHom_continuous ha).comp <| continuous_induced_rng.mpr ?_
    exact f'.toContinuousMap.continuous_precomp.comp continuous_induced_dom

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

Goal state before:
pp: case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ 0 = -0

pp: case neg.inr.hf
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ ¬ContinuousOn (fun x ↦ -f x) (spectrum R a)

Tactic:
neg_zero

Goal state after:
case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ 0 = 0

case neg.inr.hf
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ ¬ContinuousOn (fun x ↦ -f x) (spectrum R a)
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
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts a ⇑f
g : R → R
hg : ¬g 0 = 0
⊢ ¬(algebraMap R S) (g (f 0)) = 0

Tactic:
by simpa [h.map_zero]

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

Goal state before:
pp: case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
ha : p a
⊢ cfcₙ (fun x ↦ f x * g x) a =
    (cfcₙHom ha)
      ({ toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ } *
        { toFun := (σₙ R a).domRestrict g, continuous_toFun := ⋯, map_zero' := ⋯ })

Tactic:
cfcₙ_apply _ a

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

Tactic:
cfcₙ_apply _ a

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
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
ha : p a
⊢ (cfcₙHom ha) { toFun := (σₙ R a).domRestrict fun x ↦ f x + g x, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ha) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ } +
      (cfcₙHom ha) { toFun := (σₙ R a).domRestrict g, 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
S : Type u_3
inst✝⁴ : SMulZeroClass S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ cfcₙ (fun x ↦ s • f x) a = s • (cfcₙHom ha) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ }

Tactic:
cfcₙ_apply _ a

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
S : Type u_3
inst✝⁴ : SMulZeroClass S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ (cfcₙHom ha) { toFun := (σₙ R a).domRestrict fun x ↦ s • f x, continuous_toFun := ⋯, map_zero' := ⋯ } =
    s • (cfcₙHom ha) { 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
f : R → R
a : A
ha : p a
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
⊢ cfcₙ (fun x ↦ star (f x)) a =
    (cfcₙHom ha) (star { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ })

Tactic:
cfcₙ_apply _ a

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 : R → R
a : A
ha : p a
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
⊢ (cfcₙHom ha) { toFun := (σₙ R a).domRestrict fun x ↦ star (f x), continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ha) (star { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ })
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg.inr.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
⊢ 0 = -0

pp: case neg.inr.inl.hf
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
⊢ ¬ContinuousOn (fun x ↦ -f x) (σₙ R a)

Tactic:
neg_zero

Goal state after:
case neg.inr.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
⊢ 0 = 0

case neg.inr.inl.hf
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
⊢ ¬ContinuousOn (fun x ↦ -f x) (σₙ R a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg.inr.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h0 : ¬f 0 = 0
⊢ 0 = -0

pp: case neg.inr.inr.hf
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h0 : ¬f 0 = 0
⊢ ¬-f 0 = 0

Tactic:
neg_zero

Goal state after:
case neg.inr.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h0 : ¬f 0 = 0
⊢ 0 = 0

case neg.inr.inr.hf
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h0 : ¬f 0 = 0
⊢ ¬-f 0 = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case e'_2.e'_3
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
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
u v : C(↑(σₙ R a), R)₀
⊢ (((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (u, v)).1 PUnit.unit = 0 PUnit.unit

Tactic:
exact map_zero u

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✝¹⁰ : 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
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
⊢ cfcₙ f a = cfc f a

Tactic:
have hf' := hf.mono <| spectrum_subset_quasispectrum R a
    rw [cfc_apply f a ha hf', cfcₙ_apply f a hf, cfcₙHom_eq_cfcₙHom_of_cfcHom, cfcₙHom_of_cfcHom]
    dsimp only [NonUnitalStarAlgHom.comp_apply,
      NonUnitalStarAlgHom.coe_coe, compStarAlgHom'_apply]
    congr

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case refine_3.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ k • a⋆ ∈ Metric.closedBall 0 1

pp: case refine_3.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r < (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) (k • a⋆)

Tactic:
· simpa only [mem_closedBall_zero_iff, norm_smul, one_mul, norm_star] using!
          (NNReal.le_inv_iff_mul_le ha.ne').1 (one_mul ‖a‖₊⁻¹ ▸ hk₂.le : ‖k‖₊ ≤ ‖a‖₊⁻¹)

Goal state after:
case refine_3.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r < (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) (k • a⋆)
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case refine_2
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst✝¹³ : CommRing K
inst✝¹² : Ring A
inst✝¹¹ : Algebra K A
inst✝¹⁰ : TopologicalSpace K
inst✝⁹ : T1Space K
inst✝⁸ : TopologicalSpace A
inst✝⁷ : ContinuousSub A
inst✝⁶ : ContinuousSMul K A
inst✝⁵ : FunLike F A K
inst✝⁴ : AlgHomClass F K A K
inst✝³ : SetLike S A
inst✝² : OneMemClass S A
inst✝¹ : AddSubgroupClass S A
inst✝ : SMulMemClass S K A
φ : F
hφ : Continuous[inst✝⁸, inst✝¹⁰] ⇑φ
s : S
x : A
hxs : x ∈ closure[inst✝⁸] ↑s
hxφ : φ x = 0
⊢ x ∈ closure[inst✝⁸] (↑s ∩ ↑(RingHom.ker φ))

Tactic:
rw [mem_closure_iff_clusterPt, ClusterPt] at hxs

Goal state after:
case refine_2
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst✝¹³ : CommRing K
inst✝¹² : Ring A
inst✝¹¹ : Algebra K A
inst✝¹⁰ : TopologicalSpace K
inst✝⁹ : T1Space K
inst✝⁸ : TopologicalSpace A
inst✝⁷ : ContinuousSub A
inst✝⁶ : ContinuousSMul K A
inst✝⁵ : FunLike F A K
inst✝⁴ : AlgHomClass F K A K
inst✝³ : SetLike S A
inst✝² : OneMemClass S A
inst✝¹ : AddSubgroupClass S A
inst✝ : SMulMemClass S K A
φ : F
hφ : Continuous[inst✝⁸, inst✝¹⁰] ⇑φ
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 ↑s).NeBot
hxφ : φ x = 0
⊢ x ∈ closure[inst✝⁸] (↑s ∩ ↑(RingHom.ker φ))
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:
simp only [upperHemicontinuousWithinAt_iff, nhdsSet_singleton, ContinuousWithinAt,
    tendsto_iff_forall_eventually_mem]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
⊢ (∀ t ∈ 𝓝 (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝 (f x')) → ∀ s_1 ∈ 𝓝 (f x), ∀ᶠ (x : α) in 𝓝[s] x, f x ∈ s_1
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst✝¹] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
⊢ (f x₀ ∩ t).Nonempty

Tactic:
obtain ⟨x, hx, hfx⟩ := exists_seq_forall_of_frequently hft

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst✝¹] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
hfx : ∀ (n : ℕ), (f (x n) ∩ t).Nonempty
⊢ (f x₀ ∩ t).Nonempty