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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : cfcₙ f a = cfcₙ g a
ha : p a
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
⊢ Set.EqOn f g (σₙ R a)

Tactic:
rw [cfcₙ_apply f a, cfcₙ_apply g a] at h
  exact fun x hx ↦ congr($(cfcₙHom_injective ha h) ⟨x, hx⟩)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁴ : CommRing R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalRing R
inst✝⁹ : ContinuousStar R
inst✝⁸ : ContinuousSqrt R
inst✝⁷ : StarOrderedRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
r : R
a : A
ha : p a
⊢ a ≤ (algebraMap R A) r ↔ ∀ x ∈ spectrum R a, x ≤ r

Tactic:
nth_rw 1 [← cfc_id R a]
  exact cfc_le_algebraMap_iff id r a

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
⊢ eval 1 ((⇑derivative)^[n - k] p) = 0

Tactic:
refine span_induction ?_ ?_ ?_ ?_ m

Goal state after:
case refine_1
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
⊢ ∀ x ∈ Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1, eval 1 ((⇑derivative)^[n - k] x) = 0

case refine_2
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
⊢ eval 1 ((⇑derivative)^[n - k] 0) = 0

case refine_3
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
⊢ ∀ (x y : ℚ[X]),
    x ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1) →
      y ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1) →
        eval 1 ((⇑derivative)^[n - k] x) = 0 →
          eval 1 ((⇑derivative)^[n - k] y) = 0 → eval 1 ((⇑derivative)^[n - k] (x + y)) = 0

case refine_4
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
⊢ ∀ (a : ℚ),
    ∀ x ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1),
      eval 1 ((⇑derivative)^[n - k] x) = 0 → eval 1 ((⇑derivative)^[n - k] (a • x)) = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
a : A
h_cpct : IsCompact (spectrum R a)
⊢ IsCompact (spectrum R a ∪ {0})

Tactic:
exact h_cpct |>.union isCompact_singleton

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
inst✝² : TopologicalSpace A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
φ ψ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst✝²] ⇑φ
hψ : Continuous[_, inst✝²] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) = ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this :
  ∀ (ξ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A),
    Continuous[_, inst✝²] ⇑ξ →
      let ξ' := ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e);
      Continuous[_, inst✝²] ⇑ξ' ∧
        ξ' (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) = ξ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
hφ' : Continuous[_, inst✝²] ⇑(φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
hφ_id :
  (φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
      (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) =
    φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
hψ' : Continuous[_, inst✝²] ⇑(ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
hψ_id :
  (ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
      (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) =
    ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
⊢ φ = ψ

Tactic:
have hs' : CompactSpace s' := e.compactSpace

Goal state after:
X : Type u_1
inst✝⁶ : TopologicalSpace X
A : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
φ ψ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst✝²] ⇑φ
hψ : Continuous[_, inst✝²] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) = ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this :
  ∀ (ξ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A),
    Continuous[_, inst✝²] ⇑ξ →
      let ξ' := ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e);
      Continuous[_, inst✝²] ⇑ξ' ∧
        ξ' (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) = ξ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
hφ' : Continuous[_, inst✝²] ⇑(φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
hφ_id :
  (φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
      (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) =
    φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
hψ' : Continuous[_, inst✝²] ⇑(ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
hψ_id :
  (ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
      (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) =
    ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
hs' : CompactSpace ↑s'
⊢ φ = ψ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: case pos
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, ℝ)₀
r : ℝ≥0
⊢ φ (↑r • f).toNNReal - φ (-(↑r • f)).toNNReal = ↑r • (φ f.toNNReal - φ (-f).toNNReal)

Tactic:
simp only [← smul_def, toNNReal_smul, map_smul, toNNReal_neg_smul, smul_sub]

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
⊢ ∃ f ∈ (fun f ↦ ⇑f) '' ↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)),
    f x₁ ≠ f x₂

Tactic:
refine ⟨_, ⟨⟨(‖F ·‖ ^ 2), by fun_prop⟩, ?_, rfl⟩, ?_⟩

Goal state after:
case refine_1
𝕜 : 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
⊢ { toFun := fun x ↦ ‖F x‖ ^ 2, continuous_toFun := ⋯ } ∈
    ↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra))

case refine_2
𝕜 : 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
⊢ (fun f ↦ ⇑f) { toFun := fun x ↦ ‖F x‖ ^ 2, continuous_toFun := ⋯ } x₁ ≠
    (fun f ↦ ⇑f) { toFun := fun x ↦ ‖F x‖ ^ 2, continuous_toFun := ⋯ } x₂
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:

Tactic:
_ ≤ ‖star x.fst • (x.fst • b + x.snd * b) + star x.snd * (x.fst • b + x.snd * b)‖ := by
      nth_rewrite 2 [← one_mul ‖_ + _‖]
      gcongr
      exact (norm_star b).symm ▸ mem_closedBall_zero_iff.1 hb
    _ ≤ sSup (_ '' Metric.closedBall 0 1) := le_csSup ?_ ⟨b, hb, ?_⟩

Goal state after:
case calc_1
𝕜 : 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
⊢ BddAbove
    ((fun x_1 ↦ ‖((algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1 + (mul 𝕜 E) (x⋆ * x).toProd.2) x_1‖) ''
      Metric.closedBall 0 1)

case calc_2
𝕜 : 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
⊢ ‖((algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1 + (mul 𝕜 E) (x⋆ * 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)‖
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
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap (↑I) (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra))
SW : A₀.topologicalClosure = ⊤
⊢ (↑I).range ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure

Tactic:
rw [← Submodule.map_top, ← SW]

Goal state after:
𝕜 : 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
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap (↑I) (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra))
SW : A₀.topologicalClosure = ⊤
⊢ Submodule.map (↑I) A₀.topologicalClosure ≤
    (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
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 • 1 + f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

Tactic:
zero_smul,

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
⊢ 0 + f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ : t ∩ powerset '' {U | IsOpen[inst✝] U} ∪ t ∩ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V} = t
s : Set α
hs : s ∈ ⋂₀ t
h✝ : s.Nonempty
⊢ ∃ u v,
    u ⊆ powerset '' {U | IsOpen[inst✝] U} ∧ v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U} ∧ u ∪ v = t

Tactic:
exact ⟨_, _, inter_subset_right, inter_subset_right, ht₂⟩

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

Goal state before:
pp: A : Type u_3
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : A
inst✝ : CompactSpace ↑(spectrum ℝ a)
⊢ IsCompact (spectrum ℝ≥0 a)

Tactic:
isCompact_iff_compactSpace

Goal state after:
A : Type u_3
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : A
inst✝ : CompactSpace ↑(spectrum ℝ a)
⊢ CompactSpace ↑(spectrum ℝ≥0 a)
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: B : Type u_3
inst✝⁴ : NonUnitalNormedRing B
inst✝³ : NormedSpace ℝ B
inst✝² : IsScalarTower ℝ B B
inst✝¹ : SMulCommClass ℝ B B
a : B
inst✝ : CompactSpace ↑(quasispectrum ℝ a)
⊢ IsCompact (quasispectrum ℝ≥0 a)

Tactic:
isCompact_iff_compactSpace

Goal state after:
B : Type u_3
inst✝⁴ : NonUnitalNormedRing B
inst✝³ : NormedSpace ℝ B
inst✝² : IsScalarTower ℝ B B
inst✝¹ : SMulCommClass ℝ B B
a : B
inst✝ : CompactSpace ↑(quasispectrum ℝ a)
⊢ CompactSpace ↑(quasispectrum ℝ≥0 a)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
⊢ ⨅
      s_1 ∈
        {s_2 |
          s ∈ s_2 ∧
            s_2 ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}},
      Filter.principal s_1 ≤
    ⨅
      s ∈
        {s | t ∈ s ∧ s ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}},
      Filter.principal s

Tactic:
le_iInf₂_iff

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
⊢ ∀ i ∈ {s | t ∈ s ∧ s ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}},
    ⨅
        s_1 ∈
          {s_2 |
            s ∈ s_2 ∧
              s_2 ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}},
        Filter.principal s_1 ≤
      Filter.principal i
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
this : CompleteSpace ↥S
⊢ frontier (σ 𝕜 x) ⊆ σ 𝕜 ↑x

Tactic:
intro μ hμ

Goal state after:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
this : CompleteSpace ↥S
μ : 𝕜
hμ : μ ∈ frontier (σ 𝕜 x)
⊢ μ ∈ σ 𝕜 ↑x
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: r : ℝ
s : Set ℂ
hs₁ : {z | r < z.im} ⊆ s
hs₂ : s ⊆ {z | r ≤ z.im}
⊢ IsConnected s

Tactic:
refine .subset_closure ?_ hs₁ (by simpa only [closure_setOfPred_lt_im] using hs₂)

Goal state after:
r : ℝ
s : Set ℂ
hs₁ : {z | r < z.im} ⊆ s
hs₂ : s ⊆ {z | r ≤ z.im}
⊢ IsConnected {z | r < z.im}
Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula

Goal state before:
pp: A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
⊢ Tendsto (fun n ↦ ENNReal.ofReal (‖a ^ n‖ ^ (1 / ↑n))) atTop (𝓝 (spectralRadius ℂ a))

Tactic:
convert! pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius a using 1

Goal state after:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
⊢ (fun n ↦ ENNReal.ofReal (‖a ^ n‖ ^ (1 / ↑n))) = fun n ↦ ↑‖a ^ n‖₊ ^ (1 / ↑n)
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
a : A
ha : p a
h_cpct : IsCompact (σ 𝕜 a)
⊢ IsCompact (σ 𝕜 a ∪ {0})

Tactic:
exact h_cpct |>.union isCompact_singleton

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
⊢ (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) K₁ K₂

Tactic:
wlog h' : ¬(K₁ ≤ K₂) generalizing K₁ K₂
    · grind [Disjoint.symm, le_antisymm]
    rw [SetLike.not_le_iff_exists] at h'
    obtain ⟨x, hx₁, hx₂⟩ := h'
    obtain ⟨U, V, hU, hV, hU', hV', hUV⟩ := K₂.isCompact.separation_of_notMem hx₂
    exact ⟨_, _, isOpen_inter_nonempty_of_isOpen hV, isOpen_subsets_of_isOpen hU, ⟨x, hx₁, hV'⟩,
      hU', by grind [Set.Nonempty]⟩

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
x : α
hx₁ : x ∈ ↑K
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst✝³] V
hW : IsOpen[inst✝³] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ {K | (↑K ∩ V).Nonempty} ∈ 𝓝 K

Tactic:
rw [(isOpen_inter_nonempty_of_isOpen hV).mem_nhds_iff]
      exact ⟨x, hx₁, hxV <| Set.mem_singleton x⟩

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

Goal state before:
pp: case refine_1
𝕜 : 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
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s : Set E
hs : 0 ∈ s ∧ IsOpen[inst✝⁷] s ∧ AbsConvex 𝕜 s
⊢ ∃ i' ∈ (gaugeSeminormFamily 𝕜 E).basisSets, id i' ⊆ id s

pp: case refine_2
𝕜 : 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
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s : Set E
hs : s ∈ (gaugeSeminormFamily 𝕜 E).basisSets
⊢ ∃ i, (0 ∈ i ∧ IsOpen[inst✝⁷] i ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id s

Tactic:
· refine ⟨s, ⟨?_, rfl.subset⟩⟩
    convert! (gaugeSeminormFamily _ _).basisSets_singleton_mem ⟨s, hs⟩ one_pos
    rw [gaugeSeminormFamily_ball, Subtype.coe_mk]

Goal state after:
case refine_2
𝕜 : 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
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s : Set E
hs : s ∈ (gaugeSeminormFamily 𝕜 E).basisSets
⊢ ∃ i, (0 ∈ i ∧ IsOpen[inst✝⁷] i ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id s
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
⊢ NormedSpace.exp (0 • a) * (a * (a * 1 + 1 * b) + (a * 1 + 1 * b) * b) * NormedSpace.exp (0 • b) =
    a ^ 2 + 2 • (a * b) + b ^ 2

Tactic:
zero_smul,

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
⊢ NormedSpace.exp 0 * (a * (a * 1 + 1 * b) + (a * 1 + 1 * b) * b) * NormedSpace.exp 0 = a ^ 2 + 2 • (a * b) + b ^ 2
Module: Mathlib.Analysis.LocallyConvex.HahnBanach

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
S : Subspace ℝ E
f : Dual ℝ ↥S
p : Seminorm ℝ E
hp : ∀ (x : ↥S), f x ≤ p ↑x
⊢ ∃ g, (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), |g x| ≤ p x

Tactic:
by
  obtain ⟨g, hg, hl⟩ := by
    refine exists_extension_of_le_sublinear ⟨S, f⟩ p (fun _ hc _ => ?_) ?_ hp
    · simp [map_smul_eq_mul, abs_of_nonneg hc.le]
    · exact fun x y => map_add_le_add p x y
  exact ⟨g, hg, p.abs_le_of_le hl⟩

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

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

Tactic:
intro n x

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c₁ c₂ : 𝕜
⊢ dist ((lineMap p₁ p₂) c₁) ((lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₁ p₂

Tactic:
dist_comm p₁ p₂

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c₁ c₂ : 𝕜
⊢ dist ((lineMap p₁ p₂) c₁) ((lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₂ p₁
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: 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
⊢ (lineMap a b) r < (lineMap a' b') r

Tactic:
rcases h₀.eq_or_lt with (rfl | h₀)

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