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

Goal state before:
pp: case e'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : TopologicalSpace A
inst✝³ : T2Space A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra 𝕜 A
s : Set 𝕜
x✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) = ψ (ContinuousMap.restrict s (ContinuousMap.id 𝕜))
⊢ φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = φ (ContinuousMap.restrict s (ContinuousMap.id 𝕜))

Tactic:
exact congr_arg _ (by ext; simp)

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

Goal state before:
pp: case e'_3
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : TopologicalSpace A
inst✝³ : T2Space A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra 𝕜 A
s : Set 𝕜
x✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) = ψ (ContinuousMap.restrict s (ContinuousMap.id 𝕜))
⊢ ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ (ContinuousMap.restrict s (ContinuousMap.id 𝕜))

Tactic:
exact congr_arg _ (by ext; simp)

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

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
A : Type u_2
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra ℝ A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
f : C(X, ℝ≥0)
⊢ φ f - φ 0 = φ f

Tactic:
rw [map_zero, sub_zero]

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
a : E
⊢ ‖(mul 𝕜 E) a‖₊ = ‖a‖₊

Tactic:
rw [← sSup_unitClosedBall_eq_nnnorm]

Goal state after:
𝕜 : 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
a : E
⊢ sSup ((fun x ↦ ‖((mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1) = ‖a‖₊
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)₀
⊢ φ f - φ 0 = φ f

Tactic:
rw [map_zero, sub_zero]

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

Goal state before:
pp: case pos
𝕜 : 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
h₃ : ‖((splitMul 𝕜 E) (x⋆ * x)).1‖ = ‖((splitMul 𝕜 E) x).1‖ ^ 2
h : ‖((splitMul 𝕜 E) x).1‖ ≤ ‖((splitMul 𝕜 E) x).2‖
⊢ max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ * max ‖((splitMul 𝕜 E) x).1‖ ‖((splitMul 𝕜 E) x).2‖ ≤
    max (‖((splitMul 𝕜 E) x).1‖ * ‖((splitMul 𝕜 E) x).1‖) (‖((splitMul 𝕜 E) x).2‖ * ‖((splitMul 𝕜 E) x).2‖)

Tactic:
sup_eq_right.mpr h,

Goal state after:
case pos
𝕜 : 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
h₃ : ‖((splitMul 𝕜 E) (x⋆ * x)).1‖ = ‖((splitMul 𝕜 E) x).1‖ ^ 2
h : ‖((splitMul 𝕜 E) x).1‖ ≤ ‖((splitMul 𝕜 E) x).2‖
⊢ ‖((splitMul 𝕜 E) x).2‖ * ‖((splitMul 𝕜 E) x).2‖ ≤
    max (‖((splitMul 𝕜 E) x).1‖ * ‖((splitMul 𝕜 E) x).1‖) (‖((splitMul 𝕜 E) x).2‖ * ‖((splitMul 𝕜 E) x).2‖)
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
map_one' : ∀ (φ : ↑(characterSpace 𝕜 A)), φ 1 = 1
φ : ↑(characterSpace 𝕜 A)
r : 𝕜
⊢ φ ((algebraMap 𝕜 A) r) = (algebraMap 𝕜 𝕜) r

Tactic:
by
      rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_self, RingHom.id_apply]
      rw [map_smul, smul_eq_mul, map_one' φ, mul_one]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : NoZeroDivisors 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : ContinuousAdd 𝕜
inst✝⁶ : ContinuousConstSMul 𝕜 𝕜
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed (characterSpace 𝕜 A)

Tactic:
eq_set_map_one_map_mul,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : NoZeroDivisors 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : ContinuousAdd 𝕜
inst✝⁶ : ContinuousConstSMul 𝕜 𝕜
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed {φ | φ 1 = 1 ∧ ∀ (x y : A), φ (x * y) = φ x * φ y}
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C(↑s, 𝕜)
hf : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf₂ : r = 0
this : f ⟨0, h0⟩ = 0
⊢ 0 + f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

Tactic:
zero_add

Goal state after:
case mp
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C(↑s, 𝕜)
hf : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf₂ : r = 0
this : f ⟨0, h0⟩ = 0
⊢ f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
hf : UpperHemicontinuousOn f s
hg : UpperHemicontinuousOn g s
⊢ UpperHemicontinuousOn (fun x ↦ f x ∪ g x) s

Tactic:
upperHemicontinuousOn_iff

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
hg : ∀ x ∈ s, UpperHemicontinuousWithinAt g s x
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt (fun x ↦ f x ∪ g x) s x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
hf : UpperHemicontinuousOn f s
u : Set β
hu : IsClosed[inst✝] u
⊢ UpperHemicontinuousOn (fun x ↦ f x ∩ u) s

Tactic:
upperHemicontinuousOn_iff

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
u : Set β
hu : IsClosed[inst✝] u
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt (fun x ↦ f x ∩ u) s x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
s : Set α
γ : Type u_5
inst✝ : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousOn f s
hi : IsInducing i
h_cl : IsClosed[inst✝¹] (range i)
⊢ UpperHemicontinuousOn (fun x ↦ i ⁻¹' f x) s

Tactic:
upperHemicontinuousOn_iff

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
s : Set α
γ : Type u_5
inst✝ : TopologicalSpace γ
i : γ → β
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
hi : IsInducing i
h_cl : IsClosed[inst✝¹] (range i)
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt (fun x ↦ i ⁻¹' f x) s x
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
⊢ {x | x.1 ⊆ x.2 ∧ x.2 ⊆ SetRel.id.image x.1} = SetRel.id

Tactic:
image_id,

Goal state after:
α : Type u_1
⊢ {x | x.1 ⊆ x.2 ∧ x.2 ⊆ x.1} = SetRel.id
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
x₀ : α
hx₀s : x₀ ∈ s
V : Set β
hV : IsOpen[inst✝.toTopologicalSpace] V
y₀ : β
hy₀f : y₀ ∈ f x₀
hy₀V : y₀ ∈ V
W : Set (β × β)
hW : W ∈ uniformity β
hWsub : ball y₀ W ⊆ V
U₁ : Set (β × β)
hU₁ : U₁ ∈ uniformity β
hU₁sym : SetRel.IsSymm U₁
hU₁comp : SetRel.comp U₁ U₁ ⊆ W
⊢ ∀ᶠ (x' : α) in 𝓝[s] x₀, (f x' ∩ V).Nonempty

Tactic:
obtain ⟨U, hU, hUsym, hUcomp⟩ := comp_symm_mem_uniformity_sets hU₁

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
x₀ : α
hx₀s : x₀ ∈ s
V : Set β
hV : IsOpen[inst✝.toTopologicalSpace] V
y₀ : β
hy₀f : y₀ ∈ f x₀
hy₀V : y₀ ∈ V
W : Set (β × β)
hW : W ∈ uniformity β
hWsub : ball y₀ W ⊆ V
U₁ : Set (β × β)
hU₁ : U₁ ∈ uniformity β
hU₁sym : SetRel.IsSymm U₁
hU₁comp : SetRel.comp U₁ U₁ ⊆ W
U : Set (β × β)
hU : U ∈ uniformity β
hUsym : SetRel.IsSymm U
hUcomp : SetRel.comp U U ⊆ U₁
⊢ ∀ᶠ (x' : α) in 𝓝[s] x₀, (f x' ∩ V).Nonempty
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
⊢ ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊

Tactic:
simpa only [Real.toNNReal_mul (norm_nonneg _), norm_toNNReal, nnnorm_pow k (n + 1),
      ENNReal.coe_mul] using coe_mono (Real.toNNReal_mono (norm_le_norm_mul_of_mem pow_mem))

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), UpperHemicontinuousOn (F n) s
hf_compact : ∀ x ∈ s, IsCompact (f x)
x₀ : α
hx₀s : x₀ ∈ s
u : Set β
hu : IsOpen[inst✝.toTopologicalSpace] u
hx₀u : f x₀ ⊆ u
W : Set (β × β)
hW : W ∈ uniformity β
left✝ : IsOpen[instTopologicalSpaceProd] W
hWu : ∀ x ∈ f x₀, ball x W ⊆ u
V : Set (β × β)
hV : V ∈ uniformity β
hVsym : SetRel.IsSymm V
hVcomp : SetRel.comp V V ⊆ W
U : SetRel β β
hUsub : id U ⊆ V
hUmem : U ∈ uniformity β
hUopen : IsOpen[instTopologicalSpaceProd] U
hHU : hausdorffEntourage U ∈ uniformity (Set β)
N : ι
hN : ∀ x ∈ s, (f x, F N x) ∈ hausdorffEntourage U
hFN_image : F N x₀ ⊆ U.image (f x₀)
⊢ ∀ᶠ (x' : α) in 𝓝[s] x₀, f x' ⊆ u

Tactic:
upperHemicontinuousOn_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hf_compact : ∀ x ∈ s, IsCompact (f x)
x₀ : α
hx₀s : x₀ ∈ s
u : Set β
hu : IsOpen[inst✝.toTopologicalSpace] u
hx₀u : f x₀ ⊆ u
W : Set (β × β)
hW : W ∈ uniformity β
left✝ : IsOpen[instTopologicalSpaceProd] W
hWu : ∀ x ∈ f x₀, ball x W ⊆ u
V : Set (β × β)
hV : V ∈ uniformity β
hVsym : SetRel.IsSymm V
hVcomp : SetRel.comp V V ⊆ W
U : SetRel β β
hUsub : id U ⊆ V
hUmem : U ∈ uniformity β
hUopen : IsOpen[instTopologicalSpaceProd] U
hHU : hausdorffEntourage U ∈ uniformity (Set β)
N : ι
hN : ∀ x ∈ s, (f x, F N x) ∈ hausdorffEntourage U
hFN_image : F N x₀ ⊆ U.image (f x₀)
hF : ∀ (n : ι), ∀ x ∈ s, UpperHemicontinuousWithinAt (F n) s x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x₀, f x' ⊆ u
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ IsGreatest ((fun x ↦ ‖f x‖₊) '' σ 𝕜 a) ‖cfc f a‖₊

Tactic:
by
  convert! Real.toNNReal_monotone.map_isGreatest (.norm_cfc f a)
  all_goals simp [Set.image_image, norm_toNNReal]

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : T2Space A
f : ℂ → ℂ
a : A
hf_real : ∀ x ∈ σ ℂ a, star (f x) = f x
ha : IsSelfAdjoint a
⊢ cfc f a = cfc (fun x ↦ (f ↑x).re) a

Tactic:
rw [cfc_real_eq_complex ..]

Goal state after:
A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : T2Space A
f : ℂ → ℂ
a : A
hf_real : ∀ x ∈ σ ℂ a, star (f x) = f x
ha : IsSelfAdjoint a
⊢ cfc f a = cfc (fun x ↦ ↑(f ↑x.re).re) a
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : IsTopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : SMulCommClass R β β
r : R
f g : α →C₀ β
x✝ : α
⊢ r • f x✝ • g x✝ = f x✝ • r • g x✝

Tactic:
smul_comm

Goal state after:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : IsTopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : SMulCommClass R β β
r : R
f g : α →C₀ β
x✝ : α
⊢ f x✝ • r • g x✝ = f x✝ • r • g x✝
Module: Mathlib.Analysis.LocallyConvex.Polar

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ ⋂₀ (B.polar '' {F | F.Finite ∧ F ⊆ s}) = B.polar s

Tactic:
ext x
  simp only [Set.sInter_image, Set.mem_ofPred_eq, Set.mem_iInter, and_imp]
  refine ⟨fun hx a ha ↦ ?_, fun hx F _ hF₂ => polar_antitone _ hF₂ hx⟩
  simpa [mem_polar_singleton] using hx _ (Set.finite_singleton a) (Set.singleton_subset_iff.mpr ha)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ (gaugeSeminormFamily 𝕜 E s).ball 0 1 = ↑s

Tactic:
dsimp only [gaugeSeminormFamily]
  rw [Seminorm.ball_zero_eq]
  simp_rw [gaugeSeminorm_toFun]
  exact setOfPred_gauge_lt_one_eq_self_of_isOpen (s.coe_convex.lift ℝ) s.coe_zero_mem s.coe_isOpen

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this : Fintype ↑u := ⋯
⊢ (Finset.univ.sup '' univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}) ⊆
    {K | ↑K ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑K ∩ U).Nonempty) ∧ (↑K).Finite}

Tactic:
simp_rw [image_subset_iff, preimage_ofPred_eq, coe_finset_sup, Finset.sup_eq_iSup,
      iSup_eq_iUnion, Finset.mem_univ, iUnion_true, iUnion_subset_iff]
    refine fun f hf => ⟨by grind, fun U hU => ?_, finite_iUnion (by grind)⟩
    obtain ⟨h₁, -, h₂⟩ := hf ⟨U, hU⟩ trivial
    exact h₁.mono (subset_inter (subset_iUnion _ _) h₂)

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

Goal state before:
pp: case refine_1
𝕜 : 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 ∧ v i' ⊆ u i

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 _
      obtain ⟨W, ⟨hW_nhds, hW_abs⟩, hWn⟩ :=
        (nhds_hasBasis_absConvex 𝕜 E).mem_iff.mp (hu_basis.mem_of_mem trivial)
      obtain ⟨m, hm⟩ := hu_basis.mem_iff.mp hW_nhds
      exact ⟨m, trivial, (absConvexHull_min (interior_subset.trans hm) hW_abs).trans hWn⟩

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
⊢ ∀ (i' : ℕ), True → ∃ i, True ∧ u i ⊆ v i'
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ PreconnectedSpace (NonemptyCompacts α) ↔ PreconnectedSpace α

Tactic:
refine ⟨fun h => ?_, fun h => inferInstance⟩

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
h : PreconnectedSpace (NonemptyCompacts α)
⊢ PreconnectedSpace α
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: E : Type u_3
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : QuasiCompleteSpace ℝ E
s : Set E
ht : TotallyBounded s
⊢ IsCompact ((closedAbsConvexHull ℝ) s)

Tactic:
rw [closedAbsConvexHull_eq_closure_absConvexHull]

Goal state after:
E : Type u_3
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : QuasiCompleteSpace ℝ E
s : Set E
ht : TotallyBounded s
⊢ IsCompact (closure[inst✝⁴.toTopologicalSpace] ((absConvexHull ℝ) s))
Module: Mathlib.Analysis.LocallyConvex.HahnBanach

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : NormedField 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : Module 𝕜 E
S : Submodule 𝕜 E
f : Dual 𝕜 ↥S
p : Seminorm 𝕜 E
hp : ∀ (x : ↥S), ‖f x‖ ≤ p ↑x
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ ∃ g, (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), ‖g x‖ ≤ p x

Tactic:
let : Module ℝ E := .restrictScalars ℝ 𝕜 E

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : NormedField 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : Module 𝕜 E
S : Submodule 𝕜 E
f : Dual 𝕜 ↥S
p : Seminorm 𝕜 E
hp : ∀ (x : ↥S), ‖f x‖ ≤ p ↑x
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : Module ℝ E := restrictScalars ℝ 𝕜 E
⊢ ∃ g, (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), ‖g x‖ ≤ p x
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
y : X
hydl : dist (c.left.right.lim y) (c.left.right.lim x) ≤ (3 / 4) ^ n
hydr : dist (c.right.lim y) (c.right.lim x) ≤ (3 / 4) ^ n
hxl : x ∉ c.left.left.U
hyl : y ∉ c.left.left.U
⊢ ((0 + dist (c.left.right.lim y) (c.left.right.lim x)) / 2 + dist (c.right.lim y) (c.right.lim x)) / 2 ≤
    (3 / 4) ^ n * (3 / 4)

Tactic:
zero_add

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
y : X
hydl : dist (c.left.right.lim y) (c.left.right.lim x) ≤ (3 / 4) ^ n
hydr : dist (c.right.lim y) (c.right.lim x) ≤ (3 / 4) ^ n
hxl : x ∉ c.left.left.U
hyl : y ∉ c.left.left.U
⊢ (dist (c.left.right.lim y) (c.left.right.lim x) / 2 + dist (c.right.lim y) (c.right.lim x)) / 2 ≤
    (3 / 4) ^ n * (3 / 4)
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
K V : Set X
hK : IsCompact K
hV : IsOpen[inst✝²] V
hKV : K ⊆ V
⊢ ∃ f, EqOn (⇑f) 1 K ∧ IsCompact (tsupport ⇑f) ∧ tsupport ⇑f ⊆ V ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
by
  obtain ⟨U, hU1, hU2, hU3, hU4⟩ := exists_open_between_and_isCompact_closure hK hV hKV
  obtain ⟨f, hf1, hf2, hf3⟩ := exists_tsupport_one_of_isOpen_isClosed hU1 hU4
    isClosed_closure (hK.closure_subset_of_isOpen hU1 hU2)
  have hfU : tsupport f ⊆ closure U := hf1.trans subset_closure
  exact ⟨f, hf2.mono subset_closure,
    .of_isClosed_subset hU4 isClosed_closure hfU, hfU.trans hU3, hf3⟩

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ‖a‖₊ ≤ t
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ‖(algebraMap ℝ A) ↑t - a‖₊ ≤ t

Tactic:
have : IsSelfAdjoint (algebraMap ℝ A t - a) := IsSelfAdjoint.algebraMap A (.all (t : ℝ)) |>.sub ha

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ‖a‖₊ ≤ t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ‖(algebraMap ℝ A) ↑t - a‖₊ ≤ t
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
x : ℂ
⊢ x ∈ σₙ ℂ a → 0 ≤ x

Tactic:
mem_quasispectrum_iff

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
x : ℂ
⊢ x = 0 ∨ x ∈ spectrum ℂ a → 0 ≤ x