mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : ℂ
hf : Differentiable ℂ (expMulMulExp a b x)
z : ℂ
⊢ expMulMulExp a b x z ∈ Metric.sphere 0 ‖x‖

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

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommMonoid E
inst✝² : SeminormedRing 𝕜
inst✝¹ : SMul 𝕜 E
inst✝ : PartialOrder 𝕜
⊢ Nonempty (AbsConvexOpenSets 𝕜 E)

Tactic:
by
  rw [← exists_true_iff_nonempty]
  dsimp only [AbsConvexOpenSets]
  rw [Subtype.exists]
  exact ⟨Set.univ, ⟨mem_univ 0, isOpen_univ, balanced_univ, convex_univ⟩, trivial⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹² : AddCommGroup E
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : IsRCLikeNormedField 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : PolynormableSpace 𝕜 E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
S : Submodule 𝕜 E
f : ↥S →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(↑f).range
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ ∃ g, f = g ∘SL S.subtypeL

Tactic:
let b := Module.finBasis 𝕜 f.range

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝¹² : AddCommGroup E
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : IsRCLikeNormedField 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : PolynormableSpace 𝕜 E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
S : Submodule 𝕜 E
f : ↥S →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(↑f).range
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis (Fin (finrank 𝕜 ↥(↑f).range)) 𝕜 ↥(↑f).range := finBasis 𝕜 ↥(↑f).range
⊢ ∃ g, f = g ∘SL S.subtypeL
Module: Mathlib.Analysis.Normed.Algebra.Basic

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
φ : WeakDual 𝕜 A
hφ : φ ∈ characterSpace 𝕜 A
⊢ toStrongDual φ ∈ Metric.closedBall 0 ‖1‖

Tactic:
mem_closedBall_zero_iff

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
φ : WeakDual 𝕜 A
hφ : φ ∈ characterSpace 𝕜 A
⊢ ‖toStrongDual φ‖ ≤ ‖1‖
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ x ∈ c.right.C

pp: case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ x ∈ c.left.C

Tactic:
exacts [c.subset_right_C hx, hx]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
A : ∀ (n : ℕ), ∃ f, EqOn (⇑f) 1 s ∧ EqOn (⇑f) 0 (U n ∩ interior m)ᶜ ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
⊢ ∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
choose f fs fm _hf f_range using A

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : ℕ → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s
fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)
f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
⊢ ∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst✝²⁸ : CommSemiring R
inst✝²⁷ : CommRing S
inst✝²⁶ : Nontrivial R
inst✝²⁵ : StarRing R
inst✝²⁴ : MetricSpace R
inst✝²³ : IsTopologicalSemiring R
inst✝²² : ContinuousStar R
inst✝²¹ : Algebra R S
inst✝²⁰ : NonUnitalRing A
inst✝¹⁹ : NonUnitalRing B
inst✝¹⁸ : Module S A
inst✝¹⁷ : Module R A
inst✝¹⁶ : Module R B
inst✝¹⁵ : Module S B
inst✝¹⁴ : SMulCommClass R A A
inst✝¹³ : SMulCommClass R B B
inst✝¹² : IsScalarTower R A A
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : StarRing A
inst✝⁹ : StarRing B
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : IsScalarTower R S B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R (A × B) pab
inst✝³ : NonUnitalContinuousFunctionalCalculus R A pa
inst✝² : NonUnitalContinuousFunctionalCalculus R B pb
inst✝¹ : ContinuousMapZero.UniqueHom R A
inst✝ : ContinuousMapZero.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
hf₀ : f 0 = 0
⊢ (cfcₙ f (a, b)).1 = (cfcₙ f a, cfcₙ f b).1

Tactic:
let φ := NonUnitalStarAlgHom.fst S A B
      exact φ.map_cfcₙ f (a, b) (by rwa [Prod.quasispectrum_eq]) hf₀ continuous_fst hab ha

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

Goal state before:
pp: case h.right
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ (↑(realPart a))⁺ - (↑(realPart a))⁻ + (I • (↑(imaginaryPart a))⁺ - I • (↑(imaginaryPart a))⁻) =
    I ^ 0 • (↑(realPart a))⁺ + I ^ 1 • (↑(imaginaryPart a))⁺ + -1 • (↑(realPart a))⁻ + -I • (↑(imaginaryPart a))⁻

Tactic:
module

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

Goal state before:
pp: A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ ∃ x, (∀ (i : Fin 4), 0 ≤ x i) ∧ (∀ (i : Fin 4), ‖x i‖ ≤ ‖a‖) ∧ a = ∑ i, I ^ ↑i • x i

Tactic:
use ![(realPart a)⁺, (imaginaryPart a)⁺, (realPart a)⁻, (imaginaryPart a)⁻]
  rw [← and_assoc, ← forall_and]
  constructor
  · intro i
    fin_cases i
    all_goals
      constructor
      · simp
        cfc_tac
    · exact CStarAlgebra.norm_posPart_le _ |>.trans <| realPart.norm_le a
    · exact CStarAlgebra.norm_posPart_le _ |>.trans <| imaginaryPart.norm_le a
    · exact CStarAlgebra.norm_negPart_le _ |>.trans <| realPart.norm_le a
    · exact CStarAlgebra.norm_negPart_le _ |>.trans <| imaginaryPart.norm_le a
  · nth_rw 1 [← CStarAlgebra.linear_combination_nonneg a]
    simp only [Fin.sum_univ_four, Fin.coe_ofNat_eq_mod, Matrix.cons_val, Nat.reduceMod, I_sq,
      I_pow_three]
    module

Goal state after:
Module: Mathlib.Topology.ApproximateUnit

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MulOneClass α
m : α
⊢ Tendsto (fun x ↦ x * m) (pure 1) (𝓝 m)

Tactic:
by simpa using tendsto_pure_nhds (· * m) (1 : α)

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
a : A
x : ℝ
ha : IsStrictlyPositive a
⊢ a ^ (-x) * a ^ x = 1

Tactic:
by
  rw [← rpow_add ha.isUnit, neg_add_cancel, rpow_zero a]

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
⊢ cfcₙ (⇑NNReal.sqrt) a = cfc (⇑NNReal.sqrt) a

Tactic:
rw [cfcₙ_eq_cfc]

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
ha : 0 ≤ a
⊢ sqrt a ^ 2 = a

Tactic:
by
  rw [pow_two, sqrt_mul_sqrt_self (A := A) a]

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

Goal state before:
pp: case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
r : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
h✝ : Nontrivial A
⊢ ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r

Tactic:
· exact ⟨fun h x hx ↦ Real.le_norm_self x |>.trans (spectrum.norm_le_norm_of_mem hx) |>.trans h,
      fun h ↦ h ‖a‖ <| norm_mem_spectrum_of_nonneg⟩

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
inst✝ : StarModule ℂ A
z y : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext; simp

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
inst✝ : StarModule ℂ A
z : ℂ
y : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext; simp

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:
refine CStarAlgebra.norm_le_norm_of_nonneg_of_le ?_ inner_mul_inner_swap_le

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
⊢ 0 ≤ ⟪x, y⟫_A * ⟪y, x⟫_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 α
r : ℝ≥0
A : Matrix m n α
⊢ ‖A‖₊ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ ≤ r

Tactic:
by
  simp_rw [nnnorm_def, pi_nnnorm_le_iff]

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h : ‖star ↑z * (1 - ↑x) * ↑z‖ ≤ c ^ 2
⊢ 0 ≤ ↑x

Tactic:
rwa [inr_nonneg_iff]

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

Goal state before:
pp: case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j ↦ unitOf (A i j)
hxn : ‖x‖₊ = 1
hN : ‖∑ x, ↑‖A i x‖₊‖₊ * ‖1‖₊ ≤ N
⊢ ∑ j, ‖A i j‖₊ ≤ N

Tactic:
← NNReal.coe_sum,

Goal state after:
case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j ↦ unitOf (A i j)
hxn : ‖x‖₊ = 1
hN : ‖↑(∑ i_1, ‖A i i_1‖₊)‖₊ * ‖1‖₊ ≤ N
⊢ ∑ j, ‖A i j‖₊ ≤ N
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∀ (m : A), Tendsto (fun x ↦ x * m) (approximateUnit A) (𝓝 m)

Tactic:
exact tendsto_mul_right_approximateUnit

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✝¹ : AddMonoid A
inst✝ : StarAddMonoid A
⊢ conjTranspose 0 = 0

Tactic:
ext; simp

Goal state after:
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✝⁵ : Semiring R
inst✝⁴ : Semiring S
σ : R →+* S
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : Module R A
inst✝ : Module S B
f : A →ₛₗ[σ] B
M N : CStarMatrix m n A
⊢ (M + N).map ⇑f = M.map ⇑f + N.map ⇑f

Tactic:
ext; simp

Goal state after:
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✝⁵ : Semiring R
inst✝⁴ : Semiring S
σ : R →+* S
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : Module R A
inst✝ : Module S B
f : A →ₛₗ[σ] B
r : R
M : CStarMatrix m n A
⊢ (r • M).map ⇑f = σ r • M.map ⇑f

Tactic:
ext; simp

Goal state after:
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
l : Type u_7
o : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
eₘ : m ≃ l
eₙ : n ≃ o
M N : CStarMatrix m n A
⊢ (Matrix.reindex eₘ eₙ).toFun (M + N) = (Matrix.reindex eₘ eₙ).toFun M + (Matrix.reindex eₘ eₙ).toFun N

Tactic:
ext; simp

Goal state after:
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
l : Type u_7
o : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
eₘ : m ≃ l
eₙ : n ≃ o
r : R
M : CStarMatrix m n A
⊢ (Matrix.reindex eₘ eₙ).toFun (r • M) = (RingHom.id R) r • (Matrix.reindex eₘ eₙ).toFun M

Tactic:
ext; simp

Goal state after:
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
x✝¹ x✝ : A
⊢ (fun x y ↦ x✝¹ + x✝) = (fun x y ↦ x✝¹) + fun x y ↦ x✝

Tactic:
ext; simp

Goal state after:
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
x✝¹ : R
x✝ : A
⊢ (fun x y ↦ x✝¹ • x✝) = x✝¹ • fun x y ↦ x✝

Tactic:
ext; simp

Goal state after:
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
c : ℂ
M : CStarMatrix m n A
⊢ { toFun := ⇑(WithCStarModule.equivL ℂ).symm ∘ (fun v ↦ v ᵥ* (c • M)) ∘ ⇑(WithCStarModule.equivL ℂ), map_add' := ⋯,
      map_smul' := ⋯, cont := ⋯ } =
    (RingHom.id ℂ) c •
      { toFun := ⇑(WithCStarModule.equivL ℂ).symm ∘ (fun v ↦ v ᵥ* M) ∘ ⇑(WithCStarModule.equivL ℂ), map_add' := ⋯,
        map_smul' := ⋯, cont := ⋯ }

Tactic:
by
    ext x i
    simp only [ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
      WithCStarModule.equivL_apply, WithCStarModule.equivL_symm_apply,
      WithCStarModule.equiv_symm_pi_apply, _root_.smul_apply,
      WithCStarModule.smul_apply, RingHom.id_apply]
    rw [Matrix.vecMul_smul, Pi.smul_apply]

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace X
μ : Measure X
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Integrable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
⊢ cfc (fun z ↦ ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfc (f x) a ∂μ

Tactic:
have key₁ (z : spectrum 𝕜 a) :
      ∫ x, f x z ∂μ = (∫ x, mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z := by
    rw [integral_apply hf₂]
    refine integral_congr_ae ?_
    filter_upwards [hf₁] with x cont_x
    rw [mkD_apply_of_continuousOn cont_x]

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace X
μ : Measure X
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Integrable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
key₁ : ∀ (z : ↑(spectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
⊢ cfc (fun z ↦ ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfc (f x) a ∂μ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : MeasurableSpace X
μ : Measure X
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : IsScalarTower 𝕜 A A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝³ : CompleteSpace A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (s ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
⊢ IntegrableOn (fun x ↦ cfcₙ (f x) a) s μ

Tactic:
refine integrableOn_cfcₙ' _ _ ⟨?_, ?_⟩ ha
  · exact aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry hs _ _ hf f_zero
  · refine hasFiniteIntegral_mkD_restrict_of_bound f _ ?_ f_zero bound bound_int bound_ge
    exact ae_restrict_of_forall_mem hs fun x hx ↦
      hf.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨hx, hz⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Module.PerfectPairing

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
x✝ : M
y✝ : N
inst✝¹ : p.IsContPerfPair
inst✝ : IsTopologicalRing R
x y : M
⊢ { toLinearMap := p (x + y), cont := ⋯ } = { toLinearMap := p x, cont := ⋯ } + { toLinearMap := p y, cont := ⋯ }

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.PerfectPairing

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
x✝ : M
y : N
inst✝¹ : p.IsContPerfPair
inst✝ : IsTopologicalRing R
r : R
x : M
⊢ { toLinearMap := p (r • x), cont := ⋯ } = (RingHom.id R) r • { toLinearMap := p x, cont := ⋯ }

Tactic:
ext; simp

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
⊢ spectrum ℝ (φ a) = spectrum ℝ a

Tactic:
by
  have h_spec := AlgHom.spectrum_apply_subset ((φ : A →⋆ₐ[ℂ] B).restrictScalars ℝ) a
  refine Set.eq_of_subset_of_subset h_spec fun x hx ↦ ?_
  /- we prove the reverse inclusion by contradiction, so assume that `x ∈ spectrum ℝ a`, but
  `x ∉ spectrum ℝ (φ a)`. Then by Urysohn's lemma we can get a function for which `f x = 1`, but
  `f = 0` on `spectrum ℝ a`. -/
  by_contra hx'
  obtain ⟨f, h_eqOn, h_eqOn_x, -⟩ := exists_continuous_zero_one_of_isClosed
    (spectrum.isClosed (𝕜 := ℝ) (φ a)) (isClosed_singleton (x := x)) <| by simpa
  /- it suffices to show that `φ (f a) = 0`, for if so, then `f a = 0` by injectivity of `φ`, and
  hence `f = 0` on `spectrum ℝ a`, contradicting the fact that `f x = 1`. -/
  suffices φ (cfc f a) = 0 by
    rw [map_eq_zero_iff φ hφ, ← cfc_zero ℝ a, cfc_eq_cfc_iff_eqOn] at this
    exact zero_ne_one <| calc
      0 = f x := (this hx).symm
      _ = 1 := h_eqOn_x <| Set.mem_singleton x
  /- Finally, `φ (f a) = f (φ a) = 0`, where the last equality follows since `f = 0` on
  `spectrum ℝ (φ a)`. -/
  calc φ (cfc f a) = cfc f (φ a) := StarAlgHomClass.map_cfc φ f a
    _ = cfc (0 : ℝ → ℝ) (φ a) := cfc_congr h_eqOn
    _ = 0 := by simp

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

Goal state before:
pp: case refine_2.refine_1
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)
⊢ ‖e * e‖ ≤ 1

Tactic:
norm_mul_le,

Goal state after:
case refine_2.refine_1
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)
⊢ ‖e‖ * ‖e‖ ≤ 1
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : a✝ ∈ ball 0 1
hy : b✝ ∈ ball 0 1
⊢ a✝ * b✝ ∈ ball 0 1

Tactic:
by
    rw [mem_ball_zero_iff] at *
    exact (norm_mul_le _ _).trans_lt (mul_lt_one_of_nonneg_of_lt_one_left (norm_nonneg _) hx hy.le)

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

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : a✝ ∈ closedBall 0 1
hy : b✝ ∈ closedBall 0 1
⊢ a✝ * b✝ ∈ closedBall 0 1

Tactic:
mem_closedBall_zero_iff

Goal state after:
𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : ‖a✝‖ ≤ 1
hy : ‖b✝‖ ≤ 1
⊢ ‖a✝ * b✝‖ ≤ 1
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX'.prod eY').source.Nonempty
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
rw [eq_comm, prod_eq_prod_of_nonempty h, eq_comm, @eq_comm _ eY']

Goal state after: