mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case refine_3.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r / (‖a‖₊ * ‖a‖₊) < ‖k‖₊

Tactic:
div_eq_mul_inv,

Goal state after:
case refine_3.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r * (‖a‖₊ * ‖a‖₊)⁻¹ < ‖k‖₊
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
⊢ φ 1 * (1 - φ 1) = 0

Tactic:
mul_sub,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
⊢ φ 1 * 1 - φ 1 * φ 1 = 0
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ : ∀ (x : Unitization 𝕜 E), ‖((splitMul 𝕜 E) x).2‖ ≤ ‖((splitMul 𝕜 E) x⋆).2‖
h₂ : ‖((splitMul 𝕜 E) (x⋆ * x)).2‖ = ‖((splitMul 𝕜 E) x).2‖ ^ 2
h₃ : ‖((splitMul 𝕜 E) (x⋆ * x)).1‖ = ‖((splitMul 𝕜 E) x).1‖ ^ 2
h : ‖((splitMul 𝕜 E) x).2‖ ≤ ‖((splitMul 𝕜 E) x).1‖
⊢ max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ * max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ ≤
    max (‖((splitMul 𝕜 E) x).1‖ ^ 2) (‖((splitMul 𝕜 E) x).2‖ ^ 2)

Tactic:
rw [sq, sq, sup_eq_left.mpr h, sup_eq_left.mpr (mul_self_le_mul_self (norm_nonneg _) h)]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
⊢ ⇑toContinuousMapHom ⁻¹'
      closure ↑(NonUnitalStarSubalgebra.map toContinuousMapHom (adjoin 𝕜 {ContinuousMapZero.id s})) =
    Set.univ

Tactic:
NonUnitalStarAlgHom.map_adjoin_singleton,

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
⊢ ⇑toContinuousMapHom ⁻¹' closure ↑(adjoin 𝕜 {toContinuousMapHom (ContinuousMapZero.id s)}) = Set.univ
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
s : Set α
γ : Type u_5
inst✝ : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousOn f s
hi : IsInducing i
h_cl : IsClosed[inst✝¹] (range i)
⊢ UpperHemicontinuousOn (fun x ↦ i ⁻¹' f x) s

Tactic:
rw [upperHemicontinuousOn_iff] at hf ⊢
  exact fun x hx ↦ (hf x hx).isInducing_comp hi h_cl

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case a
α : Type u_1
U V : SetRel α α
s₁ s₃ s₂ : Set α
h₁₂ : (s₁, s₂).1 ⊆ U.preimage (s₁, s₂).2
h₂₁ : (s₁, s₂).2 ⊆ U.image (s₁, s₂).1
h₂₃ : (s₂, s₃).1 ⊆ V.preimage (s₂, s₃).2
h₃₂ : (s₂, s₃).2 ⊆ V.image (s₂, s₃).1
⊢ (s₁, s₃) ∈ hausdorffEntourage (U ○ V)

Tactic:
simp only at *

Goal state after:
case a
α : Type u_1
U V : SetRel α α
s₁ s₃ s₂ : Set α
h₁₂ : s₁ ⊆ U.preimage s₂
h₂₁ : s₂ ⊆ U.image s₁
h₂₃ : s₂ ⊆ V.preimage s₃
h₃₂ : s₃ ⊆ V.image s₂
⊢ (s₁, s₃) ∈ hausdorffEntourage (U ○ V)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ : (s, t) ∈ hausdorffEntourage V
hst : (s, t).1 ⊆ V.preimage (s, t).2
hts : (s, t).2 ⊆ V.image (s, t).1
⊢ closure[inst✝.toTopologicalSpace] (s, t).1 ⊆ SetRel.preimage U (closure[inst✝.toTopologicalSpace] (s, t).2) ∧
    closure[inst✝.toTopologicalSpace] (s, t).2 ⊆ SetRel.image U (closure[inst✝.toTopologicalSpace] (s, t).1)

Tactic:
simp only at *

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ : (s, t) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
⊢ closure[inst✝.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst✝.toTopologicalSpace] t) ∧
    closure[inst✝.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst✝.toTopologicalSpace] s)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : ↑K ⊆ V.preimage t
⊢ ⋃ K_1 ∈ {x | (fun K' ↦ (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}, ↑K_1 ⊆ U.preimage t

Tactic:
Set.iUnion₂_subset_iff

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : ↑K ⊆ V.preimage t
⊢ ∀ i ∈ {x | (fun K' ↦ (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}, ↑i ⊆ U.preimage t
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
⊢ s ⤳ t

Tactic:
Specializes,

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
⊢ 𝓝 s ≤ 𝓝 t
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : 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
this : CompleteSpace ↥S
μ : 𝕜
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ map (fun x_1 ↦ (algebraMap 𝕜 ↥S) x_1 - x) (𝓝 μ) ≤ 𝓝 ((algebraMap 𝕜 ↥S) μ - x)

Tactic:
← Filter.Tendsto,

Goal state after:
𝕜 : 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
this : CompleteSpace ↥S
μ : 𝕜
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ Tendsto (fun x_1 ↦ (algebraMap 𝕜 ↥S) x_1 - x) (𝓝 μ) (𝓝 ((algebraMap 𝕜 ↥S) μ - x))
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
x : α
hx : ClusterPt x l
⊢ ⋃ K_1 ∈ {x | (fun K' ↦ (↑K, ↑K') ∈ hausdorffEntourage U) x}, ↑K_1 ⊆ U.image ↑K

Tactic:
Set.iUnion₂_subset_iff

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
x : α
hx : ClusterPt x l
⊢ ∀ i ∈ {x | (fun K' ↦ (↑K, ↑K') ∈ hausdorffEntourage U) x}, ↑i ⊆ U.image ↑K
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inr
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h✝ : Nontrivial A
⊢ ‖cfc f a‖ < c

Tactic:
refine cfc_cases (‖·‖ < c) a f (by simpa) fun hf ha ↦ ?_

Goal state after:
case inr
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h✝ : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ ‖(cfcHom ha) { toFun := (σ 𝕜 a).domRestrict f, continuous_toFun := ⋯ }‖ < c
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarRing A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Module ℝ A
inst✝³ : IsScalarTower ℝ A A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ 0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal

Tactic:
by
  refine ⟨fun ha ↦ ⟨.of_nonneg ha, .nnreal_of_nonneg ha⟩, ?_⟩
  rintro ⟨ha₁, ha₂⟩
  obtain ⟨x, hx, -, rfl⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts ha₁ ha₂
  simpa [sq, hx.star_eq] using star_mul_self_nonneg x

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: A : Type u_4
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : ↑‖x‖₊ = spectralRadius ℝ a
this : 0 ≤ x
⊢ ↑‖x‖₊ ∈ spectrum ℝ a

Tactic:
convert! hx₁

Goal state after:
A : Type u_4
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : ↑‖x‖₊ = spectralRadius ℝ a
this : 0 ≤ x
⊢ ↑‖x‖₊ = x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: A : Type u_1
inst✝⁷ : Ring A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarRing A
inst✝⁴ : StarOrderedRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
ha : IsStrictlyPositive a
hb : IsStrictlyPositive b
⊢ Commute a b ↔ IsStrictlyPositive (a * b)

Tactic:
commute_iff_mul_nonneg ha.nonneg hb.nonneg

Goal state after:
A : Type u_1
inst✝⁷ : Ring A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarRing A
inst✝⁴ : StarOrderedRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
ha : IsStrictlyPositive a
hb : IsStrictlyPositive b
⊢ 0 ≤ a * b ↔ IsStrictlyPositive (a * b)
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✝ : DiscreteTopology α
⊢ DiscreteTopology (Compacts α)

Tactic:
rw [discreteTopology_iff_isOpen_singleton]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : DiscreteTopology α
⊢ ∀ (a : Compacts α), IsOpen {a}
Module: Mathlib.Analysis.CStarAlgebra.Exponential

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ selfAdjoint.expUnitary a * selfAdjoint.expUnitary b = selfAdjoint.expUnitary b * selfAdjoint.expUnitary a

Tactic:
← h.expUnitary_add,

Goal state after:
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ selfAdjoint.expUnitary (a + b) = selfAdjoint.expUnitary b * selfAdjoint.expUnitary a
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
⊢ expMulMulExp a b x z = x

Tactic:
by
  have hf : Differentiable ℂ (expMulMulExp a b x : ℂ → A) := by unfold expMulMulExp; fun_prop
  have : IsBounded (Set.range (expMulMulExp a b x)) := by
    apply Metric.isBounded_sphere (x := (0 : A)) (r := ‖x‖) |>.subset
    rintro - ⟨z, hz, rfl⟩
    rw [mem_sphere_iff_norm, sub_zero, expMulMulExp_eq_expUnitary_mul_mul_expUnitary h z,
      CStarRing.norm_mul_coe_unitary, CStarRing.norm_coe_unitary_mul]
  simpa [expMulMulExp] using hf.apply_eq_apply_of_bounded this z 0

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

Goal state before:
pp: case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : y ∈ B.polar Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖(B (c⁻¹ • x)) y‖ ≤ 1

Tactic:
exact hy _ trivial

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

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ (convexHull ℝ) (balancedHull ℝ s) ⊆ (convexHull ℝ) (s ∪ -s)

Tactic:
by
      rw [← Convex.convexHull_eq (convex_convexHull ℝ (s ∪ -s))]
      exact convexHull_mono balancedHull_subset_convexHull_union_neg

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
⊢ c⁻¹ • x' ∈ polar 𝕜 s

Tactic:
have eq : ∀ z, ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖ := fun z => norm_smul c⁻¹ _

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖x' z‖ ≤ 1
hcr : 0 < ‖c‖ / r
x : E
h₁ : r / ‖c‖ ≤ ‖x‖
h₂ : ‖x‖ < r
⊢ (‖c‖ / r)⁻¹ ≤ ‖x‖

Tactic:
by rwa [inv_div]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ approx (n + 1) c x
c : CU P
⊢ midpoint ℝ (approx n c.left x) (approx n c.right x) ≤ midpoint ℝ (approx (n + 1) c.left x) (approx (n + 1) c.right x)

Tactic:
exact midpoint_le_midpoint (ihn _) (ihn _)

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCommCStarAlgebra A
a b : A
h : a * b = 0
⊢ ‖a + b‖ = max ‖a‖ ‖b‖

Tactic:
let f := gelfandStarTransform A⁺¹ ∘ inrNonUnitalAlgHom ℂ A
  have hf : Isometry f := gelfandTransform_isometry _ |>.comp isometry_inr
  simp_rw [← hf.norm_map_of_map_zero (by simp [f]), show f (a + b) = f a + f b by simp [f]]
  exact ContinuousMap.norm_add_eq_max <| by simpa [f] using congr(f $h)

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✝ : T2Space A
a : A
⊢ (-a)⁺ = a⁻

Tactic:
by
  by_cases ha : IsSelfAdjoint a
  · rw [posPart_def, negPart_def, ← cfcₙ_comp_neg _ _]
    congr! 2
  · have ha' : ¬ IsSelfAdjoint (-a) := fun h ↦ ha (by simpa using h.neg)
    rw [posPart_def, negPart_def, cfcₙ_apply_of_not_predicate a ha,
      cfcₙ_apply_of_not_predicate _ ha']

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

Goal state before:
pp: case neg
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
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
case neg =>
    simp [nnrpow_def, cfcₙ_apply_of_not_predicate a ha]

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 : ℝ
h : IsUnit a
ha : 0 ≤ a
this : IsStrictlyPositive a
⊢ (a ^ (1 / 2)) ^ x = a ^ (x / 2)

Tactic:
div_eq_mul_inv,

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 : ℝ
h : IsUnit a
ha : 0 ≤ a
this : IsStrictlyPositive a
⊢ (a ^ (1 * 2⁻¹)) ^ x = a ^ (x / 2)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ IsClosed {a | 0 ≤ a}

Tactic:
by
  suffices IsClosed {a : A⁺¹ | 0 ≤ a} by
    rw [Unitization.isometry_inr (𝕜 := ℂ) |>.isClosedEmbedding.isClosed_iff_image_isClosed]
    convert! this.inter <| (Unitization.isometry_inr (𝕜 := ℂ)).isClosedEmbedding.isClosed_range
    ext a
    simp only [Set.mem_image, Set.mem_ofPred_eq, Set.mem_inter_iff, Set.mem_range,
      ← exists_and_left]
    congr! 2 with x
    exact and_congr_left fun h ↦ by simp [← h]
  simp only [nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts,
    and_congr_right (SpectrumRestricts.nnreal_iff_nnnorm · le_rfl), Set.ofPred_and]
  refine isClosed_eq ?_ ?_ |>.inter <| isClosed_le ?_ ?_
  all_goals fun_prop

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

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

Tactic:
rintro a b ha₁ - ha₂ -

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: 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✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
⊢ LipschitzOnWith 1 (fun f ↦ cfcₙ ((toFun {quasispectrum R a}) f) a)
    {f | ContinuousOn ((toFun {quasispectrum R a}) f) (quasispectrum R a) ∧ f 0 = 0}

Tactic:
by
  by_cases ha : p a
  · rintro f ⟨hf, hf0⟩ g ⟨hg, hg0⟩
    simp only
    rw [cfcₙ_apply .., cfcₙ_apply .., isometry_cfcₙHom (R := R) a ha |>.edist_eq]
    simp only [ENNReal.coe_one, one_mul]
    rw [← ContinuousMapZero.isometry_toContinuousMap.edist_eq,
      edist_continuousRestrict_of_singleton hf hg]
  · simpa [cfcₙ_apply_of_not_predicate a ha] using LipschitzWith.const' 0 |>.lipschitzOnWith

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

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
f : α → β
hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊
⊢ ‖A.map f‖₊ = ‖A‖₊

Tactic:
by
  simp only [nnnorm_def, Pi.nnnorm_def, Matrix.map_apply, hf]

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
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun y ↦ 1 - (1 + y)⁻¹
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
⊢ ‖m - x * m‖₊ ≤ ε

Tactic:
have hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (spectrum ℝ≥0 m) :=
    ContinuousOn.inv₀ (by fun_prop) fun _ _ ↦ by positivity

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun y ↦ 1 - (1 + y)⁻¹
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
⊢ ‖m - x * m‖₊ ≤ ε