mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K} :=
  μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x ↦ c) x‖ₑ)
x : α
hx :
  ∀ (n : ℕ),
    ∀ c ∈ t,
      Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
        (𝓝 ‖f x - (A.set n).indicator (fun x ↦ c) x‖ₑ)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
M : ∀ c ∈ t, Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)
⊢ Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)

Tactic:
apply ENNReal.tendsto_nhds_zero.2 fun ε εpos => ?_

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K} :=
  μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x ↦ c) x‖ₑ)
x : α
hx :
  ∀ (n : ℕ),
    ∀ c ∈ t,
      Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
        (𝓝 ‖f x - (A.set n).indicator (fun x ↦ c) x‖ₑ)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
M : ∀ c ∈ t, Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∀ᶠ (x_1 : Set α) in v.filterAt x, (∫⁻ (y : α) in x_1, ‖f y - f x‖ₑ ∂μ) / μ x_1 ≤ ε
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 α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ < ε
H : ∃ᶠ (x : α) in L, ε ≤ eVariationOn f (s ∩ Ici x)
y : α → α
y_mem : ∀ y_1 ∈ s, y y_1 ∈ s ∩ Ici y_1
le_y : ∀ y_1 ∈ s, δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : ℕ → α := fun n ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
J : ∀ (n : ℕ), ↑n * δ ≤ eVariationOn f s
this : Tendsto (fun n ↦ ↑n * δ) atTop (𝓝 (∞ * δ))
⊢ False

Tactic:
ENNReal.top_mul δpos.ne'

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ < ε
H : ∃ᶠ (x : α) in L, ε ≤ eVariationOn f (s ∩ Ici x)
y : α → α
y_mem : ∀ y_1 ∈ s, y y_1 ∈ s ∩ Ici y_1
le_y : ∀ y_1 ∈ s, δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : ℕ → α := fun n ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
J : ∀ (n : ℕ), ↑n * δ ≤ eVariationOn f s
this : Tendsto (fun n ↦ ↑n * δ) atTop (𝓝 ∞)
⊢ False
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✝¹⁶ : Semifield S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalSemiring S
inst✝¹² : ContinuousStar S
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus S A q
inst✝¹ : ContinuousMap.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 ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
⊢ IsClosedEmbedding ⇑(cfcHom ha)

Tactic:
have := SpectrumRestricts.cfc f halg.isClosedEmbedding h0 h
    rw [cfcHom_eq_restrict f ha ((h a).mp ha).1 ((h a).mp ha).2]
    exact isClosedEmbedding_starAlgHom (cfcHom_isClosedEmbedding ((h a).mp ha).1)
      ((h a).mp ha).2 halg

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

Goal state before:
pp: case h'f
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
H : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x) + edist (f x) l) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))
y : α
hy : y ∈ s ∩ Iio x
N : 𝓝[s ∩ Ici y ∩ Iio x] x = 𝓝[s ∩ Iio x] x
⊢ Tendsto f (𝓝[s ∩ Ici y ∩ Iio x] x) (𝓝 l)

Tactic:
· convert h'f

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
f : R → R
a : A
inst✝ : UniqueHom R A
hf : ContinuousOn f (star '' σₙ R a)
hf0 : f 0 = 0
ha : p a
⊢ cfcₙ (fun x ↦ f (star x)) a = cfcₙ f (star a)

Tactic:
cfcₙ_comp' f star a,

Goal state after:
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
inst✝ : UniqueHom R A
hf : ContinuousOn f (star '' σₙ R a)
hf0 : f 0 = 0
ha : p a
⊢ cfcₙ f (cfcₙ star a) = cfcₙ f (star a)
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: a b : ℝ
h : a < b
⊢ Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I) =
    polynomialFunctions (Set.Icc a b)

Tactic:
ext f
  fconstructor
  · rintro ⟨p, ⟨-, w⟩⟩
    rw [DFunLike.ext_iff] at w
    dsimp at w
    let q := p.comp ((b - a)⁻¹ • Polynomial.X + Polynomial.C (-a * (b - a)⁻¹))
    refine ⟨q, ⟨?_, ?_⟩⟩
    · simp
    · ext x
      simp only [q, neg_mul, map_neg, map_mul, AlgHom.coe_toRingHom,
        Polynomial.eval_X, Polynomial.eval_neg, Polynomial.eval_C, Polynomial.eval_smul,
        smul_eq_mul, Polynomial.eval_mul, Polynomial.eval_add,
        Polynomial.eval_comp, Polynomial.toContinuousMapOnAlgHom_apply,
        Polynomial.toContinuousMapOn_apply, Polynomial.toContinuousMap_apply]
      convert! w ⟨_, _⟩
      · ext
        simp only [iccHomeoI_symm_apply_coe]
        replace h : b - a ≠ 0 := sub_ne_zero_of_ne h.ne.symm
        field
      · rw [mul_comm (b - a)⁻¹, ← neg_mul, ← add_mul, ← sub_eq_add_neg]
        have w₁ : 0 < (b - a)⁻¹ := inv_pos.mpr (sub_pos.mpr h)
        have w₂ : 0 ≤ (x : ℝ) - a := sub_nonneg.mpr x.2.1
        have w₃ : (x : ℝ) - a ≤ b - a := sub_le_sub_right x.2.2 a
        fconstructor
        · exact mul_nonneg w₂ (le_of_lt w₁)
        · rw [← div_eq_mul_inv, div_le_one (sub_pos.mpr h)]
          exact w₃
  · rintro ⟨p, ⟨-, rfl⟩⟩
    let q := p.comp ((b - a) • Polynomial.X + Polynomial.C a)
    refine ⟨q, ⟨?_, ?_⟩⟩
    · simp
    · ext x
      simp [q, mul_comm]

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
f✝ g : R → R
a✝ : A
hf : ContinuousOn f✝ (σₙ R a✝)
hf0 : f✝ 0 = 0
hg : ContinuousOn g (σₙ R a✝)
hg0 : g 0 = 0
ha : p a✝
f : R → R
a : A
x✝² : ContinuousOn f (σₙ R a)
x✝¹ : { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
x✝ : p a
⊢ cfcₙ (fun x ↦ star (f x) * f x) a = cfcₙ f a * cfcₙ (fun x ↦ star (f x)) a

Tactic:
← cfcₙ_mul ..

Goal state after:
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
hf : ContinuousOn f✝ (σₙ R a✝)
hf0 : f✝ 0 = 0
hg : ContinuousOn g (σₙ R a✝)
hg0 : g 0 = 0
ha : p a✝
f : R → R
a : A
x✝² : ContinuousOn f (σₙ R a)
x✝¹ : { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
x✝ : p a
⊢ cfcₙ (fun x ↦ star (f x) * f x) a = cfcₙ (fun x ↦ f x * star (f x)) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case mp
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)₀
x : R
⊢ x ∈ range ⇑((compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }) (toContinuousMapHom f)) ∪ {0} →
    x ∈ range ⇑f

Tactic:
rintro (⟨x, rfl⟩ | rfl)
    · exact ⟨⟨x.1, spectrum_subset_quasispectrum R a x.2⟩, rfl⟩
    · exact ⟨0, map_zero f⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).topologicalClosure
frequently_mem_polynomials :
  ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).toSubsemiring
⊢ p.comp (↑f).attachBound ∈ A.topologicalClosure

Tactic:
apply mem_closure_iff_frequently.mpr

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).topologicalClosure
frequently_mem_polynomials :
  ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).toSubsemiring
⊢ ∃ᶠ (x : C(X, ℝ)) in nhds (p.comp (↑f).attachBound), x ∈ ↑A.toSubsemiring
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
⊢ UpperHemicontinuous f ↔ ∀ (x : Set β), IsOpen[inst✝] x → IsOpen[inst✝¹] (f ⁻¹' Iic x)

Tactic:
exact upperHemicontinuous_iff_isOpen_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 β
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₀
n : ℕ
h : (f (x n) ∩ U (g n)).Nonempty
⊢ y n ∈ f (x n) ∩ U (g n)

Tactic:
simpa only [y, dif_pos h] using h.some_mem

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ ⦃x : Set α × Set (Set α)⦄,
    x ∈ {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} →
      IsOpen[TopologicalSpace.vietoris α] {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty}

pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ ⦃x : Set (Set α)⦄,
    x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U} →
      ∀ x_1 ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty},
        ∃
          v ∈
            (fun p ↦ {s | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
              {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1},
          x_1 ∈ v ∧ v ⊆ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty}

Tactic:
· intro ⟨V, u⟩ ⟨hV, hu, huB, _⟩
    simp_rw [ofPred_and, ofPred_forall]
    exact hV.powerset_vietoris.inter <|
      hu.isOpen_biInter fun V hV => isOpen_inter_nonempty_of_isOpen <| hB.isOpen <| huB hV

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ ⦃x : Set (Set α)⦄,
    x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U} →
      ∀ x_1 ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty},
        ∃
          v ∈
            (fun p ↦ {s | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
              {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1},
          x_1 ∈ v ∧ v ⊆ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty}
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
U : Set α
hU : IsOpen[inst✝.toTopologicalSpace] U
⊢ IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {s | (s ∩ U).Nonempty}

Tactic:
by
  rw [isOpen_iff_mem_nhds]
  intro s ⟨x, hx₁, hx₂⟩
  rw [← hU.mem_nhds_iff, mem_nhds_iff] at hx₂
  obtain ⟨V, hV, hVU⟩ := hx₂
  rw [mem_nhds_iff]
  refine ⟨_, Filter.mem_lift' hV, ?_⟩
  rintro s' ⟨hs', -⟩
  obtain ⟨y, hy, hxy⟩ := hs' hx₁
  exact ⟨y, hy, hVU hxy⟩

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case right
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ : (s, t) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
⊢ closure[inst✝.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst✝.toTopologicalSpace] s)

Tactic:
· grw [closure_subset_image hV t, hts, ← subset_closure, ← hVU, SetRel.image_comp]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case left
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ :
  (s, t) ∈
    (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹' hausdorffEntourage V
hst : closure[inst✝.toTopologicalSpace] s ⊆ V.preimage (closure[inst✝.toTopologicalSpace] t)
hts : closure[inst✝.toTopologicalSpace] t ⊆ V.image (closure[inst✝.toTopologicalSpace] s)
⊢ s ⊆ SetRel.preimage U t

Tactic:
grw [subset_closure (s := s), hst, closure_subset_preimage hV t, ← hVU, SetRel.preimage_comp]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformly F f l
hF : ∀ (n : ι), LowerHemicontinuous (F n)
⊢ LowerHemicontinuous f

Tactic:
rw [← lowerHemicontinuousOn_univ_iff]
  exact htendsto.tendstoUniformlyOn.lowerHemicontinuousOn (fun n ↦ (hF n).lowerHemicontinuousOn _)

Goal state after:
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
  obtain ⟨x, hx⟩ := ContinuousFunctionalCalculus.isCompact_spectrum a
    |>.image_of_continuousOn hf.norm |>.exists_isGreatest <|
    (ContinuousFunctionalCalculus.spectrum_nonempty a ha).image _
  obtain ⟨x, hx', rfl⟩ := hx.1
  convert! hx
  rw [cfc_apply f a, norm_cfcHom a _]
  apply le_antisymm
  · apply ContinuousMap.norm_le _ (norm_nonneg _) |>.mpr
    rintro ⟨y, hy⟩
    exact hx.2 ⟨y, hy, rfl⟩
  · exact le_trans (by simp) <| ContinuousMap.norm_coe_le_norm _ (⟨x, hx'⟩ : σ 𝕜 a)

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

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts a ⇑Complex.reCLM
x : ℂ
hx : x ∈ σₙ ℂ a
⊢ star x = id x

Tactic:
obtain ⟨x, -, rfl⟩ := ha₂.algebraMap_image.symm ▸ hx

Goal state after:
case refine_2
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts a ⇑Complex.reCLM
x : ℝ
hx : (algebraMap ℝ ℂ) x ∈ σₙ ℂ a
⊢ star ((algebraMap ℝ ℂ) x) = id ((algebraMap ℝ ℂ) x)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: case right.right
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module ℝ A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ cfcₙ (fun x ↦ √x) a * cfcₙ (fun x ↦ √x) a = a

Tactic:
← cfcₙ_mul ..

Goal state after:
case right.right
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module ℝ A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ cfcₙ (fun x ↦ √x * √x) a = a
Module: Mathlib.Analysis.Complex.Convex

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

Tactic:
by simpa only [closure_setOfPred_im_lt] using hs₂

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

Goal state before:
pp: case e'_3
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
x : ℝ
u : ↥(unitary A) := ⟨NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a), ⋯⟩
x✝ : (x : A) → Invertible (NormedSpace.exp x) := invertibleExp
⊢ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a)) *
      (NormedSpace.exp (x • a) * NormedSpace.exp (-(x • star a))) =
    1

Tactic:
mul_assoc

Goal state after:
case e'_3
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
x : ℝ
u : ↥(unitary A) := ⟨NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a), ⋯⟩
x✝ : (x : A) → Invertible (NormedSpace.exp x) := invertibleExp
⊢ NormedSpace.exp (x • star a) *
      (NormedSpace.exp (-(x • a)) * (NormedSpace.exp (x • a) * NormedSpace.exp (-(x • star a)))) =
    1
Module: Mathlib.Analysis.Normed.Module.HahnBanach

Goal state before:
pp: 𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : ‖x‖ = 0
⊢ 0 x = ↑‖x‖

Tactic:
by simp [hx]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.HahnBanach

Goal state before:
pp: 𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : ‖y‖ ≠ 0
g : StrongDual 𝕜 E
hg : ‖g‖ = 1 ∧ g y = ↑‖y‖
⊢ g x = ↑‖x‖

Tactic:
by simp [hx]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ ⋂₀ (polar 𝕜 '' {F | F.Finite ∧ F ⊆ closedBall 0 r⁻¹}) = closedBall 0 r⁻¹⁻¹

Tactic:
← polar_closedBall (inv_pos_of_pos hr),

Goal state after:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ ⋂₀ (polar 𝕜 '' {F | F.Finite ∧ F ⊆ closedBall 0 r⁻¹}) = polar 𝕜 (closedBall 0 r⁻¹)
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < (1 - r) * (b - a)
⊢ f ((lineMap b a) (1 - r)) ≤ (lineMap (f b) (f a)) (1 - r) ↔ slope f a b ≤ slope f ((lineMap b a) (1 - r)) b

Tactic:
revert h

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
⊢ 0 < (1 - r) * (b - a) →
    (f ((lineMap b a) (1 - r)) ≤ (lineMap (f b) (f a)) (1 - r) ↔ slope f a b ≤ slope f ((lineMap b a) (1 - r)) b)
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: case empty
A : Type u_1
inst✝ : NonUnitalCommCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
⊢ ‖∑ i ∈ ∅, f i‖₊ = ∅.sup fun x ↦ ‖f x‖₊

Tactic:
| empty =>

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

Goal state before:
pp: case empty
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
h : ∀ i ∈ ∅, IsSelfAdjoint (f i)
⊢ ‖∑ i ∈ ∅, f i‖₊ = ∅.sup fun x ↦ ‖f x‖₊

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric

Goal state before:
pp: case pos.inl
A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
h : x ≤ 0
⊢ ‖x⁺‖ ≤ ‖a‖

Tactic:
simp [posPart_def, max_eq_right h]

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

Goal state before:
pp: case h.right
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ a = ∑ i, I ^ ↑i • ![(↑(realPart a))⁺, (↑(imaginaryPart a))⁺, (↑(realPart a))⁻, (↑(imaginaryPart a))⁻] i

Tactic:
← CStarAlgebra.linear_combination_nonneg a

Goal state after:
case h.right
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ (↑(realPart a))⁺ - (↑(realPart a))⁻ + (I • (↑(imaginaryPart a))⁺ - I • (↑(imaginaryPart a))⁻) =
    ∑ i, I ^ ↑i • ![(↑(realPart a))⁺, (↑(imaginaryPart a))⁺, (↑(realPart a))⁻, (↑(imaginaryPart a))⁻] i