mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ 0 ≤ ↑1

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℂ
y x✝ : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
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:
rw [Ring.inverse_of_isUnit (by grind), 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⁻¹ ≤ ↑⋯.unit⁻¹
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
hx : x ≠ 0
H : x = 0
⊢ False

Tactic:
exact hx H

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
this : ‖⟪x, y⟫_A‖ ^ 2 ≤ (‖x‖ * ‖y‖) ^ 2
⊢ 2 ≠ 0

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : ‖x + y‖ ^ 2 ≤ (‖x‖ + ‖y‖) ^ 2
⊢ 2 ≠ 0

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
w : E
hw : ‖w‖ ≤ 1
⊢ 1 * ‖v‖ = ‖v‖

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y : A
⊢ star (y * star x) = x * star y

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul A E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul A F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x y : C⋆ᵐᵒᵈ(A, E × F)
⊢ star (⟪x.1, y.1⟫_A + ⟪x.2, y.2⟫_A) = ⟪y.1, x.1⟫_A + ⟪y.2, x.2⟫_A

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : 0 ≤ c
x : ℝ≥0
x✝ : x ∈ σ ℝ≥0 c
⊢ (1 + x)⁻¹ ≤ 1

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul A (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x y : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ star (∑ i, ⟪x i, y i⟫_A) = ∑ i, ⟪y i, x i⟫_A

Tactic:
simp

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

Goal state before:
pp: case inl
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
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f ⊥ (quasispectrum R a)
hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in ⊥, F x 0 = 0
⊢ Tendsto (fun x ↦ cfcₙ (F x) a) ⊥ (𝓝 (cfcₙ f a))

Tactic:
simp

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

Goal state before:
pp: case right
this : (fun x ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
⊢ x = x * (1 + x - x)

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x ↦ x * (1 - x)⁻¹
this : ∀ (a b : A), 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
a : A
ha₁ : 0 ≤ a
b : A
hb₁ : 0 ≤ b
ha₂ : ‖a‖ < 1
hb₂ : ‖b‖ < 1
⊢ cfcₙ f (cfcₙ g a + cfcₙ g b) ∈ {x | 0 ≤ x}

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul A (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ∑ x_1, ‖(equiv A ((i : ι) → E i)) x‖ ≤ ↑(Fintype.card ι) * ‖(equiv A ((i : ι) → E i)) x‖

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℂ E
⊢ ∀ {x : E}, ⟪x, x⟫_ℂ = 0 ↔ x = 0

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℂ E
x✝¹ x✝ : E
⊢ star ⟪x✝¹, x✝⟫_ℂ = ⟪x✝, x✝¹⟫_ℂ

Tactic:
simp

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

Goal state before:

Tactic:
a = cfcₙ (f ∘ g) a := by
      conv_lhs => rw [← cfcₙ_id ℝ≥0 a]
      refine cfcₙ_congr (Set.InvOn.one_sub_one_add_inv.1.eqOn.symm.mono fun x hx ↦ ?_)
      exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
    _ = cfcₙ f (cfcₙ g a) := by
      rw [cfcₙ_comp f g a ?_ (by simp [f, tsub_self]) ?_ (by simp [g]) ha₁]
      · fun_prop (disch := intro _ _; positivity)
      · have (x) (hx : x ∈ σₙ ℝ≥0 a) : 1 - x ≠ 0 := by
          refine tsub_pos_of_lt ?_ |>.ne'
          exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
        fun_prop
    _ ≤ cfcₙ f (cfcₙ g a + cfcₙ g b) := by
      have hab' : cfcₙ g a ≤ cfcₙ g a + cfcₙ g b := le_add_of_nonneg_right cfcₙ_nonneg_of_predicate
      exact CFC.monotoneOn_one_sub_one_add_inv cfcₙ_nonneg_of_predicate
        (cfcₙ_nonneg_of_predicate.trans hab') hab'

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

Goal state before:
pp: A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∀ᶠ (x : A) in pure 1, 0 ≤ x

Tactic:
simp

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

Goal state before:
pp: A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ : Nontrivial A
⊢ ∀ᶠ (x : A) in pure 1, ‖x‖ ≤ 1

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x ↦ x * m) l (𝓝 m)
m : A
⊢ Tendsto (fun x ↦ x * m) l (𝓝 m)

Tactic:
have : m ∈ span ℂ ({x | 0 ≤ x} ∩ ball 0 1) := by simp [span_nonneg_inter_unitBall]
  obtain ⟨n, c, x, rfl⟩ := mem_span_set'.mp this
  simp_rw [Finset.mul_sum]
  refine tendsto_finsetSum _ fun i _ ↦ ?_
  simp_rw [mul_smul_comm]
  exact tendsto_const_nhds.smul <| h (x i) (x i).2.1 <| by simpa using (x i).2.2

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ 0 ≤ 0 ∧ ‖0‖ < 1

Tactic:
simp

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

Goal state before:
pp: m : Type u_3
α : Type u_5
ι : Type u_7
inst✝² : Fintype m
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ (Finset.univ.sup fun i ↦ ∑ j, ‖replicateCol ι v i j‖₊) = Finset.univ.sup fun b ↦ ‖v b‖₊

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : a = 0
⊢ ‖1‖₊ = 1

Tactic:
simp

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

Goal state before:
pp: case inl
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊
i : m
x✝ : i ∈ Finset.univ
h✝ : IsEmpty n
⊢ ∑ j, ‖A i j‖₊ ≤ N

Tactic:
simp

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

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
f : α → β
hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊
⊢ (∑ i, ∑ j, ‖f (A i j)‖₊ ^ 2) ^ (1 / 2) = (∑ i, ∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2)

Tactic:
hf

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

Goal state before:
pp: B₁ : Type u_3
B₂ : Type u_4
inst✝⁵ : CStarAlgebra B₁
inst✝⁴ : CStarAlgebra B₂
inst✝³ : PartialOrder B₁
inst✝² : PartialOrder B₂
inst✝¹ : StarOrderedRing B₁
inst✝ : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
⊢ ‖‖x‖‖ = ‖x‖

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ (0 ≤ 0 ∧ ‖0‖ < 1) ∧ ∀ ⦃x : A⦄, x ∈ {x | 0 ≤ x} → 0 ≤ x

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∀ᶠ (x : A) in 𝓟 (closedBall 0 1), ‖x‖ ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : TopologicalSpace Y
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x
h : IsEmpty Y
⊢ HasFiniteIntegral f μ

Tactic:
simp

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

Goal state before:
pp: case zero
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
⊢ Commute ((cfcₙHom ha) 0) b

Tactic:
simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : StarAddMonoid A
i✝ : n
j✝ : m
⊢ conjTranspose 0 i✝ j✝ = 0 i✝ j✝

Tactic:
simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
σ : R →+* S
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : Module R A
inst✝ : Module S B
f : A →ₛₗ[σ] B
M N : CStarMatrix m n A
i✝ : m
j✝ : n
⊢ (M + N).map (⇑f) i✝ j✝ = (M.map ⇑f + N.map ⇑f) i✝ j✝

Tactic:
simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
σ : R →+* S
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : Module R A
inst✝ : Module S B
f : A →ₛₗ[σ] B
r : R
M : CStarMatrix m n A
i✝ : m
j✝ : n
⊢ (r • M).map (⇑f) i✝ j✝ = (σ r • M.map ⇑f) i✝ j✝

Tactic:
simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
l : Type u_7
o : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
eₘ : m ≃ l
eₙ : n ≃ o
M N : CStarMatrix m n A
i✝ : l
j✝ : o
⊢ (Matrix.reindex eₘ eₙ).toFun (M + N) i✝ j✝ = ((Matrix.reindex eₘ eₙ).toFun M + (Matrix.reindex eₘ eₙ).toFun N) i✝ j✝

Tactic:
simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
l : Type u_7
o : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
eₘ : m ≃ l
eₙ : n ≃ o
r : R
M : CStarMatrix m n A
i✝ : l
j✝ : o
⊢ (Matrix.reindex eₘ eₙ).toFun (r • M) i✝ j✝ = ((RingHom.id R) r • (Matrix.reindex eₘ eₙ).toFun M) i✝ j✝

Tactic:
simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R✝ : Type u_3
S : Type u_4
A✝ : Type u_5
B : Type u_6
R : Type ?u.14
A : Type ?u.16
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Module R A
inst✝ : Star A
e : m ≃ n
M N : CStarMatrix m m A
i j : n
k : m
⊢ (fun j ↦ ofMatrix.symm M (e.symm i) j) k * (fun j_1 ↦ ofMatrix.symm N j_1 (e.symm j)) k =
    (↑(reindexₗ R A e e)).toFun M i (e k) * (↑(reindexₗ R A e e)).toFun N (e k) j

Tactic:
simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : Semiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : Star A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : Module R B
inst✝ : Star B
f : A →⋆ₙₐ[R] B
⊢ ∀ (m : R) (x : CStarMatrix n n A), (mapₗ ↑f) (m • x) = (MonoidHom.id R) m • (mapₗ ↑f) x

Tactic:
simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝ : A
⊢ (fun M ↦ M default default) ((fun a x y ↦ a) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝¹ x✝ : A
i✝ j✝ : n
⊢ x✝¹ + x✝ = ((fun x y ↦ x✝¹) + fun x y ↦ x✝) i✝ j✝

Tactic:
simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝¹ : R
x✝ : A
i✝ j✝ : n
⊢ x✝¹ • x✝ = (x✝¹ • fun x y ↦ x✝) i✝ j✝

Tactic:
simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝² : Fintype m
inst✝¹ : NonUnitalCStarAlgebra A
inst✝ : Fintype n
⊢ (↑(MulOpposite.opLinearEquiv ℂ) ∘ₗ toCLM).toFun 0 = 0

Tactic:
simp

Goal state after:
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
inst✝ : DecidableEq m
M : CStarMatrix m n A
i : m
j : n
a : A
⊢ (toCLM M) ((equiv A (m → A)).symm (Pi.single i a)) j = a * M i j

Tactic:
simp

Goal state after:
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
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ(A, m → A)) (w : C⋆ᵐᵒᵈ(A, n → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
⊢ 0 ≤ ↑C

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℜ a))
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' quasispectrum ℂ a)

Tactic:
quasispectrum_realPart' a

Goal state after:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (re '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' quasispectrum ℂ a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: 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✝² : ContinuousStar A
inst✝¹ : StarModule ℝ A
inst✝ : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : f ∈ (fun x ↦ cfc x a) ⁻¹' {a | 0 ≤ a}
⊢ 0 ∈ {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x}

Tactic:
simp

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

Goal state before:
pp: 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✝² : ContinuousStar A
inst✝¹ : StarModule ℝ A
inst✝ : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : f ∈ (fun x ↦ cfc x a) ⁻¹' {a | 0 ≤ a}
⊢ (fun x ↦ cfc x a) 0 = 0

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℜ a))
hf0 : f 0 = 0
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' quasispectrum ℂ a)
| cfcₙ (fun x ↦ ↑(f (↑x.re).re)) a

Tactic:
simp

Goal state after:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℜ a))
hf0 : f 0 = 0
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' quasispectrum ℂ a)
| cfcₙ (fun x ↦ ↑(f x.re)) 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
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
h₁ : ‖⟪v, (toCLM Mᴴ) ((toCLM M) v)⟫_A‖ ≤ ‖M * star M‖ * ‖v‖ ^ 2
⊢ ‖v‖ = √(‖v‖ ^ 2)

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℑ a))
hf0 : f 0 = 0
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' quasispectrum ℂ a)
| cfcₙ (fun x ↦ ↑(f (↑x.im).re)) a

Tactic:
simp

Goal state after:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℑ a))
hf0 : f 0 = 0
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' quasispectrum ℂ a)
| cfcₙ (fun x ↦ ↑(f x.im)) 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
x : ℂ
y z : CStarMatrix n n A
⊢ (x • y) • z = x • y • z

Tactic:
simp

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
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' spectrum ℂ a)
| cfc (fun x ↦ ↑(f (↑x.re).re)) a

Tactic:
simp

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 (spectrum ℝ ↑(ℜ a))
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' spectrum ℂ a)
| cfc (fun x ↦ ↑(f x.re)) a