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

Goal state before:
pp: case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ cfc (fun x ↦ star (f x)) a = star (cfc f a)

Tactic:
· rw [cfc_apply_of_not_continuousOn a hf, cfc_apply_of_not_continuousOn, star_zero]
      exact fun hf_star ↦ hf <| by simpa using hf_star.star

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✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
⊢ cfc (g ∘ f) a = cfc g (cfc f a)

Tactic:
have sp_eq : spectrum R (cfcHom (show p a from ha) (ContinuousMap.mk _ hf.domRestrict)) =
      f '' (spectrum R a) := by
    rw [cfcHom_map_spectrum (by exact ha) _]
    ext
    simp

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }) = f '' spectrum R a
⊢ cfc (g ∘ f) a = cfc g (cfc f a)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
⊢ (𝓝[s ∩ Icc y x ∩ Iio x] x).NeBot

pp: case inr.refine_2
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
⊢ ContinuousWithinAt f (s ∩ Icc y x ∩ Iic x) x

Tactic:
· rwa [show s ∩ Icc y x ∩ Iio x = (s ∩ Iio x) ∩ Ici y by grind, nhdsWithin_inter_of_mem']
    apply mem_nhdsWithin_of_mem_nhds
    exact Ici_mem_nhds hy

Goal state after:
case inr.refine_2
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
⊢ ContinuousWithinAt f (s ∩ Icc y x ∩ Iic x) x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁵ : Semifield R
inst✝²⁴ : StarRing R
inst✝²³ : MetricSpace R
inst✝²² : IsTopologicalSemiring R
inst✝²¹ : ContinuousStar R
inst✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : TopologicalSpace A
inst✝⁴ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus S A q
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : UniqueHom R A
inst✝ : CompleteSpace R
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
⊢ IsClosedEmbedding ⇑(cfcₙHom ha)

Tactic:
by
    have := QuasispectrumRestricts.cfc f halg.isClosedEmbedding h0 h
    rw [cfcₙHom_eq_restrict f ha ((h a).mp ha).1 ((h a).mp ha).2]
    exact isClosedEmbedding_nonUnitalStarAlgHom (cfcₙHom_isClosedEmbedding ((h a).mp ha).1)
      ((h a).mp ha).2 halg

Goal state after:
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a)) (h0 : { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯ } 0 = 0) (ha : p a),
    P ((cfcₙHom ha) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := h0 })
⊢ P (cfcₙ f a)

Tactic:
by_cases h : ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a
  · rw [cfcₙ_apply f a h.1 h.2.1 h.2.2]
    exact haf h.1 h.2.1 h.2.2
  · simp only [not_and_or] at h
    obtain (h | h | h) := h
    · rwa [cfcₙ_apply_of_not_continuousOn _ h]
    · rwa [cfcₙ_apply_of_not_map_zero _ h]
    · rwa [cfcₙ_apply_of_not_predicate _ h]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n ν : ℕ
this :
  ↑((n + 1).choose (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) -
      ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν) - ↑(n.choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
⊢ Polynomial.derivative (↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n + 1 - (ν + 1))) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))

Tactic:
simpa [Polynomial.derivative_pow, ← sub_eq_add_neg, Nat.succ_sub_succ_eq_sub,
      Polynomial.derivative_mul, Polynomial.derivative_natCast, zero_mul,
      Nat.cast_add, algebraMap.coe_one, Polynomial.derivative_X, mul_one, zero_add,
      Polynomial.derivative_sub, Polynomial.derivative_one, zero_sub, mul_neg, Nat.sub_zero,
      bernsteinPolynomial, map_add, map_natCast, Nat.cast_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
w : k < n - ν
⊢ eval 1 ((⇑derivative)^[k] ((bernsteinPolynomial R n (n - ν)).comp (1 - X))) = 0

Tactic:
simp [Polynomial.eval_comp, iterate_derivative_at_0_eq_zero_of_lt R n w]

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

Goal state before:
pp: a b : ℝ
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
by
  rcases lt_or_ge a b with h | h
  -- (Otherwise it's easy; we'll deal with that later.)
  · -- We can pullback continuous functions on `[a,b]` to continuous functions on `[0,1]`,
    -- by precomposing with an affine map.
    let W : C(Set.Icc a b, ℝ) →ₐ[ℝ] C(I, ℝ) :=
      compRightAlgHom ℝ ℝ (iccHomeoI a b h).symm
    -- This operation is itself a homeomorphism
    -- (with respect to the norm topologies on continuous functions).
    let W' : C(Set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := (iccHomeoI a b h).arrowCongr (.refl _)
    have w : (W : C(Set.Icc a b, ℝ) → C(I, ℝ)) = W' := rfl
    -- Thus we take the statement of the Weierstrass approximation theorem for `[0,1]`,
    have p := polynomialFunctions_closure_eq_top'
    -- and pullback both sides, obtaining an equation between subalgebras of `C([a,b], ℝ)`.
    apply_fun fun s => s.comap W at p
    simp only [Algebra.comap_top] at p
    -- Since the pullback operation is continuous, it commutes with taking `topologicalClosure`,
    rw [Subalgebra.topologicalClosure_comap_homeomorph _ W W' w] at p
    -- and precomposing with an affine map takes polynomial functions to polynomial functions.
    rw [polynomialFunctions.comap_compRightAlgHom_iccHomeoI] at p
    -- 🎉
    exact p
  · -- Otherwise, `b ≤ a`, and the interval is a subsingleton,
    subsingleton [(Set.subsingleton_Icc_of_ge h).coe_sort]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
⊢ (MvPolynomial.aeval e) (n • (x + y) ^ (n - 1) • (1 + 0)) * X = n • X

Tactic:
simp only [x, y, e, smul_eq_mul, nsmul_eq_mul, map_natCast, map_pow, map_add,
      map_mul, Bool.cond_true, Bool.cond_false, MvPolynomial.aeval_X, add_sub_cancel,
      one_pow, add_zero, mul_one]

Goal state after:
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
ha : p a
⊢ ∀ (f : C(↑(σₙ R a), R)₀), σₙ R ((cfcₙHom_of_cfcHom R ha) f) = range ⇑f

Tactic:
intro f

Goal state after:
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
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ σₙ R ((cfcₙHom_of_cfcHom R ha) f) = range ⇑f
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν

Tactic:
lhs

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
      (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
    n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
Module: Mathlib.Analysis.Normed.Algebra.Unitization

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
a✝ : Nontrivial A
⊢ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖ ≤ 2 * max ‖((addEquiv 𝕜 A) x).1‖ ‖((addEquiv 𝕜 A) x).2‖

Tactic:
calc
      ‖algebraMap 𝕜 _ x.fst + mul 𝕜 A x.snd‖ ≤ ‖algebraMap 𝕜 _ x.fst‖ + ‖mul 𝕜 A x.snd‖ :=
        norm_add_le _ _
      _ = ‖x.fst‖ + ‖x.snd‖ := by
        rw [norm_algebraMap', (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 A)).mp (isometry_mul 𝕜 A)]
      _ ≤ _ := (add_le_add (le_max_left _ _) (le_max_right _ _)).trans_eq (two_mul _).symm

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
⊢ ‖((x.toProd.1 • b)⋆ + (x.toProd.2 * b)⋆) * (x.toProd.1 • b + x.toProd.2 * b)‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1 + (mul 𝕜 E) (x⋆ * x).toProd.2‖

Tactic:
star_mul,

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
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖((x.toProd.1 • b)⋆ + b⋆ * x.toProd.2⋆) * (x.toProd.1 • b + x.toProd.2 * b)‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1 + (mul 𝕜 E) (x⋆ * x).toProd.2‖
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
key : (↑I).range ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
⊢ ∀ (x : C(X, 𝕜)), x ∈ A.topologicalClosure

Tactic:
intro f

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
key : (↑I).range ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
⊢ f ∈ A.topologicalClosure
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
⊢ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ⊆ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Tactic:
intro f

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
⊢ f ∈ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) → f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
Module: Mathlib.Topology.Sets.VietorisTopology

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

Tactic:
obtain ⟨u, v, hu, hv, rfl⟩ : ∃ u v, u ⊆ powerset '' {U | IsOpen U} ∧
        v ⊆ (fun V => {s | (s ∩ V).Nonempty}) '' {U | IsOpen U} ∧ u ∪ v = t := by
      rw [← inter_eq_left, inter_union_distrib_left] at ht₂
      exact ⟨_, _, inter_subset_right, inter_subset_right, ht₂⟩

Goal state after:
case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h✝ : s.Nonempty
u v : Set (Set (Set α))
hu : u ⊆ powerset '' {U | IsOpen[inst✝] U}
hv : v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}
ht₁ : (u ∪ v).Finite
ht₂ : u ∪ v ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hs : s ∈ ⋂₀ (u ∪ v)
⊢ ∃ x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
    s ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∧ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ (u ∪ v)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h✝ : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U | IsOpen[inst✝] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U | IsOpen[inst✝] U}
v : Set (Set α)
hv₁ : v ⊆ {U | IsOpen[inst✝] U}
hv₂ : v.Finite
hv : (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}
ht₁ : (powerset '' u).Finite ∧ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' v).Finite
ht₂ :
  powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
U : Set α := ⋂₀ u
hU : IsOpen[inst✝] U
hs : s ⊆ U ∧ ∀ i ∈ v, s ∈ {s | (s ∩ i).Nonempty}
⊢ insert U ((fun x ↦ U ∩ x) '' v) ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U} ∧
    s ∈ {s | s ⊆ ⋃₀ insert U ((fun x ↦ U ∩ x) '' v) ∧ ∀ U_1 ∈ insert U ((fun x ↦ U ∩ x) '' v), (s ∩ U_1).Nonempty} ∧
      {s | s ⊆ ⋃₀ insert U ((fun x ↦ U ∩ x) '' v) ∧ ∀ U_1 ∈ insert U ((fun x ↦ U ∩ x) '' v), (s ∩ U_1).Nonempty} ⊆
        𝒫 U ∩ ⋂ a ∈ v, {s | (s ∩ a).Nonempty}

Tactic:
show ⋃₀ (insert U ((U ∩ ·) '' v)) = U by simp,

Goal state after:
case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h✝ : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U | IsOpen[inst✝] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U | IsOpen[inst✝] U}
v : Set (Set α)
hv₁ : v ⊆ {U | IsOpen[inst✝] U}
hv₂ : v.Finite
hv : (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}
ht₁ : (powerset '' u).Finite ∧ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' v).Finite
ht₂ :
  powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
U : Set α := ⋂₀ u
hU : IsOpen[inst✝] U
hs : s ⊆ U ∧ ∀ i ∈ v, s ∈ {s | (s ∩ i).Nonempty}
⊢ insert U ((fun x ↦ U ∩ x) '' v) ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U} ∧
    s ∈ {s | s ⊆ U ∧ ∀ U_1 ∈ insert U ((fun x ↦ U ∩ x) '' v), (s ∩ U_1).Nonempty} ∧
      {s | s ⊆ U ∧ ∀ U_1 ∈ insert U ((fun x ↦ U ∩ x) '' v), (s ∩ U_1).Nonempty} ⊆ 𝒫 U ∩ ⋂ a ∈ v, {s | (s ∩ a).Nonempty}
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
U : SetRel α α
hU : U ∈ 𝓤 α
this : U.IsRefl
⊢ (hausdorffEntourage U).IsRefl

Tactic:
exact isRefl_hausdorffEntourage U

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst✝¹] U → IsOpen[t] {s | (s ∩ U).Nonempty}
x : α
hs : {x} ∈ (range fun x ↦ {x})ᶜ
h : {x}.Nonempty
⊢ (range fun x ↦ {x})ᶜ ∈ 𝓝 {x}

pp: case inr.inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst✝¹] U → IsOpen[t] {s | (s ∩ U).Nonempty}
s : Set α
hs : s ∈ (range fun x ↦ {x})ᶜ
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ (range fun x ↦ {x})ᶜ ∈ 𝓝 s

Tactic:
· cases hs <| Set.mem_range_self x

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst✝¹] U → IsOpen[t] {s | (s ∩ U).Nonempty}
s : Set α
hs : s ∈ (range fun x ↦ {x})ᶜ
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ (range fun x ↦ {x})ᶜ ∈ 𝓝 s
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ Metric.eball 0 (↑‖a‖₊)⁻¹
h : ¬‖a‖₊ = 0
nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹
⊢ ‖y • a‖ < 1

Tactic:
rwa [← coe_nnnorm, ← Real.lt_toNNReal_iff_coe_lt, Real.toNNReal_one, nnnorm_smul,
            ← NNReal.lt_inv_iff_mul_lt h]

Goal state after:
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
⊢ frontier (σ 𝕜 x) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 ↑x) ∩
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 ↑x)ᶜ

Tactic:
(spectrum.isClosed (x : A)).closure_eq

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
⊢ frontier (σ 𝕜 x) ⊆ σ 𝕜 ↑x ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 ↑x)ᶜ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case e'_4.a
𝕜 : 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
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest ((fun x ↦ ‖f x‖) '' σ 𝕜 a) ((fun x ↦ ‖f x‖) x)
⊢ ‖{ toFun := (σ 𝕜 a).domRestrict f, continuous_toFun := ⋯ }‖ ≤ (fun x ↦ ‖f x‖) x

Tactic:
apply ContinuousMap.norm_le _ (norm_nonneg _) |>.mpr

Goal state after:
case e'_4.a
𝕜 : 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
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest ((fun x ↦ ‖f x‖) '' σ 𝕜 a) ((fun x ↦ ‖f x‖) x)
⊢ ∀ (x_1 : ↑(σ 𝕜 a)), ‖{ toFun := (σ 𝕜 a).domRestrict f, continuous_toFun := ⋯ } x_1‖ ≤ ‖f x‖
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
⊢ (∀ x ∈ spectrum ℝ a, 0 ≤ x) ↔ spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t

Tactic:
refine ⟨fun h ↦ iSup₂_le fun x hx ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
x : ℝ
hx : x ∈ spectrum ℝ ((algebraMap ℝ A) ↑t - a)
⊢ ↑‖x‖₊ ≤ ↑t

case refine_2
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x