mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case pos
α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS : S ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hKS : {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U | IsOpen[inst✝] U ∧ {s | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hLT : L ⊆ ⋃ i ∈ T, i
⊢ {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ {x | (x ∩ ⋃ i ∈ T, i).Nonempty}

Tactic:
← hLT

Goal state after:
case pos
α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS : S ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hKS : {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U | IsOpen[inst✝] U ∧ {s | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hLT : L ⊆ ⋃ i ∈ T, i
⊢ {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ {x | (x ∩ L).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
⊢ IsOpen {p | Disjoint ↑p.1 ↑p.2}

Tactic:
by
  rw [isOpen_iff_forall_mem_open]
  intro ⟨K, L⟩ hKL
  obtain ⟨U, V, hU, hV, hKU, hLV, hUV⟩ :=
    SeparatedNhds.of_isCompact_isCompact K.isCompact L.isCompact hKL
  exact ⟨{K' : Compacts α | ↑K' ⊆ U} ×ˢ {L' : Compacts α | ↑L' ⊆ V}, by grind,
    (isOpen_subsets_of_isOpen hU).prod (isOpen_subsets_of_isOpen hV), hKU, hLV⟩

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
⊢ connectedComponentIn (σ 𝕜 ↑x)ᶜ z ⊆ σ 𝕜 x

Tactic:
rw [spectrum_sUnion_connectedComponentIn S]

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 ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 ↑x, connectedComponentIn (σ 𝕜 ↑x)ᶜ z
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case e'_3
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
g₁ g₂ : C(↑(σ R a), R)
x : ↑(σ R a)
x' : ↑(σ S a) := Subtype.map ⇑(algebraMap R S) ⋯ x
⊢ x = Subtype.map ⇑f ⋯ (Subtype.map ⇑(algebraMap R S) ⋯ x)

Tactic:
ext; exact haf.left_inv _ |>.symm

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

Goal state before:
pp: case e'_4
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
g₁ g₂ : C(↑(σ R a), R)
x : ↑(σ R a)
x' : ↑(σ S a) := Subtype.map ⇑(algebraMap R S) ⋯ x
⊢ x = Subtype.map ⇑f ⋯ (Subtype.map ⇑(algebraMap R S) ⋯ x)

Tactic:
ext; exact haf.left_inv _ |>.symm

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

Goal state before:
pp: case e'_3
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✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : MetricSpace A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts a ⇑f
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a)) R
x : ↑(σₙ R a)
x' : ↑(σₙ S a) := Subtype.map ⇑(algebraMap R S) ⋯ x
⊢ x = Subtype.map ⇑f ⋯ (Subtype.map ⇑(algebraMap R S) ⋯ x)

Tactic:
ext; exact haf.left_inv _ |>.symm

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

Goal state before:
pp: case e'_4
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✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : MetricSpace A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts a ⇑f
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a)) R
x : ↑(σₙ R a)
x' : ↑(σₙ S a) := Subtype.map ⇑(algebraMap R S) ⋯ x
⊢ x = Subtype.map ⇑f ⋯ (Subtype.map ⇑(algebraMap R S) ⋯ x)

Tactic:
ext; exact haf.left_inv _ |>.symm

Goal state after:
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 : α → β
inst✝ : SeparableSpace α
⊢ SeparableSpace (Compacts α)

Tactic:
obtain ⟨s, hs₁, hs₂⟩ := exists_countable_dense α

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : SeparableSpace α
s : Set α
hs₁ : s.Countable
hs₂ : Dense s
⊢ SeparableSpace (Compacts α)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : TopologicalSpace α✝
α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
hK : K ≠ ⊥
hL : IsPreconnected ↑L
hKL : K ≤ L
⊢ IsPreconnected (Icc K L)

Tactic:
convert (isPreconnected_nonempty_subsets hL).image (K ⊔ ·) (by fun_prop)

Goal state after:
α✝ : Type u_1
inst✝¹ : TopologicalSpace α✝
α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
hK : K ≠ ⊥
hL : IsPreconnected ↑L
hKL : K ≤ L
⊢ Icc K L = (fun x ↦ K ⊔ x) '' {K | (↑K).Nonempty ∧ ↑K ⊆ ↑L}
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
⊢ ((absConvexHull 𝕜) s).Nonempty ↔ s.Nonempty

Tactic:
nonempty_iff_ne_empty,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
⊢ (absConvexHull 𝕜) s ≠ ∅ ↔ s.Nonempty
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
⊢ (absConvexHull 𝕜) s ≠ ∅ ↔ s.Nonempty

Tactic:
nonempty_iff_ne_empty,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
⊢ (absConvexHull 𝕜) s ≠ ∅ ↔ s ≠ ∅
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
S : Set (NonemptyCompacts α)
hs : IsCompact S
⊢ IsCompact (⋃ K ∈ S, ↑K)

Tactic:
convert! Compacts.isCompact_biUnion_coe_of_isCompact (hs.image continuous_toCompacts)

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
S : Set (NonemptyCompacts α)
hs : IsCompact S
⊢ ⋃ K ∈ S, ↑K = ⋃ K ∈ toCompacts '' S, ↑K
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
this : NormedSpace ℝ E := restrictScalars ℝ 𝕜 E
⊢ polar 𝕜 (ball 0 r) = closedBall 0 r⁻¹

Tactic:
rw [← polar_closedBall hr, ← closure_ball _ hr.ne', polar_closure]

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

Goal state before:
pp: ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : IsUniformAddGroup E
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst✝ : PolynormableSpace 𝕜₂ F
H : ∀ (x : E), IsVonNBounded 𝕜₂ (range fun i ↦ (𝓕 i) x)
⊢ UniformEquicontinuous (DFunLike.coe ∘ 𝓕)

Tactic:
have hp := PolynormableSpace.withSeminorms 𝕜₂ F

Goal state after:
ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : IsUniformAddGroup E
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst✝ : PolynormableSpace 𝕜₂ F
H : ∀ (x : E), IsVonNBounded 𝕜₂ (range fun i ↦ (𝓕 i) x)
hp : WithSeminorms fun p ↦ ↑p
⊢ UniformEquicontinuous (DFunLike.coe ∘ 𝓕)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case neg
A : Type u_1
inst✝¹³ : NonUnitalCStarAlgebra A
R : Type u_2
inst✝¹² : Semifield R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
⊢ ↑(cfcₙ f a) = cfc f ↑a

Tactic:
· obtain (hf | ha) := not_and_or.mp h
    · rw [cfcₙ_apply_of_not_continuousOn a hf, inr_zero,
        cfc_apply_of_not_continuousOn _ (quasispectrum_eq_spectrum_inr' R ℂ a ▸ hf)]
    · rw [cfcₙ_apply_of_not_predicate a ha, inr_zero,
        cfc_apply_of_not_predicate _ (not_iff_not.mpr hp |>.mpr ha)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: case inr.inr
A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ≥0
ha : 0 ≤ a
hx : 0 < x
hy : 0 < y
u : ℝ≥0
⊢ ↑(((fun x ↦ x.nnrpow y) ∘ fun x_1 ↦ x_1.nnrpow x) u) = ↑(u.nnrpow (x * y))

Tactic:
simp [Real.rpow_mul]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
a✝ : Nontrivial A
h : IsUnit (a ^ y)
⊢ IsUnit a

Tactic:
rw [rpow_def] at h

Goal state after:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
a✝ : Nontrivial A
h : IsUnit (cfc (fun x ↦ x ^ y) a)
⊢ IsUnit a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
⊢ cfcₙ (fun x ↦ f x - g x) a = cfcₙ f a - cfcₙ g a

Tactic:
have ha' := QuasispectrumRestricts.nnreal_of_nonneg ha
  have : (σₙ ℝ a).EqOn (fun x ↦ ((f x.toNNReal - g x.toNNReal : ℝ≥0) : ℝ))
      (fun x ↦ f x.toNNReal - g x.toNNReal) :=
    fun x hx ↦ NNReal.coe_sub <| hfg _ <| ha'.apply_mem hx
  rw [cfcₙ_nnreal_eq_real .., cfcₙ_nnreal_eq_real .., cfcₙ_nnreal_eq_real .., cfcₙ_congr this]
  refine cfcₙ_sub _ _ a ?_ (by simpa) ?_
  all_goals
    exact continuous_subtype_val.comp_continuousOn <|
      ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image ..

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✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
hs : s ∈ 𝓝ˢ (⋃ x, spectrum 𝕜 (a x))
ha_cont : ContinuousOn a Set.univ
ha' : ∀ (x : X), p (a x)
hf : ContinuousOn f s
⊢ ContinuousOn (fun x ↦ cfc f (a x)) Set.univ

Tactic:
exact ha_cont.cfc_of_mem_nhdsSet f (by simpa) (by simpa)

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 : ℝ
x y : E
⊢ ⟪z •> x, y⟫ = z •> ⟪x, y⟫

Tactic:
have h₁ : z • x = (z : ℂ) • x := by simp
  rw [h₁, ← star_inner, inner_smul_right_complex]
  simp

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

Goal state before:
pp: case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ : inr ∘ cfcₙ f = fun x ↦ ↑(cfcₙ f x)
h₂ : (fun x ↦ ↑(cfcₙ f x)) = fun x ↦ cfc f ↑x
⊢ ConvexOn ℝ s (inr ∘ cfcₙ f)

Tactic:
rw [h₁, h₂]

Goal state after:
case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ : inr ∘ cfcₙ f = fun x ↦ ↑(cfcₙ f x)
h₂ : (fun x ↦ ↑(cfcₙ f x)) = fun x ↦ cfc f ↑x
⊢ ConvexOn ℝ s fun x ↦ cfc f ↑x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
⊢ Commute ((cfcHom ha) { toFun := (spectrum ℝ a).domRestrict f, continuous_toFun := ⋯ }) b

Tactic:
rw [← cfc_apply ..]
    exact hb.cfc (ha.star_eq.symm ▸ hb) _

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
M₁ M₂ : CStarMatrix m n A
x✝ : C⋆ᵐᵒᵈ(A, m → A)
i✝ : n
⊢ ((WithCStarModule.equiv A (m → A)) x✝ ᵥ* (M₁ + M₂)) i✝ =
    ((WithCStarModule.equiv A (m → A)) x✝ ᵥ* M₁) i✝ + ((WithCStarModule.equiv A (m → A)) x✝ ᵥ* M₂) i✝

Tactic:
rw [Matrix.vecMul_add, Pi.add_apply]

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

Goal state before:
pp: case hbc
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
i : n
a✝¹ : i ∈ Finset.univ
j : m
a✝ : j ∈ Finset.univ
⊢ ‖v j‖ ≤ ‖v‖

Tactic:
exact norm_apply_le_norm v j

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
a : A
ha : IsStarNormal a
⊢ spectrum ℂ ↑(ℑ a) = (fun x ↦ ↑x.im) '' spectrum ℂ a

Tactic:
← cfc_im_id 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
a : A
ha : IsStarNormal a
⊢ spectrum ℂ (cfc (fun x ↦ ↑x.im) a) = (fun x ↦ ↑x.im) '' spectrum ℂ a
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
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun x ↦ ↑x.im) '' spectrum ℂ a)
ha : IsStarNormal a
⊢ cfc f ↑(ℑ a) = cfc (fun x ↦ f ↑x.im) a

Tactic:
← cfc_im_id 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
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun x ↦ ↑x.im) '' spectrum ℂ a)
ha : IsStarNormal a
⊢ cfc f (cfc (fun x ↦ ↑x.im) a) = cfc (fun x ↦ f ↑x.im) a
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.im) '' spectrum ℂ a)
| cfc (fun x ↦ ↑(f x.re)) ↑(ℑ a)

Tactic:
← cfc_im_id 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 (spectrum ℝ ↑(ℑ a))
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' spectrum ℂ a)
| cfc (fun x ↦ ↑(f x.re)) (cfc (fun x ↦ ↑x.im) a)
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫ = ⟪b i, y⟫
i : ι
⊢ ⟪x, b i⟫ = ⟪y, b i⟫

Tactic:
← inner_conj_symm

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫ = ⟪b i, y⟫
i : ι
⊢ (starRingEnd 𝕜) ⟪b i, x⟫ = ⟪y, b i⟫
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫ = ⟪b i, y⟫
i : ι
| ⟪y, b i⟫

Tactic:
← inner_conj_symm

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫ = ⟪b i, y⟫
i : ι
| (starRingEnd 𝕜) ⟪b i, y⟫
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, b i⟫ = ⟪y, b i⟫
i : ι
⊢ ⟪b i, x⟫ = ⟪b i, y⟫

Tactic:
← inner_conj_symm

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, b i⟫ = ⟪y, b i⟫
i : ι
⊢ (starRingEnd 𝕜) ⟪x, b i⟫ = ⟪b i, y⟫
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, b i⟫ = ⟪y, b i⟫
i : ι
| ⟪b i, y⟫

Tactic:
← inner_conj_symm

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, b i⟫ = ⟪y, b i⟫
i : ι
| (starRingEnd 𝕜) ⟪y, b i⟫
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a b : A
⊢ f.leftMulMapPreGNS (a * b) = f.leftMulMapPreGNS a ∘SL f.leftMulMapPreGNS b

Tactic:
ext c

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a b : A
c : f.PreGNS
⊢ (f.leftMulMapPreGNS (a * b)) c = (f.leftMulMapPreGNS a ∘SL f.leftMulMapPreGNS b) c