mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ -a
⊢ a = -a⁻

Tactic:
rw [negPart_def, ← cfcₙ_neg]

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ -a
⊢ a = cfcₙ (fun x ↦ -x⁻) a
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
⊢ 𝓤 (α →ᵤ β) = comap (fun x ↦ edist x.1 x.2) (𝓝 0)

Tactic:
ENNReal.nhds_zero_basis_Iic.comap _ |>.eq_biInf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
⊢ 𝓤 (α →ᵤ β) = ⨅ i, ⨅ (_ : 0 < i), 𝓟 ((fun x ↦ edist x.1 x.2) ⁻¹' Set.Iic 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
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
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
mul₁ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hb' hbs) f * (cfcₙHomSuperset hc' hcs) g = 0
mul₂ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hc' hcs) f * (cfcₙHomSuperset hb' hbs) g = 0
ψ : C(↑s, ℝ)₀ →⋆ₙₐ[ℝ] A :=
  let __src := ↑(cfcₙHomSuperset hb' hbs) + ↑(cfcₙHomSuperset hc' hcs);
  { toFun := ⇑(cfcₙHomSuperset hb' hbs) + ⇑(cfcₙHomSuperset hc' hcs), map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
    map_mul' := ⋯, map_star' := ⋯ }
f : C(↑s, ℝ)₀ := { toFun := fun x ↦ (↑x)⁺, continuous_toFun := ⋯, map_zero' := ⋯ }
key :
  cfcₙ
      (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id has, continuous_toFun := ⋯, map_zero' := ⋯ })
        fun x ↦ x⁺)
      a =
    cfcₙ
        (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id hbs, continuous_toFun := ⋯, map_zero' := ⋯ })
          fun x ↦ x⁺)
        b +
      cfcₙ
        (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id hcs, continuous_toFun := ⋯, map_zero' := ⋯ })
          fun x ↦ x⁺)
        (-c)
x : { x // x ∈ σₙ ℝ a }
⊢ Function.extend Subtype.val (⇑(f.comp { toFun := Subtype.map id has, continuous_toFun := ⋯, map_zero' := ⋯ }))
      (fun x ↦ x⁺) ↑x =
    (↑x)⁺

Tactic:
simp [f]

Goal state after:
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))⁺ ∈ {a | 0 ≤ a}

Tactic:
apply CFC.posPart_nonneg

Goal state after:
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))⁺ ∈ {a | 0 ≤ a}

Tactic:
apply CFC.posPart_nonneg

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
⊢ QuasispectrumRestricts 0 ⇑ContinuousMap.realToNNReal

Tactic:
quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ,

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
⊢ SpectrumRestricts ↑0 ⇑ContinuousMap.realToNNReal
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

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

Tactic:
quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ,

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
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
⊢ QuasispectrumRestricts ((fun s ↦ star s * s) s) ⇑ContinuousMap.realToNNReal

Tactic:
quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ,

Goal state after:
case mpr.mem
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p s : A
⊢ SpectrumRestricts ↑((fun s ↦ star s * s) s) ⇑ContinuousMap.realToNNReal
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case mpr.zero
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p : A
⊢ IsSelfAdjoint 0 ∧ QuasispectrumRestricts 0 ⇑ContinuousMap.realToNNReal

Tactic:
quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ,

Goal state after:
case mpr.zero
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p : A
⊢ IsSelfAdjoint 0 ∧ SpectrumRestricts ↑0 ⇑ContinuousMap.realToNNReal
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: case h.left.«3».right
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ ‖![(↑(realPart a))⁺, (↑(imaginaryPart a))⁺, (↑(realPart a))⁻, (↑(imaginaryPart a))⁻] ((fun i ↦ i) ⟨3, ⋯⟩)‖ ≤ ‖a‖

Tactic:
exact CStarAlgebra.norm_negPart_le _ |>.trans <| imaginaryPart.norm_le a

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : ContinuousStar A
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
⊢ ContinuousOn (fun x ↦ cfc f (a x)) t

Tactic:
rw [ContinuousOn] at ha_cont ⊢

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : ContinuousStar A
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
⊢ ∀ x ∈ t, ContinuousWithinAt (fun x ↦ cfc f (a x)) t x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ a ^ (-(1 / 2)) * a * a ^ (-(1 / 2)) = 1

Tactic:
by
  lift a to Aˣ using ha.isUnit
  nth_rw 2 [← rpow_one (a : A)]
  simp only [← rpow_add a.isUnit]
  norm_num
  exact rpow_zero _

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : 0 ≤ ↑a
⊢ ↑a⁻¹ ≤ 1 ↔ 1 ≤ a

Tactic:
by
  simpa using! CStarAlgebra.inv_le_iff ha (b := 1) (by simp)

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
apos : IsStrictlyPositive a
b : A
bpos : IsStrictlyPositive b
hab : a ≤ b
⊢ Ring.inverse b ≤ Ring.inverse a

Tactic:
Ring.inverse_of_isUnit (by grind),

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
apos : IsStrictlyPositive a
b : A
bpos : IsStrictlyPositive b
hab : a ≤ b
⊢ ↑⋯.unit⁻¹ ≤ Ring.inverse a
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
x : E
h : x = 0
⊢ ‖x‖ = 0

Tactic:
by simp [h, norm_eq_sqrt_norm_inner_self (A := A)]

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

Goal state before:
pp: X : Type u_1
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✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
⊢ ContinuousOn (fun x ↦ cfc f (a x)) t

Tactic:
rw [ContinuousOn] at ha_cont ⊢

Goal state after:
X : Type u_1
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✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
⊢ ∀ x ∈ t, ContinuousWithinAt (fun x ↦ cfc f (a x)) t x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
h_cont : ContinuousOn (fun x ↦ (ofFun {quasispectrum R a}) (f x)) s
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ (f x) a) s

Tactic:
rw [ContinuousOn] at h_cont ⊢
  simp only [ContinuousWithinAt, UniformOnFun.tendsto_iff_tendstoUniformlyOn, Set.mem_singleton_iff,
    Function.comp_def, toFun_ofFun, forall_eq] at h_cont
  refine fun x hx ↦ continuousWithinAt_cfcₙ_fun (h_cont x hx) ?_ ?_
  all_goals filter_upwards [self_mem_nhdsWithin] with x hx
  exacts [hf x hx, hf0 x hx]

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

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
r : ℝ
hr : 0 < r
A : Matrix m n α
⊢ ‖A‖ < r ↔ ∀ (i : m) (j : n), ‖A i j‖ < r

Tactic:
simp_rw [norm_def, pi_norm_lt_iff hr]

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

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ a, 0 ≤ a ∧ ↑C * ‖a‖ < ‖f a‖
n : ℕ
⊢ ∃ x, 0 ≤ x ∧ ‖x‖ = 1 ∧ 2 ^ (2 * n) < ‖f x‖

Tactic:
obtain ⟨hx₁, hx₂⟩ := Classical.choose_spec (hcontra (2 ^ (2 * n)))

Goal state after:
A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ a, 0 ≤ a ∧ ↑C * ‖a‖ < ‖f a‖
n : ℕ
hx₁ : 0 ≤ Classical.choose ⋯
hx₂ : ↑(2 ^ (2 * n)) * ‖Classical.choose ⋯‖ < ‖f (Classical.choose ⋯)‖
⊢ ∃ x, 0 ≤ x ∧ ‖x‖ = 1 ∧ 2 ^ (2 * n) < ‖f x‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t

Tactic:
rw [ContinuousOn] at ha_cont ⊢

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
⊢ ∀ x ∈ t, ContinuousWithinAt (fun x ↦ cfcₙ f (a x)) t x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t

Tactic:
rw [ContinuousOn] at ha_cont ⊢

Goal state after:
X : Type u_1
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
⊢ ∀ x ∈ t, ContinuousWithinAt (fun x ↦ cfcₙ f (a x)) t x
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
⊢ Function.Injective ⇑toCLM

Tactic:
rw [injective_iff_map_eq_zero]
  intro M h
  ext i j
  rw [zero_apply, ← norm_eq_zero, ← sq_eq_zero_iff, sq, ← CStarRing.norm_star_mul_self,
    ← toCLM_apply_single_apply]
  simp [h]

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

Goal state before:
pp: case mpr
A : Type u_1
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : Algebra ℝ A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : PartialOrder A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : StarOrderedRing A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
x✝ : A
⊢ x✝ ∈ (fun x ↦ cfc x a) '' {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x} → x✝ ∈ Set.range fun x ↦ cfc x a

Tactic:
rintro ⟨f, hf, rfl⟩
    simp only [cfc_real_eq_nnreal a hf]
    exact ⟨_, rfl⟩

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℂ A
inst✝³ : StarModule ℂ A
inst✝² : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (spectrum ℝ ↑(ℑ a))
ha : IsStarNormal a
⊢ ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' spectrum ℂ a)

Tactic:
spectrum_imaginaryPart' a

Goal state after:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℂ A
inst✝³ : StarModule ℂ A
inst✝² : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (im '' spectrum ℂ a)
ha : IsStarNormal a
⊢ ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' spectrum ℂ a)
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x

Tactic:
by
  refine ⟨fun h ↦ ⟨h.1, fun x₁ hx₁ x₂ hx₂ hx ↦ ⟨h.2 hx₁ hx₂ hx, ?_⟩⟩,
    fun h ↦ ⟨h.1, fun x₁ hx₁ x₂ hx₂ hx ↦ (h.2 x₁ hx₁ x₂ hx₂ hx).1⟩⟩
  apply h.2 hx₂ hx₁
  rwa [openSegment_symm]

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
h_spec : spectrum ℝ ((StarAlgHom.restrictScalars ℝ ↑φ) a) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ x ∈ spectrum ℝ (φ a)

Tactic:
by_contra hx'

Goal state after:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
h_spec : spectrum ℝ ((StarAlgHom.restrictScalars ℝ ↑φ) a) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum ℝ (φ a)
⊢ False
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x y : ↑(sphere 0 1)
⊢ 1 / ‖↑y‖ = 1

Tactic:
mem_sphere_zero_iff_norm.1 y.coe_prop,

Goal state after:
𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x y : ↑(sphere 0 1)
⊢ 1 / 1 = 1
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 → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖T (toLp 2 (Pi.single i 1))‖ ≤ ‖T‖

Tactic:
T.le_opNorm

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖T‖ * ‖toLp 2 (Pi.single i 1)‖ ≤ ‖T‖
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:
by
  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.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case pos
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
F : X' → Z := extend f ↑e fun x ↦ Classical.arbitrary Z
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
heq : EqOn F (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
this : ContinuousOn (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
⊢ ContinuousOn F (f '' e.source)

Tactic:
exact ContinuousOn.congr this heq

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

Goal state before:
pp: B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := ⋯
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := ⋯
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
⊢ ∃ d ∈ Ioc c b, ∃ e, Icc a d ⊆ e.baseSet

Tactic:
obtain ⟨d, hdcb, hd⟩ : ∃ d ∈ Ioc c b, Ico c d ⊆ ec.baseSet :=
    (mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset hlt).1
      (mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds ec.open_baseSet (hec ⟨hc.1, le_rfl⟩))

Goal state after:
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
⊢ ∃ d ∈ Ioc c b, ∃ e, Icc a d ⊆ e.baseSet