mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
huU : {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty} ⊆ U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
⊢ ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s

Tactic:
← huU

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
huU : {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty} ⊆ U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
⊢ ∃ s ∈ 𝓝 K, s ⊆ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty} ∧ IsCompact s
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp (z • star b) * NormedSpace.exp (-(star z • b)) * x *
      (NormedSpace.exp (star z • a) * NormedSpace.exp (z • star (-a))) =
    ↑(expUnitary (2 • ℑ (z • star b))) * x * ↑(expUnitary (2 • ℑ (star z • a)))

Tactic:
congr!

Goal state after:
case e'_5
A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp (z • star b) * NormedSpace.exp (-(star z • b)) = ↑(expUnitary (2 • ℑ (z • star b)))

case e'_6
A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp (star z • a) * NormedSpace.exp (z • star (-a)) = ↑(expUnitary (2 • ℑ (star z • a)))
Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : ContinuousSMul ℝ E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s : Set E
hs : s ∈ (gaugeSeminormFamily 𝕜 E).basisSets
⊢ 0 ∈ s ∧ IsOpen[inst✝⁷] s ∧ AbsConvex 𝕜 s

Tactic:
SeminormFamily.basisSets_iff

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : ContinuousSMul ℝ E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s : Set E
hs : ∃ i r, 0 < r ∧ s = (i.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r
⊢ 0 ∈ s ∧ IsOpen[inst✝⁷] s ∧ AbsConvex 𝕜 s
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𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
⊢ Continuous[t₁, t𝕜] ⇑φ ↔ ∃ s, Continuous[t₂ s, t𝕜] ⇑φ

Tactic:
simp_rw [WithSeminorms.continuous_iff_continuous_comp (norm_withSeminorms 𝕜 𝕜), forall_const]

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𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
⊢ Continuous[t₁, _] ⇑((normSeminorm 𝕜 𝕜).comp φ) ↔ ∃ s, Continuous[t₂ s, _] ⇑((normSeminorm 𝕜 𝕜).comp φ)
Module: Mathlib.Analysis.LocallyConvex.WeakDual

Goal state before:
pp: case mpr
ι : 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
this : WithSeminorms fun i ↦ (f i).toSeminorm
H : ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm
⊢ Continuous[⨅ i, induced (⇑(f i)) inferInstance, inferInstance] ⇑φ

Tactic:
exact WithSeminorms.continuous_normedSpace_rng _ this _ H

Goal state after:
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 →ₗ[𝕜] 𝕜
⊢ φ ∈ Submodule.span 𝕜 (Set.range f) ↔ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm

Tactic:
let t𝕜 : TopologicalSpace 𝕜 := inferInstance
  let t := ⨅ i, induced (f i) t𝕜
  have : IsTopologicalAddGroup E := topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _
  have : WithSeminorms (fun i ↦ (f i).toSeminorm) := by
    simp_rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf, nhds_iInf, nhds_induced, map_zero,
      ← comap_norm_nhds_zero (E := 𝕜), Filter.comap_comap]
    rfl
  rw [LinearMap.mem_span_iff_continuous]
  constructor <;> intro H
  · rw [WithSeminorms.continuous_iff_continuous_comp (norm_withSeminorms 𝕜 𝕜), forall_const] at H
    rcases Seminorm.bound_of_continuous this _ H with ⟨s, C, -, hC⟩
    exact ⟨s, C, hC⟩
  · exact WithSeminorms.continuous_normedSpace_rng _ this _ H

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
⊢ x ∈ ⇑{ toFun := g, continuous_toFun := ⋯ } ⁻¹' {1}

Tactic:
simp [g, fs _ hx, hu]

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

Goal state before:
pp: A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
⊢ z ∈ Set.range ⇑((gelfandTransform ℂ A) a) ↔ z ∈ spectrum ℂ a

Tactic:
WeakDual.CharacterSpace.mem_spectrum_iff_exists

Goal state after:
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
⊢ z ∈ Set.range ⇑((gelfandTransform ℂ A) a) ↔ ∃ f, f a = z
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst✝²⁸ : CommSemiring R
inst✝²⁷ : CommRing S
inst✝²⁶ : Nontrivial R
inst✝²⁵ : StarRing R
inst✝²⁴ : MetricSpace R
inst✝²³ : IsTopologicalSemiring R
inst✝²² : ContinuousStar R
inst✝²¹ : Algebra R S
inst✝²⁰ : NonUnitalRing A
inst✝¹⁹ : NonUnitalRing B
inst✝¹⁸ : Module S A
inst✝¹⁷ : Module R A
inst✝¹⁶ : Module R B
inst✝¹⁵ : Module S B
inst✝¹⁴ : SMulCommClass R A A
inst✝¹³ : SMulCommClass R B B
inst✝¹² : IsScalarTower R A A
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : StarRing A
inst✝⁹ : StarRing B
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : IsScalarTower R S B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R (A × B) pab
inst✝³ : NonUnitalContinuousFunctionalCalculus R A pa
inst✝² : NonUnitalContinuousFunctionalCalculus R B pb
inst✝¹ : ContinuousMapZero.UniqueHom R A
inst✝ : ContinuousMapZero.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
hf₀ : f 0 = 0
φ : A × B →⋆ₙₐ[S] B := NonUnitalStarAlgHom.snd S A B
⊢ (cfcₙ f (a, b)).2 = (cfcₙ f a, cfcₙ f b).2

Tactic:
exact φ.map_cfcₙ f (a, b) (by rwa [Prod.quasispectrum_eq]) hf₀ continuous_snd hab hb

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
a : A
ha : IsSelfAdjoint a
⊢ a⁻ = 0 ↔ a = a⁺

Tactic:
nth_rw 2 [← posPart_sub_negPart a]

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
a : A
ha : IsSelfAdjoint a
⊢ a⁻ = 0 ↔ a⁺ - a⁻ = a⁺
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
a : A
ha : IsSelfAdjoint a
⊢ a⁺ = 0 ↔ -a = a⁻

Tactic:
nth_rw 2 [← posPart_sub_negPart a]

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
a : A
ha : IsSelfAdjoint a
⊢ a⁺ = 0 ↔ -(a⁺ - a⁻) = a⁻
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace β
x : α
⊢ LipschitzWith 1 fun f ↦ toFun f x

Tactic:
intro f g

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace β
x : α
f g : α →ᵤ β
⊢ edist ((fun f ↦ toFun f x) f) ((fun f ↦ toFun f x) g) ≤ ↑1 * edist f g
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
x : α
hx : x ∈ ⋃₀ 𝔖
⊢ LipschitzWith 1 fun f ↦ (toFun 𝔖) f x

Tactic:
intro f g

Goal state after:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
x : α
hx : x ∈ ⋃₀ 𝔖
f g : α →ᵤ[𝔖] β
⊢ edist ((fun f ↦ (toFun 𝔖) f x) f) ((fun f ↦ (toFun 𝔖) f x) g) ≤ ↑1 * edist f g
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:
by
      cases isEmpty_or_nonempty (⋃₀ 𝔖)
      · simp_all [edist_def]
      have : BddAbove (.range fun x : ⋃₀ 𝔖 ↦ dist (toFun 𝔖 f x) (toFun 𝔖 g x)) := by
        use (Metric.ediam (.univ : Set β)).toReal
        simp +contextual [mem_upperBounds, eq_comm (a := dist _ _), ← edist_dist,
          ← ENNReal.ofReal_le_iff_le_toReal BoundedSpace.bounded_univ.ediam_ne_top,
          Metric.edist_le_ediam_of_mem]
      refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_
      simp [edist_def, ciSup_le_iff this]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst✝³ : Finite ↑𝔖
inst✝² : PseudoMetricSpace β
inst✝¹ : TopologicalSpace α
f g : α →ᵤ[𝔖] β
inst✝ : CompactSpace ↑(⋃₀ 𝔖)
hf : ContinuousOn ((toFun 𝔖) f) (⋃₀ 𝔖)
hg : ContinuousOn ((toFun 𝔖) g) (⋃₀ 𝔖)
⊢ edist { toFun := (⋃₀ 𝔖).domRestrict ((toFun 𝔖) f), continuous_toFun := ⋯ }
      { toFun := (⋃₀ 𝔖).domRestrict ((toFun 𝔖) g), continuous_toFun := ⋯ } =
    edist f g

Tactic:
by
  simp [ContinuousMap.edist_eq_iSup, iSup_subtype, edist_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace β
inst✝¹ : TopologicalSpace α
s : Set α
f g : α →ᵤ[{s}] β
inst✝ : CompactSpace ↑s
hf : ContinuousOn ((toFun {s}) f) s
hg : ContinuousOn ((toFun {s}) g) s
⊢ edist { toFun := s.domRestrict ((toFun {s}) f), continuous_toFun := ⋯ }
      { toFun := s.domRestrict ((toFun {s}) g), continuous_toFun := ⋯ } =
    edist f g

Tactic:
by
  simp [ContinuousMap.edist_eq_iSup, iSup_subtype, edist_def]

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C(↑(σₙ ℂ a), ℂ)₀
⊢ ‖((inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha)) f‖ = ‖f‖

Tactic:
inr_comp_cfcₙHom_eq_cfcₙAux a,

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C(↑(σₙ ℂ a), ℂ)₀
⊢ ‖(cfcₙAux ⋯ a ha) f‖ = ‖f‖
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case a.hx
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✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
x✝ : x ∈ ⊤
⊢ (↑(ℜ x))⁺ ∈ span ℂ {a | 0 ≤ a}

Tactic:
refine subset_span ?_

Goal state after:
case a.hx
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✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
x✝ : x ∈ ⊤
⊢ (↑(ℜ x))⁺ ∈ {a | 0 ≤ a}
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case a.hy
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✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
x✝ : x ∈ ⊤
⊢ (↑(ℜ x))⁻ ∈ span ℂ {a | 0 ≤ a}

Tactic:
refine subset_span ?_

Goal state after:
case a.hy
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✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
x✝ : x ∈ ⊤
⊢ (↑(ℜ x))⁻ ∈ {a | 0 ≤ a}
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case a.hx
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✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
x✝ : x ∈ ⊤
⊢ (↑(ℑ x))⁺ ∈ span ℂ {a | 0 ≤ a}

Tactic:
refine subset_span ?_

Goal state after:
case a.hx
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✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
x✝ : x ∈ ⊤
⊢ (↑(ℑ x))⁺ ∈ {a | 0 ≤ a}
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case a.hy
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✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
x✝ : x ∈ ⊤
⊢ (↑(ℑ x))⁻ ∈ span ℂ {a | 0 ≤ a}

Tactic:
refine subset_span ?_

Goal state after:
case a.hy
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✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
x✝ : x ∈ ⊤
⊢ (↑(ℑ x))⁻ ∈ {a | 0 ≤ a}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : CommSemiring R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun x ↦ f x) (f x) (𝓝[s] x) (spectrum R a)
x✝ : X
hx✝ : x✝ ∈ s
x : X
hx : x ∈ s
⊢ ContinuousOn (f x) (spectrum R a)

Tactic:
exact hf x hx

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

Goal state before:
pp: case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : MetricSpace A
inst✝¹ : Algebra R A
inst✝ : IsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{spectrum R a}] R
hf : f ∈ {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}
g : R →ᵤ[{spectrum R a}] R
hg : g ∈ {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}
⊢ edist { toFun := (spectrum R a).domRestrict ((toFun {spectrum R a}) f), continuous_toFun := ⋯ }
      { toFun := (spectrum R a).domRestrict ((toFun {spectrum R a}) g), continuous_toFun := ⋯ } ≤
    edist f g

Tactic:
edist_continuousRestrict_of_singleton hf hg

Goal state after:
case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : MetricSpace A
inst✝¹ : Algebra R A
inst✝ : IsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{spectrum R a}] R
hf : f ∈ {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}
g : R →ᵤ[{spectrum R a}] R
hg : g ∈ {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}
⊢ edist f g ≤ edist f g
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: 𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
x : ↑{a | p a ∧ spectrum 𝕜 a ⊆ s}
⊢ (cfcHom ⋯) { toFun := (spectrum 𝕜 ↑x).domRestrict f, continuous_toFun := ⋯ } =
    (cfcHom ⋯)
      ({ toFun := s.domRestrict f, continuous_toFun := ⋯ }.comp { toFun := Subtype.map id ⋯, continuous_toFun := ⋯ })

Tactic:
congr!

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 = a ∧ e * a = a

Tactic:
suffices a * e = a from
    ⟨this, by simpa [ha.star_eq, he.isSelfAdjoint.star_eq] using congr(star $this)⟩

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 = a
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: case left
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
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

pp: case right
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
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
all_goals
    refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (A := A) ?_ ?_
    all_goals
      aesop (add safe apply CStarModule.inner_self_nonneg)

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul A (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
x✝ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ ∀ (i : ι), ‖(equiv A ((i : ι) → E i)) x i‖ ≤ ‖x‖

Tactic:
simpa using norm_apply_le_norm x

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

Goal state before:
pp: case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{quasispectrum R a}] R
hf : ContinuousOn ((toFun {quasispectrum R a}) f) (quasispectrum R a)
hf0 : f 0 = 0
g : R →ᵤ[{quasispectrum R a}] R
hg : ContinuousOn ((toFun {quasispectrum R a}) g) (quasispectrum R a)
hg0 : g 0 = 0
⊢ edist
      { toFun := (quasispectrum R a).domRestrict ((toFun {quasispectrum R a}) f), continuous_toFun := ⋯,
          map_zero' := hf0 }.toContinuousMap
      { toFun := (quasispectrum R a).domRestrict ((toFun {quasispectrum R a}) g), continuous_toFun := ⋯,
          map_zero' := hg0 }.toContinuousMap ≤
    edist f g

Tactic:
edist_continuousRestrict_of_singleton hf hg

Goal state after:
case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{quasispectrum R a}] R
hf : ContinuousOn ((toFun {quasispectrum R a}) f) (quasispectrum R a)
hf0 : f 0 = 0
g : R →ᵤ[{quasispectrum R a}] R
hg : ContinuousOn ((toFun {quasispectrum R a}) g) (quasispectrum R a)
hg0 : g 0 = 0
⊢ edist f g ≤ edist f g