mathlib-initiative/mathlib-tactics huggingface dataset:
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
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
⊢ ∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
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

Goal state after:
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
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
A : ∀ (n : ℕ), ∃ f, EqOn (⇑f) 1 s ∧ EqOn (⇑f) 0 (U n ∩ interior m)ᶜ ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
⊢ ∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
h : ∀ (c : α), LipschitzWith K (f c)
⊢ UniformEquicontinuous f

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
h : ∀ (c : α), LipschitzWith K (f c)
⊢ UniformContinuous (⇑ofFun ∘ Function.swap f)
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
s : Set γ
h : ∀ (c : α), LipschitzOnWith K (f c) s
⊢ UniformContinuousOn (⇑ofFun ∘ Function.swap f) s

Tactic:
← lipschitzOnWith_ofFun_iff

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
s : Set γ
h : LipschitzOnWith K (fun x ↦ ofFun fun c ↦ f c x) s
⊢ UniformContinuousOn (⇑ofFun ∘ Function.swap f) s
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
f₁ f₂ f₃ : α →ᵤ[𝔖] β
⊢ edist f₁ f₃ ≤ edist f₁ f₂ + edist f₂ f₃

Tactic:
simp [edist_eq_restrict_sUnion, edist_triangle]

Goal state after:
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' := ⋯ }
key : cfcₙHomSuperset ha has = ψ
⊢ ↑0 ≤ 0

Tactic:
norm_cast

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
x : ℂ
x✝ : x = 0 ∨ x ∈ spectrum ℂ a
hx : x ∈ spectrum ℂ a
⊢ 0 ≤ x

Tactic:
obtain ⟨y, hy, rfl⟩ := (IsSelfAdjoint.of_nonneg ha).spectrumRestricts.algebraMap_image ▸ hx

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
y : ℝ
hy : y ∈ spectrum ℝ a
x✝ : (algebraMap ℝ ℂ) y = 0 ∨ (algebraMap ℝ ℂ) y ∈ spectrum ℂ a
hx : (algebraMap ℝ ℂ) y ∈ spectrum ℂ a
⊢ 0 ≤ (algebraMap ℝ ℂ) y
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: 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 : ℝ≥0
hx : x ≠ 0
ha : 0 ≤ a
⊢ (a ^ x⁻¹) ^ x = a

Tactic:
by
  simp [inv_mul_cancel₀ hx, nnrpow_one _ ha]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: case refine_1
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‖
this : (↑r * ↑‖x‖⁻¹)⁻¹ • (↑r * ↑‖x‖⁻¹) • x = x
⊢ (↑r * ↑‖x‖⁻¹) • x ∈ {x | 0 ≤ x}

Tactic:
norm_cast

Goal state after:
case refine_1
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‖
this : (↑r * ↑‖x‖⁻¹)⁻¹ • (↑r * ↑‖x‖⁻¹) • x = x
⊢ (r * ‖x‖⁻¹) • x ∈ {x | 0 ≤ x}
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: 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
B : Type u_2
inst✝¹³ : PartialOrder B
inst✝¹² : NonUnitalRing B
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : StarRing B
inst✝⁹ : Module ℝ B
inst✝⁸ : SMulCommClass ℝ B B
inst✝⁷ : IsScalarTower ℝ B B
inst✝⁶ : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝⁴ : IsSemitopologicalRing B
inst✝³ : T2Space B
inst✝² : NonnegSpectrumClass ℝ B
inst✝¹ : NonnegSpectrumClass ℝ (A × B)
inst✝ : StarOrderedRing B
a : A
b : B
x : ℝ≥0
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ (a, b)

Tactic:
rw [Prod.le_def]

Goal state after:
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
B : Type u_2
inst✝¹³ : PartialOrder B
inst✝¹² : NonUnitalRing B
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : StarRing B
inst✝⁹ : Module ℝ B
inst✝⁸ : SMulCommClass ℝ B B
inst✝⁷ : IsScalarTower ℝ B B
inst✝⁶ : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝⁴ : IsSemitopologicalRing B
inst✝³ : T2Space B
inst✝² : NonnegSpectrumClass ℝ B
inst✝¹ : NonnegSpectrumClass ℝ (A × B)
inst✝ : StarOrderedRing B
a : A
b : B
x : ℝ≥0
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0.1 ≤ (a, b).1 ∧ 0.2 ≤ (a, b).2
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: 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‖
⊢ ↑r * ↑‖x‖⁻¹ ≠ 0

Tactic:
norm_cast

Goal state after:
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‖
⊢ ¬r * ‖x‖⁻¹ = 0
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: case h.left
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ ∀ (x : Fin 4),
    0 ≤ ![(↑(realPart a))⁺, (↑(imaginaryPart a))⁺, (↑(realPart a))⁻, (↑(imaginaryPart a))⁻] x ∧
      ‖![(↑(realPart a))⁺, (↑(imaginaryPart a))⁺, (↑(realPart a))⁻, (↑(imaginaryPart a))⁻] x‖ ≤ ‖a‖

Tactic:
intro i

Goal state after:
case h.left
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
i : Fin 4
⊢ 0 ≤ ![(↑(realPart a))⁺, (↑(imaginaryPart a))⁺, (↑(realPart a))⁻, (↑(imaginaryPart a))⁻] i ∧
    ‖![(↑(realPart a))⁺, (↑(imaginaryPart a))⁺, (↑(realPart a))⁻, (↑(imaginaryPart a))⁻] i‖ ≤ ‖a‖
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
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : 0 ≤ ↑a
⊢ ↑a ^ (-x) = ↑a⁻¹ ^ x

Tactic:
suffices h₁ : ContinuousOn (fun z ↦ z ^ x) (Inv.inv '' (spectrum ℝ≥0 (a : A))) by
    rw [← cfc_inv_id (R := ℝ≥0) a, rpow_def, rpow_def,
        ← cfc_comp' (fun z => z ^ x) (Inv.inv : ℝ≥0 → ℝ≥0) (a : A) h₁]
    refine cfc_congr fun _ _ => ?_
    simp [NNReal.rpow_neg, NNReal.inv_rpow]

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
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : 0 ≤ ↑a
⊢ ContinuousOn (fun z ↦ z ^ x) (Inv.inv '' spectrum ℝ≥0 ↑a)
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
inst✝¹⁴ : IsSemitopologicalRing A
inst✝¹³ : T2Space A
B : Type u_2
inst✝¹² : PartialOrder B
inst✝¹¹ : Ring B
inst✝¹⁰ : StarRing B
inst✝⁹ : TopologicalSpace B
inst✝⁸ : StarOrderedRing B
inst✝⁷ : Algebra ℝ B
inst✝⁶ : ContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁵ : ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝⁴ : IsSemitopologicalRing B
inst✝³ : T2Space B
inst✝² : StarOrderedRing (A × B)
inst✝¹ : NonnegSpectrumClass ℝ B
inst✝ : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
x : ℝ
ha : IsUnit a
hb : IsUnit b
ha' : 0 ≤ a
hb' : 0 ≤ b
ha'' : 0 ∉ spectrum ℝ≥0 a
hb'' : 0 ∉ spectrum ℝ≥0 b
⊢ 0 ≤ (a, b)

Tactic:
rw [Prod.le_def]

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
inst✝¹⁴ : IsSemitopologicalRing A
inst✝¹³ : T2Space A
B : Type u_2
inst✝¹² : PartialOrder B
inst✝¹¹ : Ring B
inst✝¹⁰ : StarRing B
inst✝⁹ : TopologicalSpace B
inst✝⁸ : StarOrderedRing B
inst✝⁷ : Algebra ℝ B
inst✝⁶ : ContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁵ : ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝⁴ : IsSemitopologicalRing B
inst✝³ : T2Space B
inst✝² : StarOrderedRing (A × B)
inst✝¹ : NonnegSpectrumClass ℝ B
inst✝ : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
x : ℝ
ha : IsUnit a
hb : IsUnit b
ha' : 0 ≤ a
hb' : 0 ≤ b
ha'' : 0 ∉ spectrum ℝ≥0 a
hb'' : 0 ∉ spectrum ℝ≥0 b
⊢ 0.1 ≤ (a, b).1 ∧ 0.2 ≤ (a, b).2
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝³ : CStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Nontrivial A
a : A
ha : 0 ≤ a
⊢ ‖a‖₊ ∈ spectrum ℝ≥0 a

Tactic:
by
  have : IsSelfAdjoint a := .of_nonneg ha
  convert! NNReal.spectralRadius_mem_spectrum (a := a) ?_ (.nnreal_of_nonneg ha)
  · simp [this.spectrumRestricts.spectralRadius_eq, this.spectralRadius_eq_nnnorm]
  · exact this.spectrumRestricts.image ▸ (spectrum.nonempty a).image _

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
x : A
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ x → (x ≤ (algebraMap ℝ A) r ↔ ‖x‖ ≤ r)

Tactic:
iff_comm

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ x → (‖x‖ ≤ r ↔ x ≤ (algebraMap ℝ A) r)
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
h₁ : z •> y = ↑z •> y
⊢ star ⟪↑z •> y, x⟫ = z •> ⟪x, y⟫

Tactic:
inner_smul_left_complex

Goal state after:
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
h₁ : z •> y = ↑z •> y
⊢ star (star ↑z •> ⟪y, x⟫) = z •> ⟪x, y⟫
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ 0 ≤ ↑x → (↑x ≤ 1 ↔ ‖↑x‖ ≤ 1)

Tactic:
iff_comm

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ 0 ≤ ↑x → (‖↑x‖ ≤ 1 ↔ ↑x ≤ 1)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: case h.h
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ∀ x ∈ spectrum ℝ a, 1 ≤ x
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
x : ℝ
hx : x ∈ spectrum ℝ a
this : 1 ≤ x
⊢ x ^ n ≤ x ^ m

Tactic:
exact pow_le_pow_right₀ (ha x hx) hnm

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✝⁴ : StarOrderedRing A
inst✝³ : SMul A E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CStarModule A E
x y : E
⊢ ‖(innerₛₗ x) y‖ ≤ 1 * ‖x‖ * ‖y‖

Tactic:
by
    simp [innerₛₗ_apply, norm_inner_le E]

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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ ∑ i_1, ⟪Pi.single i y i_1, x i_1⟫_A = ⟪y, x i⟫_A

Tactic:
rw [Finset.sum_eq_single i]

Goal state after:
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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ ⟪Pi.single i y i, x i⟫_A = ⟪y, x i⟫_A

case h₀
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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ ∀ b ∈ Finset.univ, b ≠ i → ⟪Pi.single i y b, x b⟫_A = 0

case h₁
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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ i ∉ Finset.univ → ⟪Pi.single i y i, x i⟫_A = 0
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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ ∑ i_1, ⟪x i_1, Pi.single i y i_1⟫_A = ⟪x i, y⟫_A

Tactic:
rw [Finset.sum_eq_single i]

Goal state after:
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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ ⟪x i, Pi.single i y i⟫_A = ⟪x i, y⟫_A

case h₀
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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ ∀ b ∈ Finset.univ, b ≠ i → ⟪x b, Pi.single i y b⟫_A = 0

case h₁
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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ i ∉ Finset.univ → ⟪x i, Pi.single i y i⟫_A = 0
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
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
i : n
⊢ (toCLM M) v i = (WithCStarModule.equiv A (n → A)).symm (fun j ↦ ∑ i, v i * M i j) i

Tactic:
simp [toCLM_apply, Matrix.vecMul, dotProduct]

Goal state after:
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
⊢ StarSubalgebra.map (cfcHom ha)
      (adjoin 𝕜 {ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)}).topologicalClosure ≤
    elemental 𝕜 a

Tactic:
StarSubalgebra.map_topologicalClosure_le _ _ (cfcHom_continuous ha (R := 𝕜)),

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
⊢ (StarSubalgebra.map (cfcHom ha)
        (adjoin 𝕜 {ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)})).topologicalClosure ≤
    elemental 𝕜 a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: 𝕜 : 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✝⁴ : ContinuousConstSMul 𝕜 A
inst✝³ : StarModule 𝕜 A
inst✝² : IsTopologicalRing A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ NonUnitalStarSubalgebra.map (cfcₙHom ha) (adjoin 𝕜 {ContinuousMapZero.id (quasispectrum 𝕜 a)}).topologicalClosure ≤
    elemental 𝕜 a

Tactic:
NonUnitalStarSubalgebra.map_topologicalClosure_le (R := 𝕜) _ (cfcₙHom_continuous ha),

Goal state after:
𝕜 : 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✝⁴ : ContinuousConstSMul 𝕜 A
inst✝³ : StarModule 𝕜 A
inst✝² : IsTopologicalRing A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ (NonUnitalStarSubalgebra.map (cfcₙHom ha) (adjoin 𝕜 {ContinuousMapZero.id (quasispectrum 𝕜 a)})).topologicalClosure ≤
    elemental 𝕜 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 : ι), ↑((toDualMap 𝕜 E) x) (b i) = ↑((toDualMap 𝕜 E) y) (b i)

Tactic:
intro i

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 : ι
⊢ ↑((toDualMap 𝕜 E) x) (b i) = ↑((toDualMap 𝕜 E) y) (b i)
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
htriv : Y = ⊤
⊢ ∃ a, (toDualMap 𝕜 E) a = ℓ

Tactic:
have hℓ : ℓ = 0 := by
          have h' := LinearMap.ker_eq_top.mp htriv
          norm_cast at h'
        exact ⟨0, by simp [hℓ]⟩

Goal state after:
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
ι : Sort u_6
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
⊢ IsExtreme 𝕜 A (⋂ i, F i)

Tactic:
inhabit ι
  refine ⟨iInter_subset_of_subset default (hAF default).1, fun x₁ hx₁A x₂ hx₂A x hxF hx ↦ ?_⟩
  rw [mem_iInter] at hxF ⊢
  exact fun i ↦ (hAF i).2 hx₁A hx₂A (hxF i) hx

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y z : Completion E
a b c : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by simp only [← coe_add, inner_coe, inner_add_left]

Goal state after:
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 : f.PreGNS
⊢ ↑‖a‖ ^ 2 = f (star (f.ofPreGNS a) * f.ofPreGNS a)

Tactic:
by
  have : 0 ≤ f (star (f.ofPreGNS a) * f.ofPreGNS a) := f.map_nonneg (star_mul_self_nonneg _)
  simp [preGNS_norm_def, ← ofReal_pow, Real.sq_sqrt this.1, conj_eq_iff_re.mp this.star_eq]

Goal state after: