mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : IsStarNormal a
⊢ abs (star a) = abs a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
⊢ abs 0 = 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA✝ : IsSelfAdjoint A
hA : A.IsHermitian
f : C(↑(spectrum ℝ A), ℝ)
⊢ RCLike.ofReal ∘ 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
⊢ Commute (star a * a) b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
⊢ Commute (star a * a) (star b * b)

Tactic:
by

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

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
h_li : LinearIndependent 𝕜 v
⊢ (gram 𝕜 v).PosDef

Tactic:
by

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

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → E
⊢ (gram 𝕜 v).det ≠ 0 ↔ LinearIndependent 𝕜 v

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsSelfAdjoint A
⊢ Isometry ⇑(cfcHom hA)

Tactic:
by

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

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_5
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : n → E
⊢ gram 𝕜 v = (of fun i j ↦ (b.repr (v j)).ofLp i)ᴴ * of fun i j ↦ (b.repr (v j)).ofLp i

Tactic:
by

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

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq n
v : n → E
⊢ gram 𝕜 v = 1 ↔ Orthonormal 𝕜 v

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopologyEither α E
f : α →ᵇ E
⊢ AEStronglyMeasurable (⇑f) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ Lp E p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ‖⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : IsFiniteMeasure μ
inst✝ : Fact (1 ≤ p)
⊢ ((ContinuousMap.toAEEqFunAddHom μ).comp (toContinuousMapAddMonoidHom α E)).range ≤ Lp E p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : IsFiniteMeasure μ
inst✝ : Fact (1 ≤ p)
⊢ (toLpHom p μ).range = Lp.boundedContinuousFunction E p μ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
⊢ abs (a * b) = abs a * abs b

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
f g : α →ᵇ E
inst✝ : μ.IsOpenPosMeasure
⊢ f = g → (toLp p μ 𝕜) f = (toLp p μ 𝕜) g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : IsStarNormal a
⊢ abs (a * a) = star a * a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
⊢ abs a ^ 2 = star a * a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
⊢ abs a ^ (2 * x) = (star a * a) ^ x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
⊢ abs a ^ x = (star a * a) ^ (x / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ abs a = a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : a ≤ 0
⊢ abs a = -a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
f g : α →ᵇ E
inst✝ : μ.IsOpenPosMeasure
⊢ (toLp p μ 𝕜) f = (toLp p μ 𝕜) g ↔ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ abs a = cfcₙ (fun x ↦ ‖x‖) a

Tactic:
by

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

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ ↑‖f (∑ x ∈ c.support, c x • v x)‖ ^ 2 ≤ ‖f‖ ^ 2 • ↑‖∑ i ∈ c.support, c i • v i‖ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ a⁺ + a⁻ = abs a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ abs a - a = 2 • a⁻

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ abs a + a = 2 • a⁺

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹⁶ : NonUnitalRing A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module ℝ A
inst✝¹² : SMulCommClass ℝ A A
inst✝¹¹ : IsScalarTower ℝ A A
inst✝¹⁰ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁹ : PartialOrder A
inst✝⁸ : StarOrderedRing A
inst✝⁷ : NonnegSpectrumClass ℝ A
inst✝⁶ : IsTopologicalRing A
inst✝⁵ : T2Space A
inst✝⁴ : StarModule ℝ A
R : Type u_3
inst✝³ : Semiring R
inst✝² : SMulWithZero R ℝ≥0
inst✝¹ : SMul R A
inst✝ : IsScalarTower R ℝ≥0 A
r : R
a : A
this : ∀ (r : ℝ≥0), abs (r • a) = r • abs a
⊢ abs (r • a) = r • abs a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : CompactSpace α
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
⊢ (↑(toLp p μ 𝕜)).range.toAddSubgroup = Lp.boundedContinuousFunction E p μ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹⁶ : NonUnitalRing A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module ℝ A
inst✝¹² : SMulCommClass ℝ A A
inst✝¹¹ : IsScalarTower ℝ A A
inst✝¹⁰ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁹ : PartialOrder A
inst✝⁸ : StarOrderedRing A
inst✝⁷ : NonnegSpectrumClass ℝ A
inst✝⁶ : IsTopologicalRing A
inst✝⁵ : T2Space A
inst✝⁴ : StarModule ℝ A
R : Type u_3
inst✝³ : Semiring R
inst✝² : SMulWithZero R ℝ≥0
inst✝¹ : SMul R A
inst✝ : IsScalarTower R ℝ≥0 A
r✝ : R
a : A
r : ℝ≥0
⊢ 0 ≤ r

Tactic:
by

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

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
⊢ (‖f‖ ^ 2 • gram 𝕜 v - gram 𝕜 (⇑f ∘ v)).PosSemidef

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : BorelSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : SecondCountableTopologyEither α E
inst✝⁶ : CompactSpace α
inst✝⁵ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
β : Type u_4
inst✝ : μ.IsOpenPosMeasure
g : β → C(α, E)
f : C(α, E)
hg : Summable g
hg2 : HasSum (⇑(toLp p μ 𝕜) ∘ g) ((toLp p μ 𝕜) f)
⊢ HasSum g f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹⁶ : NonUnitalRing A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module ℝ A
inst✝¹² : SMulCommClass ℝ A A
inst✝¹¹ : IsScalarTower ℝ A A
inst✝¹⁰ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁹ : PartialOrder A
inst✝⁸ : StarOrderedRing A
inst✝⁷ : NonnegSpectrumClass ℝ A
inst✝⁶ : IsTopologicalRing A
inst✝⁵ : T2Space A
inst✝⁴ : StarModule ℝ A
R : Type u_3
inst✝³ : Semiring R
inst✝² : SMulWithZero R ℝ≥0
inst✝¹ : SMul R A
inst✝ : IsScalarTower R ℝ≥0 A
r : R
a : A
⊢ abs (r • a) = r • abs a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Module 𝕜 A
inst✝⁵ : StarRing A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
x✝¹ : 𝕜
x✝ : x✝¹ ∈ quasispectrum 𝕜 a
⊢ 0 ≤ ↑‖f x✝¹‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
A : 𝓓^{n₁}_{K₁}(E, F) → E → F'
hadd : ∀ (f g : 𝓓^{n₁}_{K₁}(E, F)) (x : E), A (f + g) x = A f x + A g x
hsmul : ∀ (c : 𝕜) (f : 𝓓^{n₁}_{K₁}(E, F)) (x : E), A (c • f) x = c • A f x
hsmooth : ∀ (f : 𝓓^{n₁}_{K₁}(E, F)), ContDiff ℝ (↑n₂) (A f)
hsupp : ∀ (f : 𝓓^{n₁}_{K₁}(E, F)), EqOn (A f) 0 (↑K₂)ᶜ
hbound :
  ∀ (i : ℕ),
    ↑i ≤ n₂ →
      ∃ s C,
        0 ≤ C ∧
          ∀ (f : 𝓓^{n₁}_{K₁}(E, F)),
            ∀ x ∈ K₂, ‖iteratedFDeriv ℝ i (A f) x‖ ≤ C * (s.sup fun j ↦ ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ j) f
Φ : 𝓓^{n₁}_{K₁}(E, F) →ₗ[𝕜] 𝓓^{n₂}_{K₂}(E, F') :=
  { toFun := fun f ↦ { toFun := A f, contDiff' := ⋯, zero_on_compl' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }
i : ℕ
hi : ¬↑i ≤ n₂
f : 𝓓^{n₁}_{K₁}(E, F)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F' n₂ K₂ i) (Φ f) ≤ 0 * (∅.sup (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁)) f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h : MemLp f 2 μ
⊢ Integrable (fun x ↦ f x ^ 2) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ MemLp f 2 μ ↔ Integrable (fun x ↦ ‖f x‖ ^ 2) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : CompactSpace α
inst✝³ : IsFiniteMeasure μ
inst✝² : Fact (1 ≤ p)
𝕜 : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
⊢ ‖toLp p μ 𝕜‖ ≤ ↑(measureUnivNNReal μ) ^ p.toReal⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
⊢ MemLp f 2 μ ↔ Integrable (fun x ↦ f x ^ 2) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : MemLp f p μ
c : E
x : α
⊢ ‖⟪f x, c⟫‖ ≤ ‖c‖ * ‖f x‖

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : CompactSpace α
inst✝³ : IsFiniteMeasure μ
inst✝² : Fact (1 ≤ p)
𝕜' : Type u_5
inst✝¹ : NormedField 𝕜'
inst✝ : NormedSpace 𝕜' E
f : C(α, E)
⊢ MemLp (⇑f) p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
c : E
hf : Integrable f μ
⊢ Integrable (fun x ↦ ⟪c, f x⟫) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : Integrable f μ
c : E
⊢ Integrable (fun x ↦ ⟪f x, c⟫) μ

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst✝⁴, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst✝⁴] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n) f U
⊢ ∀ (x : M), dist (f x) (f x) < ε x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst✝⁴, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst✝⁴] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun x ↦ {y | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
this : ∃ g, ∀ (x : M), g x ∈ t x
⊢ ∃ g, (∀ (x : M), dist (g x) (f x) < ε x) ∧ EqOn (⇑g) f S ∧ support ⇑g ⊆ support f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝¹⁸ : RCLike 𝕜
inst✝¹⁷ : NonUnitalRing A
inst✝¹⁶ : TopologicalSpace A
inst✝¹⁵ : Module 𝕜 A
inst✝¹⁴ : StarRing A
inst✝¹³ : PartialOrder A
inst✝¹² : StarOrderedRing A
inst✝¹¹ : IsScalarTower 𝕜 A A
inst✝¹⁰ : SMulCommClass 𝕜 A A
inst✝⁹ : Module ℝ A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : IsScalarTower ℝ A A
inst✝⁶ : NonnegSpectrumClass ℝ A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : StarModule 𝕜 A
inst✝¹ : StarModule ℝ A
inst✝ : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
⊢ abs (r • a) = ‖r‖ • abs a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
hf_int : ∀ (c : E), ∫ (x : α), ⟪c, f x⟫ ∂μ = 0
⊢ ∫ (x : α), f x ∂μ = 0

Tactic:
by

Goal state after: