mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
A : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
φ ψ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst✝²] ⇑φ
hψ : Continuous[_, inst✝²] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) = ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
⊢ φ = ψ

Tactic:
have (ξ : C(s, ℝ≥0) →⋆ₐ[ℝ≥0] A) (hξ : Continuous ξ) :
        (let ξ' := ξ.realContinuousMapOfNNReal.comp <| ContinuousMap.compStarAlgHom' ℝ ℝ e
        Continuous ξ' ∧ ξ' (.restrict s' <| .id ℝ) = ξ (.restrict s <| .id ℝ≥0)) := by
      intro ξ'
      refine ⟨ξ.continuous_realContinuousMapOfNNReal hξ |>.comp <|
        ContinuousMap.continuous_precomp _, ?_⟩
      exact ξ.realContinuousMapOfNNReal_apply_comp_toReal (.restrict s <| .id ℝ≥0)

Goal state after:
X : Type u_1
inst✝⁶ : TopologicalSpace X
A : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
φ ψ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst✝²] ⇑φ
hψ : Continuous[_, inst✝²] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) = ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this :
  ∀ (ξ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A),
    Continuous[_, inst✝²] ⇑ξ →
      let ξ' := ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e);
      Continuous[_, inst✝²] ⇑ξ' ∧
        ξ' (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) = ξ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
⊢ φ = ψ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
⊢ (↑r • -f).toNNReal = r • (-f).toNNReal

Tactic:
← NNReal.smul_def,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
⊢ (r • -f).toNNReal = r • (-f).toNNReal
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ : ∀ (x : Unitization 𝕜 E), ‖((splitMul 𝕜 E) x).2‖ ≤ ‖((splitMul 𝕜 E) x⋆).2‖
h₂ : ‖((splitMul 𝕜 E) (x⋆ * x)).2‖ = ‖((splitMul 𝕜 E) x).2‖ ^ 2
⊢ max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ * max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ ≤
    max ‖((splitMul 𝕜 E) (x⋆ * x)).1‖ ‖((splitMul 𝕜 E) (x⋆ * x)).2‖

Tactic:
have h₃ : ‖(Unitization.splitMul 𝕜 E (star x * x)).fst‖
        = ‖(Unitization.splitMul 𝕜 E x).fst‖ ^ 2 := by
      simp only [Unitization.splitMul_apply, Unitization.fst_mul, Unitization.fst_star,
        norm_mul, norm_star, sq]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ : ∀ (x : Unitization 𝕜 E), ‖((splitMul 𝕜 E) x).2‖ ≤ ‖((splitMul 𝕜 E) x⋆).2‖
h₂ : ‖((splitMul 𝕜 E) (x⋆ * x)).2‖ = ‖((splitMul 𝕜 E) x).2‖ ^ 2
h₃ : ‖((splitMul 𝕜 E) (x⋆ * x)).1‖ = ‖((splitMul 𝕜 E) x).1‖ ^ 2
⊢ max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ * max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ ≤
    max ‖((splitMul 𝕜 E) (x⋆ * x)).1‖ ‖((splitMul 𝕜 E) (x⋆ * x)).2‖
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)
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R ↑φ
this✝ : Continuous[inst✝¹⁹, inst✝¹³] ⇑ψ
h_spec : quasispectrum R (φ a) ⊆ quasispectrum R a
hψa : q (ψ a)
ι : C(↑(quasispectrum R (ψ a)), ↑(quasispectrum R a))₀ :=
  { toFun := Set.inclusion h_spec, continuous_toFun := ⋯, map_zero' := ⋯ }
this : ψ.comp (cfcₙHom ha) = (cfcₙHom hψa).comp (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι)
⊢ φ (cfcₙ f a) = cfcₙ f (φ a)

Tactic:
by
    have hf' : ContinuousOn f (quasispectrum R (ψ a)) := hf.mono h_spec
    rw [cfcₙ_apply .., cfcₙ_apply ..]
    exact DFunLike.congr_fun this _

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✝²³ : 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✝¹⁵ : Ring B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Algebra R B
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : ContinuousFunctionalCalculus R A p
inst✝⁴ : ContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMap.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst✝¹⁷, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R ↑φ
this : Continuous[inst✝¹⁷, inst✝¹³] ⇑ψ
h_spec : spectrum R (ψ a) ⊆ spectrum R a
hψa : q (ψ a)
ι : C(↑(spectrum R (ψ a)), ↑(spectrum R a)) := { toFun := Set.inclusion h_spec, continuous_toFun := ⋯ }
⊢ (ψ.comp (cfcHom ha)) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) =
    ((cfcHom hψa).comp (ContinuousMap.compStarAlgHom' R R ι))
      (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R))

Tactic:
trans cfcHom hψa (.restrict (spectrum R (ψ a)) (.id R))
    · simp [cfcHom_id]
    · congr

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 : α
γ : Type u_5
inst✝ : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousWithinAt f s x
hi : IsInducing i
h_cl : IsClosed[inst✝¹] (range i)
v : Set β
hv : IsOpen[inst✝¹] v
hu : IsOpen[inst✝] (i ⁻¹' v)
hifu : f x ∩ range i ⊆ v
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ range i ⊆ v

Tactic:
exact hf.inter h_cl |>.forall_isOpen v hv hifu

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
t : Set β
ht : IsClosed[inst✝¹] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : ℕ → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
y₀ : β
h : y₀ ∈ f x₀
hy₀ : y₀ ∈ K
φ : ℕ → ℕ
hφ : StrictMono φ
hyφ : Tendsto (y ∘ φ) atTop (𝓝 y₀)
⊢ (f x₀ ∩ t).Nonempty

Tactic:
exact ⟨y₀, h, ht.closure_eq ▸ mem_closure_of_tendsto hyφ <| .of_forall fun n ↦ (hy _).2⟩

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

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
⊢ ∀ (U : Set β), IsOpen[inst✝] U → IsOpen[TopologicalSpace.vietoris α] {a | a ⊆ f ⁻¹' U}

Tactic:
exact fun U hU => (hU.preimage hf).powerset_vietoris

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

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
⊢ ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[TopologicalSpace.vietoris α] {a | a ⊆ f ⁻¹' F}

Tactic:
exact fun U hU => (hU.preimage hf).powerset_vietoris

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
⊢ IsCompact {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}

Tactic:
refine isCompact_generateFrom rfl fun S hS hKS => ?_

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS : S ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hKS : {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
x : α
hx : x ∈ s
⊢ {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s} = ⋃ n, range '' univ.pi fun x ↦ s

Tactic:
refine subset_antisymm (fun t ht => ?_)
    (iUnion_subset fun _ => image_subset_iff.mpr fun f hf =>
      ⟨range_nonempty _, finite_range _, by grind⟩)

Goal state after:
case inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
x : α
hx : x ∈ s
t : Set α
ht : t ∈ {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s}
⊢ t ∈ ⋃ n, range '' univ.pi fun x ↦ s
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
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑ψ

Tactic:
isometry_inr (𝕜 := 𝕜) |>.isEmbedding.continuous_iff

Goal state after:
𝕜 : 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
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
⊢ Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (Unitization.inr ∘ ⇑ψ)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKV : ↑K ⊆ V
hKu : ∀ U ∈ u, (↑K ∩ U).Nonempty
⊢ ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
    K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
obtain ⟨w, hwB, hwV⟩ := hB.open_eq_sUnion hV

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKV : ↑K ⊆ V
hKu : ∀ U ∈ u, (↑K ∩ U).Nonempty
w : Set (Set α)
hwB : w ⊆ B
hwV : V = ⋃₀ w
⊢ ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
    K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
⊢ ‖cfc f a‖₊ < c

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial A
  · rw [Subsingleton.elim (cfc f a) 0]
    simpa
  · refine cfc_cases (‖·‖₊ < c) a f (by simpa) fun hf ha ↦ ?_
    simp only [← cfc_apply f a, (IsGreatest.nnnorm_cfc_nnreal f a hf ha |>.lt_iff)]
    rintro - ⟨x, hx, rfl⟩
    exact h x hx

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
⊢ ‖φ a‖₊ ≤ ‖a‖₊

Tactic:
have h (ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B) (x : Unitization ℂ A) :
      ‖ψ x‖₊ ≤ ‖x‖₊ := by
    suffices ∀ {s}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊ by
      refine nonneg_le_nonneg_of_sq_le_sq zero_le ?_
      simp_rw [← nnnorm_star_mul_self, ← map_star, ← map_mul]
      exact this <| .star_mul_self x
    intro s hs
    suffices this : spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s by
      rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
        at this
    exact iSup_le_iSup_of_subset (AlgHom.spectrum_apply_subset ψ s)
  simpa [nnnorm_inr] using h (starLift (inrNonUnitalStarAlgHom ℂ B |>.comp (φ : A →⋆ₙₐ[ℂ] B))) a

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ IsPreconnected {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ s}

Tactic:
rw [← isEmbedding_coe.isPreconnected_image]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ IsPreconnected (SetLike.coe '' {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ s})
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
ι : Type u_2
F : ι → α →C₀ β
f : α →C₀ β
l : Filter ι
⊢ Tendsto F l (𝓝 f) ↔ TendstoUniformly (fun i ↦ ⇑(F i)) (⇑f) l

Tactic:
by
  simpa only [Metric.tendsto_nhds] using!
    @BoundedContinuousFunction.tendsto_iff_tendstoUniformly _ _ _ _ _ (fun i => (F i).toBCF)
      f.toBCF l

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

Goal state before:

Tactic:
dist (f x) 0 ≤ dist (g.toBCF x) (f x) + dist (g x) 0 := dist_triangle_left _ _ _
      _ < dist g.toBCF f + ε / 2 := add_lt_add_of_le_of_lt (dist_coe_le_dist x) hx
      _ ≤ ε := by grw [mem_ball.1 hg, add_halves ε]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ Continuous fun p ↦ p.1 ×ˢ p.2

Tactic:
by
  simp_rw [isEmbedding_toCompacts.continuous_iff, Function.comp_def, toCompacts_prod]
  fun_prop

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

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

Tactic:
intro x' hx'
  rw [StrongDual.mem_polar_iff] at hx'
  simp only [mem_closedBall_zero_iff, mem_ball_zero_iff] at *
  have hcr : 0 < ‖c‖ / r := div_pos (zero_lt_one.trans hc) hr
  refine ContinuousLinearMap.opNorm_le_of_shell hr hcr.le hc fun x h₁ h₂ => ?_
  calc
    ‖x' x‖ ≤ 1 := hx' _ h₂
    _ ≤ ‖c‖ / r * ‖x‖ := (inv_le_iff_one_le_mul₀' hcr).1 (by rwa [inv_div])

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ ⇑(RingHom.id 𝕜) ⁻¹' Set.range ⇑f = Set.range ⇑f

Tactic:
exact Set.preimage_id

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case h.refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (⇑g) 0 s
hgt : EqOn (⇑g) 1 t
hicc : ∀ (x : X), 0 ≤ g x ∧ g x ≤ 1
⊢ EqOn (⇑(1 - g)) 0 t

pp: case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (⇑g) 0 s
hgt : EqOn (⇑g) 1 t
hicc : ∀ (x : X), 0 ≤ g x ∧ g x ≤ 1
⊢ EqOn (⇑(1 - g)) 1 s

pp: case h.refine_3
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (⇑g) 0 s
hgt : EqOn (⇑g) 1 t
hicc : ∀ (x : X), 0 ≤ g x ∧ g x ≤ 1
⊢ ∀ (x : X), (1 - g) x ∈ Icc 0 1

Tactic:
· intro x hx
    simp only [ContinuousMap.sub_apply, ContinuousMap.one_apply, Pi.zero_apply]
    exact sub_eq_zero_of_eq (hgt.symm hx)

Goal state after:
case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (⇑g) 0 s
hgt : EqOn (⇑g) 1 t
hicc : ∀ (x : X), 0 ≤ g x ∧ g x ≤ 1
⊢ EqOn (⇑(1 - g)) 1 s

case h.refine_3
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (⇑g) 0 s
hgt : EqOn (⇑g) 1 t
hicc : ∀ (x : X), 0 ≤ g x ∧ g x ≤ 1
⊢ ∀ (x : X), (1 - g) x ∈ Icc 0 1
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ᶜ
n : ℕ
⊢ s ⊆ U n ∩ interior m

Tactic:
exact subset_inter ((hU.subset.trans (iInter_subset U n))) sm

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

Goal state before:
pp: case refine_2
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
φ : ↑(characterSpace 𝕜 C(X, 𝕜))
⊢ ∃ a, (continuousMapEval X 𝕜) a = φ

Tactic:
· obtain ⟨x, hx⟩ := (ideal_isMaximal_iff (RingHom.ker φ)).mp inferInstance
    refine ⟨x, CharacterSpace.ext_ker <| Ideal.ext fun f => ?_⟩
    simpa only [RingHom.mem_ker, continuousMapEval_apply_apply, mem_idealOfSet_compl_singleton,
      RingHom.mem_ker] using SetLike.ext_iff.mp hx f

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case refine_2
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
⊢ s = ⇑{ toFun := g, continuous_toFun := ⋯ } ⁻¹' {1}

Tactic:
apply Subset.antisymm (fun x hx ↦ by simp [g, fs _ hx, hu]) ?_
    apply compl_subset_compl.1
    intro x hx
    obtain ⟨n, hn⟩ : ∃ n, x ∉ U n := by simpa [hU] using hx
    have fnx : f n x = 0 := fm _ (by simp [hn])
    have : g x < 1 := by
      apply lt_of_lt_of_le ?_ hu.le
      exact (S x).tsum_lt_tsum (i := n) (fun i ↦ I i x) (by simp [fnx, u_pos n]) u_sum
    simpa using this.ne

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

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

Tactic:
Unitization.inr_zero,

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x y : A
hxy : IsSelfAdjoint (↑y - ↑x) ∧ SpectrumRestricts (↑y - ↑x) ⇑ContinuousMap.realToNNReal
hyx : IsSelfAdjoint (↑x - ↑y) ∧ SpectrumRestricts (↑x - ↑y) ⇑ContinuousMap.realToNNReal
⊢ ↑(x - y) = 0
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
B : Type u_2
inst✝¹³ : PartialOrder B
inst✝¹² : NonUnitalRing B
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : StarRing B
inst✝⁹ : Module ℝ B
inst✝⁸ : SMulCommClass ℝ B B
inst✝⁷ : IsScalarTower ℝ B B
inst✝⁶ : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝⁴ : IsSemitopologicalRing B
inst✝³ : T2Space B
inst✝² : NonnegSpectrumClass ℝ B
inst✝¹ : NonnegSpectrumClass ℝ (A × B)
inst✝ : StarOrderedRing B
a : A
b : B
x : ℝ≥0
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ (a, b)

Tactic:
Prod.le_def

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
B : Type u_2
inst✝¹³ : PartialOrder B
inst✝¹² : NonUnitalRing B
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : StarRing B
inst✝⁹ : Module ℝ B
inst✝⁸ : SMulCommClass ℝ B B
inst✝⁷ : IsScalarTower ℝ B B
inst✝⁶ : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝⁴ : IsSemitopologicalRing B
inst✝³ : T2Space B
inst✝² : NonnegSpectrumClass ℝ B
inst✝¹ : NonnegSpectrumClass ℝ (A × B)
inst✝ : StarOrderedRing B
a : A
b : B
x : ℝ≥0
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0.1 ≤ (a, b).1 ∧ 0.2 ≤ (a, b).2