mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.UniformConvergence

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace β
x : α
f g : α →ᵤ β
⊢ edist ((fun f ↦ toFun f x) f) ((fun f ↦ toFun f x) g) ≤ ↑1 * edist f g

Tactic:
simpa using edist_eval_le

Goal state after:
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 : α →ᵤ[𝔖] β
⊢ edist f f = 0

Tactic:
simp [edist_eq_restrict_sUnion]

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

Goal state before:
pp: case inr
A : Type u_1
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedSpace ℝ A
inst✝⁷ : IsScalarTower ℝ A A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : ContinuousStar A
inst✝ : CompleteSpace A
r : ℝ≥0
hr : 0 < r
⊢ ContinuousOn (fun x ↦ x ^ r) {a | 0 ≤ a}

Tactic:
· exact continuousOn_id.cfcₙ_nnreal_of_mem_nhdsSet _ Filter.univ_mem

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
⊢ ∀ (x y : A), x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), y = x + p

Tactic:
intro x y

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x y : A
⊢ x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), y = x + p
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✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun x ↦ f x) (f x) (𝓝[s] x) (spectrum R a)
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, ContinuousOn (f x) (spectrum R a)

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

Goal state after:
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✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun x ↦ f x) (f x) (𝓝[s] x) (spectrum R a)
x✝ : X
hx✝ : x✝ ∈ s
x : X
hx : x ∈ s
⊢ ContinuousOn (f x) (spectrum R a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
⊢ cfc (fun x ↦ f x - g x) a = cfc f a - cfc g a

Tactic:
have ha' := SpectrumRestricts.nnreal_of_nonneg ha

Goal state after:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ cfc (fun x ↦ f x - g x) a = cfc f a - cfc g a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
⊢ ?m.41

Tactic:
← Unitization.inr_nonneg_iff

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha✝ : 0 ≤ a
ha : 0 ≤ ↑a
⊢ ?m.41
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬0 ≤ a
⊢ ?m.53

Tactic:
← Unitization.inr_nonneg_iff

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha✝ : ¬0 ≤ a
ha : ¬0 ≤ ↑a
⊢ ?m.53
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 : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, spectrum 𝕜 (a x) ⊆ s
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
x✝¹ : X
x✝ : x✝¹ ∈ t
⊢ ∀ᶠ (x : X) in 𝓝[t] x✝¹, spectrum 𝕜 (a x) ⊆ s

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

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 : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, spectrum 𝕜 (a x) ⊆ s
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
x✝¹ : X
x✝ : x✝¹ ∈ t
x : X
hx : x ∈ t
⊢ spectrum 𝕜 (a x) ⊆ s
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 ℝ a

Tactic:
simpa using spectrum.algebraMap_mem ℝ <| nnnorm_mem_spectrum_of_nonneg ha

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
⊢ ‖⟪x, y⟫_A * ⟪y, x⟫_A‖ ≤ ‖‖x‖ ^ 2 •> ⟪y, y⟫_A‖

Tactic:
by
                refine CStarAlgebra.norm_le_norm_of_nonneg_of_le ?_ inner_mul_inner_swap_le
                rw [← star_inner x]
                exact mul_star_self_nonneg ⟪x, y⟫_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 : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
x✝¹ : X
x✝ : x✝¹ ∈ t
⊢ ∀ᶠ (x : X) in 𝓝[t] x✝¹, spectrum ℝ≥0 (a x) ⊆ s

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

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 : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
x✝¹ : X
x✝ : x✝¹ ∈ t
x : X
hx : x ∈ t
⊢ spectrum ℝ≥0 (a x) ⊆ s
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case refine_1
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
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun x ↦ f x) (f x) (𝓝[s] x) (quasispectrum R a)
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, ContinuousOn (f x) (quasispectrum R a)

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

Goal state after:
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
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun x ↦ f x) (f x) (𝓝[s] x) (quasispectrum R a)
x✝ : X
hx✝ : x✝ ∈ s
x : X
hx : x ∈ s
⊢ ContinuousOn (f x) (quasispectrum R a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case refine_2
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
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun x ↦ f x) (f x) (𝓝[s] x) (quasispectrum R a)
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, f x 0 = 0

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

Goal state after:
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
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun x ↦ f x) (f x) (𝓝[s] x) (quasispectrum R a)
x✝ : X
hx✝ : x✝ ∈ s
x : X
hx : x ∈ s
⊢ f x 0 = 0
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ‖toLp 2 (Function.const n 1)‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊

Tactic:
PiLp.nnnorm_toLp_const (ENNReal.ofNat_ne_top (n := 2))

Goal state after:
n : Type u_4
α : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ↑(Fintype.card n) ^ (1 / OfNat.ofNat 2).toReal * ‖1‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊
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 approximateUnit A, IsSelfAdjoint x

Tactic:
rw [(hasBasis_approximateUnit A).eventually_iff]
      peel (hasBasis_approximateUnit A).ex_mem with x hx
      exact ⟨hx, fun y hy ↦ (hx.1.trans hy.1).isSelfAdjoint⟩

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✝⁷ : 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 : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
x✝¹ : X
x✝ : x✝¹ ∈ t
⊢ ∀ᶠ (x : X) in 𝓝[t] x✝¹, quasispectrum 𝕜 (a x) ⊆ s

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

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 : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
x✝¹ : X
x✝ : x✝¹ ∈ t
x : X
hx : x ∈ t
⊢ quasispectrum 𝕜 (a x) ⊆ s
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case neg
A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : IsTopologicalRing A
inst✝³ : T2Space A
inst✝² : PartialOrder A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : ¬0 ≤ a
⊢ Commute (cfcₙ f a) b

Tactic:
simp [cfcₙ_apply_of_not_predicate a ha]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Field R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ IsIdempotentElem a ↔ quasispectrum R a ⊆ {0, 1}

Tactic:
refine ⟨IsIdempotentElem.quasispectrum_subset R, fun h ↦ ?_⟩

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Field R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
h : quasispectrum R a ⊆ {0, 1}
⊢ IsIdempotentElem a
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 : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
x✝¹ : X
x✝ : x✝¹ ∈ t
⊢ ∀ᶠ (x : X) in 𝓝[t] x✝¹, quasispectrum ℝ≥0 (a x) ⊆ s

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

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 : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
x✝¹ : X
x✝ : x✝¹ ∈ t
x : X
hx : x ∈ t
⊢ quasispectrum ℝ≥0 (a x) ⊆ s
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
⊢ Function.LeftInverse (fun M ↦ M default default) fun a x y ↦ a

Tactic:
intro; 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
i : m
j : n
⊢ ‖toCLM M‖ * ‖(equiv A (m → A)).symm (Pi.single i (star (M i j)))‖ ≤ ‖M‖ * ‖M i j‖

Tactic:
simp [norm_def]

Goal state after:
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A \ (convexHull 𝕜) (A \ {x})

Tactic:
by
  rw [hA.mem_extremePoints_iff_convex_sdiff, hA.convex_remove_iff_notMem_convexHull_remove,
    mem_sdiff]

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 : A
⊢ ∀ (x y : Completion f.PreGNS),
    ⟪(f.leftMulMapPreGNS (star a)).completion x, y⟫_ℂ = ⟪x, (f.leftMulMapPreGNS a).completion y⟫_ℂ

Tactic:
intro x y

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x y : Completion f.PreGNS
⊢ ⟪(f.leftMulMapPreGNS (star a)).completion x, y⟫_ℂ = ⟪x, (f.leftMulMapPreGNS a).completion y⟫_ℂ
Module: Mathlib.Analysis.CStarAlgebra.Extreme

Goal state before:
pp: case refine_2.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
x✝ :
  (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : 0 ≤ ↑(2 • e - e * e)
⊢ ‖↑(2 • e - e * e)‖ ≤ 1

Tactic:
norm_le_one_iff_of_nonneg _ this,

Goal state after:
case refine_2.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
x✝ :
  (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : 0 ≤ ↑(2 • e - e * e)
⊢ ↑(2 • e - e * e) ≤ 1
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ e.target ∩ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' e'.source = e.target ∩ (↑e '' s ∩ ↑e.symm ⁻¹' e'.source)

Tactic:
← inter_assoc

Goal state after:
case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ e.target ∩ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' e'.source = e.target ∩ ↑e '' s ∩ ↑e.symm ⁻¹' e'.source
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case hf
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 := ⋯
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
heq : EqOn F (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)

Tactic:
have : ContinuousOn (hf.toOpenPartialHomeomorph).symm (f '' univ) :=
        (hf.toOpenPartialHomeomorph).continuousOn_invFun

Goal state after:
case hf
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 (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' univ)
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), ↑e x = ↑e' x
h₂ : ∀ (x : B × F), ↑e.symm x = ↑e'.symm x
h₃ : e.baseSet = e'.baseSet
⊢ e = e'

Tactic:
ext1 <;> [ext1; exact h₃]
  · apply h₁
  · apply h₂
  · rw [e.source_eq, e'.source_eq, h₃]

Goal state after:
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : AddAction G E
hf : IsAddQuotientCoveringMap f G
e₁ e₂ : E
⊢ f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit (Multiplicative G) e₂

Tactic:
simp [hf.apply_eq_iff_mem_orbit]

Goal state after:
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
e₁ e₂ : E
⊢ f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit (Additive G) e₂

Tactic:
simp [hf.apply_eq_iff_mem_orbit]

Goal state after: