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

Goal state before:
pp: case h₂
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.1 • y.ofLp.toProd.2 + (y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2)‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
      (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)

Tactic:
· apply (norm_add_le _ _).trans
      gcongr
      · simp [norm_smul]
      · apply (norm_add_le _ _).trans
        gcongr
        · simp [norm_smul, mul_comm]
        · exact norm_mul_le _ _

Goal state after:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: A : Type u_1
inst✝⁴ : Semiring A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : T2Space A
s : Set ℝ
inst✝ : CompactSpace ↑s
φ ψ : C(↑s, ℝ) →ₐ[ℝ] A
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ (polynomialFunctions s).topologicalClosure ≤ φ.equalizer ψ

Tactic:
exact Subalgebra.topologicalClosure_minimal
    (polynomialFunctions.le_equalizer s φ ψ h) (isClosed_eq hφ hψ)

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁹ : CommSemiring R
inst✝²⁸ : Nontrivial R
inst✝²⁷ : StarRing R
inst✝²⁶ : MetricSpace R
inst✝²⁵ : IsTopologicalSemiring R
inst✝²⁴ : ContinuousStar R
inst✝²³ : CommRing S
inst✝²² : Algebra R S
inst✝²¹ : NonUnitalRing A
inst✝²⁰ : StarRing A
inst✝¹⁹ : TopologicalSpace A
inst✝¹⁸ : Module R A
inst✝¹⁷ : IsScalarTower R A A
inst✝¹⁶ : SMulCommClass R A A
inst✝¹⁵ : NonUnitalRing B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Module R B
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : SMulCommClass R B B
inst✝⁹ : Module S A
inst✝⁸ : Module S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus R A p
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMapZero.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst✝¹⁹, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
⊢ φ (cfcₙ f a) = cfcₙ f (φ a)

Tactic:
by
  let ψ : A →⋆ₙₐ[R] B := (φ : A →⋆ₙₐ[S] B).restrictScalars R
  have : Continuous ψ := hφ
  have h_spec := NonUnitalAlgHom.quasispectrum_apply_subset' (R := R) S φ a
  have hψa : q (ψ a) := hφa
  let ι : C(quasispectrum R (ψ a), quasispectrum R a)₀ :=
    ⟨⟨Set.inclusion h_spec, continuous_id.subtype_map h_spec⟩, rfl⟩
  suffices ψ.comp (cfcₙHom ha) =
      (cfcₙHom hψa).comp (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι) by
    have hf' : ContinuousOn f (quasispectrum R (ψ a)) := hf.mono h_spec
    rw [cfcₙ_apply .., cfcₙ_apply ..]
    exact DFunLike.congr_fun this _
  refine ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id _ _ _ ?_ ?_ ?apply_id
  case apply_id =>
    trans cfcₙHom hψa (.id (quasispectrum R (ψ a)))
    · simp [cfcₙHom_id]
    · congr
  all_goals
    dsimp [ContinuousMapZero.nonUnitalStarAlgHom_precomp]
    fun_prop

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
x : α
hf : UpperHemicontinuousWithinAt f s x
u : Set β
hu : IsClosed[inst✝] u
⊢ UpperHemicontinuousWithinAt (fun x ↦ f x ∩ u) s x

Tactic:
rw [upperHemicontinuousWithinAt_iff_forall_isOpen] at hf ⊢

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
x : α
hf : ∀ (u : Set β), IsOpen[inst✝] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
u : Set β
hu : IsClosed[inst✝] u
⊢ ∀ (u_1 : Set β), IsOpen[inst✝] u_1 → f x ∩ u ⊆ u_1 → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ u ⊆ u_1
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
hf : UpperHemicontinuous f
u : Set β
hu : IsClosed[inst✝] u
⊢ UpperHemicontinuous fun x ↦ f x ∩ u

Tactic:
rw [upperHemicontinuous_iff] at hf ⊢

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
hf : ∀ (x : α), UpperHemicontinuousAt f x
u : Set β
hu : IsClosed[inst✝] u
⊢ ∀ (x : α), UpperHemicontinuousAt (fun x ↦ f x ∩ u) x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
γ : Type u_5
inst✝ : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuous f
hi : IsInducing i
h_cl : IsClosed[inst✝¹] (range i)
⊢ UpperHemicontinuous fun x ↦ i ⁻¹' f x

Tactic:
rw [upperHemicontinuous_iff] at hf ⊢

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
γ : Type u_5
inst✝ : TopologicalSpace γ
i : γ → β
hf : ∀ (x : α), UpperHemicontinuousAt f x
hi : IsInducing i
h_cl : IsClosed[inst✝¹] (range i)
⊢ ∀ (x : α), UpperHemicontinuousAt (fun x ↦ i ⁻¹' f x) x
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case right
α : Type u_1
inst✝ : UniformSpace α
⊢ IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {∅}

Tactic:
simp_rw [isOpen_iff_mem_nhds, Set.mem_singleton_iff, forall_eq, nhds_eq_uniformity]
    filter_upwards [Filter.mem_lift' <| Filter.mem_lift' Filter.univ_mem] with F ⟨_, hF⟩
    simpa using hF

Goal state after:
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) \ σ 𝕜 ↑x ∪ frontier (σ 𝕜 x) \ σ 𝕜 ↑x)

Tactic:
sdiff_eq_empty.mpr (frontier_spectrum S x),

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 ∪ ∅)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: case right.right
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module ℝ A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ cfcₙ (fun x ↦ √x * √x) a = a

Tactic:
nth_rw 2 [← cfcₙ_id ℝ a]

Goal state after:
case right.right
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module ℝ A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ cfcₙ (fun x ↦ √x * √x) a = cfcₙ id a
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: A : Type u_2
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : CompleteSpace A
h₂ : IsClosed (range NNReal.toReal)
h₁ : IsInducing NNReal.toReal
⊢ UpperHemicontinuous (quasispectrum ℝ≥0)

Tactic:
simpa [← NNReal.algebraMap_eq_coe] using
    upperHemicontinuous_quasispectrum ℝ A |>.isInducing_comp h₁ h₂

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
⊢ HasDerivAt (resolvent a) (-resolvent a k ^ 2) k

Tactic:
have H₁ : HasFDerivAt Ring.inverse _ (algebraMap 𝕜 A k - a) :=
    hasFDerivAt_ringInverse (𝕜 := 𝕜) hk.unit

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
H₁ :
  HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 A) ↑(IsUnit.unit hk)⁻¹) ↑(IsUnit.unit hk)⁻¹)
    ((algebraMap 𝕜 A) k - a)
⊢ HasDerivAt (resolvent a) (-resolvent a k ^ 2) k
Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
⊢ HasFDerivAt (fun x ↦ resolvent x k) (((ContinuousLinearMap.mulLeftRight 𝕜 A) (resolvent a k)) (resolvent a k)) a

Tactic:
have H₁ : HasFDerivAt Ring.inverse _ (algebraMap 𝕜 A k - a) :=
    hasFDerivAt_ringInverse (𝕜 := 𝕜) hk.unit

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
H₁ :
  HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 A) ↑(IsUnit.unit hk)⁻¹) ↑(IsUnit.unit hk)⁻¹)
    ((algebraMap 𝕜 A) k - a)
⊢ HasFDerivAt (fun x ↦ resolvent x k) (((ContinuousLinearMap.mulLeftRight 𝕜 A) (resolvent a k)) (resolvent a k)) a
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
x✝ : ℂ
⊢ x✝ ∈ {z | z.im < 0} → x✝ ∈ {z | z.im ≤ 0}

Tactic:
simpa using le_of_lt

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
x✝ : ℂ
⊢ x✝ ∈ {z | 0 < z.im} → x✝ ∈ {z | 0 ≤ z.im}

Tactic:
simpa using le_of_lt

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 := ⋯ }
⊢ ‖((↑(ContinuousMap.compStarAlgHom' 𝕜 𝕜 { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
          ContinuousMapZero.toContinuousMapHom)
        f‖ =
    ‖f‖

Tactic:
change ‖(f : C(σₙ 𝕜 a, 𝕜)).comp ι‖ = ‖(f : C(σₙ 𝕜 a, 𝕜))‖

Goal state after:
𝕜 : 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 := ⋯ }
⊢ ‖(↑f).comp ι‖ = ‖↑f‖
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
h : LocallyConnectedSpace (NonemptyCompacts α)
x : α
U : Set α
x✝ : x ∈ U ∧ IsOpen[inst✝] U
hx : x ∈ U
hU : IsOpen[inst✝] U
V : Set (NonemptyCompacts α)
hV₁ : IsOpen V
hV₂ : IsPreconnected V
hxV : {x} ∈ V
hKV : V ⊆ {K | ↑K ⊆ U}
⊢ ⋃ L ∈ V, ↑L ∈ 𝓝 x

Tactic:
filter_upwards [continuous_singleton.tendsto x (hV₁.mem_nhds hxV)] with y hy

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
h : LocallyConnectedSpace (NonemptyCompacts α)
x : α
U : Set α
x✝ : x ∈ U ∧ IsOpen[inst✝] U
hx : x ∈ U
hU : IsOpen[inst✝] U
V : Set (NonemptyCompacts α)
hV₁ : IsOpen V
hV₂ : IsPreconnected V
hxV : {x} ∈ V
hKV : V ⊆ {K | ↑K ⊆ U}
y : α
hy : y ∈ (fun x ↦ {x}) ⁻¹' V
⊢ y ∈ ⋃ L ∈ V, ↑L
Module: Mathlib.Analysis.Normed.Operator.Completeness

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup Fₗ
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f✝ g : E →SL[σ₁₂] F
E' : Type u_6
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : RingHomIsometric σ₁₂
f : E' → F
s : Set (E' →SL[σ₁₂] F)
hs : Bornology.IsBounded s
hf : f ∈ closure[Pi.topologicalSpace] (DFunLike.coe '' s)
⊢ E' →SL[σ₁₂] F

Tactic:
refine (linearMapOfMemClosureRangeCoe f ?_).mkContinuousOfExistsBound ?_
  · refine closure_mono (image_subset_iff.2 fun g _ => ?_) hf
    exact ⟨g, rfl⟩
  · -- We need to show that `f` has bounded norm. Choose `C` such that `‖g‖ ≤ C` for all `g ∈ s`.
    rcases isBounded_iff_forall_norm_le.1 hs with ⟨C, hC⟩
    -- Then `‖g x‖ ≤ C * ‖x‖` for all `g ∈ s`, `x : E`, hence `‖f x‖ ≤ C * ‖x‖` for all `x`.
    have : ∀ x, IsClosed { g : E' → F | ‖g x‖ ≤ C * ‖x‖ } := fun x =>
      isClosed_Iic.preimage (@continuous_apply E' (fun _ => F) _ x).norm
    refine ⟨C, fun x => (this x).closure_subset_iff.2 (image_subset_iff.2 fun g hg => ?_) hf⟩
    exact g.le_of_opNorm_le (hC _ hg) _

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

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

Tactic:
simp only [approx, midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul, ← div_eq_inv_mul]

Goal state after:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ 1
c : CU P
⊢ (approx n c.left x + approx n c.right x) / 2 ≤ 1
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ 1
c : CU P
this : approx n c.left x + approx n c.right x ≤ 1 + 1
⊢ (approx n c.left x + approx n c.right x) / 2 ≤ 1

Tactic:
norm_num at this

Goal state after:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ 1
c : CU P
this : approx n c.left x + approx n c.right x ≤ 2
⊢ (approx n c.left x + approx n c.right x) / 2 ≤ 1
Module: Mathlib.Analysis.Normed.Module.WeakDual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SeparableSpace E
inst✝ : ProperSpace 𝕜
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
hc : IsClosed s
⊢ IsSeqCompact s

Tactic:
have b_isCompact' : CompactSpace s :=
    isCompact_iff_compactSpace.mp <| isCompact_of_bounded_of_closed hb hc

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SeparableSpace E
inst✝ : ProperSpace 𝕜
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
hc : IsClosed s
b_isCompact' : CompactSpace ↑s
⊢ IsSeqCompact s
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ f ∈ idealOfSet R s ↔ ∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0

Tactic:
by
  convert! Iff.rfl

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : (i : ι) → NonUnitalRing (A i)
inst✝⁹ : (i : ι) → Module S (A i)
inst✝⁸ : (i : ι) → Module R (A i)
inst✝⁷ : ∀ (i : ι), IsScalarTower R S (A i)
inst✝⁶ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R (A i) (A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMapZero.UniqueHom R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ i, quasispectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
hf₀ : f 0 = 0
i : ι
this : Nonempty ι
φ : ((i : ι) → A i) →⋆ₙₐ[S] A i := Pi.evalNonUnitalStarAlgHom S A i
⊢ ContinuousOn f (quasispectrum R a)

Tactic:
Pi.quasispectrum_eq

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : (i : ι) → NonUnitalRing (A i)
inst✝⁹ : (i : ι) → Module S (A i)
inst✝⁸ : (i : ι) → Module R (A i)
inst✝⁷ : ∀ (i : ι), IsScalarTower R S (A i)
inst✝⁶ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R (A i) (A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMapZero.UniqueHom R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ i, quasispectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
hf₀ : f 0 = 0
i : ι
this : Nonempty ι
φ : ((i : ι) → A i) →⋆ₙₐ[S] A i := Pi.evalNonUnitalStarAlgHom S A i
⊢ ContinuousOn f (⋃ i, quasispectrum R (a i))
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
⊢ a⁻ = -a ↔ a ≤ 0

Tactic:
by
  rw [← neg_inj, neg_neg, eq_comm]
  refine ⟨fun ha ↦ by rw [ha, neg_nonpos]; exact negPart_nonneg a, fun ha ↦ ?_⟩
  rw [← neg_nonneg] at ha
  rw [negPart_def, ← cfcₙ_neg]
  have _ : IsSelfAdjoint a := neg_neg a ▸ (IsSelfAdjoint.neg <| .of_nonneg ha)
  conv_lhs => rw [← cfcₙ_id ℝ a]
  refine cfcₙ_congr fun x hx ↦ ?_
  rw [Unitization.quasispectrum_eq_spectrum_inr ℝ, ← neg_neg x, ← Set.mem_neg,
    spectrum.neg_eq, ← Unitization.inr_neg, ← Unitization.quasispectrum_eq_spectrum_inr ℝ] at hx
  rw [← neg_eq_iff_eq_neg, eq_comm]
  simpa using quasispectrum_nonneg_of_nonneg _ ha _ hx

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

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

Tactic:
have hs : CompactSpace s := by
    refine isCompact_iff_compactSpace.mp <| (IsCompact.union ?_ ?_).union ?_
    all_goals exact isCompact_quasispectrum _

Goal state after:
A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : Module ℝ A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
⊢ a⁺ = b
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
s : Set γ
h : ∀ (c : α), LipschitzOnWith K (f c) s
⊢ UniformContinuousOn (⇑ofFun ∘ Function.swap f) s

Tactic:
rw [← lipschitzOnWith_ofFun_iff] at h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
s : Set γ
h : LipschitzOnWith K (fun x ↦ ofFun fun c ↦ f c x) s
⊢ UniformContinuousOn (⇑ofFun ∘ Function.swap f) s
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
ha : IsStrictlyPositive a
ax : Aˣ
hax : ↑ax = a
⊢ Ring.inverse a = a ^ (-1)

Tactic:
simp only [← hax, Ring.inverse_invertible, invOf_units, CFC.rpow_neg_one_eq_inv ax]

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, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖

Tactic:
gcongr <;> exact norm_inner_le E

Goal state after:
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‖

Tactic:
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: 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:
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.ApproximateUnit

Goal state before:
pp: case funProp.discharger
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : 0 ≤ c
⊢ ∀ x ∈ σ ℝ≥0 ↑?a, x ≠ 0

Tactic:
intro _ _

Goal state after:
case funProp.discharger
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : 0 ≤ c
x✝ : ℝ≥0
a✝ : x✝ ∈ σ ℝ≥0 ↑?a
⊢ x✝ ≠ 0