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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] sᶜᶜ)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen[inst✝¹] u
hvIsOpen : IsOpen[inst✝¹] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst✝¹] u ⊆ vᶜ
P : Set X → Set X → Prop := fun C x ↦ sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed[inst✝¹] c
Pc : P c u0
u0IsOpen : IsOpen[inst✝¹] u0
csubu0 : c ⊆ u0
u1 : Set X
hu1 : ∃ V, IsOpen[inst✝¹] u1 ∧ IsOpen[inst✝¹] V ∧ c ⊆ u1 ∧ u0ᶜ ⊆ V ∧ u1 ⊆ Vᶜ
⊢ ∃ v, IsOpen[inst✝¹] v ∧ c ⊆ v ∧ closure[inst✝¹] v ⊆ u0 ∧ P c v ∧ P (closure[inst✝¹] v) u0

Tactic:
compl_subset_comm (s := u0)

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] sᶜᶜ)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen[inst✝¹] u
hvIsOpen : IsOpen[inst✝¹] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst✝¹] u ⊆ vᶜ
P : Set X → Set X → Prop := fun C x ↦ sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed[inst✝¹] c
Pc : P c u0
u0IsOpen : IsOpen[inst✝¹] u0
csubu0 : c ⊆ u0
u1 : Set X
hu1 : ∃ V, IsOpen[inst✝¹] u1 ∧ IsOpen[inst✝¹] V ∧ c ⊆ u1 ∧ Vᶜ ⊆ u0 ∧ u1 ⊆ Vᶜ
⊢ ∃ v, IsOpen[inst✝¹] v ∧ c ⊆ v ∧ closure[inst✝¹] v ⊆ u0 ∧ P c v ∧ P (closure[inst✝¹] v) u0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case refine_1
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)
⊢ IsCompact (σₙ ℝ a)

pp: case refine_2
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)
⊢ IsCompact (σₙ ℝ b)

pp: case refine_3
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)
⊢ IsCompact (σₙ ℝ (-c))

Tactic:
all_goals exact isCompact_quasispectrum _

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
this : Isometry ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
f : C(↑(spectrum ℂ a), ℂ)
⊢ spectrum ℂ ↑((continuousFunctionalCalculus a) f) = Set.range ⇑f

Tactic:
← StarSubalgebra.spectrum_eq (hS := StarAlgebra.elemental.isClosed ℂ a),

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
this : Isometry ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
f : C(↑(spectrum ℂ a), ℂ)
⊢ spectrum ℂ ((continuousFunctionalCalculus a) f) = Set.range ⇑f
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
ha : 0 ≤ a
⊢ a ^ 1 = a

Tactic:
nnrpow_one a

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
a : A
ha : 0 ≤ a
⊢ a = a
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
⊢ sqrt (a ^ x) = a ^ (x / 2)

Tactic:
simp [sqrt_eq_nnrpow, div_eq_mul_inv]

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
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
ha₁' : 0 ∉ spectrum ℝ≥0 a
x✝¹ : ℝ≥0
x✝ : x✝¹ ∈ spectrum ℝ≥0 a
⊢ ((fun x ↦ x ^ y) ∘ fun x_1 ↦ x_1 ^ x) x✝¹ = x✝¹ ^ (x * y)

Tactic:
simp [NNReal.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
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha : 0 ≤ a
x✝¹ : ℝ≥0
x✝ : x✝¹ ∈ spectrum ℝ≥0 a
⊢ ((fun x ↦ x ^ y) ∘ fun x_1 ↦ x_1 ^ x) x✝¹ = x✝¹ ^ (x * y)

Tactic:
simp [NNReal.rpow_mul]

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

Goal state before:
pp: case neg
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
⊢ 0 ≤ ↑a ↔ 0 ≤ a

Tactic:
refine ⟨?_, ?_⟩
    all_goals refine fun h ↦ (ha ?_).elim
    · exact isSelfAdjoint_inr (R := ℂ) |>.mp <| .of_nonneg h
    · exact .of_nonneg h

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

Tactic:
← star_star (r := ⟪x + y, z⟫)

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
x y z : E
⊢ star (star ⟪x + y, z⟫) = ⟪x, z⟫ + ⟪y, z⟫
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ inr '' Ici 0 ⊆ Ici 0

Tactic:
by
  rintro - ⟨a, ha, rfl⟩
  exact Unitization.inr_nonneg_iff.mpr ha

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

Goal state before:
pp: case pos
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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
⊢ Tendsto ((fun x ↦ cfcₙ (F x) a) ∘ Subtype.val) (comap Subtype.val l) (𝓝 (cfcₙ f a))

Tactic:
conv =>
      enter [1, x]
      rw [Function.comp_apply, cfcₙ_apply (hf := x.2.1) (hf0 := x.2.2)]

Goal state after:
case pos
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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
⊢ Tendsto
    (fun x ↦ (cfcₙHom ha) { toFun := (quasispectrum R a).domRestrict (F ↑x), continuous_toFun := ⋯, map_zero' := ⋯ })
    (comap Subtype.val l) (𝓝 (cfcₙ f a))
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 → α
⊢ ‖replicateRow ι v‖ = ‖toLp 2 v‖

Tactic:
rw [frobenius_norm_def, Fintype.sum_unique, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow]
  simp only [replicateRow_apply, Real.rpow_two]

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
i✝ : A
hx : 0 ≤ i✝ ∧ ‖i✝‖ < 1
⊢ i✝ ∈ closedBall 0 1

Tactic:
simpa using hx.2.le

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

Goal state before:
pp: case smul
𝕜 : 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
r : 𝕜
f : C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : Commute ((cfcₙHom ha) f) b
⊢ Commute ((cfcₙHom ha) (r • f)) b

Tactic:
rw [map_smul]; exact hf.smul_left r

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
a : A
ha : IsStarNormal a
this : cfcₙ (fun z ↦ ↑z.re) a + I • cfcₙ (fun z ↦ ↑z.im) a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ cfcₙ (fun x ↦ ↑x.im) a = ↑(ℑ a)

Tactic:
cfcₙ_re_id 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
a : A
ha : IsStarNormal a
this : ↑(ℜ a) + I • cfcₙ (fun z ↦ ↑z.im) a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ cfcₙ (fun x ↦ ↑x.im) a = ↑(ℑ a)
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✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : ContinuousStar A
a : A
ha : p a
⊢ StarSubalgebra.map (cfcHom ha) ⊤ = elemental 𝕜 a

Tactic:
← ContinuousMap.elemental_id_eq_top,

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✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : ContinuousStar A
a : A
ha : p a
⊢ StarSubalgebra.map (cfcHom ha) (elemental 𝕜 (ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜))) =
    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✝⁷ : 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) ⊤ ≤ elemental 𝕜 a

Tactic:
← ContinuousMap.elemental_id_eq_top,

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) (elemental 𝕜 (ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜))) ≤
    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✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ ⇑(cfcₙHom ha) '' {ContinuousMapZero.id (quasispectrum 𝕜 a)} = {a}

Tactic:
simpa using cfcₙHom_id ha

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✝¹⁰ : 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
⊢ (Set.range fun x ↦ cfcₙ x a) ⊆ ↑(elemental 𝕜 a)

Tactic:
grw [range_cfcₙ_eq_range_cfcₙHom 𝕜 ha, range_cfcₙHom_le 𝕜 ha]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.UnitBall

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

Tactic:
norm_inv,

Goal state after:
𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x : ↑(sphere 0 1)
⊢ ‖↑x‖⁻¹ = 1
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 : Pretrivialization F proj
s : Set B
x : B
y : F
⊢ (x, y) ∈ ↑e.symm ⁻¹' proj ⁻¹' s ∩ e.baseSet ×ˢ univ ↔ (x, y) ∈ (s ∩ e.baseSet) ×ˢ univ

Tactic:
suffices x ∈ e.baseSet → (proj (e.toPartialEquiv.symm (x, y)) ∈ s ↔ x ∈ s) by
    simpa only [prodMk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ, and_congr_left_iff]

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
s : Set B
x : B
y : F
⊢ x ∈ e.baseSet → (proj (↑e.symm (x, y)) ∈ s ↔ x ∈ s)
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (Z.localTrivAsPartialEquiv i).invFun ⁻¹' ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s))

Tactic:
let f := e.symm.trans e'

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (Z.localTrivAsPartialEquiv i).invFun ⁻¹' ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s))
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: case refine_1
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x₁ x₂ : X
x✝¹ : f x₁ = f x₂
x✝ : x₁ ≠ x₂
h : ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂
⊢ (Function.pullbackDiagonal f)ᶜ ∈ comap Subtype.val (𝓝 x₁ ×ˢ 𝓝 x₂)

Tactic:
← Filter.disjoint_iff,

Goal state after:
case refine_1
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x₁ x₂ : X
x✝¹ : f x₁ = f x₂
x✝ : x₁ ≠ x₂
h : Disjoint (𝓝 x₁) (𝓝 x₂)
⊢ (Function.pullbackDiagonal f)ᶜ ∈ comap Subtype.val (𝓝 x₁ ×ˢ 𝓝 x₂)
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
x : ↑s
f : E → ↑s
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set ↑s
hxU : x ∈ U
hU : IsOpen[instTopologicalSpaceSubtype] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
this : Subtype.val ∘ f ⁻¹' Subtype.val '' U = f ⁻¹' U
⊢ IsOpen[inst✝²] (Subtype.val ∘ f ⁻¹' Subtype.val '' U)

Tactic:
by rwa [this]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑(x.path y) '' univ ∩ ⇑(y.path x) '' univ = {x, y}

Tactic:
unitInterval.univ_eq_Icc,

Goal state after:
x y : Circle
h : x ≠ y
⊢ ⇑(x.path y) '' Icc 0 1 ∩ ⇑(y.path x) '' Icc 0 1 = {x, y}
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
hz : ∀ n > 0, z ^ n ∈ centeredArc (π / 2)
⊢ z = 1

Tactic:
have hz1 : z ∈ centeredArc (π / 2) := by simpa using hz 1
  have h (n : ℕ) : z ∈ centeredArc (π / 2 ^ (n + 1)) := by
    induction n with
    | zero => simpa using hz1
    | succ n ih =>
        simpa [div_div, ← pow_succ'] using mem_centeredArc_div
          (div_le_self pi_nonneg one_le_two) (by simpa) (hz (2 ^ (n + 1)) (by positivity))
  simpa [h] using Set.ext_iff.mp hasBasis_centeredArc_div_two_pow.ker z

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : A = adjoint B
x : E
y : F
⊢ ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜

Tactic:
rw [h, adjoint_inner_left]

Goal state after:
Module: Mathlib.Analysis.Calculus.AddTorsor.AffineMap

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : WithTop ℕ∞
f : V →ᴬ[𝕜] W
⊢ ContDiff 𝕜 n ⇑f

Tactic:
by
  rw [f.decomp]
  apply f.contLinear.contDiff.add
  exact contDiff_const

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
⊢ ‖A‖ * ‖A‖ ≤ ‖adjoint A ∘SL A‖

Tactic:
rw [← sq, ← Real.sqrt_le_sqrt_iff (norm_nonneg _), Real.sqrt_sq (norm_nonneg _)]

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
⊢ ‖A‖ ≤ √‖adjoint A ∘SL A‖
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = adjoint B
x : E
y : F
⊢ ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜

Tactic:
rw [h, adjoint_inner_left]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ Finset.centroid k univ (s.face h).points = Finset.centroid k fs s.points

Tactic:
by
  convert! (Finset.univ.centroid_map k (fs.orderEmbOfFin h).toEmbedding s.points).symm
  rw [← Finset.coe_inj, Finset.coe_map, Finset.coe_univ, Set.image_univ]
  simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = adjoint B
x : ι₁
y : ι₂
⊢ ⟪A (b₁ x), b₂ y⟫_𝕜 = ⟪b₁ x, B (b₂ y)⟫_𝕜

Tactic:
rw [h, adjoint_inner_left]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = adjoint B
x : ι
y : F
⊢ ⟪A (b x), y⟫_𝕜 = ⟪b x, B y⟫_𝕜

Tactic:
rw [h, adjoint_inner_left]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = adjoint B
x : ι
y : E
⊢ ⟪A y, b x⟫_𝕜 = ⟪y, B (b x)⟫_𝕜

Tactic:
rw [h, adjoint_inner_left]

Goal state after: