mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
h : variationOnFromTo f s a b = 0
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
    LocallyBoundedVariationOn f s →
      ∀ {a b : α}, a ∈ s → b ∈ s → variationOnFromTo f s a b = 0 → a ≤ b → edist (f a) (f b) = 0
h' : ¬a ≤ b
⊢ variationOnFromTo f s b a = 0

Tactic:
rw [variationOnFromTo.eq_neg_swap, h, neg_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝¹ : SigmaFinite ν
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (ν (s n) < ∞)
ξ : ℕ → Measure α := fun n ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun n ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
n : ℕ
⊢ ξ n ⟂ₘ ν

Tactic:
rw [← ν.restrict_add_restrict_compl (hsm n)]

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝¹ : SigmaFinite ν
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (ν (s n) < ∞)
ξ : ℕ → Measure α := fun n ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun n ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
n : ℕ
⊢ ξ n ⟂ₘ ν.restrict (s n) + ν.restrict (s n)ᶜ
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Iio b] b) (𝓝 l)
H : Tendsto (fun x ↦ (eVariationOn f (s ∩ Icc x b)).toReal) (𝓝[s ∩ Iio b] b) (𝓝 (dist (f b) l))
x : α
hx : x ∈ s ∩ Iio b
⊢ (eVariationOn f (s ∩ Icc x b)).toReal = variationOnFromTo f s x b

Tactic:
by simp [variationOnFromTo, hx.2.le]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
hxy : y ≤ x
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
let u : ℕ → α := fun n => if n = 0 then y else x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
hxy : y ≤ x
u : ℕ → α := fun n ↦ if n = 0 then y else x
⊢ edist (f x) (f y) ≤ eVariationOn f s
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Ioi b] b) (𝓝 l)
H : Tendsto (fun x ↦ (eVariationOn f (s ∩ Icc b x)).toReal) (𝓝[s ∩ Ioi b] b) (𝓝 (dist (f b) l))
x : α
hx : x ∈ s ∩ Ioi b
⊢ (eVariationOn f (s ∩ Icc b x)).toReal = variationOnFromTo f s b x

Tactic:
by simp [variationOnFromTo, hx.2.le]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
⊢ ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i)) +
      ∑ i ∈ Finset.range (m, ⟨v, ⋯⟩).1, edist (f (↑(m, ⟨v, ⋯⟩).2 (i + 1))) (f (↑(m, ⟨v, ⋯⟩).2 i)) ≤
    eVariationOn f (s ∪ t)

Tactic:
let w i := if i ≤ n then u i else v (i - (n + 1))

Goal state after:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : ℕ → α := fun i ↦ if i ≤ n then u i else v (i - (n + 1))
⊢ ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i)) +
      ∑ i ∈ Finset.range (m, ⟨v, ⋯⟩).1, edist (f (↑(m, ⟨v, ⋯⟩).2 (i + 1))) (f (↑(m, ⟨v, ⋯⟩).2 i)) ≤
    eVariationOn f (s ∪ t)
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : Measurable f
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))

Tactic:
let ρ := μ.withDensity f

Goal state after:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : Measurable f
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
ρ : Measure α := μ.withDensity f
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : CompleteSpace E
inst✝ : DenselyOrdered α
f : α → E
a : α
hf : BoundedVariationOn f univ
⊢ eVariationOn f (Ici a) = eVariationOn f (Ioi a) + edist (f a) (Function.rightLim f a)

Tactic:
← eVariationOn.comp_ofDual f,

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : CompleteSpace E
inst✝ : DenselyOrdered α
f : α → E
a : α
hf : BoundedVariationOn f univ
⊢ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Ici a) = eVariationOn f (Ioi a) + edist (f a) (Function.rightLim f a)
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 : R → R
a : A
hf : ¬f 0 = 0
⊢ cfcₙ f a = 0

Tactic:
rw [cfcₙ_def, dif_neg (not_and_of_not_right _ (not_and_of_not_right _ hf))]

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

Goal state before:
pp: case neg.inl
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 })
h : ¬ContinuousOn f (σₙ R a)
⊢ P (cfcₙ f a)

Tactic:
rwa [cfcₙ_apply_of_not_continuousOn _ h]

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✝¹² : PartialOrder R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring 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
a : A
h : ∀ x ∈ spectrum R a, x ≤ 1
ha : p a
⊢ a ≤ 1

Tactic:
simpa using le_algebraMap_of_spectrum_le h

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

Goal state before:
pp: case succ.left
n k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν ↦ bernsteinPolynomial ℚ n ↑ν
h : k + 1 ≤ n + 1
⊢ LinearIndependent ℚ (Fin.init fun ν ↦ bernsteinPolynomial ℚ n ↑ν)

pp: case succ.right
n k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν ↦ bernsteinPolynomial ℚ n ↑ν
h : k + 1 ≤ n + 1
⊢ bernsteinPolynomial ℚ n ↑(Fin.last k) ∉ span ℚ (Set.range (Fin.init fun ν ↦ bernsteinPolynomial ℚ n ↑ν))

Tactic:
· exact ih (le_of_lt h)

Goal state after:
case succ.right
n k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν ↦ bernsteinPolynomial ℚ n ↑ν
h : k + 1 ≤ n + 1
⊢ bernsteinPolynomial ℚ n ↑(Fin.last k) ∉ span ℚ (Set.range (Fin.init fun ν ↦ bernsteinPolynomial ℚ n ↑ν))
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p f g : R[X]
hf : (toContinuousMapOnAlgHom s) f ∈ R[(toContinuousMapOnAlgHom s) X]
hg : (toContinuousMapOnAlgHom s) g ∈ R[(toContinuousMapOnAlgHom s) X]
⊢ (toContinuousMapOnAlgHom s) (f + g) ∈ R[(toContinuousMapOnAlgHom s) X]

pp: case refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
n : ℕ
r : R
hn : (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ n) ∈ R[(toContinuousMapOnAlgHom s) X]
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ (n + 1)) ∈ R[(toContinuousMapOnAlgHom s) X]

Tactic:
· rw [map_add]
    exact add_mem hf hg

Goal state after:
case refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
n : ℕ
r : R
hn : (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ n) ∈ R[(toContinuousMapOnAlgHom s) X]
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ (n + 1)) ∈ R[(toContinuousMapOnAlgHom s) X]
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set R
φ ψ : C(↑s, R) →ₐ[R] A
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ polynomialFunctions s ≤ φ.equalizer ψ

Tactic:
rw [polynomialFunctions.eq_adjoin_X s]
  exact φ.adjoin_le_equalizer ψ fun x hx => (Set.mem_singleton_iff.1 hx).symm ▸ h

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

Goal state before:
pp: case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : (polynomialFunctions I).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
apply_fun fun s => s.comap W at p

Goal state after:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : Subalgebra.comap W (polynomialFunctions I).topologicalClosure = Subalgebra.comap W ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ 2⁻¹ • (↑f + ↑g + |↑g - ↑f|) ∈ A.topologicalClosure

Tactic:
refine
    A.topologicalClosure.smul_mem
      (A.topologicalClosure.add_mem
        (A.topologicalClosure.add_mem (A.le_topologicalClosure f.property)
          (A.le_topologicalClosure g.property))
        ?_)
      _

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ |↑g - ↑f| ∈ A.topologicalClosure
Module: Mathlib.Analysis.Real.Spectrum

Goal state before:
pp: A : Type u_1
inst✝³ : NonUnitalRing A
inst✝² : Module ℝ A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : SMulCommClass ℝ A A
a : A
⊢ SpectrumRestricts ↑a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ σₙ ℝ a, 0 ≤ x

Tactic:
Unitization.quasispectrum_eq_spectrum_inr' _ ℝ,

Goal state after:
A : Type u_1
inst✝³ : NonUnitalRing A
inst✝² : Module ℝ A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : SMulCommClass ℝ A A
a : A
⊢ SpectrumRestricts ↑a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ spectrum ℝ ↑a, 0 ≤ x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
inst✝ : TopologicalSpace β
⊢ UpperHemicontinuousOn f s ↔ ∀ x ∈ s, ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝[s] x

Tactic:
by
  simp [upperHemicontinuousOn_iff, upperHemicontinuousWithinAt_iff_preimage_Iic]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
ι : Type u_5
inst✝ : RegularSpace β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst✝¹] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
this✝ : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
this : ∃ᶠ (n : ι) in l, y n ∈ s
⊢ False

Tactic:
apply this

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
ι : Type u_5
inst✝ : RegularSpace β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst✝¹] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
this✝ : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
this : ∃ᶠ (n : ι) in l, y n ∈ s
⊢ ∀ᶠ (x : ι) in l, ¬(fun n ↦ y n ∈ s) x
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}
hs : s ∈ ⋂₀ (powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v)
U : Set α := ⋂₀ u
hU : IsOpen[inst✝] U
⊢ ∃ 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} ⊆ ⋂₀ (powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v)

Tactic:
sInter_union,

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 ∈ ⋂₀ (powerset '' u) ∩ ⋂₀ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' 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} ⊆ ⋂₀ (powerset '' u) ∩ ⋂₀ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' v)
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
h : ∀ (x : ℕ → α), Tendsto x atTop (𝓝 x₀) → ∀ y₀ ∈ f x₀, ∃ y, (∀ (n : ℕ), y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)
⊢ LowerHemicontinuousAt f x₀

Tactic:
by
  rw [lowerHemicontinuousAt_iff]
  intro U hU ⟨y₀, hy₀f, hy₀U⟩
  by_contra hc
  rw [Filter.not_eventually] at hc
  obtain ⟨x, hx, hxU⟩ := exists_seq_forall_of_frequently hc
  obtain ⟨y, hy_mem, hy_lim⟩ := h x hx y₀ hy₀f
  obtain ⟨n, hn⟩ := (hy_lim.eventually (hU.mem_nhds hy₀U)).exists
  exact hxU n ⟨y n, hy_mem n, hn⟩

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
hf : LowerHemicontinuousAt f x₀
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y₀ : β
hy₀ : y₀ ∈ f x₀
inst✝ : (𝓝 y₀).IsCountablyGenerated
U : ℕ → Set β
hU : ∀ (i : ℕ), y₀ ∈ U i ∧ IsOpen[inst✝¹] (U i)
hUbasis : (𝓝 y₀).HasAntitoneBasis fun i ↦ U i
hev : ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, (f (x n) ∩ U k).Nonempty
g : ℕ → ℕ := fun n ↦ Nat.findGreatest (fun k ↦ (f (x n) ∩ U k).Nonempty) n
key : ∀ (n k : ℕ), k ≤ n → (f (x n) ∩ U k).Nonempty → (f (x n) ∩ U (g n)).Nonempty
y : ℕ → β := fun n ↦ if h : (f (x n) ∩ U (g n)).Nonempty then h.some else y₀
hy : ∀ (n : ℕ), (f (x n) ∩ U (g n)).Nonempty → y n ∈ f (x n) ∩ U (g n)
k : ℕ
a✝ : True
n : ℕ
hk : (f (x n) ∩ U k).Nonempty
hkn : k ≤ n
⊢ y n ∈ U k

Tactic:
exact hUbasis.antitone (Nat.le_findGreatest hkn hk) (hy n (key n k hkn hk)).2

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)‖.toNNReal * r ^ n ≤ max 1 ‖1‖₊

Tactic:
norm_mkPiRing,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a ^ n‖.toNNReal * r ^ n ≤ max 1 ‖1‖₊
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑ψ

Tactic:
rw [isometry_inr (𝕜 := 𝕜) |>.isEmbedding.continuous_iff]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
⊢ Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (Unitization.inr ∘ ⇑ψ)
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
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ ‖x‖₊ ≤ t

Tactic:
← ENNReal.coe_le_coe

Goal state after:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ ↑‖x‖₊ ≤ ↑t
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 ..]
  refine cfc_congr fun x hx ↦ ?_
  simp_rw [RCLike.star_def, RCLike.conj_eq_iff_re, RCLike.re_eq_complex_re,
    RCLike.ofReal_eq_complex_ofReal] at hf_real
  rw [← SpectrumRestricts.real_iff.mp ha.spectrumRestricts _ hx, hf_real _ hx]

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
⊢ (spectralRadius ℂ (a * a⋆)).toReal = ‖a⋆‖ ^ 2

Tactic:
← toReal_spectralRadius_star_mul_self_eq_norm_sq,

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
⊢ (spectralRadius ℂ (a * a⋆)).toReal = (spectralRadius ℂ (a⋆⋆ * a⋆)).toReal
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
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ ∀ (x : ↑(σ 𝕜 a)), ‖((↑f).comp ι) x‖ ≤ ‖↑f‖

Tactic:
rintro ⟨x, hx⟩

Goal state after:
𝕜 : 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
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
x : 𝕜
hx : x ∈ σ 𝕜 a
⊢ ‖((↑f).comp ι) ⟨x, hx⟩‖ ≤ ‖↑f‖
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
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ ∀ (x : ↑(σₙ 𝕜 a)), ‖↑f x‖ ≤ ‖(↑f).comp ι‖

Tactic:
rintro ⟨x, hx⟩

Goal state after:
𝕜 : 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
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
x : 𝕜
hx : x ∈ σₙ 𝕜 a
⊢ ‖↑f ⟨x, hx⟩‖ ≤ ‖(↑f).comp ι‖
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
h : CompactSpace (Compacts α)
⊢ ∀ (x : α), ∃ i, x ∈ ↑i

Tactic:
exact fun x => ⟨{x}, Set.mem_singleton x⟩

Goal state after: