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 β
f : α → γ → β
K : ℝ≥0
s : Set γ
h : ∀ (c : α), LipschitzOnWith K (f c) s
⊢ UniformEquicontinuousOn f s

Tactic:
rw [uniformEquicontinuousOn_iff_uniformContinuousOn]

Goal state after:
α : 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
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
r : ℝ≥0
hr : 0 < ↑r
⊢ ‖a ^ r‖₊ = ‖a‖₊ ^ ↑r

pp: A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
r : ℝ≥0
hr : 0 < ↑r
⊢ 0 < r

Tactic:
← nnnorm_nnrpow a

Goal state after:
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
r : ℝ≥0
hr : 0 < ↑r
⊢ ‖a ^ r‖₊ = ‖a ^ r‖₊

A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
r : ℝ≥0
hr : 0 < ↑r
⊢ 0 < r

A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
r : ℝ≥0
hr : 0 < ↑r
⊢ 0 < r
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ ‖a⁺‖ ≤ ‖a‖

Tactic:
by
  by_cases ha : IsSelfAdjoint a
  case neg => simp [CFC.posPart_def, cfcₙ_apply_of_not_predicate a ha]
  refine norm_cfcₙ_le fun x hx ↦ ?_
  obtain (h | h) := le_or_gt x 0
  · simp [posPart_def, max_eq_right h]
  · simp only [posPart_def, max_eq_left h.le]
    exact NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le a hx 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
y : ℝ
ha : 0 ≤ a
⊢ a ^ y = cfc (fun x ↦ x ^ y) a

Tactic:
CFC.rpow_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
a : A
y : ℝ
ha : 0 ≤ a
⊢ cfc (fun x ↦ x ^ y) a = cfc (fun x ↦ x ^ y) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

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

Tactic:
exact .of_nonneg h

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.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
this : a * star a ≤ (algebraMap ℝ A) ‖a * star a‖
⊢ a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)

Tactic:
CStarRing.norm_self_mul_star,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
this : a * star a ≤ (algebraMap ℝ A) (‖a‖ * ‖a‖)
⊢ a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
| ‖sqrt a * ↑b ^ (-(1 / 2))‖ ≤ 1

Tactic:
← sq_le_one_iff₀ (norm_nonneg _),

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
| ‖sqrt a * ↑b ^ (-(1 / 2))‖ ^ 2 ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖sqrt ↑a * sqrt ↑b⁻¹‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Tactic:
← sq_le_one_iff₀ (norm_nonneg _),

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖sqrt ↑a * sqrt ↑b⁻¹‖ ^ 2 ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ↑b⁻¹ ≤ ↑a⁻¹
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a‖ ≤ 1

Tactic:
← sq_le_one_iff₀ (norm_nonneg _),

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a‖ ^ 2 ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑b⁻¹) * star (sqrt ↑a) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a * (star (sqrt ↑a) * star (sqrt ↑b⁻¹))‖ ≤ 1

Tactic:
IsSelfAdjoint.of_nonneg (sqrt_nonneg _),

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖sqrt ↑b⁻¹ * star (sqrt ↑a) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a * (sqrt ↑a * star (sqrt ↑b⁻¹))‖ ≤ 1
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‖ ^ 2 = ‖⟪x, y⟫_A * star ⟪x, y⟫_A‖

Tactic:
CStarRing.norm_self_mul_star,

Goal state after:
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‖ ^ 2 = ‖⟪x, y⟫_A‖ * ‖⟪x, y⟫_A‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc f)
⊢ ConcaveOn ℝ s (-cfcₙ (-f))

Tactic:
refine (convexOn_cfcₙ_of_convexOn_cfc ?_).neg

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc f)
⊢ ConvexOn ℝ (inr '' s) (cfc (-f))
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x ↦ x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → ↑({x | 0 ≤ x} ∩ ball 0 1)
this : ∑ i, c i • ↑(x i) ∈ span ℂ ({x | 0 ≤ x} ∩ ball 0 1)
i : Fin n
x✝ : i ∈ Finset.univ
⊢ ‖↑(x i)‖ < 1

Tactic:
by simpa using (x i).2.2

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

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
r : ℝ≥0
hr : 0 < r
A : Matrix m n α
⊢ ‖fun i j ↦ A i j‖₊ < r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ < r

Tactic:
pi_nnnorm_lt_iff hr

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:
frobenius_nnnorm_def,

Goal state after:
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‖₊
⊢ (∑ i, ∑ j, ‖A.map f i j‖₊ ^ 2) ^ (1 / 2) = (∑ i, ∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2)
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖Aᵀ‖₊ = ‖A‖₊

Tactic:
frobenius_nnnorm_def,

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ (∑ i, ∑ j, ‖Aᵀ i j‖₊ ^ 2) ^ (1 / 2) = ‖A‖₊
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ (∑ i, ∑ j, ‖Aᵀ i j‖₊ ^ 2) ^ (1 / 2) = ‖A‖₊

Tactic:
frobenius_nnnorm_def,

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ (∑ i, ∑ j, ‖Aᵀ i j‖₊ ^ 2) ^ (1 / 2) = (∑ i, ∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2)
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
⊢ ‖diagonal v‖₊ = ‖toLp 2 v‖₊

Tactic:
frobenius_nnnorm_def,

Goal state after:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
⊢ (∑ i, ∑ j, ‖diagonal v i j‖₊ ^ 2) ^ (1 / 2) = ‖toLp 2 v‖₊
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
⊢ ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊

Tactic:
frobenius_nnnorm_def,

Goal state after:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
⊢ (∑ i, ∑ j, ‖(A * B) i j‖₊ ^ 2) ^ (1 / 2) ≤ (∑ i, ∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ i, ∑ j, ‖B i j‖₊ ^ 2) ^ (1 / 2)
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ a, 0 ≤ a ∧ ↑C * ‖a‖ < ‖f a‖
x : ℕ → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), 2 ^ (2 * x_1) < ‖f (x x_1)‖
⊢ False

Tactic:
have x_summable : Summable fun n : ℕ => (2 : ℝ) ^ (-(n : ℤ)) • x n := by
    refine Summable.of_norm ?_
    have : (2 : ℝ)⁻¹ < 1 := by norm_num
    simp [norm_smul, hx_norm, ← inv_pow, this]

Goal state after:
A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ a, 0 ≤ a ∧ ↑C * ‖a‖ < ‖f a‖
x : ℕ → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), 2 ^ (2 * x_1) < ‖f (x x_1)‖
x_summable : Summable fun n ↦ 2 ^ (-↑n) • x n
⊢ False
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: 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
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (quasispectrum ℝ a)
hf0 : { toFun := (quasispectrum ℝ a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : IsSelfAdjoint a
⊢ Commute ((cfcₙHom ha) { toFun := (quasispectrum ℝ a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }) b

Tactic:
rw [← cfcₙ_apply ..]

Goal state after:
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
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (quasispectrum ℝ a)
hf0 : { toFun := (quasispectrum ℝ a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : IsSelfAdjoint a
⊢ Commute (cfcₙ f a) b
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝² : Fintype m
inst✝¹ : NonUnitalCStarAlgebra A
inst✝ : Fintype n
⊢ ∀ (x y : CStarMatrix n n A),
    (↑(MulOpposite.opLinearEquiv ℂ) ∘ₗ toCLM).toFun (x * y) =
      (↑(MulOpposite.opLinearEquiv ℂ) ∘ₗ toCLM).toFun x * (↑(MulOpposite.opLinearEquiv ℂ) ∘ₗ toCLM).toFun y

Tactic:
intros

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝² : Fintype m
inst✝¹ : NonUnitalCStarAlgebra A
inst✝ : Fintype n
x✝ y✝ : CStarMatrix n n A
⊢ (↑(MulOpposite.opLinearEquiv ℂ) ∘ₗ toCLM).toFun (x✝ * y✝) =
    (↑(MulOpposite.opLinearEquiv ℂ) ∘ₗ toCLM).toFun x✝ * (↑(MulOpposite.opLinearEquiv ℂ) ∘ₗ toCLM).toFun y✝
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
⊢ ∀ (i i_1 : n), ‖U i i_1‖ ≤ 1

Tactic:
intros

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i✝¹ i✝ : n
⊢ ‖U i✝¹ i✝‖ ≤ 1
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst✝] (f.target ∩ ↑f.symm ⁻¹' ↑s)
⊢ (f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans ((s.openPartialHomeomorphSubtypeCoe hs).trans f') ≈
    (f.symm.trans f').restr (f.target ∩ ↑f.symm ⁻¹' ↑s)

Tactic:
← ofSet_trans _ openness₁,

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst✝] (f.target ∩ ↑f.symm ⁻¹' ↑s)
⊢ (f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans ((s.openPartialHomeomorphSubtypeCoe hs).trans f') ≈
    (ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans (f.symm.trans f')
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
n : ℕ
x y : A
⊢ (↑n).2 x * y = x * (↑n).1 y

Tactic:
by
      rw [Prod.snd_natCast, Prod.fst_natCast]
      simp only [← Nat.smul_one_eq_cast, smul_apply, one_apply_eq_self, mul_smul_comm,
        smul_mul_assoc]

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsOpen[instTopologicalSpaceSubtype] (Set.range (toPullbackDiag f)) ↔ IsOpenEmbedding (toPullbackDiag f)

Tactic:
exact ⟨fun h ↦ ⟨.toPullbackDiag f, h⟩, fun h ↦ h.isOpen_range⟩

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsLocalHomeomorph f
hs : Function.Surjective f
⊢ DiscreteTopology X ↔ DiscreteTopology Y

Tactic:
by
  rw [← (Homeomorph.Set.univ Y).discreteTopology_iff, ← hs.range_eq, h.discreteTopology_range_iff]

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
inst✝ : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
e : ↑(f ⁻¹' t.baseSet)
⊢ (f ⁻¹' t.baseSet).domRestrict (↑t.toPartialEquiv) e = (Prod.map Subtype.val id ∘ fun e ↦ (⟨f ↑e, ⋯⟩, (↑t ↑e).2)) e

Tactic:
by simp [t.mk_proj_snd' e.2]

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_3
inst✝¹ : Group G
inst✝ : MulAction G E
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
x : X
⊢ x ∈ f '' {e | MulAction.stabilizer G e = ⊥}

Tactic:
obtain ⟨e, rfl⟩ := h.surjective x

Goal state after:
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
e : E
⊢ f e ∈ f '' {e | MulAction.stabilizer G e = ⊥}
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
⊢ ((expSeries 𝕜 C(α, 𝕜)).sum f) a = { toFun := exp ∘ ⇑f, continuous_toFun := ⋯ } a

Tactic:
FormalMultilinearSeries.sum

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
⊢ (∑' (n : ℕ), (expSeries 𝕜 C(α, 𝕜) n) fun x ↦ f) a = { toFun := exp ∘ ⇑f, continuous_toFun := ⋯ } a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
⊢ exp f = { toFun := exp ∘ ⇑f, continuous_toFun := ⋯ }

Tactic:
by
  ext a
  simp_rw [NormedSpace.exp_eq_expSeries_sum (𝔸 := C(α, 𝕜)) 𝕜, FormalMultilinearSeries.sum]
  have h_sum := NormedSpace.expSeries_summable (𝕂 := 𝕜) f
  simp_rw [← ContinuousMap.tsum_apply h_sum a, NormedSpace.expSeries_apply_eq]
  simp [NormedSpace.exp_eq_tsum 𝕜]

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

Goal state before:
pp: r : ℝ
hr : r ≤ π
⊢ BijOn (⇑exp) (Ioo (-r) r) (⇑exp '' {x | |x| < r})

Tactic:
abs_lt,

Goal state after:
r : ℝ
hr : r ≤ π
⊢ BijOn (⇑exp) (Ioo (-r) r) (⇑exp '' {x | -r < x ∧ x < r})
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
⊢ range ⇑(x.path y) = ⇑exp '' Icc (↑x).arg (x.angleDiff y + (↑x).arg)

Tactic:
rw [coe_path, range_comp, Path.range_segment, segment_eq_Icc (by simp)]

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

Goal state before:
pp: ⊢ (Filter.map (⇑exp) (nhds 0)).HasBasis (fun x ↦ True) fun n ↦ ⇑exp '' {x | |x| < π / 2 ^ (n + 1)}

Tactic:
abs_lt,

Goal state after:
⊢ (Filter.map (⇑exp) (nhds 0)).HasBasis (fun x ↦ True) fun n ↦
    ⇑exp '' {x | -(π / 2 ^ (n + 1)) < x ∧ x < π / 2 ^ (n + 1)}
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a + I • cfcₙ Real.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a

pp: case nonneg
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ 0 ≤ 1 - a ^ 2

Tactic:
case nonneg =>
      rwa [sub_nonneg, ← CStarAlgebra.norm_le_one_iff_of_nonneg (a ^ 2), sq, ha.norm_mul_self,
        sq_le_one_iff₀ (by positivity)]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a + I • cfcₙ Real.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
⊢ IsIdempotentElem T ∧ IsSelfAdjoint T ↔ IsIdempotentElem T ∧ IsStarNormal T

Tactic:
and_congr_right_iff

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
⊢ IsIdempotentElem T → (IsSelfAdjoint T ↔ IsStarNormal T)
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : #s = finrank k ↥sp.direction + 1
⊢ affineSpan k ↑(Finset.image p s) = sp

Tactic:
have hn : s.Nonempty := by
    rw [← Finset.card_pos, hc]
    apply Nat.succ_pos

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : #s = finrank k ↥sp.direction + 1
hn : s.Nonempty
⊢ affineSpan k ↑(Finset.image p s) = sp
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 : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hmem1 : s.medial.points 0 ∈ affineSpan k (Set.range s.medial.points)
hmem2 : s.medial.points 0 ∈ affineSpan k (Set.range s.points)
v : V
this : (∃ a b, (↑n)⁻¹ • (s.points b -ᵥ s.points a) = v) ↔ ∃ a b, -((↑n)⁻¹ • (s.points a -ᵥ s.points b)) = v
⊢ v ∈ Set.range s.medial.points -ᵥ Set.range s.medial.points ↔ v ∈ (-↑n)⁻¹ • (Set.range s.points -ᵥ Set.range s.points)

Tactic:
simpa [Set.mem_vsub, Set.mem_smul_set, medial_points,
      faceOppositeCentroid_vsub_faceOppositeCentroid]

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : x ∈ ball c f.rOut
⊢ ↑f x ≠ 0

Tactic:
by rwa [← support_eq, mem_support] at hx

Goal state after: