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 : α → NonemptyCompacts β
g : α → β → γ
hf : Continuous[inst✝², _] f
hg : Continuous[instTopologicalSpaceProd, inst✝] (Function.uncurry g)
⊢ Continuous[inst✝², _] fun x ↦ NonemptyCompacts.map (g x) ⋯ (f x)

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

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

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x ↦ r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ ((1 + r) / 2) • y + ((1 - r) / 2) • -y = (fun x ↦ r • x) y

Tactic:
smul_neg,

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x ↦ r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ ((1 + r) / 2) • y + -(((1 - r) / 2) • y) = (fun x ↦ r • x) y
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖
le : ∀ z ∈ s, ‖c⁻¹ • x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s

Tactic:
have cancel : ‖c⁻¹‖ * ‖c‖ = 1 := by
    simp only [c_zero, norm_eq_zero, Ne, not_false_iff, inv_mul_cancel₀, norm_inv]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖
le : ∀ z ∈ s, ‖c⁻¹ • x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
cancel : ‖c⁻¹‖ * ‖c‖ = 1
⊢ c⁻¹ • x' ∈ polar 𝕜 s
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (ball 0 r) = closedBall 0 r⁻¹

Tactic:
by
  let : NormedSpace ℝ E := .restrictScalars ℝ 𝕜 E
  rw [← polar_closedBall hr, ← closure_ball _ hr.ne', polar_closure]

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 →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
this✝ : IsTopologicalAddGroup E
this : WithSeminorms fun i ↦ (f i).toSeminorm
⊢ Continuous[⨅ i, induced (⇑(f i)) inferInstance, inferInstance] ⇑φ ↔
    ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm

Tactic:
constructor <;> intro H

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

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] ⇑φ
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), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ midpoint ℝ 0 0 = 0

pp: case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ x ∈ c.right.C

pp: case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ x ∈ c.left.C

Tactic:
midpoint_self

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), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ 0 = 0

case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ x ∈ c.right.C

case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ x ∈ c.left.C
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), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ midpoint ℝ 1 1 = 1

pp: case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ x ∉ c.right.U

pp: case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ x ∉ c.left.U

Tactic:
midpoint_self

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), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ 1 = 1

case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ x ∉ c.right.U

case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ x ∉ c.left.U
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' * (a - b) + b) ≤ r' • -(f b - f a) + f b ↔ f (r' * (a - b) + b) ≤ f b - r' • (f b - f a)

pp: case h
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)
⊢ b - a ≠ 0

Tactic:
smul_neg,

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' * (a - b) + b) ≤ -(r' • (f b - f a)) + f b ↔ f (r' * (a - b) + b) ≤ f b - r' • (f b - f a)

case h
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)
⊢ b - a ≠ 0
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : g x ≠ 0
this : ∀ᶠ (z : X) in nhds x, g z ≠ 0
a✝ : X
⊢ (algebraMap ℝ≥0 𝕜) ‖g a✝‖₊ ^ 2 = (starRingEnd 𝕜) (g a✝) * g a✝

Tactic:
simp only [RCLike.conj_mul]

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : g x ≠ 0
this : ∀ᶠ (z : X) in nhds x, g z ≠ 0
a✝ : X
⊢ (algebraMap ℝ≥0 𝕜) ‖g a✝‖₊ ^ 2 = ↑‖g a✝‖ ^ 2
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
this : spectralRadius ℂ ((gelfandTransform ℂ A) (star a * a)) = spectralRadius ℂ (star a * a)
⊢ ‖(gelfandTransform ℂ A) a‖ = ‖a‖

Tactic:
map_mul,

Goal state after:
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
this : spectralRadius ℂ ((gelfandTransform ℂ A) (star a) * (gelfandTransform ℂ A) a) = spectralRadius ℂ (star a * a)
⊢ ‖(gelfandTransform ℂ A) a‖ = ‖a‖
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
⊢ ∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
rcases h's.eq_iInter_nat with ⟨U, U_open, hU⟩
  obtain ⟨m, m_comp, -, sm, mt⟩ : ∃ m, IsCompact m ∧ IsClosed m ∧ s ⊆ interior m ∧ m ⊆ tᶜ :=
    exists_compact_closed_between hs ht.isOpen_compl hd.symm.subset_compl_left
  have A n : ∃ f : C(X, ℝ), EqOn f 1 s ∧ EqOn f 0 (U n ∩ interior m)ᶜ ∧ HasCompactSupport f
      ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := by
    apply exists_continuous_one_zero_of_isCompact hs
      ((U_open n).inter isOpen_interior).isClosed_compl
    rw [disjoint_compl_right_iff_subset]
    exact subset_inter ((hU.subset.trans (iInter_subset U n))) sm
  choose f fs fm _hf f_range using A
  obtain ⟨u, u_pos, u_sum, hu⟩ : ∃ (u : ℕ → ℝ), (∀ i, 0 < u i) ∧ Summable u ∧ ∑' i, u i = 1 :=
    ⟨fun n ↦ 1/2/2^n, fun n ↦ by positivity, summable_geometric_two' 1, tsum_geometric_two' 1⟩
  let g : X → ℝ := fun x ↦ ∑' n, u n * f n x
  have hgmc : EqOn g 0 mᶜ := by
    intro x hx
    have B n : f n x = 0 := by
      have : mᶜ ⊆ (U n ∩ interior m)ᶜ := by
        simpa using inter_subset_right.trans interior_subset
      exact fm n (this hx)
    simp [g, B]
  have I n x : u n * f n x ≤ u n := mul_le_of_le_one_right (u_pos n).le (f_range n x).2
  have S x : Summable (fun n ↦ u n * f n x) := Summable.of_nonneg_of_le
      (fun n ↦ mul_nonneg (u_pos n).le (f_range n x).1) (fun n ↦ I n x) u_sum
  refine ⟨⟨g, ?_⟩, ?_, hgmc.mono (subset_compl_comm.mp mt), ?_, fun x ↦ ⟨?_, ?_⟩⟩
  · apply continuous_tsum (fun n ↦ by fun_prop) u_sum (fun n x ↦ ?_)
    simpa [abs_of_nonneg, (u_pos n).le, (f_range n x).1] using I n x
  · 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
  · exact HasCompactSupport.of_support_subset_isCompact m_comp
      (Function.support_subset_iff'.mpr hgmc)
  · exact tsum_nonneg (fun n ↦ mul_nonneg (u_pos n).le (f_range n x).1)
  · apply le_trans _ hu.le
    exact (S x).tsum_le_tsum (fun n ↦ I n x) u_sum

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
⊢ 𝓤 (α →ᵤ β) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
suffices 𝓤 (α →ᵤ β) = comap (fun x ↦ edist x.1 x.2) (𝓝 0) by
      simp [this, ENNReal.nhds_zero_basis.comap _ |>.eq_biInf, Set.Iio]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
⊢ 𝓤 (α →ᵤ β) = comap (fun x ↦ edist x.1 x.2) (𝓝 0)
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}

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}

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}

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:
all_goals
    refine subset_span ?_
    first | apply CFC.negPart_nonneg | apply CFC.posPart_nonneg

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

Goal state before:
pp: case mpr.mem
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p s : A
⊢ IsSelfAdjoint ((fun s ↦ star s * s) s) ∧ QuasispectrumRestricts ((fun s ↦ star s * s) s) ⇑ContinuousMap.realToNNReal

Tactic:
refine ⟨IsSelfAdjoint.star_mul_self s, ?_⟩

Goal state after:
case mpr.mem
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p s : A
⊢ QuasispectrumRestricts ((fun s ↦ star s * s) s) ⇑ContinuousMap.realToNNReal
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.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✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : ContinuousStar A
inst✝ : CompleteSpace A
r : ℝ
a : A
ha : a ∈ {a | IsStrictlyPositive a}
⊢ spectrum ℝ≥0 (id a) ⊆ {0}ᶜ

Tactic:
by simpa using spectrum.zero_notMem _ ha.isUnit

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ‖cfcₙ (fun x ↦ x) a‖ ≤ max ‖a⁺‖ ‖a⁻‖

Tactic:
rw [norm_cfcₙ_le_iff ..]

Goal state after:
A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ∀ x ∈ quasispectrum ℝ a, ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : x ∈ {a | 0 ≤ a}
⊢ x ∈ ↑(span ℂ ({x | 0 ≤ x} ∩ Metric.closedBall 0 r))

Tactic:
obtain (rfl | hx_pos) := eq_zero_or_norm_pos x

Goal state after:
case inl
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
hx : 0 ∈ {a | 0 ≤ a}
⊢ 0 ∈ ↑(span ℂ ({x | 0 ≤ x} ∩ Metric.closedBall 0 r))

case inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : x ∈ {a | 0 ≤ a}
hx_pos : 0 < ‖x‖
⊢ x ∈ ↑(span ℂ ({x | 0 ≤ x} ∩ Metric.closedBall 0 r))
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: A : Type u_2
inst✝¹⁰ : NormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedAlgebra ℝ A
inst✝⁷ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁶ : ContinuousStar A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : CompleteSpace A
s : Set ℝ≥0
x✝¹ : (ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0) × A
f : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a : A
x✝ : (f, a) ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (spectrum ℝ≥0 a)}
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s}
ha : 0 ≤ (f, a).2
has : s ∈ 𝓝ˢ (spectrum ℝ≥0 (f, a).2)
hs : IsCompact (spectrum ℝ≥0 a)
k : Set ℝ≥0
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (spectrum ℝ≥0 a)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (spectrum ℝ≥0 x)}
⊢ ContinuousOn (fun fa ↦ cfc ((toFun {k}) ((ofFun {k}) ((toFun {t | IsCompact t ∧ t ⊆ s}) fa.1))) fa.2)
    ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (spectrum ℝ≥0 a)} ∩
      Set.univ ×ˢ {x | k ∈ 𝓝ˢ (spectrum ℝ≥0 x)})

Tactic:
refine continuousOn_cfc_nnreal_setProd hk |>.comp'
    (uniformContinuous_ofFun_toFun_of_mem _ {t | IsCompact t ∧ t ⊆ s} _ ⟨hk, hks⟩ |>.prodMap
      uniformContinuous_id).continuous.continuousOn ?_

Goal state after:
A : Type u_2
inst✝¹⁰ : NormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedAlgebra ℝ A
inst✝⁷ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁶ : ContinuousStar A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : CompleteSpace A
s : Set ℝ≥0
x✝¹ : (ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0) × A
f : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a : A
x✝ : (f, a) ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (spectrum ℝ≥0 a)}
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s}
ha : 0 ≤ (f, a).2
has : s ∈ 𝓝ˢ (spectrum ℝ≥0 (f, a).2)
hs : IsCompact (spectrum ℝ≥0 a)
k : Set ℝ≥0
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (spectrum ℝ≥0 a)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (spectrum ℝ≥0 x)}
⊢ Set.MapsTo (fun fa ↦ fa)
    ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (spectrum ℝ≥0 a)} ∩
      Set.univ ×ˢ {x | k ∈ 𝓝ˢ (spectrum ℝ≥0 x)})
    ({f | ContinuousOn ((toFun {k}) f) k} ×ˢ {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ k})
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: case e_a.e_a
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun y ↦ 1 - (1 + y)⁻¹
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
⊢ cfc 1 m - cfc g (ε⁻¹ ^ 2 • m) = cfc (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) m

Tactic:
← cfc_comp_smul _ _ _ hg.continuousOn hm₁,

Goal state after:
case e_a.e_a
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun y ↦ 1 - (1 + y)⁻¹
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
⊢ cfc 1 m - cfc (fun x ↦ g (ε⁻¹ ^ 2 • x)) m = cfc (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) m
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : Algebra 𝕜 A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarModule 𝕜 A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : ContinuousStar A
a : A
ha : p a
⊢ ↑(cfcHom ha).range ⊆ ↑(elemental 𝕜 a)

Tactic:
range_cfcHom_le 𝕜 ha

Goal state after:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : Algebra 𝕜 A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarModule 𝕜 A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : ContinuousStar A
a : A
ha : p a
⊢ ↑(elemental 𝕜 a) ⊆ ↑(elemental 𝕜 a)
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
⊢ 𝓤 (CStarMatrix m n A) = 𝓤 (CStarMatrix m n A)

pp: A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
x✝ : Set (CStarMatrix m n A)
⊢ Bornology.IsBounded x✝ ↔ Bornology.IsBounded x✝

Tactic:
finally
  exacts [CStarMatrix.uniformity_eq_aux.symm, Filter.ext_iff.1 CStarMatrix.cobounded_eq_aux.symm _]

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
u : A
⊢ IsStarNormal u ∧ u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ ↑(unitary ℂ)

Tactic:
refine and_congr_right fun hu ↦ ?_

Goal state after:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
u : A
hu : IsStarNormal u
⊢ u ∈ unitary A ↔ spectrum ℂ u ⊆ ↑(unitary ℂ)
Module: Mathlib.Analysis.CStarAlgebra.Extreme

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
x✝ : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : ↑a ∈ Icc 0 1
hb01 : ↑b ∈ Icc 0 1
⊢ 0 ≤ 1 - ↑a

Tactic:
simpa using ha01.2

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
⊢ ‖diagonal v‖ = ‖v‖

Tactic:
set T := toEuclideanCLM (n := n) (𝕜 := 𝕜) (diagonal v)
  rw [← l2_opNorm_toEuclideanCLM]
  refine le_antisymm ?_ ?_
  · refine T.opNorm_le_bound (norm_nonneg _) fun x ↦ ?_
    refine (sq_le_sq₀ (by positivity) (by positivity)).mp ?_
    simp only [(T x).norm_sq_eq, ofLp_toEuclideanCLM, mulVec_diagonal, norm_mul, T]
    calc _ ≤ _ := Finset.sum_le_sum fun i _ ↦ by grw [mul_pow, norm_le_pi_norm v i]
      _ = _ := by simp [mul_pow, EuclideanSpace.norm_sq_eq x, Finset.mul_sum]
  · refine (pi_norm_le_iff_of_nonneg (norm_nonneg T)).mpr fun i ↦ ?_
    calc _ = ‖T (toLp 2 (Pi.single i (1 : 𝕜)))‖ := by
          rw [toEuclideanCLM_toLp (diagonal v) (Pi.single i (1 : 𝕜))]
          simp
      _ ≤ _ := by grw [T.le_opNorm]; simp

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
p : Z
h : proj p ∈ e₁.baseSet
⊢ e₁.coordChange e₂ (proj p) (↑e₁ p).2 = (↑e₂ p).2

Tactic:
coordChange,

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
p : Z
h : proj p ∈ e₁.baseSet
⊢ (↑e₂ (↑e₁.symm (proj p, (↑e₁ p).2))).2 = (↑e₂ p).2