mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : IsCompact s
⊢ 𝓝 s ≤ 𝓝 s

Tactic:
simp_rw [TopologicalSpace.nhds_generateFrom, le_iInf₂_iff, Filter.le_principal_iff]

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : IsCompact s
⊢ ∀
    i ∈
      {s_1 |
        s ∈ s_1 ∧
          s_1 ∈
            Set.powerset '' {U | IsOpen[inst✝.toTopologicalSpace] U} ∪
              (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝.toTopologicalSpace] U}},
    i ∈ 𝓝 s
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n ↦ (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
⊢ exp (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b

Tactic:
exp_eq_tsum 𝕜

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n ↦ (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
⊢ (fun x ↦ ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
x✝ : CompleteSpace (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
K : NonemptyCompacts α
hK : Filter.map (fun x ↦ {x}) f ≤ 𝓝 K
x : α
hx : x ∈ ↑K
⊢ f ≤ 𝓝 x

Tactic:
(nhds_basis_opens x).ge_iff

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
x✝ : CompleteSpace (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
K : NonemptyCompacts α
hK : Filter.map (fun x ↦ {x}) f ≤ 𝓝 K
x : α
hx : x ∈ ↑K
⊢ ∀ (i' : Set α), x ∈ i' ∧ IsOpen[inst✝.toTopologicalSpace] i' → i' ∈ f
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
this : CompleteSpace ↥S
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((interior (σ 𝕜 x) ∪ frontier (σ 𝕜 x)) \ σ 𝕜 ↑x)

Tactic:
union_sdiff_distrib,

Goal state after:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
this : CompleteSpace ↥S
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (σ 𝕜 x) \ σ 𝕜 ↑x ∪ frontier (σ 𝕜 x) \ σ 𝕜 ↑x)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
x✝ : NonUnitalContinuousFunctionalCalculus 𝕜 A p := RCLike.nonUnitalContinuousFunctionalCalculus fun {x} ↦ hp₁
⊢ ((inrNonUnitalStarAlgHom 𝕜 A).comp (cfcₙHom ha)) (ContinuousMapZero.id (σₙ 𝕜 a)) =
    (cfcₙAux ⋯ a ha) (ContinuousMapZero.id (σₙ 𝕜 a))

Tactic:
by simp [cfcₙHom_id ha, cfcₙAux_id hp₁ a ha]

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarRing A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Module ℝ A
inst✝³ : IsScalarTower ℝ A A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ 0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal

Tactic:
refine ⟨fun ha ↦ ⟨.of_nonneg ha, .nnreal_of_nonneg ha⟩, ?_⟩
  rintro ⟨ha₁, ha₂⟩
  obtain ⟨x, hx, -, rfl⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts ha₁ ha₂
  simpa [sq, hx.star_eq] using star_mul_self_nonneg x

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

Goal state before:
pp: A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
h₂ : IsClosed (range NNReal.toReal)
h₁ : IsInducing NNReal.toReal
⊢ UpperHemicontinuous (spectrum ℝ≥0)

Tactic:
exact upperHemicontinuous_spectrum ℝ A |>.isInducing_comp h₁ h₂

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k ∈ σ 𝕜 ↑(toUnits u)
hnk : k ≠ 0
⊢ 1 ≤ ‖k‖

Tactic:
rw [← inv_inv (Unitary.toUnits u), ← spectrum.map_inv, Set.mem_inv] at hk

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k⁻¹ ∈ σ 𝕜 ↑(toUnits u)⁻¹
hnk : k ≠ 0
⊢ 1 ≤ ‖k‖
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ (a⋆ * a)
ha₂ : 0 ∉ σ ℂ (a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsUnit a

pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ (a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a * a⋆)

pp: A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ ↑(a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a⋆ * a)

Tactic:
spectrum.zero_notMem_iff

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsUnit a

A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ (a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a * a⋆)

A : Type u_1
inst✝ : CStarAlgebra A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ ↑(a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a⋆ * a)
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: 𝕜 : 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 𝕜
s : Set E
hs_zero : 0 ∈ s
hs_open : IsOpen[inst✝⁴] s
W : Set E
hW_open : IsOpen[inst✝⁴] W
hW_zero : 0 ∈ W
hW_add : W + W ⊆ s
⊢ ∃ i', (i' ∈ 𝓝 0 ∧ IsClosed[inst✝⁴] i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ s

Tactic:
obtain ⟨V, ⟨hV_zero, hV_open, hV_abs⟩, hVW⟩ :=
    (nhds_hasBasis_absConvex_open 𝕜 E).mem_iff.mp (hW_open.mem_nhds hW_zero)

Goal state after:
𝕜 : 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 𝕜
s : Set E
hs_zero : 0 ∈ s
hs_open : IsOpen[inst✝⁴] s
W : Set E
hW_open : IsOpen[inst✝⁴] W
hW_zero : 0 ∈ W
hW_add : W + W ⊆ s
V : Set E
hVW : id V ⊆ W
hV_zero : 0 ∈ V
hV_open : IsOpen[inst✝⁴] V
hV_abs : AbsConvex 𝕜 V
⊢ ∃ i', (i' ∈ 𝓝 0 ∧ IsClosed[inst✝⁴] i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ s
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x✝ : LocallyCompactSpace (NonemptyCompacts α)
x : α
U : Set α
hU : ↑{x} ⊆ interior U
K : Set (NonemptyCompacts α)
hK : IsCompact K
hxK : {x} ∈ interior K
hKU : K ⊆ {K | ↑K ⊆ interior U}
⊢ ∃ s ∈ 𝓝 x, s ⊆ U ∧ IsCompact s

Tactic:
refine ⟨⋃ L ∈ K, L, ?_, iUnion₂_subset <| by grind [interior_subset],
    isCompact_biUnion_coe_of_isCompact hK⟩

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x✝ : LocallyCompactSpace (NonemptyCompacts α)
x : α
U : Set α
hU : ↑{x} ⊆ interior U
K : Set (NonemptyCompacts α)
hK : IsCompact K
hxK : {x} ∈ interior K
hKU : K ⊆ {K | ↑K ⊆ interior U}
⊢ ⋃ L ∈ K, ↑L ∈ 𝓝 x
Module: Mathlib.Analysis.LocallyConvex.HahnBanach

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : NormedField 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : Module 𝕜 E
S : Submodule 𝕜 E
f : Dual 𝕜 ↥S
p : Seminorm 𝕜 E
hp : ∀ (x : ↥S), ‖f x‖ ≤ p ↑x
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ : Module ℝ E := restrictScalars ℝ 𝕜 E
this : IsScalarTower ℝ 𝕜 E := IsScalarTower.restrictScalars ℝ 𝕜 E
fr : Dual ℝ ↥S := reLm ∘ₗ ↑ℝ f
g : Dual ℝ E
hg : ∀ (x : ↥S), g ↑x = fr x
hgp : ∀ (x : E), |g x| ≤ (Seminorm.restrictScalars ℝ p) x
x : E
⊢ ‖g.extendRCLike x‖ ≤ p x

Tactic:
apply norm_extendRCLike_le_seminorm

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : NormedField 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : Module 𝕜 E
S : Submodule 𝕜 E
f : Dual 𝕜 ↥S
p : Seminorm 𝕜 E
hp : ∀ (x : ↥S), ‖f x‖ ≤ p ↑x
this✝¹ : RCLike 𝕜 := ⋯
this✝ : Module ℝ E := ⋯
this : IsScalarTower ℝ 𝕜 E := ⋯
fr : Dual ℝ ↥S := ⋯
g : Dual ℝ E
hg : ∀ (x : ↥S), g ↑x = fr x
hgp : ∀ (x : E), |g x| ≤ (Seminorm.restrictScalars ℝ p) x
x : E
⊢ ∀ (x : E), |g x| ≤ p x
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
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s

Tactic:
by
  by_cases c_zero : c = 0
  · simp only [c_zero, inv_zero, zero_smul]
    exact (topDualPairing 𝕜 E).flip.zero_mem_polar _
  have eq : ∀ z, ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖ := fun z => norm_smul c⁻¹ _
  have le : ∀ z, z ∈ s → ‖c⁻¹ • x' z‖ ≤ ‖c⁻¹‖ * ‖c‖ := by
    intro z hzs
    rw [eq z]
    apply mul_le_mul (le_of_eq rfl) (hc z hzs) (norm_nonneg _) (norm_nonneg _)
  have cancel : ‖c⁻¹‖ * ‖c‖ = 1 := by
    simp only [c_zero, norm_eq_zero, Ne, not_false_iff, inv_mul_cancel₀, norm_inv]
  rwa [cancel] at le

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) + a ≤ r' • (b - a) + a ↔ r ≤ r'

Tactic:
add_le_add_iff_right,

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 • (b - a) ≤ r' • (b - a) ↔ r ≤ r'
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] sᶜᶜ)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen[inst✝¹] u
hvIsOpen : IsOpen[inst✝¹] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst✝¹] u ⊆ vᶜ
P : Set X → Set X → Prop := fun C x ↦ sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed[inst✝¹] c
Pc : P c u0
u0IsOpen : IsOpen[inst✝¹] u0
⊢ c ⊆ u0 → ∃ v, IsOpen[inst✝¹] v ∧ c ⊆ v ∧ closure[inst✝¹] v ⊆ u0 ∧ P c v ∧ P (closure[inst✝¹] v) u0

Tactic:
csubu0

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] sᶜᶜ)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen[inst✝¹] u
hvIsOpen : IsOpen[inst✝¹] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst✝¹] u ⊆ vᶜ
P : Set X → Set X → Prop := fun C x ↦ sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed[inst✝¹] c
Pc : P c u0
u0IsOpen : IsOpen[inst✝¹] u0
csubu0 : c ⊆ u0
⊢ ∃ v, IsOpen[inst✝¹] v ∧ c ⊆ v ∧ closure[inst✝¹] v ⊆ u0 ∧ P c v ∧ P (closure[inst✝¹] v) u0
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 : ℝ
h : IsUnit a
ha : 0 ≤ a
this : IsStrictlyPositive a
⊢ sqrt a ^ x = a ^ (x / 2)

Tactic:
sqrt_eq_rpow,

Goal state after:
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 : ℝ
h : IsUnit a
ha : 0 ≤ a
this : IsStrictlyPositive a
⊢ (a ^ (1 / 2)) ^ x = a ^ (x / 2)
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
ha : 0 ≤ a
hx : ¬x = 0
h₁ : 0 ≤ ↑x
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

Tactic:
sqrt_eq_rpow,

Goal state after:
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
ha : 0 ≤ a
hx : ¬x = 0
h₁ : 0 ≤ ↑x
⊢ (a ^ (1 / 2)) ^ ↑x = a ^ (↑x / 2)
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
⊢ a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)

Tactic:
by
  have : a * star a ≤ algebraMap ℝ A ‖a * star a‖ := IsSelfAdjoint.le_algebraMap_norm_self
  rwa [CStarRing.norm_self_mul_star, ← pow_two] at this

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
a : A
a✝ : Nontrivial A
h : IsStrictlyPositive a⁻¹ʳ
ha : IsUnit a
⊢ IsStrictlyPositive a⁻¹ʳ⁻¹ʳ

Tactic:
exact h.ringInverse

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)⁻¹ʳ

Tactic:
sqrt_eq_rpow,

Goal state after:
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
⊢ a⁻¹ʳ ^ (1 / 2) = (sqrt a)⁻¹ʳ
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
⊢ a⁻¹ʳ ^ (1 / 2) = (sqrt a)⁻¹ʳ

Tactic:
sqrt_eq_rpow,

Goal state after:
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
⊢ a⁻¹ʳ ^ (1 / 2) = (a ^ (1 / 2))⁻¹ʳ
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
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖

Tactic:
have h : ‖x + y‖ ^ 2 ≤ (‖x‖ + ‖y‖) ^ 2 := by
    calc _ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by
          simp only [norm_eq_sqrt_norm_inner_self (A := A), inner_add_right, inner_add_left,
            ← add_assoc, norm_nonneg, Real.sq_sqrt]
          exact norm_add₃_le
      _ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by gcongr; exact norm_add_le _ _
      _ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ := by gcongr <;> exact norm_inner_le E
      _ = ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖y‖ ^ 2 := by
          simp [norm_eq_sqrt_norm_inner_self (A := A)]
      _ = (‖x‖ + ‖y‖) ^ 2 := by simp only [add_pow_two, add_left_inj]; ring
  refine (pow_le_pow_iff_left₀ (CStarModule.norm_nonneg A) ?_ (by simp)).mp h
  exact add_nonneg (CStarModule.norm_nonneg A) (CStarModule.norm_nonneg A)

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ e✝ : A
he✝ : IsStarProjection e✝
ha✝ : 0 ≤ a✝
hae✝ : a✝ ≤ e✝
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ star (1 - e) * a * (1 - e) ≤ 0

Tactic:
star_left_conjugate_le_conjugate hae (1 - e),

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ e✝ : A
he✝ : IsStarProjection e✝
ha✝ : 0 ≤ a✝
hae✝ : a✝ ≤ e✝
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ star (1 - e) * e * (1 - e) ≤ 0
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompactSpace Y
inst✝³ : Zero Y
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)₀
f_cont : Continuous (Function.uncurry f)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
⊢ AEStronglyMeasurable (fun x ↦ mkD (f x) g) μ

Tactic:
rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompactSpace Y
inst✝³ : Zero Y
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)₀
f_cont : Continuous (Function.uncurry f)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
⊢ AEStronglyMeasurable (fun x ↦ ↑(mkD (f x) g)) μ
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompactSpace Y
inst✝³ : Zero Y
s : Set X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(Y, E)
hs : MeasurableSet s
f : X → Y → E
g : C(Y, E)₀
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
⊢ AEStronglyMeasurable (fun x ↦ mkD (f x) g) (μ.restrict s)

Tactic:
rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompactSpace Y
inst✝³ : Zero Y
s : Set X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(Y, E)
hs : MeasurableSet s
f : X → Y → E
g : C(Y, E)₀
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
⊢ AEStronglyMeasurable (fun x ↦ ↑(mkD (f x) g)) (μ.restrict s)
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
t : Set Y
inst✝⁴ : CompactSpace ↑t
inst✝³ : Zero ↑t
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(↑t, E)
f : X → Y → E
g : C(↑t, E)₀
f_cont : ContinuousOn (Function.uncurry f) (univ ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x ↑0 = 0
⊢ AEStronglyMeasurable (fun x ↦ mkD (t.domRestrict (f x)) g) μ

Tactic:
rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
t : Set Y
inst✝⁴ : CompactSpace ↑t
inst✝³ : Zero ↑t
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(↑t, E)
f : X → Y → E
g : C(↑t, E)₀
f_cont : ContinuousOn (Function.uncurry f) (univ ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x ↑0 = 0
⊢ AEStronglyMeasurable (fun x ↦ ↑(mkD (t.domRestrict (f x)) g)) μ