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

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
r : ℝ
f : C(X, ℝ)₀
⊢ φ (r • f).toNNReal - φ (-(r • f)).toNNReal = (MonoidHom.id ℝ) r • (φ f.toNNReal - φ (-f).toNNReal)

Tactic:
by

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
x y : ↑K
hxy : x ≠ y
w✝ : X → ℝ
hg_sep : w✝ ↑x ≠ w✝ ↑y
g : C(X, ℝ)
hg1 : g ∈ ↑A
hg2 : (fun f ↦ ⇑f) g = w✝
⊢ (restrict_on_K g) x ≠ (restrict_on_K g) y

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
⊢ φ (toNNReal 0) - φ (-0).toNNReal = 0

Tactic:
by

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
⊢ AK.SeparatesPoints

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f g : C(X, ℝ)₀
⊢ φ (f + g).toNNReal - φ (-(f + g)).toNNReal = φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)

Tactic:
by

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
hsep : AK.SeparatesPoints
gK : C(↑K, ℝ)
hgKAK✝ : gK ∈ AK
hgapprox : ∀ (x : ↑K), ‖↑⟨gK, hgKAK✝⟩ x - K.domRestrict (⇑f) x‖ < ε
g : C(X, ℝ)
hgA : g ∈ A
hgKAK : ↑restrict_on_K g = gK
x : X
hxK : x ∈ K
⊢ g x = gK ⟨x, hxK⟩

Tactic:
by

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖g x - f x‖ < ε

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f g : C(X, ℝ)₀
⊢ φ (f * g).toNNReal - φ (-(f * g)).toNNReal = (φ f.toNNReal - φ (-f).toNNReal) * (φ g.toNNReal - φ (-g).toNNReal)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f : C(X, ℝ)₀
⊢ φ (star f).toNNReal - φ (-star f).toNNReal = star (φ f.toNNReal - φ (-f).toNNReal)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝¹] ⇑φ
⊢ Continuous[_, inst✝¹] ⇑φ.realContinuousMapZeroOfNNReal

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f : C(X, ℝ≥0)₀
⊢ φ ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal -
      φ (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal =
    φ f

Tactic:
convert_to φ f - φ 0 = φ f using 2

Goal state after:
case e'_5
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f : C(X, ℝ≥0)₀
⊢ φ ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal = φ f

case e'_6
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f : C(X, ℝ≥0)₀
⊢ φ (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal = φ 0

X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f : C(X, ℝ≥0)₀
⊢ φ f - φ 0 = φ f
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f ↦ ⇑f) f x₁ ≠ (fun f ↦ ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
⊢ F ∈ A

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f ↦ ⇑f) f x₁ ≠ (fun f ↦ ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
hFA : F ∈ A
⊢ Continuous fun x ↦ ‖F x‖ ^ 2

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f : C(X, ℝ≥0)₀
⊢ φ.realContinuousMapZeroOfNNReal ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f) = φ f

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
⊢ Function.Injective realContinuousMapZeroOfNNReal

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖b⋆‖ * ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖ ≤
    ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
⊢ (comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)).SeparatesPoints

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
⊢ (↑I).range ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
⊢ ‖((splitMul 𝕜 E) x).2‖ ^ 2 ≤ ‖((splitMul 𝕜 E) (x⋆ * x)).2‖

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NonUnitalNormedRing A
inst✝ : NormedSpace 𝕜 A
x : WithLp 1 (Unitization 𝕜 A)
⊢ 0 < ENNReal.toReal 1

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NonUnitalNormedRing A
inst✝ : NormedSpace 𝕜 A
x : WithLp 1 (Unitization 𝕜 A)
⊢ (‖x.ofLp.toProd.1‖ ^ ENNReal.toReal 1 + ‖x.ofLp.toProd.2‖ ^ ENNReal.toReal 1) ^ (1 / ENNReal.toReal 1) =
    ‖x.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NonUnitalNormedRing A
inst✝ : NormedSpace 𝕜 A
x : A
⊢ ‖toLp 1 ↑x‖ = ‖x‖

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NonUnitalNormedRing A
inst✝ : NormedSpace 𝕜 A
x : A
⊢ ‖toLp 1 ↑x‖₊ = ‖x‖₊

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x✝ x : Unitization 𝕜 E
h : ¬(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2 = 0
⊢ ‖((splitMul 𝕜 E) (x⋆ * x)).2‖ ≤ ‖((splitMul 𝕜 E) x⋆).2‖ * ‖((splitMul 𝕜 E) x).2‖

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁹ : TopologicalSpace X
inst✝⁸ : Zero X
A : Type u_2
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsSemitopologicalRing A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this : Fact (0 ∈ s')
e0 : e 0 = 0
e0' : e.symm 0 = 0
ξ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hξ : Continuous[_, inst✝⁴] ⇑ξ
⊢ let ξ' :=
    ξ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 });
  Continuous[_, inst✝⁴] ⇑ξ' ∧ ξ' (ContinuousMapZero.id s') = ξ (ContinuousMapZero.id s)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
⊢ A.topologicalClosure = ⊤

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
⊢ elemental 𝕜 (restrict s (ContinuousMap.id 𝕜)) = ⊤

Tactic:
by

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

Goal state before:
pp: case h₁
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖y.ofLp.toProd.1 • x.ofLp.toProd.2‖ ≤ ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖

pp: case h₂
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤ ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖

Tactic:
· simp [norm_smul, mul_comm]

Goal state after:
case h₂
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤ ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x : Unitization 𝕜 E
⊢ ∀ (x : Unitization 𝕜 E), ‖((splitMul 𝕜 E) x).2‖ ≤ ‖((splitMul 𝕜 E) x⋆).2‖

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
r : 𝕜
x : WithLp 1 (Unitization 𝕜 A)
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_4
F : Type u_5
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : CommSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
l : Filter α
f : α → WeakBilin B
x : WeakBilin B
hB : Function.Injective ⇑B
⊢ Tendsto f l (𝓝 x) ↔ ∀ (y : F), Tendsto (fun i ↦ (B (f i)) y) l (𝓝 ((B x) y))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ ContinuousAdd (WeakBilin B)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousSMul 𝕜 𝕜
⊢ ContinuousSMul 𝕜 (WeakBilin B)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
f : F
⊢ Continuous[instTopologicalSpace B, inst✝⁷] (B.flip f).toFun

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
x✝¹ x✝ : F
⊢ { toLinearMap := B.flip (x✝¹ + x✝), cont := ⋯ } =
    { toLinearMap := B.flip x✝¹, cont := ⋯ } + { toLinearMap := B.flip x✝, cont := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
x✝¹ : 𝕜
x✝ : F
⊢ { toLinearMap := B.flip (x✝¹ • x✝), cont := ⋯ } = (RingHom.id 𝕜) x✝¹ • { toLinearMap := B.flip x✝, cont := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ ContinuousAdd (WeakBilin B)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ Continuous[instTopologicalSpace B, instTopologicalSpace B] fun a ↦ -a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f : C(↑s, 𝕜)
⊢ p f

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁹ : TopologicalSpace X
inst✝⁸ : Zero X
A : Type u_2
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsSemitopologicalRing A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this✝¹ : Fact (0 ∈ s')
e0 : e 0 = 0
e0' : e.symm 0 = 0
this✝ :
  ∀ (ξ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A),
    Continuous[_, inst✝⁴] ⇑ξ →
      let ξ' :=
        ξ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 });
      Continuous[_, inst✝⁴] ⇑ξ' ∧ ξ' (ContinuousMapZero.id s') = ξ (ContinuousMapZero.id s)
hφ' :
  Continuous[_, inst✝⁴]
    ⇑(φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
hφ_id :
  (φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
      (ContinuousMapZero.id s') =
    φ (ContinuousMapZero.id s)
hψ' :
  Continuous[_, inst✝⁴]
    ⇑(ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
hψ_id :
  (ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
      (ContinuousMapZero.id s') =
    ψ (ContinuousMapZero.id s)
hs' : CompactSpace ↑s'
this : ContinuousMapZero.UniqueHom ℝ A
h' :
  φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }) =
    ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })
h'' :
  (φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })).comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e.symm, map_zero' := e0' }) =
    (ψ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })).comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e.symm, map_zero' := e0' })
⊢ (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }).comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e.symm, map_zero' := e0' }) =
    NonUnitalStarAlgHom.id ℝ C(↑s, ℝ)₀

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
frequently : ∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g) → p f
f : C(↑s, 𝕜)
⊢ p f

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : Semiring A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : T2Space A
s : Set ℝ
inst✝ : CompactSpace ↑s
φ ψ : C(↑s, ℝ) →ₐ[ℝ] A
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
this : ⊤ ≤ φ.equalizer ψ
x : C(↑s, ℝ)
⊢ x ∈ ⊤

Tactic:
by

Goal state after: