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

Goal state before:
pp: case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : y ∈ B.polar Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖(B (c⁻¹ • x)) y‖ ≤ 1

Tactic:
;

Goal state after:
case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : y ∈ B.polar Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖(B (c⁻¹ • x)) y‖ ≤ 1
Module: Mathlib.Analysis.LocallyConvex.Polar

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
x✝ : F
⊢ x✝ ∈ B.polar ↑m ↔ x✝ ∈ ↑(⨅ x ∈ m, (B x).ker)

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
x✝ : F
⊢ x✝ ∈ B.polar ↑m ↔ x✝ ∈ ↑(⨅ x ∈ m, (B x).ker)
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a✝ : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a✝) * NormedSpace.exp (-x • star a✝) ∈ unitary A
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a✝) * NormedSpace.exp (x • star a✝) =
      NormedSpace.exp (x • star a✝) * NormedSpace.exp (-x • a✝)
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
a b : A
y x : ℝ
| NormedSpace.exp (x • a)

Tactic:
;

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a✝ : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a✝) * NormedSpace.exp (-x • star a✝) ∈ unitary A
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a✝) * NormedSpace.exp (x • star a✝) =
      NormedSpace.exp (x • star a✝) * NormedSpace.exp (-x • a✝)
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
a b : A
y x : ℝ
| NormedSpace.exp (x • a)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
K : NonemptyCompacts α
hu : ∅.Finite
huB : ∅ ⊆ B
hK₁ : ↑K.toCompacts ⊆ ⋃₀ ∅
hK₂ : ∀ U ∈ ∅, (↑K.toCompacts ∩ U).Nonempty
⊢ ¬(⋃₀ ∅).Nonempty

Tactic:
;

Goal state after:
case refine_2.inl
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
K : NonemptyCompacts α
hu : ∅.Finite
huB : ∅ ⊆ B
hK₁ : ↑K.toCompacts ⊆ ⋃₀ ∅
hK₂ : ∀ U ∈ ∅, (↑K.toCompacts ∩ U).Nonempty
⊢ ¬(⋃₀ ∅).Nonempty
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: 𝕜 : 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
hv_basis : (𝓝 0).HasAntitoneBasis v
m : ℕ
W : Set E
hW_open : IsOpen[inst✝⁵] W
hW_zero : 0 ∈ W
hW_add : W + W ⊆ v m
N : ℕ
hN : v N ⊆ W
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, v n + v n ⊆ v m

Tactic:
filter_upwards [Filter.eventually_ge_atTop N] with M hM

Goal state after:
𝕜 : 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
hv_basis : (𝓝 0).HasAntitoneBasis v
m : ℕ
W : Set E
hW_open : IsOpen[inst✝⁵] W
hW_zero : 0 ∈ W
hW_add : W + W ⊆ v m
N : ℕ
hN : v N ⊆ W
M : ℕ
hM : N ≤ M
⊢ v M + v M ⊆ v m
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ -s
⊢ ∃ r, ‖r‖ ≤ 1 ∧ x✝¹ ∈ r • s

Tactic:
;

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ -s
⊢ ∃ r, ‖r‖ ≤ 1 ∧ x✝¹ ∈ r • s
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ -s
⊢ ‖-1‖ ≤ 1 ∧ x✝¹ ∈ -1 • s

Tactic:
;

Goal state after:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ -s
⊢ ‖-1‖ ≤ 1 ∧ x✝¹ ∈ -1 • s
Module: Mathlib.Topology.ContinuousMap.Units

Goal state before:
pp: X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
a✝ : X
⊢ { toFun := fun x ↦ ↑((unitsOfForallIsUnit h) x), continuous_toFun := ⋯ } a✝ = f a✝

Tactic:
;

Goal state after:
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
a✝ : X
⊢ { toFun := fun x ↦ ↑((unitsOfForallIsUnit h) x), continuous_toFun := ⋯ } a✝ = f a✝
Module: Mathlib.Topology.ContinuousMap.Units

Goal state before:
pp: X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
a✝ : X
⊢ ↑(unitsLift (unitsOfForallIsUnit h)) a✝ = f a✝

Tactic:
;

Goal state after:
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
a✝ : X
⊢ ↑(unitsLift (unitsOfForallIsUnit h)) a✝ = f a✝
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case hf
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ 0 ≤ 1

Tactic:
;

Goal state after:
case hf
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ 0 ≤ 1
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : PartialOrder k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b b' : E
r : k
hb : b < b'
hr : 0 < r
⊢ (1 - r) • a + r • b < (1 - r) • a + r • b'

Tactic:
;

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : PartialOrder k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a b b' : E
r : k
hb : b < b'
hr : 0 < r
⊢ (1 - r) • a + r • b < (1 - r) • a + r • b'
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: case inl
k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a a' b b' : E
ha : a < a'
hb : b < b'
h₀ : 0 ≤ 0
h₁ : 0 ≤ 1
⊢ (lineMap a b) 0 < (lineMap a' b') 0

pp: case inr
k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a a' b b' : E
r : k
ha : a < a'
hb : b < b'
h₀✝ : 0 ≤ r
h₁ : r ≤ 1
h₀ : 0 < r
⊢ (lineMap a b) r < (lineMap a' b') r

Tactic:
;

Goal state after:
case inl
k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a a' b b' : E
ha : a < a'
hb : b < b'
h₀ : 0 ≤ 0
h₁ : 0 ≤ 1
⊢ (lineMap a b) 0 < (lineMap a' b') 0

case inr
k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a a' b b' : E
r : k
ha : a < a'
hb : b < b'
h₀✝ : 0 ≤ r
h₁ : r ≤ 1
h₀ : 0 < r
⊢ (lineMap a b) r < (lineMap a' b') r
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
h : x ∈ c.C
⊢ c.lim x = 0

Tactic:
simp only [CU.lim, approx_of_mem_C, h, ciSup_const]

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✝⁵ : 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
⊢ 0 < (1 - r) * (b - a) →
    (f ((lineMap b a) (1 - r)) ≤ (lineMap (f b) (f a)) (1 - r) ↔ slope f a b ≤ slope f ((lineMap b a) (1 - r)) b)

Tactic:
;

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder 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
⊢ 0 < (1 - r) * (b - a) →
    (f ((lineMap b a) (1 - r)) ≤ (lineMap (f b) (f a)) (1 - r) ↔ slope f a b ≤ slope f ((lineMap b a) (1 - r)) b)
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder 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 r' : k
⊢ 0 < r' * (b - a) → (f ((lineMap b a) r') ≤ (lineMap (f b) (f a)) r' ↔ slope f a b ≤ slope f ((lineMap b a) r') b)

Tactic:
;

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder 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 r' : k
⊢ 0 < r' * (b - a) → (f ((lineMap b a) r') ≤ (lineMap (f b) (f a)) r' ↔ slope f a b ≤ slope f ((lineMap b a) r') b)
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder 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
⊢ 0 < r' * (b - a) → (f ((lineMap b a) r') ≤ (lineMap (f b) (f a)) r' ↔ slope f a b ≤ slope f ((lineMap b a) r') b)

Tactic:
;

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder 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
⊢ 0 < r' * (b - a) → (f ((lineMap b a) r') ≤ (lineMap (f b) (f a)) r' ↔ slope f a b ≤ slope f ((lineMap b a) r') b)
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ (¬∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0) ↔ ∃ x ∈ sᶜ, f x ≠ 0

Tactic:
;

Goal state after:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ (¬∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0) ↔ ∃ x ∈ sᶜ, f x ≠ 0
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ (∃ x ∈ sᶜ, f x ≠ 0) ↔ ∃ x ∈ sᶜ, f x ≠ 0

Tactic:
;

Goal state after:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ (∃ x ∈ sᶜ, f x ≠ 0) ↔ ∃ x ∈ sᶜ, f x ≠ 0
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ (¬∀ f ∈ I, f x = 0) ↔ ∃ f ∈ I, f x ≠ 0

Tactic:
;

Goal state after:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ (¬∀ f ∈ I, f x = 0) ↔ ∃ f ∈ I, f x ≠ 0
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ (∃ f ∈ I, f x ≠ 0) ↔ ∃ f ∈ I, f x ≠ 0

Tactic:
;

Goal state after:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ (∃ f ∈ I, f x ≠ 0) ↔ ∃ f ∈ I, f x ≠ 0
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: case refine_2
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
hs : s₁ ⊆ s₂
g : C(X, ℝ≥0)
hI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hgt : ∀ x ∈ s₂, 0 < g x
⊢ ∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ s₁, 0 < g' x

Tactic:
;

Goal state after:
case refine_2
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
hs : s₁ ⊆ s₂
g : C(X, ℝ≥0)
hI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hgt : ∀ x ∈ s₂, 0 < g x
⊢ ∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ s₁, 0 < g' x
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CommRing 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : IsTopologicalRing 𝕜
inst✝¹ : Nontrivial 𝕜
inst✝ : NoZeroDivisors 𝕜
x : X
⊢ { toFun := fun f ↦ f x, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } ∈
    {φ | φ 1 = 1 ∧ ∀ (x y : C(X, 𝕜)), φ (x * y) = φ x * φ y}

Tactic:
;

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CommRing 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : IsTopologicalRing 𝕜
inst✝¹ : Nontrivial 𝕜
inst✝ : NoZeroDivisors 𝕜
x : X
⊢ { toFun := fun f ↦ f x, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } ∈
    {φ | φ 1 = 1 ∧ ∀ (x y : C(X, 𝕜)), φ (x * y) = φ x * φ y}
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
⊢ ⨆ k ∈ spectrum ℂ ((gelfandTransform ℂ A) (star a * a)), ↑‖k‖₊ = ⨆ k ∈ spectrum ℂ (star a * a), ↑‖k‖₊

Tactic:
;

Goal state after:
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
⊢ ⨆ k ∈ spectrum ℂ ((gelfandTransform ℂ A) (star a * a)), ↑‖k‖₊ = ⨆ k ∈ spectrum ℂ (star a * a), ↑‖k‖₊
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := ⋯
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
x✝¹ : NonUnitalCommRing ↥S := ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S := ⋯
⊢ ↑(⟨a, ?m.172⟩ * ⟨b, ?m.175⟩) = ↑0

Tactic:
;

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := ⋯
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
x✝¹ : NonUnitalCommRing ↥S := ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S := ⋯
⊢ ↑(⟨a, ?m.172⟩ * ⟨b, ?m.175⟩) = ↑0
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := ⋯
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
x✝¹ : NonUnitalCommRing ↥S := ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S := ⋯
⊢ a ∈ adjoin ℂ {a, b}

Tactic:
;

Goal state after:
case refine_1
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := ⋯
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
x✝¹ : NonUnitalCommRing ↥S := ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S := ⋯
⊢ a ∈ adjoin ℂ {a, b}
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := ⋯
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
x✝¹ : NonUnitalCommRing ↥S := ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S := ⋯
⊢ b ∈ adjoin ℂ {a, b}

Tactic:
;

Goal state after:
case refine_2
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := ⋯
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
x✝¹ : NonUnitalCommRing ↥S := ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S := ⋯
⊢ b ∈ adjoin ℂ {a, b}
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✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : a = -a⁻
⊢ 0 ≤ a⁻

Tactic:
;

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✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : a = -a⁻
⊢ 0 ≤ a⁻
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
x✝ : Fintype ↑𝔖 := Fintype.ofFinite ↑𝔖
⊢ 𝓤 (α →ᵤ[𝔖] β) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
x✝ : Fintype ↑𝔖 := Fintype.ofFinite ↑𝔖
⊢ 𝓤 (α →ᵤ[𝔖] β) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
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✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
mul₁ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hb' hbs) f * (cfcₙHomSuperset hc' hcs) g = 0
mul₂ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hc' hcs) f * (cfcₙHomSuperset hb' hbs) g = 0
ψ : C(↑s, ℝ)₀ →⋆ₙₐ[ℝ] A :=
  let __src := ↑(cfcₙHomSuperset hb' hbs) + ↑(cfcₙHomSuperset hc' hcs);
  { toFun := ⇑(cfcₙHomSuperset hb' hbs) + ⇑(cfcₙHomSuperset hc' hcs), map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
    map_mul' := ⋯, map_star' := ⋯ }
key : cfcₙHomSuperset ha has = ψ
⊢ ↑0 ≤ 0

Tactic:
;

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✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
mul₁ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hb' hbs) f * (cfcₙHomSuperset hc' hcs) g = 0
mul₂ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hc' hcs) f * (cfcₙHomSuperset hb' hbs) g = 0
ψ : C(↑s, ℝ)₀ →⋆ₙₐ[ℝ] A :=
  let __src := ↑(cfcₙHomSuperset hb' hbs) + ↑(cfcₙHomSuperset hc' hcs);
  { toFun := ⇑(cfcₙHomSuperset hb' hbs) + ⇑(cfcₙHomSuperset hc' hcs), map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
    map_mul' := ⋯, map_star' := ⋯ }
key : cfcₙHomSuperset ha has = ψ
⊢ ↑0 ≤ 0
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))
f : C(↑(spectrum ℂ a), ℂ)
⊢ Commute (((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)) (star f))
    (((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)) f)

Tactic:
;

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal
⊢ SpectrumRestricts (a + b) ⇑ContinuousMap.realToNNReal

Tactic:
rw [SpectrumRestricts.nnreal_iff_nnnorm (ha₁.add hb₁) (nnnorm_add_le a b), NNReal.coe_add,
    map_add, add_sub_add_comm]
  refine nnnorm_add_le _ _ |>.trans ?_
  gcongr
  all_goals rw [← SpectrumRestricts.nnreal_iff_nnnorm] <;> first | rfl | assumption

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

Goal state before:
pp: case h.left.«1».right
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ ‖![(↑(realPart a))⁺, (↑(imaginaryPart a))⁺, (↑(realPart a))⁻, (↑(imaginaryPart a))⁻] ((fun i ↦ i) ⟨1, ⋯⟩)‖ ≤ ‖a‖

Tactic:
exact CStarAlgebra.norm_posPart_le _ |>.trans <| imaginaryPart.norm_le a

Goal state after: