mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : LocallyConvexSpace 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : FirstCountableTopology E
u : ℕ → Set E
hu_basis : (𝓝 0).HasAntitoneBasis u
hu_zero : ∀ (n : ℕ), 0 ∈ interior (u n)
v : ℕ → Set E := fun n ↦ (absConvexHull 𝕜) (interior (u n))
hv_open : ∀ (n : ℕ), IsOpen[inst✝⁵] (v n)
hv_nhds : ∀ (n : ℕ), v n ∈ 𝓝 0
⊢ ∀ (i' : ℕ), True → ∃ i, True ∧ u i ⊆ v i'

Tactic:
intro n

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : LocallyConvexSpace 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : FirstCountableTopology E
u : ℕ → Set E
hu_basis : (𝓝 0).HasAntitoneBasis u
hu_zero : ∀ (n : ℕ), 0 ∈ interior (u n)
v : ℕ → Set E := fun n ↦ (absConvexHull 𝕜) (interior (u n))
hv_open : ∀ (n : ℕ), IsOpen[inst✝⁵] (v n)
hv_nhds : ∀ (n : ℕ), v n ∈ 𝓝 0
n : ℕ
⊢ True → ∃ i, True ∧ u i ⊆ v n
Module: Mathlib.Analysis.LocallyConvex.WeakDual

Goal state before:
pp: case mp
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
this✝ : IsTopologicalAddGroup E
this : WithSeminorms fun i ↦ (f i).toSeminorm
H : Continuous[⨅ i, induced (⇑(f i)) inferInstance, inferInstance] ⇑φ
⊢ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm

Tactic:
rw [WithSeminorms.continuous_iff_continuous_comp (norm_withSeminorms 𝕜 𝕜), forall_const] at H
    rcases Seminorm.bound_of_continuous this _ H with ⟨s, C, -, hC⟩
    exact ⟨s, C, hC⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Completeness

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (fun n x ↦ (f n) x) atTop (𝓝 ⇑g)
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hb_lim : Tendsto b atTop (𝓝 0)
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N
⊢ ∀ (n : ℕ) (x : E'), ‖(f n) x - g x‖ ≤ b n * ‖x‖

Tactic:
intro n

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (fun n x ↦ (f n) x) atTop (𝓝 ⇑g)
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hb_lim : Tendsto b atTop (𝓝 0)
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N
n : ℕ
⊢ ∀ (x : E'), ‖(f n) x - g x‖ ≤ b n * ‖x‖
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : LinearOrder k
inst✝⁵ : IsStrictOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b : E
r : k
h : a < b
⊢ a ≤ (lineMap a b) r ↔ 0 ≤ r

Tactic:
rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : LinearOrder k
inst✝⁵ : IsStrictOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b : E
r : k
h : a < b
⊢ (lineMap a b) r ≤ a ↔ r ≤ 0

Tactic:
rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁸ : Field k
inst✝⁷ : LinearOrder k
inst✝⁶ : IsStrictOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
⊢ f ((lineMap a b) r) ≤ (lineMap (f a) (f b)) r ↔ slope f a ((lineMap a b) r) ≤ slope f ((lineMap a b) r) b

Tactic:
rw [map_le_lineMap_iff_slope_le_slope_left (mul_pos h₀ (sub_pos.2 hab)), ←
    lineMap_slope_lineMap_slope_lineMap f a b r, right_le_lineMap_iff_le h₁]

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

Goal state before:
pp: 𝕜 : Type u_5
F : Type u_7
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
f : WeakDual ℝ F
x : F
⊢ im ((extendRCLikeL f) x) = -f (I • x)

Tactic:
by
  simp [extendRCLikeL_apply, extendRCLikeₗ_apply]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : (i : ι) → Ring (A i)
inst✝⁷ : (i : ι) → Algebra S (A i)
inst✝⁶ : (i : ι) → Algebra R (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R S (A i)
hinst : IsScalarTower R S ((i : ι) → A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : ContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), ContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMap.UniqueHom R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ i, spectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
i : ι
φ : ((i : ι) → A i) →⋆ₐ[S] A i := Pi.evalStarAlgHom S A i
⊢ ContinuousOn f (spectrum R a)

Tactic:
by rwa [Pi.spectrum_eq]

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
inst✝ : StarModule ℝ A
r : ℝ
hr : 0 ≤ r
a : A
| - -r • a⁻

Tactic:
neg_neg

Goal state after:
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
inst✝ : StarModule ℝ A
r : ℝ
hr : 0 ≤ r
a : A
| r • a⁻
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case refine_4
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
φ : ↑(characterSpace ℂ ↥(elemental ℂ a))
hz : φ ⟨a, ⋯⟩ ∈ spectrum ℂ a
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = ⟨φ ⟨a, ⋯⟩, hz⟩

Tactic:
exact ⟨φ, rfl⟩

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))
⊢ ∃ φ,
    Continuous ⇑φ ∧
      Function.Injective ⇑φ ∧
        φ (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) = a ∧
          (∀ (f : C(↑(spectrum ℂ a), ℂ)), spectrum ℂ (φ f) = Set.range ⇑f) ∧
            ∀ (f : C(↑(spectrum ℂ a), ℂ)), IsStarNormal (φ f)

Tactic:
refine ⟨_, this.continuous, this.injective, ?hom_id, ?hom_map_spectrum, ?predicate_hom⟩

Goal state after:
case hom_id
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
this : Isometry ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
⊢ ((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
      (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) =
    a

case hom_map_spectrum
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 ℂ (((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)) f) = Set.range ⇑f

case predicate_hom
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
this : Isometry ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
⊢ ∀ (f : C(↑(spectrum ℂ a), ℂ)), IsStarNormal (((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)) f)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x ↦ ContinuousMap.realToNNReal x
h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
rw [h_c_spec₁.mul_comm.eq_zero_of_neg (.star_mul_self c) h_c_spec₀, neg_zero, CFC.negPart_def,
    cfcₙ_eq_cfc (hf0 := by simp), ← cfc_pow _ _ (ha := ha), ← cfc_zero a (R := ℝ)] at h_eq_negPart_a

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : cfc 0 a = cfc (fun x ↦ x⁻ ^ 3) a
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x ↦ ContinuousMap.realToNNReal x
h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
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:
by
  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
ha : 0 ≤ a
⊢ sqrt (a ^ 2) = a

Tactic:
pow_two,

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
ha : 0 ≤ a
⊢ sqrt (a * a) = a
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:
pow_two,

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
ha : 0 ≤ a
⊢ sqrt a * sqrt a = a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : ContinuousStar A
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, spectrum 𝕜 (a x) ⊆ s
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
x✝¹ : X
x✝ : x✝¹ ∈ t
x : X
hx : x ∈ t
⊢ spectrum 𝕜 (a x) ⊆ s

Tactic:
exact ha x hx

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

Tactic:
simp [← innerₛₗ_apply]

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

Tactic:
simp [← innerₛₗ_apply]

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

Tactic:
simp [← innerₛₗ_apply]

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

Tactic:
simp [← innerₛₗ_apply]

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

Tactic:
simp [← innerₛₗ_apply]

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

Tactic:
simp [← innerₛₗ_apply]

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
h : x ≠ 0
a : A
⊢ ⟪a •> x - ‖x‖ ^ 2 •> y, a •> x - ‖x‖ ^ 2 •> y⟫_A =
    a * ⟪x, x⟫_A * star a - ‖x‖ ^ 2 •> (a * ⟪y, x⟫_A) - ‖x‖ ^ 2 •> (⟪x, y⟫_A * star a) + ‖x‖ ^ 2 •> ‖x‖ ^ 2 •> ⟪y, y⟫_A

Tactic:
simp only [inner_sub_right, inner_op_smul_right, inner_sub_left,
                        inner_op_smul_left, inner_smul_left_real, mul_sub, mul_smul_comm,
                        inner_smul_right_real, smul_sub, mul_assoc]
                      abel

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

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹⁰ : NormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedAlgebra ℝ A
inst✝⁷ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁶ : ContinuousStar A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
x✝¹ : X
x✝ : x✝¹ ∈ t
x : X
hx : x ∈ t
⊢ spectrum ℝ≥0 (a x) ⊆ s

Tactic:
exact ha x hx

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
ha : 1 ≤ a
ha' : 0 ≤ a
⊢ Monotone fun x ↦ a ^ x

Tactic:
intro n

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
n : ℕ
⊢ ∀ ⦃b : ℕ⦄, n ≤ b → (fun x ↦ a ^ x) n ≤ (fun x ↦ a ^ x) b
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
ha₁ : a ≤ 1
⊢ Antitone fun x ↦ a ^ x

Tactic:
intro n

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
⊢ ∀ ⦃b : ℕ⦄, n ≤ b → (fun x ↦ a ^ x) b ≤ (fun x ↦ a ^ x) n
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) a = cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) a

Tactic:
by
          rw [cfcₙ_nnreal_eq_real _ _ ha]
          refine cfcₙ_congr ?_
          intro x hx
          have hx' : 0 ≤ x := by grind
          simp [hx']

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

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

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

Goal state after:
n : Type u_4
α : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ↑(Fintype.card n) ^ (1 / OfNat.ofNat 2).toReal * ‖1‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: case h
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 : l
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖∑ j_1, A i j_1 * B j_1 j‖₊ ^ (2 * (1 / 2)) ≤ ((∑ j, ‖A i j‖₊ ^ 2) * ∑ x, ‖B x j‖₊ ^ 2) ^ (1 / 2)

Tactic:
mul_div_cancel₀ (1 : ℝ) two_ne_zero,

Goal state after:
case h
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 : l
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖∑ j_1, A i j_1 * B j_1 j‖₊ ^ 1 ≤ ((∑ j, ‖A i j‖₊ ^ 2) * ∑ x, ‖B x j‖₊ ^ 2) ^ (1 / 2)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
x✝¹ : X
x✝ : x✝¹ ∈ t
x : X
hx : x ∈ t
⊢ quasispectrum 𝕜 (a x) ⊆ s

Tactic:
exact ha x hx

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : TopologicalSpace Y
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompactSpace Y
f : X → Y → E
g : C(Y, E)
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
⊢ HasFiniteIntegral (fun x ↦ mkD (f x) g) μ

Tactic:
refine hasFiniteIntegral_of_bound _ bound bound_int ?_
  filter_upwards [bound_ge, f_ae_cont] with x bound_ge_x cont_x
  simpa only [mkD_apply_of_continuous cont_x] using bound_ge_x

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:
map_smul

Goal state after:
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 (r • (cfcₙHom ha) f) b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
x✝¹ : X
x✝ : x✝¹ ∈ t
x : X
hx : x ∈ t
⊢ quasispectrum ℝ≥0 (a x) ⊆ s

Tactic:
exact ha x hx

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✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : IsScalarTower 𝕜 A A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝ : CompleteSpace A
f : X → 𝕜 → 𝕜
a : A
hf : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
⊢ Integrable (fun x ↦ cfcₙ (f x) a) μ

Tactic:
by
  conv in cfcₙ _ _ => rw [cfcₙ_eq_cfcₙL_mkD _ a]
  exact cfcₙL_integrable _ _ hf ha

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
y : StrongDual 𝕜 E
⊢ ((toDual 𝕜 E) ((toDual 𝕜 E).symm y)) x = y x

Tactic:
simp only [LinearIsometryEquiv.apply_symm_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x : E
h : x ∈ extremePoints 𝕜 A
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₂ = x

Tactic:
apply h.2 hx₂ hx₁

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x : E
h : x ∈ extremePoints 𝕜 A
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x ∈ openSegment 𝕜 x₂ x₁