mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: case refine_1
𝕜 : 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
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
⊢ φ ∈ characterSpace 𝕜 A → φ ∈ {φ | φ 1 = 1 ∧ ∀ (x y : A), φ (x * y) = φ x * φ y}

pp: case refine_2
𝕜 : 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
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
⊢ φ ∈ {φ | φ 1 = 1 ∧ ∀ (x y : A), φ (x * y) = φ x * φ y} → φ ∈ characterSpace 𝕜 A

Tactic:
· rintro hφ
    lift φ to characterSpace 𝕜 A using hφ
    exact ⟨map_one φ, map_mul φ⟩

Goal state after:
case refine_2
𝕜 : 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
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
⊢ φ ∈ {φ | φ 1 = 1 ∧ ∀ (x y : A), φ (x * y) = φ x * φ y} → φ ∈ characterSpace 𝕜 A
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case a
α : Type u_1
U V : SetRel α α
⊢ hausdorffEntourage U ○ hausdorffEntourage V ⊆ hausdorffEntourage (U ○ V)

Tactic:
intro ⟨s₁, s₃⟩ ⟨s₂, ⟨h₁₂, h₂₁⟩, ⟨h₂₃, h₃₂⟩⟩

Goal state after:
case a
α : Type u_1
U V : SetRel α α
s₁ s₃ s₂ : Set α
h₁₂ : (s₁, s₂).1 ⊆ U.preimage (s₁, s₂).2
h₂₁ : (s₁, s₂).2 ⊆ U.image (s₁, s₂).1
h₂₃ : (s₂, s₃).1 ⊆ V.preimage (s₂, s₃).2
h₃₂ : (s₂, s₃).2 ⊆ V.image (s₂, s₃).1
⊢ (s₁, s₃) ∈ hausdorffEntourage (U ○ V)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
U₁ : SetRel α α
U₂ : SetRel β β
s₁ t₁ : Set α
s₂ t₂ : Set β
h₁ : s₁ ⊆ U₁.preimage t₁ ∧ t₁ ⊆ U₁.image s₁
h₂ : s₂ ⊆ U₂.preimage t₂ ∧ t₂ ⊆ U₂.image s₂
⊢ s₁ ×ˢ s₂ ⊆ (entourageProd U₁ U₂).preimage (t₁ ×ˢ t₂) ∧ t₁ ×ˢ t₂ ⊆ (entourageProd U₁ U₂).image (s₁ ×ˢ s₂)

Tactic:
grind [preimage_entourageProd_prod, image_entourageProd_prod]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case e'_3.hn
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊
hn : 0 < ↑(n + 1)
⊢ n + 1 ≠ 0

Tactic:
positivity

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
z : ℂ
⊢ z ∈ ofReal ∘ re '' σ ℂ a → z ∈ σ ℂ a

Tactic:
rintro ⟨z, hz, rfl⟩
    simpa only [(ha.mem_spectrum_eq_re hz).symm, Function.comp_apply] using hz

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 := ⋯ }
⊢ 0 ≤ ‖↑f‖

Tactic:
positivity

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 := ⋯ }
⊢ 0 ≤ ‖(↑f).comp ι‖

Tactic:
positivity

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

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x ↦ r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ 0 ≤ (1 + r) / 2

Tactic:
positivity

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

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x ↦ r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ 0 ≤ (1 - r) / 2

Tactic:
positivity

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x✝ : SeparableSpace (NonemptyCompacts α)
⊢ SeparableSpace α

Tactic:
rw [← Compacts.separableSpace_iff, ← isSeparable_univ_iff, ← union_compl_self {⊥},
    ← range_toCompacts]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x✝ : SeparableSpace (NonemptyCompacts α)
⊢ IsSeparable ({⊥} ∪ range toCompacts)
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: E : Type u_3
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : QuasiCompleteSpace ℝ E
s : Set E
ht : TotallyBounded s
⊢ IsCompact ((closedAbsConvexHull ℝ) s)

Tactic:
closedAbsConvexHull_eq_closure_absConvexHull

Goal state after:
E : Type u_3
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : QuasiCompleteSpace ℝ E
s : Set E
ht : TotallyBounded s
⊢ IsCompact (closure[inst✝⁴.toTopologicalSpace] ((absConvexHull ℝ) s))
Module: Mathlib.Analysis.Normed.Module.HahnBanach

Goal state before:
pp: 𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety : ∀ (c : 𝕜), ‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) c‖ = ‖x‖ * ‖c‖
⊢ 0 < ‖x‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.HahnBanach

Goal state before:
pp: 𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety : ∀ (c : 𝕜), ‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) c‖ = ‖x‖ * ‖c‖
coord : ↥(𝕜 ∙ x) →L[𝕜] 𝕜 := ↑(ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯ hhomothety).symm
g : StrongDual 𝕜 E
hg : (∀ (x_1 : ↥(𝕜 ∙ x)), g ↑x_1 = (↑‖x‖ • coord) x_1) ∧ ‖g‖ = ‖↑‖x‖ • coord‖
hval : g x = ↑‖x‖
⊢ 0 ≤ ‖x‖⁻¹

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.HahnBanach

Goal state before:
pp: 𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety : ∀ (c : 𝕜), ‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) c‖ = ‖x‖ * ‖c‖
coord : ↥(𝕜 ∙ x) →L[𝕜] 𝕜 := ↑(ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯ hhomothety).symm
g : StrongDual 𝕜 E
hg : (∀ (x_1 : ↥(𝕜 ∙ x)), g ↑x_1 = (↑‖x‖ • coord) x_1) ∧ ‖g‖ = ‖↑‖x‖ • coord‖
hval : g x = ↑‖x‖
y : ↥(𝕜 ∙ x)
⊢ 0 < ‖x‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.HahnBanach

Goal state before:
pp: 𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety : ∀ (c : 𝕜), ‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) c‖ = ‖x‖ * ‖c‖
coord : ↥(𝕜 ∙ x) →L[𝕜] 𝕜 := ↑(ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯ hhomothety).symm
g : StrongDual 𝕜 E
hg : (∀ (x_1 : ↥(𝕜 ∙ x)), g ↑x_1 = (↑‖x‖ • coord) x_1) ∧ ‖g‖ = ‖↑‖x‖ • coord‖
hval : g x = ↑‖x‖
hle : ‖x‖ ≤ ‖g‖ * ‖x‖
⊢ 0 < ‖x‖

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NormedField 𝕜
inst✝⁸ : IsRCLikeNormedField 𝕜
F : Type u_3
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : T2Space F
inst✝¹ : PolynormableSpace 𝕜 F
S : Submodule 𝕜 F
inst✝ : FiniteDimensional 𝕜 ↥S
⊢ S.ClosedComplemented

Tactic:
let ⟨g, hg⟩ := (ContinuousLinearMap.id 𝕜 S).exist_extension_of_finiteDimensional_range

Goal state after:
𝕜 : Type u_1
inst✝⁹ : NormedField 𝕜
inst✝⁸ : IsRCLikeNormedField 𝕜
F : Type u_3
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : T2Space F
inst✝¹ : PolynormableSpace 𝕜 F
S : Submodule 𝕜 F
inst✝ : FiniteDimensional 𝕜 ↥S
g : F →L[𝕜] ↥S
hg : ContinuousLinearMap.id 𝕜 ↥S = g ∘SL S.subtypeL
⊢ S.ClosedComplemented
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (ball 0 r) ⊆ closedBall 0 (‖c‖ / r)

Tactic:
intro x' hx'

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
hx' : x' ∈ polar 𝕜 (ball 0 r)
⊢ x' ∈ closedBall 0 (‖c‖ / r)
Module: Mathlib.Analysis.LocallyConvex.WeakDual

Goal state before:
pp: ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
this : IsTopologicalAddGroup E
⊢ WithSeminorms fun i ↦ (f i).toSeminorm

Tactic:
SeminormFamily.withSeminorms_iff_nhds_eq_iInf,

Goal state after:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
this : IsTopologicalAddGroup E
⊢ 𝓝 0 = ⨅ i, Filter.comap (⇑(f i).toSeminorm) (𝓝 0)
Module: Mathlib.Analysis.Normed.Operator.Completeness

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (fun n x ↦ (f n) x) atTop (𝓝 ⇑g)
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hb_lim : Tendsto b atTop (𝓝 0)
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N
⊢ Tendsto f atTop (𝓝 g)

Tactic:
suffices ∀ n x, ‖f n x - g x‖ ≤ b n * ‖x‖ from
    tendsto_iff_norm_sub_tendsto_zero.2
    (squeeze_zero (fun n => norm_nonneg _) (fun n => opNorm_le_bound _ (hb₀ n) (this n)) hb_lim)

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (fun n x ↦ (f n) x) atTop (𝓝 ⇑g)
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hb_lim : Tendsto b atTop (𝓝 0)
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N
⊢ ∀ (n : ℕ) (x : E'), ‖(f n) x - g x‖ ≤ b n * ‖x‖
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p q : P
⊢ dist ((Equiv.pointReflection p) q) p = dist p q

Tactic:
by
  simp [dist_eq_norm_vsub V, Equiv.pointReflection_vsub_left (G := V)]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case hf
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ 0 ≤ 1

Tactic:
positivity

Goal state after:
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
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
n : ℕ
⊢ 0 < (fun n ↦ 1 / 2 / 2 ^ n) n

Tactic:
positivity

Goal state after:
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
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
x : X
hx : x ∈ sᶜ
n : ℕ
hn : x ∉ U n
⊢ x ∈ (U n ∩ interior m)ᶜ

Tactic:
simp [hn]

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCommCStarAlgebra A
a b : A
h : a * b = 0
f : A → C(↑(characterSpace ℂ (Unitization ℂ A)), ℂ) :=
  ⇑(gelfandStarTransform (Unitization ℂ A)) ∘ ⇑(inrNonUnitalAlgHom ℂ A)
⊢ ‖a + b‖ = max ‖a‖ ‖b‖

Tactic:
have hf : Isometry f := gelfandTransform_isometry _ |>.comp isometry_inr

Goal state after:
A : Type u_1
inst✝ : NonUnitalCommCStarAlgebra A
a b : A
h : a * b = 0
f : A → C(↑(characterSpace ℂ (Unitization ℂ A)), ℂ) :=
  ⇑(gelfandStarTransform (Unitization ℂ A)) ∘ ⇑(inrNonUnitalAlgHom ℂ A)
hf : Isometry f
⊢ ‖a + b‖ = max ‖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
a : A
x : ℝ
x✝ : x ∈ quasispectrum ℝ a
⊢ 0 ≤ x⁺

Tactic:
positivity

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
a : A
x : ℝ
x✝ : x ∈ quasispectrum ℝ a
⊢ 0 ≤ x⁻

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
⊢ Bornology.IsBounded Set.univ

Tactic:
Metric.isBounded_iff_ediam_ne_top,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
⊢ Metric.ediam Set.univ ≠ ∞
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
⊢ 𝓤 (α →ᵤ[𝔖] β) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
let _ := Fintype.ofFinite 𝔖

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
x✝ : Fintype ↑𝔖 := Fintype.ofFinite ↑𝔖
⊢ 𝓤 (α →ᵤ[𝔖] β) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst✝² : Finite ↑𝔖
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
f g : α →ᵤ[𝔖] β
⊢ edist f g = ENNReal.ofReal (⨆ x, dist ((toFun 𝔖) f ↑x) ((toFun 𝔖) g ↑x))

Tactic:
cases isEmpty_or_nonempty (⋃₀ 𝔖)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst✝² : Finite ↑𝔖
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
f g : α →ᵤ[𝔖] β
h✝ : IsEmpty ↑(⋃₀ 𝔖)
⊢ edist f g = ENNReal.ofReal (⨆ x, dist ((toFun 𝔖) f ↑x) ((toFun 𝔖) g ↑x))

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst✝² : Finite ↑𝔖
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
f g : α →ᵤ[𝔖] β
h✝ : Nonempty ↑(⋃₀ 𝔖)
⊢ edist f g = ENNReal.ofReal (⨆ x, dist ((toFun 𝔖) f ↑x) ((toFun 𝔖) g ↑x))
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
this : Isometry ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
f : C(↑(spectrum ℂ a), ℂ)
⊢ Commute (star (((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)) f))
    (((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)) f)

Tactic:
rw [← map_star]; exact Commute.all (star f) f |>.map _

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
x : ℝ
⊢ 0 ≤ (fun x ↦ x⁻ ^ 3) x

Tactic:
positivity

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

Goal state before:
pp: case pos.inr
A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
h : 0 < x
⊢ ‖x‖ ≤ ‖a‖

Tactic:
exact NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le a hx ha

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : x ∈ {a | 0 ≤ a}
hx_pos : 0 < ‖x‖
this : (↑r * ↑‖x‖⁻¹)⁻¹ • (↑r * ↑‖x‖⁻¹) • x = x
⊢ 0 ≤ r * ‖x‖⁻¹

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: case inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : x ∈ {a | 0 ≤ a}
hx_pos : 0 < ‖x‖
⊢ ¬r * ‖x‖⁻¹ = 0

Tactic:
positivity

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
htriv : 0 ≤ a
h₁ : 0 < x
h₂ : ↑x / 2 = ↑(x / 2)
⊢ 0 < x / 2

Tactic:
positivity

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

Goal state before:
pp: case pos
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : IsStrictlyPositive a
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ

pp: case neg
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : ¬IsStrictlyPositive a
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ

Tactic:
· rw [sqrt_eq_rpow, sqrt_eq_rpow, inverse_rpow _ _ (by grind),
        inverse_eq_rpow_neg_one, rpow_rpow _ _ _ (by grind)]
    grind only

Goal state after:
case neg
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : ¬IsStrictlyPositive a
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: case neg
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : ¬IsStrictlyPositive a
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ

Tactic:
· have ha' : ¬IsUnit (sqrt a) := by rwa [CFC.isUnit_sqrt_iff_isStrictlyPositive]
    obtain (H | H) : ¬0 ≤ a ∨ ¬IsUnit a := by grind
    · rw [sqrt_of_not_nonneg H, inverse_zero]
      by_cases hunit : IsUnit a
      · have h₂ : ¬0 ≤ inverse a := by grind [CFC.ringInverse_nonneg_iff_nonneg_of_isUnit]
        rw [sqrt_of_not_nonneg h₂]
      · simp [inverse_non_unit _ hunit]
    · simp [inverse_non_unit _ ha', inverse_non_unit _ H]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
| ‖↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))‖ ≤ 1

Tactic:
CStarAlgebra.norm_le_one_iff_of_nonneg _ hbab

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
| ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
⊢ 0 ≤ ‖⟪x, x⟫_A‖

Tactic:
positivity

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ 0 ≤ ‖v‖

Tactic:
positivity

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ 0 ≤ √‖x * star x‖

Tactic:
positivity

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalCStarAlgebra A
inst✝⁸ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : Module ℂ E
inst✝⁵ : SMul A E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module ℂ F
inst✝² : SMul A F
inst✝¹ : CStarModule A E
inst✝ : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ 0 ≤ ‖x.1‖ + ‖x.2‖

Tactic:
positivity

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

Goal state before:
pp: case h₂
A : Type u_1
inst✝⁹ : NonUnitalCStarAlgebra A
inst✝⁸ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : Module ℂ E
inst✝⁵ : SMul A E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module ℂ F
inst✝² : SMul A F
inst✝¹ : CStarModule A E
inst✝ : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ 0 ≤ 2 * ‖x.1‖ * ‖x.2‖

Tactic:
positivity

Goal state after: