mathlib-initiative/mathlib-tactics huggingface dataset:
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
μ : 𝕜
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ False

Tactic:
apply hμ₂

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
μ : 𝕜
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ μ ∈ (σ 𝕜 x)ᶜ
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
x : 𝕜
hx : x ∈ σ 𝕜 a
ha : p a
⊢ ‖x‖ ≤ ‖a‖

Tactic:
by
  simpa only [cfc_id 𝕜 a] using! norm_apply_le_norm_cfc (id : 𝕜 → 𝕜) a hx

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

Goal state before:
pp: case refine_1
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
y : ℝ
hy : y ∈ spectrum ℝ a
hx : ↑t - y ∈ {↑t} - spectrum ℝ a
hty : -↑t ≤ y
hyt : y ≤ ↑t
⊢ ↑‖↑t - y‖₊ ≤ ↑t

Tactic:
lift y to ℝ≥0 using h y hy

Goal state after:
case refine_1
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
y : ℝ≥0
hy : ↑y ∈ spectrum ℝ a
hx : ↑t - ↑y ∈ {↑t} - spectrum ℝ a
hty : -↑t ≤ ↑y
hyt : ↑y ≤ ↑t
⊢ ↑‖↑t - ↑y‖₊ ≤ ↑t
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
a : A
x : 𝕜
hx : x ∈ σₙ 𝕜 a
ha : p a
⊢ ‖x‖ ≤ ‖a‖

Tactic:
simpa only [cfcₙ_id 𝕜 a] using! norm_apply_le_norm_cfcₙ (id : 𝕜 → 𝕜) a hx

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n ↦ ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
n : ℕ
⊢ ↑‖a‖₊ = (↑‖a‖₊ ^ 2 ^ n) ^ (1 / ↑(2 ^ n))

Tactic:
← rpow_natCast,

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n ↦ ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
n : ℕ
⊢ ↑‖a‖₊ = (↑‖a‖₊ ^ ↑(2 ^ n)) ^ (1 / ↑(2 ^ n))
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
n : ℕ
⊢ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n) = (↑‖a ^ n‖₊ ^ (1 / ↑n)) ^ 2

Tactic:
← rpow_natCast,

Goal state after:
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
n : ℕ
⊢ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n) = (↑‖a ^ n‖₊ ^ (1 / ↑n)) ^ ↑2
Module: Mathlib.Analysis.LocallyConvex.Polar

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
⊢ B.polar Set.univ = {0}

Tactic:
rw [Set.eq_singleton_iff_unique_mem]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
⊢ 0 ∈ B.polar Set.univ ∧ ∀ x ∈ B.polar Set.univ, x = 0
Module: Mathlib.Analysis.LocallyConvex.Polar

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
⊢ B.polar ↑m = {y | ∀ x ∈ m, (B x) y = 0}

Tactic:
by
  ext y
  constructor
  · intro hy x hx
    obtain ⟨r, hr⟩ := NormedField.exists_lt_norm 𝕜 ‖B x y‖⁻¹
    contrapose! hr
    rw [← one_div, le_div_iff₀ (norm_pos_iff.2 hr)]
    simpa using hy _ (SMulMemClass.smul_mem r hx)
  · intro h x hx
    simp [h x hx]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹² : AddCommGroup E
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : IsRCLikeNormedField 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : PolynormableSpace 𝕜 E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
S : Submodule 𝕜 E
f : ↥S →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(↑f).range
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis (Fin (finrank 𝕜 ↥(↑f).range)) 𝕜 ↥(↑f).range := finBasis 𝕜 ↥(↑f).range
e : ↥(↑f).range ≃L[𝕜] Fin (finrank 𝕜 ↥(↑f).range) → 𝕜 := b.equivFunL
fi : Fin (finrank 𝕜 ↥(↑f).range) → ↥S →L[𝕜] 𝕜 :=
  fun i ↦ LinearMap.toContinuousLinearMap (b.coord i) ∘SL f.codRestrict (↑f).range ⋯
gi : Fin (finrank 𝕜 ↥(↑f).range) → StrongDual 𝕜 E
hgf : ∀ (i : Fin (finrank 𝕜 ↥(↑f).range)) (x : ↥S), (gi i) ↑x = (fi i) x
⊢ ∃ g, f = g ∘SL S.subtypeL

Tactic:
use f.range.subtypeL.comp <| e.symm.toContinuousLinearMap.comp (.pi gi)

Goal state after:
case h
𝕜 : Type u_1
E : Type u_2
inst✝¹² : AddCommGroup E
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : IsRCLikeNormedField 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : PolynormableSpace 𝕜 E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
S : Submodule 𝕜 E
f : ↥S →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(↑f).range
this : RCLike 𝕜 := ⋯
b : Basis (Fin (finrank 𝕜 ↥(↑f).range)) 𝕜 ↥(↑f).range := ⋯
e : ↥(↑f).range ≃L[𝕜] Fin (finrank 𝕜 ↥(↑f).range) → 𝕜 := ⋯
fi : Fin (finrank 𝕜 ↥(↑f).range) → ↥S →L[𝕜] 𝕜 := ⋯
gi : Fin (finrank 𝕜 ↥(↑f).range) → StrongDual 𝕜 E
hgf : ∀ (i : Fin (finrank 𝕜 ↥(↑f).range)) (x : ↥S), (gi i) ↑x = (fi i) x
⊢ f = ((↑f).range.subtypeL ∘SL ↑e.symm ∘SL pi gi) ∘SL S.subtypeL
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: case refine_1
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ ∃ f, f a = z

pp: case refine_2
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
⊢ (∃ f, f a = z) → z ∈ spectrum ℂ a

Tactic:
· obtain ⟨f, hf⟩ := WeakDual.CharacterSpace.exists_apply_eq_zero hz
    simp only [map_sub, sub_eq_zero, AlgHomClass.commutes] at hf
    exact ⟨_, hf.symm⟩

Goal state after:
case refine_2
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
⊢ (∃ f, f a = z) → z ∈ spectrum ℂ a
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
⊢ spectrum ℂ ((gelfandTransform ℂ A) a) = spectrum ℂ a

Tactic:
ext z
  rw [ContinuousMap.spectrum_eq_range, WeakDual.CharacterSpace.mem_spectrum_iff_exists]
  exact Iff.rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
h : ∀ (c : α), LipschitzWith K (f c)
⊢ UniformEquicontinuous f

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous]
  rw [← lipschitzWith_ofFun_iff] at h
  exact h.uniformContinuous

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

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

Tactic:
by simpa using hyz.1.add hxy.1

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : a ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
x✝ : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this✝ : StarOrderedRing (Unitization ℂ A)
this :
  (Unitization.inrNonUnitalStarAlgHom ℂ A) a ∈
    AddSubmonoid.map (Unitization.inrNonUnitalStarAlgHom ℂ A) (AddSubmonoid.closure (Set.range fun s ↦ star s * s))
⊢ ↑a ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)

Tactic:
rw [AddMonoidHom.map_mclosure, ← Set.range_comp] at this

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : a ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
x✝ : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this✝ : StarOrderedRing (Unitization ℂ A)
this :
  (Unitization.inrNonUnitalStarAlgHom ℂ A) a ∈
    AddSubmonoid.closure (Set.range (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) ∘ fun s ↦ star s * s))
⊢ ↑a ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
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
a : A
ha : 0 ≤ a
⊢ a ^ 3 = a * a * a

Tactic:
by
  simp only [nnrpow_def, NNReal.nnrpow_def, NNReal.coe_ofNat, NNReal.rpow_ofNat, pow_three]
  change cfcₙ (fun z : ℝ≥0 => id z * (id z * id z)) a = a * a * a
  rw [cfcₙ_mul id _ a, cfcₙ_mul id _ a, ← mul_assoc, cfcₙ_id ℝ≥0 a]

Goal state after:
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
tfae_1_iff_9 : 0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ [0 ≤ a, a = sqrt a * sqrt a, ∃ b, 0 ≤ b ∧ a = b * b, ∃ b, IsSelfAdjoint b ∧ a = b * b, ∃ b, a = star b * b,
      ∃ b, a = b * star b, a = a⁺, IsSelfAdjoint a ∧ a⁻ = 0,
      IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal].TFAE

Tactic:
tfae_have 1 ↔ 7 := eq_comm.eq ▸ (CFC.posPart_eq_self a).symm

Goal state after:
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
tfae_1_iff_9 : 0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
tfae_1_iff_7 : 0 ≤ a ↔ a = a⁺
⊢ [0 ≤ a, a = sqrt a * sqrt a, ∃ b, 0 ≤ b ∧ a = b * b, ∃ b, IsSelfAdjoint b ∧ a = b * b, ∃ b, a = star b * b,
      ∃ b, a = b * star b, a = a⁺, IsSelfAdjoint a ∧ a⁻ = 0,
      IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal].TFAE
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, spectrum 𝕜 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
⊢ ContinuousOn (fun x ↦ cfc f (a x)) t

Tactic:
by
  have hs' := hs
  simp only [nhdsSet_iUnion, mem_iSup] at hs'
  have (x : t) : ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a x), spectrum 𝕜 x' ⊆ S) ∧ S ⊆ s := by
    obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
      spectrum.isCompact (𝕜 := 𝕜) (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)
    refine ⟨S, hS₂, ?_, hS₃⟩
    exact upperHemicontinuous_spectrum 𝕜 A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
      fun _ ↦ subset_of_mem_nhdsSet
  choose S hS₁ hS₂ hS₃ using this
  classical
  refine ha_cont.cfc (s := fun x : X ↦ if hx : x ∈ t then S ⟨x, hx⟩ else ∅) f
    (by simpa +contextual using hS₁) ?_ ha' ?_
  all_goals simp +contextual only [↓reduceDIte]
  · exact fun x₀ hx₀ ↦ ha_cont.continuousWithinAt hx₀ |>.eventually <| hS₂ ⟨x₀, hx₀⟩
  · exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩

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
x y : E
⊢ ‖x + y‖ ^ 2 ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖

Tactic:
simp only [norm_eq_sqrt_norm_inner_self (A := A), inner_add_right, inner_add_left,
            ← add_assoc, norm_nonneg, Real.sq_sqrt]

Goal state after:
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, x⟫ + ⟪y, x⟫ + ⟪x, y⟫ + ⟪y, y⟫‖ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ({x | 0 ≤ x} ∩ Metric.ball 0 1)

Tactic:
let f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x ↦ 1 - (1 + x)⁻¹
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ({x | 0 ≤ x} ∩ Metric.ball 0 1)
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
⊢ f 0 = 0

Tactic:
by simp [f, tsub_self]

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

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A₁
inst✝⁵ : NonUnitalCStarAlgebra A₂
inst✝⁴ : PartialOrder A₁
inst✝³ : PartialOrder A₂
inst✝² : StarOrderedRing A₁
inst✝¹ : StarOrderedRing A₂
n : Type u_3
inst✝ : Fintype n
φ : A₁ →CP A₂
M : CStarMatrix n n A₁
hM : 0 ≤ M
k : ℕ := Fintype.card n
e : n ≃ Fin (Fintype.card n) := Fintype.equivFinOfCardEq ⋯
⊢ 0 ≤ ((reindexₐ ℂ A₁ e) M).map ⇑φ

Tactic:
exact CompletelyPositiveMapClass.map_cstarMatrix_nonneg' _ k _ (map_nonneg _ hM)

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

Goal state before:
pp: 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, p (a x)
ha₀ : quasispectrum 𝕜 a₀ ⊆ s
ha₀' : p a₀
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Tendsto (fun x ↦ cfcₙ f (a x)) l (𝓝 (cfcₙ f a₀))

Tactic:
apply continuousOn_cfcₙ A hs f |>.continuousWithinAt ⟨ha₀', ha₀⟩ |>.tendsto.comp

Goal state after:
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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, p (a x)
ha₀ : quasispectrum 𝕜 a₀ ⊆ s
ha₀' : p a₀
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Tendsto a l (𝓝[{a | p a ∧ quasispectrum 𝕜 a ⊆ s}] a₀)
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap

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
f : X → Y → E
g : C(Y, E)
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
x : X
bound_ge_x : ∀ (y : Y), ‖f x y‖ ≤ bound x
⊢ Continuous (f x) → ∀ (y : Y), ‖(mkD (f x) g) y‖ ≤ bound x

Tactic:
cont_x

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
f : X → Y → E
g : C(Y, E)
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
x : X
bound_ge_x : ∀ (y : Y), ‖f x y‖ ≤ bound x
cont_x : Continuous (f x)
⊢ ∀ (y : Y), ‖(mkD (f x) g) y‖ ≤ bound x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra 𝕜 A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C(↑(spectrum 𝕜 a), 𝕜)
⊢ Commute ((cfcHom ha) f) b

Tactic:
by
  open scoped ContinuousFunctionalCalculus in
  induction f using ContinuousMap.induction_on_of_compact with
  | const r =>
    conv =>
      enter [1, 2]
      equals algebraMap 𝕜 _ r => rfl
    rw [AlgHomClass.commutes]
    exact Algebra.commute_algebraMap_left r b
  | id => rwa [cfcHom_id ha]
  | star_id => rwa [map_star, cfcHom_id]
  | add f g hf hg => rw [map_add]; exact hf.add_left hg
  | mul f g hf hg => rw [map_mul]; exact mul_left hf hg
  | frequently f hf =>
    rw [commute_iff_eq, ← Set.mem_ofPred (p := fun x => x * b = b * x),
      ← (isClosed_eq (by fun_prop) (by fun_prop)).closure_eq]
    apply mem_closure_of_frequently_of_tendsto hf
    exact cfcHom_continuous ha |>.tendsto _

Goal state after:
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
f : X → Y → E
g : C(Y, E)₀
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
f_ae_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
x : X
bound_ge_x : ∀ (y : Y), ‖f x y‖ ≤ bound x
⊢ Continuous (f x) → f x 0 = 0 → ∀ (y : Y), ‖(mkD (f x) g) y‖ ≤ bound x

Tactic:
cont_x

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
f : X → Y → E
g : C(Y, E)₀
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
f_ae_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
x : X
bound_ge_x : ∀ (y : Y), ‖f x y‖ ≤ bound x
cont_x : Continuous (f x)
⊢ f x 0 = 0 → ∀ (y : Y), ‖(mkD (f x) g) y‖ ≤ bound x
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
f : X → Y → E
g : C(Y, E)₀
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
f_ae_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
⊢ ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(mkD (f x) g) y‖ ≤ bound x

Tactic:
filter_upwards [bound_ge, f_ae_cont, f_ae_zero] with x bound_ge_x cont_x zero_x

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
f : X → Y → E
g : C(Y, E)₀
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
f_ae_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
x : X
bound_ge_x : ∀ (y : Y), ‖f x y‖ ≤ bound x
cont_x : Continuous (f x)
zero_x : f x 0 = 0
⊢ ∀ (y : Y), ‖(mkD (f x) g) y‖ ≤ bound x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
pp: case refine_1
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✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf : ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a)
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
⊢ AEStronglyMeasurable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) (μ.restrict s)

Tactic:
exact aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry hs _ _ hf

Goal state after:
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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Integrable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
z : ↑(spectrum 𝕜 a)
x : X
⊢ ContinuousOn (f x) (spectrum 𝕜 a) → f x ↑z = (mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) z

Tactic:
cont_x

Goal state after:
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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Integrable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
z : ↑(spectrum 𝕜 a)
x : X
cont_x : ContinuousOn (f x) (spectrum 𝕜 a)
⊢ f x ↑z = (mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) z