mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: A : Type u_4
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : ↑‖x‖₊ = spectralRadius ℝ a
⊢ (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a

Tactic:
simp only [← hx₂, ENNReal.coe_toReal, coe_nnnorm, Real.norm_eq_abs]

Goal state after:
A : Type u_4
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : ↑‖x‖₊ = spectralRadius ℝ a
⊢ |x| ∈ spectrum ℝ a ∨ -|x| ∈ spectrum ℝ a
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})
⊢ IsConnected (σ ℂ a)ᶜ

Tactic:
rw [← Set.inter_union_distrib_left, ← Set.ofPred_or] at this
    rw [← Set.inter_univ (σ ℂ a)ᶜ]
    convert this
    exact Eq.symm <| Set.eq_univ_of_forall (fun z ↦ le_total 0 z.im)

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
x : 𝕜
hx : x ∈ σₙ 𝕜 a
⊢ x = 0 ∨ x ∈ σ 𝕜 a

Tactic:
simpa [quasispectrum_eq_spectrum_union_zero] using hx

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : EquivLike F A B
inst✝¹ : NonUnitalAlgEquivClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
⊢ ‖a‖₊ ≤ ‖φ a‖₊

Tactic:
by
    simpa using! NonUnitalStarAlgHom.nnnorm_apply_le (symm (φ : A ≃⋆ₐ[ℂ] B)) ((φ : A ≃⋆ₐ[ℂ] B) a)

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : IsTopologicalBasis b
⊢ SecondCountableTopology (Compacts α)

Tactic:
exact hb₂.compacts.secondCountableTopology <| (countable_ofPred_finite_subset hb₁).image _

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ selfAdjoint.expUnitary (a + b) = selfAdjoint.expUnitary b * selfAdjoint.expUnitary a

Tactic:
← h.symm.expUnitary_add,

Goal state after:
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ selfAdjoint.expUnitary (a + b) = selfAdjoint.expUnitary (b + a)
Module: Mathlib.Analysis.LocallyConvex.Polar

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ (B.polar s).Nonempty

Tactic:
by
  use 0
  exact zero_mem_polar B s

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

Goal state before:
pp: A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a b x : A
ha : IsStarNormal a
hb : IsStarNormal b
h : SemiconjBy x a b
⊢ SemiconjBy x (star a) (star b)

Tactic:
apply Unitization.inr_injective (R := ℂ)
  simp only [Unitization.inr_mul, Unitization.inr_star]
  apply SemiconjBy.star_right_of_unital
  simpa [SemiconjBy] using mod_cast h.eq

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : LocallyConvexSpace 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : FirstCountableTopology E
u : ℕ → Set E
hu_basis : (𝓝 0).HasAntitoneBasis u
hu_zero : ∀ (n : ℕ), 0 ∈ interior (u n)
v : ℕ → Set E := fun n ↦ (absConvexHull 𝕜) (interior (u n))
hv_open : ∀ (n : ℕ), IsOpen[inst✝⁵] (v n)
hv_nhds : ∀ (n : ℕ), v n ∈ 𝓝 0
n : ℕ
a✝ : True
W : Set E
hWn : id W ⊆ u ?m.227
hW_nhds : W ∈ 𝓝 0
hW_abs : AbsConvex 𝕜 W
m : ℕ
hm : u m ⊆ W
⊢ ∃ i', True ∧ v i' ⊆ u n

Tactic:
exact ⟨m, trivial, (absConvexHull_min (interior_subset.trans hm) hW_abs).trans hWn⟩

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Barrelled

Goal state before:
pp: ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜₁ E
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : UniformSpace E
inst✝⁴ : UniformSpace F
inst✝³ : IsUniformAddGroup E
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i ↦ (q k) ((𝓕 i) x))
k : κ
this : BddAbove (range fun i ↦ (q k).comp ↑(𝓕 i))
⊢ BddAbove (range fun k_1 ↦ (q k).comp ((toLinearMap ∘ 𝓕) k_1)) ∧
    Continuous[inst✝⁵.toTopologicalSpace, _] (⨆ k_1, ⇑((q k).comp ((toLinearMap ∘ 𝓕) k_1)))

Tactic:
exact ⟨this, Seminorm.continuous_iSup _
    (fun i ↦ (hq.continuous_seminorm k).comp (𝓕 i).continuous) this⟩

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
hx : x ∉ c.U
⊢ approx n c x = 1

Tactic:
by
  induction n generalizing c with
  | zero =>
    rw [← mem_compl_iff] at hx
    exact indicator_of_mem hx _
  | succ n ihn =>
    simp only [approx]
    rw [ihn, ihn, midpoint_self]
    exacts [hx, fun hU => hx <| c.left_U_subset hU]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
⊢ approx n c x ≤ approx (n + 1) c x

Tactic:
by
  induction n generalizing c with
  | zero =>
    simp only [approx, right_U, right_le_midpoint]
    exact (approx_mem_Icc_right_left c 0 x).2
  | succ n ihn =>
    rw [approx, approx]
    exact midpoint_le_midpoint (ihn _) (ihn _)

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : LinearOrder k
inst✝⁵ : IsStrictOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b : E
r r' : k
h : a < b
⊢ r • (b - a) < r' • (b - a) ↔ r < r'

Tactic:
smul_lt_smul_iff_of_pos_right (sub_pos.mpr h)

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : LinearOrder k
inst✝⁵ : IsStrictOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b : E
r r' : k
h : a < b
⊢ r < r' ↔ r < r'
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst✝²] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst✝², _] f
hfs : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 0 s
hft : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 1 (interior k)ᶜ
h'f : ∀ (x : X), { toFun := f, continuous_toFun := hf } x ∈ Icc 0 1
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∈ t
⊢ { toFun := fun x ↦ 1 - f x, continuous_toFun := ⋯ } x = 0 x

Tactic:
by simpa [sub_eq_zero] using (hft (A hx)).symm

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : ℕ → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s
fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)
f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : ∑' (i : ℕ), u i = 1
g : X → ℝ := fun x ↦ ∑' (n : ℕ), u n * (f n) x
hgmc : EqOn g 0 mᶜ
I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n
S : ∀ (x : X), Summable fun n ↦ u n * (f n) x
⊢ Continuous[inst✝², _] g

Tactic:
apply continuous_tsum (fun n ↦ by fun_prop) u_sum (fun n x ↦ ?_)
    simpa [abs_of_nonneg, (u_pos n).le, (f_range n x).1] using I n x

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : Module ℝ A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
⊢ a⁺ = b

Tactic:
have : Fact (0 ∈ s) := ⟨by aesop⟩

Goal state after:
A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : Module ℝ A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
⊢ a⁺ = b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : Module ℝ A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
f g : C(↑s, ℝ)₀
⊢ (cfcₙHomSuperset hb' hbs) f * (cfcₙHomSuperset hc' hcs) g = 0

Tactic:
refine f.nonUnitalStarAlgHom_apply_mul_eq_zero _ _ ?id ?star_id
      (cfcₙHomSuperset_continuous hb' hbs)

Goal state after:
case id
A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : Module ℝ A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
f g : C(↑s, ℝ)₀
⊢ (cfcₙHomSuperset hb' hbs) (ContinuousMapZero.id s) * (cfcₙHomSuperset hc' hcs) g = 0

case star_id
A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : Module ℝ A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
f g : C(↑s, ℝ)₀
⊢ (cfcₙHomSuperset hb' hbs) (star (ContinuousMapZero.id s)) * (cfcₙHomSuperset hc' hcs) g = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x y : A
hxy : IsSelfAdjoint (↑y - ↑x) ∧ SpectrumRestricts (↑y - ↑x) ⇑ContinuousMap.realToNNReal
hyx : IsSelfAdjoint (↑x - ↑y) ∧ SpectrumRestricts (↑x - ↑y) ⇑ContinuousMap.realToNNReal
⊢ x = y

Tactic:
rw [← sub_eq_zero]

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x y : A
hxy : IsSelfAdjoint (↑y - ↑x) ∧ SpectrumRestricts (↑y - ↑x) ⇑ContinuousMap.realToNNReal
hyx : IsSelfAdjoint (↑x - ↑y) ∧ SpectrumRestricts (↑x - ↑y) ⇑ContinuousMap.realToNNReal
⊢ x - y = 0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ≥0
ha : ¬0 ≤ a
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
simp [nnrpow_def, cfcₙ_apply_of_not_predicate a ha]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ ContinuousOn g (σₙ ℝ≥0 a)

Tactic:
have (x) (hx : x ∈ σₙ ℝ≥0 a) : 1 - x ≠ 0 := by
          refine tsub_pos_of_lt ?_ |>.ne'
          exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
this : ∀ x ∈ σₙ ℝ≥0 a, 1 - x ≠ 0
⊢ ContinuousOn g (σₙ ℝ≥0 a)
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
r : ℝ
hr : 0 ≤ r
A : Matrix m n α
⊢ ‖A‖ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖ ≤ r

Tactic:
by
  simp_rw [norm_def, pi_norm_le_iff_of_nonneg hr]

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

Goal state before:
pp: case frequently
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f : C(↑s, 𝕜)₀
hf :
  ∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) g
ε : ℝ
hε : 0 < ε
g : C(↑s, 𝕜)₀
g_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) g
hg : ‖f - g‖ ≤ ε
x : X
⊢ ‖(cfcₙHomSuperset ⋯ ⋯) f - (cfcₙHomSuperset ⋯ ⋯) g‖ ≤ ε

Tactic:
rw [← map_sub, cfcₙHomSuperset_apply]

Goal state after:
case frequently
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f : C(↑s, 𝕜)₀
hf :
  ∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) g
ε : ℝ
hε : 0 < ε
g : C(↑s, 𝕜)₀
g_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) g
hg : ‖f - g‖ ≤ ε
x : X
⊢ ‖(cfcₙHom ⋯) ((f - g).comp { toFun := Subtype.map id ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })‖ ≤ ε
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
⊢ Commute ((cfcHom ha) { toFun := (spectrum ℝ a).domRestrict f, continuous_toFun := ⋯ }) b

Tactic:
rw [← cfc_apply ..]

Goal state after:
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
⊢ Commute (cfc f a) b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : MeasurableSpace X
μ : Measure X
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra 𝕜 A
inst✝⁵ : ContinuousFunctionalCalculus 𝕜 A p
inst✝⁴ : CompleteSpace A
inst✝³ : NormedSpace ℝ A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf : ContinuousOn (Function.uncurry f) (univ ×ˢ spectrum 𝕜 a)
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ cfc (fun r ↦ ∫ (x : X), f x r ∂μ) a = ∫ (x : X), cfc (f x) a ∂μ

Tactic:
by
  have : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a) := .of_forall fun x ↦
    hf.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨Set.mem_univ _, hz⟩
  refine cfc_integral' _ _ this ⟨?_, ?_⟩ ha
  · exact aeStronglyMeasurable_mkD_restrict_of_uncurry _ _ hf
  · exact hasFiniteIntegral_mkD_restrict_of_bound f _ this bound bound_int bound_ge

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℜ a))
hf0 : f 0 = 0
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' quasispectrum ℂ a)
| cfcₙ f ↑(ℜ a)

Tactic:
cfcₙ_real_eq_complex,

Goal state after:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℜ a))
hf0 : f 0 = 0
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' quasispectrum ℂ a)
| cfcₙ (fun x ↦ ↑(f x.re)) ↑(ℜ a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℜ a))
hf0 : f 0 = 0
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' quasispectrum ℂ a)
⊢ cfcₙ (fun x ↦ ↑(f x.re)) a = cfcₙ f ↑(ℜ a)

Tactic:
conv_rhs =>
    rw [cfcₙ_real_eq_complex, ← cfcₙ_re_id a, ← cfcₙ_comp' ..]
    simp

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℑ a))
hf0 : f 0 = 0
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' quasispectrum ℂ a)
| cfcₙ f ↑(ℑ a)

Tactic:
cfcₙ_real_eq_complex,

Goal state after:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℑ a))
hf0 : f 0 = 0
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' quasispectrum ℂ a)
| cfcₙ (fun x ↦ ↑(f x.re)) ↑(ℑ a)
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
A : Set E
ι : Sort u_6
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
inhabited_h : Inhabited ι
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxF : ∀ (i : ι), x ∈ F i
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ ∀ (i : ι), x₁ ∈ F i

Tactic:
exact fun i ↦ (hAF i).2 hx₁A hx₂A (hxF i) hx

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : p ≤ q → q * p = p
h : q * p = p
⊢ p * q = p

Tactic:
simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $h)

Goal state after:
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: case h
⊢ Circle.exp (2⁻¹ * 2 * π) ≠ 1

Tactic:
inv_mul_cancel₀ (by positivity),

Goal state after:
case h
⊢ Circle.exp (1 * π) ≠ 1
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
⊢ ‖diagonal v‖ = ‖v‖

Tactic:
set T := toEuclideanCLM (n := n) (𝕜 := 𝕜) (diagonal v)

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
⊢ ‖diagonal v‖ = ‖v‖