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

Goal state before:
pp: case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : p a
f_cont : ContinuousOn f (σₙ R a)
⊢ cfcₙ f a = (cfcₙHom ha) (mkD ((σₙ R a).domRestrict f) 0)

Tactic:
by_cases f_zero : f 0 = 0
    · rw [cfcₙ_apply f a, mkD_of_continuousOn f_cont f_zero]
    · rw [cfcₙ_apply_of_not_map_zero a f_zero, mkD_of_not_zero, map_zero]
      exact f_zero

Goal state after:
Module: Mathlib.Topology.Algebra.StarSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Semiring A
inst✝¹² : StarRing A
inst✝¹¹ : IsSemitopologicalSemiring A
inst✝¹⁰ : ContinuousStar A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : StarRing B
inst✝⁴ : Algebra R B
inst✝³ : T2Space B
F : Type u_4
a : A
inst✝² : FunLike F (↥(elemental R a)) B
inst✝¹ : AlgHomClass F R (↥(elemental R a)) B
inst✝ : StarHomClass F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst✝⁷] ⇑φ
hψ : Continuous[instTopologicalSpaceSubtype, inst✝⁷] ⇑ψ
h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
x : ↥(adjoin R {a})
r : R
⊢ φ ((inclusion ⋯) ((algebraMap R ↥(adjoin R {a})) r)) = ψ ((inclusion ⋯) ((algebraMap R ↥(adjoin R {a})) r))

Tactic:
by
    simp only [AlgHomClass.commutes]

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

Goal state before:
pp: case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : (Subalgebra.comap W (polynomialFunctions I)).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
rw [polynomialFunctions.comap_compRightAlgHom_iccHomeoI] at p

Goal state after:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
n : ℕ
f : C(↑I, E)
⊢ (bernsteinApproximation n f) 0 = f 0

Tactic:
simp [apply, Fin.sum_univ_succ, bernstein_apply, z]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
C : ℝ
hC : ∀ (x y : ↑I), gauge U (f x - f y) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ : ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2
nhds_zero : Tendsto (fun n ↦ C / δ ^ 2 / ↑n) atTop (𝓝 0)
n : ℕ
⊢ C / δ ^ 2 / ↑n < 1 / 2 → n ≠ 0 → ∀ (x : ↑I), gauge U ((bernsteinApproximation n f) x - f x) < 1

Tactic:
nh

Goal state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
C : ℝ
hC : ∀ (x y : ↑I), gauge U (f x - f y) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ : ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2
nhds_zero : Tendsto (fun n ↦ C / δ ^ 2 / ↑n) atTop (𝓝 0)
n : ℕ
nh : C / δ ^ 2 / ↑n < 1 / 2
⊢ n ≠ 0 → ∀ (x : ↑I), gauge U ((bernsteinApproximation n f) x - f x) < 1
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
x z : X
⊢ f z - ε < ↑(h x) z

Tactic:
obtain ⟨y, ym, zm⟩ := Set.exists_set_mem_of_union_eq_top _ _ (ys_w x) z

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
x z y : X
ym : y ∈ ↑(ys x)
zm : z ∈ U x y
⊢ f z - ε < ↑(h x) z
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:

Tactic:
∑ k ∈ Sᶜ, bernstein n k x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ Sᶜ, C * bernstein n k x := by
        simp only [mul_comm (bernstein n _ x)]
        gcongr
        apply hC
      _ = C * ∑ k ∈ Sᶜ, bernstein n k x := by rw [Finset.mul_sum]
      _ ≤ C * ∑ k ∈ Sᶜ, ((x : ℝ) - k/ₙ) ^ 2 / δ ^ 2 * bernstein n k x := by
        gcongr with k hk
        conv_lhs => rw [← one_mul (bernstein _ _ _)]
        gcongr
        simpa [one_le_div₀, hδ₀, sq_le_sq, S, abs_of_pos, ← Real.dist_eq, dist_comm (x : ℝ)]
          using! hk
      -- Again enlarging the sum from `Sᶜ` to all of `Fin (n+1)`
      _ ≤ C * ∑ k : Fin (n + 1), ((x : ℝ) - k/ₙ) ^ 2 / δ ^ 2 * bernstein n k x := by
        gcongr; exact Sᶜ.subset_univ
      _ = C * (∑ k : Fin (n + 1), ((x : ℝ) - k/ₙ) ^ 2 * bernstein n k x) / δ ^ 2 := by
        simp only [← mul_div_right_comm, ← mul_div_assoc, ← Finset.sum_div]
      -- `bernstein.variance` and `x ∈ [0,1]` gives the uniform bound
      _ = C / δ ^ 2 * x * (1 - x) / n := by rw [variance hn₀]; ring
      _ ≤ C / δ ^ 2 * 1 * 1 / n := by gcongr <;> unit_interval
      _ < 1 / 2 := by simpa only [mul_one]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NonUnitalNormedRing E
inst✝⁵ : StarRing E
inst✝⁴ : NormedStarGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : IsScalarTower 𝕜 E E
inst✝¹ : SMulCommClass 𝕜 E E
inst✝ : RegularNormedAlgebra 𝕜 E
a b : E
⊢ ‖((mul 𝕜 E).flip a) b⋆‖ ≤ ‖(mul 𝕜 E).flip a‖ * ‖b‖

Tactic:
simpa only [flip_apply, mul_apply', norm_star] using! le_opNorm ((mul 𝕜 E).flip a) (star b)

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] ((fun x y ↦ (B x) y) ∘ fun p ↦ p.1 + p.2)

Tactic:
refine
    cast (congr_arg _ ?_)
      (((coeFn_continuous B).comp continuous_fst).add ((coeFn_continuous B).comp continuous_snd))

Goal state after:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ (fun x y ↦ (B x) y) ∘ Prod.fst + (fun x y ↦ (B x) y) ∘ Prod.snd = (fun x y ↦ (B x) y) ∘ fun p ↦ p.1 + p.2
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
h : ∀ (x : ℕ → α), Tendsto x atTop (𝓝 x₀) → ∀ y₀ ∈ f x₀, ∃ y, (∀ (n : ℕ), y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)
U : Set β
hU : IsOpen[inst✝¹] U
y₀ : β
hy₀f : y₀ ∈ f x₀
hy₀U : y₀ ∈ U
hc : ¬∀ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ U).Nonempty
⊢ False

Tactic:
rw [Filter.not_eventually] at hc

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
h : ∀ (x : ℕ → α), Tendsto x atTop (𝓝 x₀) → ∀ y₀ ∈ f x₀, ∃ y, (∀ (n : ℕ), y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)
U : Set β
hU : IsOpen[inst✝¹] U
y₀ : β
hy₀f : y₀ ∈ f x₀
hy₀U : y₀ ∈ U
hc : ∃ᶠ (x : α) in 𝓝 x₀, ¬(f x ∩ U).Nonempty
⊢ False
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball x V ⊆ U
s' : Set α
hs' : (s, s').1 ⊆ SetRel.preimage V (s, s').2
⊢ s' ∈ {s | (s ∩ U).Nonempty}

Tactic:
obtain ⟨y, hy, hxy⟩ := hs' hx₁

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball x V ⊆ U
s' : Set α
hs' : (s, s').1 ⊆ SetRel.preimage V (s, s').2
y : α
hy : y ∈ (s, s').2
hxy : (x, y) ∈ V
⊢ s' ∈ {s | (s ∩ U).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ closure[TopologicalSpace.vietoris α] {t | t.Finite ∧ t ⊆ s} ⊆ 𝒫 closure[inst✝] s

Tactic:
rw [isClosed_closure.powerset_vietoris.closure_subset_iff]
    exact fun K ⟨_, h⟩ => h.trans subset_closure

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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
⊢ ‖cfc f a‖ ≤ c

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

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

Goal state before:
pp: case neg
𝕜 : 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
z : 𝕜
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 ↑x
this : CompleteSpace ↥S
⊢ Bornology.IsBounded (connectedComponentIn (σ 𝕜 ↑x)ᶜ z)

Tactic:
suffices connectedComponentIn (σ 𝕜 (x : A))ᶜ z ⊆ σ 𝕜 x from spectrum.isBounded x |>.subset this

Goal state after:
case neg
𝕜 : 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
z : 𝕜
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 ↑x
this : CompleteSpace ↥S
⊢ connectedComponentIn (σ 𝕜 ↑x)ᶜ z ⊆ σ 𝕜 x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Semifield S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalSemiring S
inst✝¹² : ContinuousStar S
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
this : ContinuousFunctionalCalculus R A p
⊢ Isometry ⇑(cfcHom ha)

Tactic:
cfcHom_eq_restrict f ha ha' haf

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Semifield S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalSemiring S
inst✝¹² : ContinuousStar S
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
this : ContinuousFunctionalCalculus R A p
⊢ Isometry ⇑(starAlgHom (cfcHom ha') haf)
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t

Tactic:
have : spectrum ℝ a ⊆ Set.Icc (-t) t := by
    intro x hx
    rw [Set.mem_Icc, ← abs_le, ← Real.norm_eq_abs, ← coe_nnnorm, NNReal.coe_le_coe,
      ← ENNReal.coe_le_coe]
    exact le_iSup₂ (α := ℝ≥0∞) x hx |>.trans ht
  rw [nnreal_iff]
  refine ⟨fun h ↦ iSup₂_le fun x hx ↦ ?_, fun h ↦ ?_⟩
  · rw [← spectrum.singleton_sub_eq] at hx
    obtain ⟨y, hy, rfl⟩ : ∃ y ∈ spectrum ℝ a, ↑t - y = x := by simpa using hx
    obtain ⟨hty, hyt⟩ := Set.mem_Icc.mp <| this hy
    lift y to ℝ≥0 using h y hy
    rw [← NNReal.coe_sub (by exact_mod_cast hyt)]
    simp
  · replace h : ∀ x ∈ spectrum ℝ a, ‖t - x‖₊ ≤ t := by
      simpa [spectralRadius, iSup₂_le_iff, ← spectrum.singleton_sub_eq] using h
    peel h with x hx h_le
    rw [← NNReal.coe_le_coe, coe_nnnorm, Real.norm_eq_abs, abs_le] at h_le
    linarith [h_le.2]

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this : Fintype ↑u := hu'.fintype
⊢ (univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}) ⊆
    {a | ↑(Finset.univ.sup a) ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑(Finset.univ.sup a) ∩ U).Nonempty) ∧ (↑(Finset.univ.sup a)).Finite}

Tactic:
coe_finset_sup,

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this : Fintype ↑u := hu'.fintype
⊢ (univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}) ⊆
    {a |
      (Finset.univ.sup fun i ↦ ↑(a i)) ⊆ ⋃₀ u ∧
        (∀ U ∈ u, ((Finset.univ.sup fun i ↦ ↑(a i)) ∩ U).Nonempty) ∧ (Finset.univ.sup fun i ↦ ↑(a i)).Finite}
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
h : (absConvexHull 𝕜) s = ∅
⊢ s = ∅

Tactic:
← Set.subset_empty_iff,

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
h : (absConvexHull 𝕜) s = ∅
⊢ s ⊆ ∅
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : LocallyConvexSpace 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : FirstCountableTopology E
⊢ ∃ x,
    (𝓝 0).HasAntitoneBasis x ∧
      ∀ (n : ℕ),
        IsOpen[inst✝⁵] (x n) ∧ AbsConvex 𝕜 (x n) ∧ x (n + 1) + x (n + 1) ⊆ x n ∧ closure[inst✝⁵] (x (n + 1)) ⊆ x n

Tactic:
obtain ⟨u, hu_basis, -⟩ := IsTopologicalAddGroup.exists_antitone_basis_nhds_zero E

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : LocallyConvexSpace 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : FirstCountableTopology E
u : ℕ → Set E
hu_basis : (𝓝 0).HasAntitoneBasis u
⊢ ∃ x,
    (𝓝 0).HasAntitoneBasis x ∧
      ∀ (n : ℕ),
        IsOpen[inst✝⁵] (x n) ∧ AbsConvex 𝕜 (x n) ∧ x (n + 1) + x (n + 1) ⊆ x n ∧ closure[inst✝⁵] (x (n + 1)) ⊆ x n
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
h_deriv₂ :
  ∀ (a b : A),
    deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 = a ^ 2 + 2 • (a * b) + b ^ 2
h₄ : a ^ 2 + 2 • (-a * star a) + star a ^ 2 = star a ^ 2 + 2 • (star a * -a) + a ^ 2
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))
h₃ :
  deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    a ^ 2 + 2 • (-a * star a) + star a ^ 2
⊢ star a * a = a * star a

Tactic:
apply nsmul_right_injective two_ne_zero

Goal state after:
case refine_2
A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := ⋯
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
h_deriv₂ :
  ∀ (a b : A),
    deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 = a ^ 2 + 2 • (a * b) + b ^ 2
h₄ : a ^ 2 + 2 • (-a * star a) + star a ^ 2 = star a ^ 2 + 2 • (star a * -a) + a ^ 2
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))
h₃ :
  deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    a ^ 2 + 2 • (-a * star a) + star a ^ 2
⊢ (fun a ↦ 2 • a) (star a * a) = (fun a ↦ 2 • a) (a * star a)
Module: Mathlib.Analysis.Normed.Module.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
fr : Dual ℝ E
p : Seminorm 𝕜 E
hp : ∀ (x : E), |fr x| ≤ p x
x : E
hx : ¬fr.extendRCLike x = 0
⊢ ‖(starRingEnd 𝕜) (fr.extendRCLike x)‖ * p x = ‖fr.extendRCLike x‖ * p x

Tactic:
norm_conj

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
fr : Dual ℝ E
p : Seminorm 𝕜 E
hp : ∀ (x : E), |fr x| ≤ p x
x : E
hx : ¬fr.extendRCLike x = 0
⊢ ‖fr.extendRCLike x‖ * p x = ‖fr.extendRCLike x‖ * p x
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhds : s ∈ 𝓝 0
⊢ IsBounded (polar 𝕜 s)

Tactic:
obtain ⟨a, ha⟩ : ∃ a : 𝕜, 1 < ‖a‖ := NormedField.exists_one_lt_norm 𝕜
  obtain ⟨r, r_pos, r_ball⟩ : ∃ r : ℝ, 0 < r ∧ ball 0 r ⊆ s := Metric.mem_nhds_iff.1 s_nhds
  exact isBounded_closedBall.subset
    (((topDualPairing 𝕜 E).flip.polar_antitone r_ball).trans <|
      polar_ball_subset_closedBall_div ha r_pos)

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f ((lineMap a b) r) ≤ (lineMap (f a) (f b)) r ↔ slope f a ((lineMap a b) r) ≤ slope f a b

Tactic:
lineMap_apply,

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r • (b -ᵥ a) +ᵥ a) ≤ (lineMap (f a) (f b)) r ↔ slope f a (r • (b -ᵥ a) +ᵥ a) ≤ slope f a b
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r • (b -ᵥ a) +ᵥ a) ≤ (lineMap (f a) (f b)) r ↔ slope f a (r • (b -ᵥ a) +ᵥ a) ≤ slope f a b

Tactic:
lineMap_apply,

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔ slope f a (r • (b -ᵥ a) +ᵥ a) ≤ slope f a b
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r * (b - a) + a) ≤ r • (f b - f a) + f a ↔
    (r * (b - a))⁻¹ • f (r * (b - a) + a) ≤ (b - a)⁻¹ • (f b - f a + r⁻¹ • f a)

Tactic:
inv_smul_le_iff_of_pos h,

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r * (b - a) + a) ≤ r • (f b - f a) + f a ↔
    f (r * (b - a) + a) ≤ (r * (b - a)) • (b - a)⁻¹ • (f b - f a + r⁻¹ • f a)