mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst✝ : IsProbabilityMeasure μ
hint : ∫⁻ (a : α), f a ∂μ ≠ ∞
hN : μ N = 0
⊢ ∃ x ∉ N, ∫⁻ (a : α), f a ∂μ ≤ f x

Tactic:
simpa only [laverage_eq_lintegral] using
    exists_notMem_null_laverage_le (IsProbabilityMeasure.ne_zero μ) hint hN

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ≤ μ

Tactic:
by_cases hl : HaveLebesgueDecomposition μ ν
  · conv_rhs => rw [haveLebesgueDecomposition_add μ ν]
    exact Measure.le_add_right le_rfl
  · rw [singularPart, dif_neg hl]
    exact Measure.zero_le μ

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
⊢ s = μ.singularPart ν

Tactic:
have heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ := by
    ext1 A hA
    have hf : ν.withDensity f (A ∩ (S ∩ T)ᶜ) = 0 := by
      refine withDensity_absolutelyContinuous ν _ ?_
      rw [← nonpos_iff_eq_zero]
      exact hνinter ▸ measure_mono inter_subset_right
    have hrn : ν.withDensity (μ.rnDeriv ν) (A ∩ (S ∩ T)ᶜ) = 0 := by
      refine withDensity_absolutelyContinuous ν _ ?_
      rw [← nonpos_iff_eq_zero]
      exact hνinter ▸ measure_mono inter_subset_right
    rw [restrict_apply hA, restrict_apply hA, ← add_zero (s (A ∩ (S ∩ T)ᶜ)), ← hf, ← add_apply, ←
      hadd, add_apply, hrn, add_zero]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
⊢ s = μ.singularPart ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ (μ.restrict s).rnDeriv ν =ᵐ[ν] s.indicator (μ.rnDeriv ν)

Tactic:
refine (eq_rnDeriv (s := (μ.restrict s).singularPart ν)
    ((measurable_rnDeriv _ _).indicator hs) (mutuallySingular_singularPart _ _) ?_).symm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ μ.restrict s = (μ.restrict s).singularPart ν + ν.withDensity (s.indicator (μ.rnDeriv ν))
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ≥0
h : ∀ (x : α), ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧ ∃ r, a ⊆ closedBall x r ∧ μ (closedBall x (3 * r)) ≤ ↑C * μ a}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      μ (closedBall p.2.1 (3 * p.1)) ≤ ↑C * μ p.2.2 ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
t' : Set (ℝ × α × Set α)
t't : t' ⊆ t
left✝ : t'.Countable
t'_disj : t'.PairwiseDisjoint fun p ↦ p.2.2
μt' : μ (s \ ⋃ a ∈ t', a.2.2) = 0
q : ℝ × α × Set α
hq : q ∈ t'
⊢ ((fun p ↦ p.2) q).1 ∈ s

Tactic:
exact (t't hq).2.2.2.2.2

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 : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : N = 0
⊢ ∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)) ≤
    ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j))

Tactic:
rw [Finset.range_eq_Ico]
        gcongr
        exact zero_le_one

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 : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : N = 0
⊢ ∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)) ≤
    ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j))

Tactic:
by
        rw [Finset.range_eq_Ico]
        gcongr
        exact zero_le_one

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 α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ ∀ (i : ℕ), 0 < i → i < n → E i ∈ s

Tactic:
intros; apply hn <;> omega

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case e_a
α : 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 μ
I : Integrable (AEStronglyMeasurable.mk f ⋯) μ
x : α
hx :
  Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ) / μ a)
    (v.filterAt x) (𝓝 0)
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
a : Set α
⊢ ∀ᵐ (x_1 : α) ∂μ,
    (fun a ↦ ‖AEStronglyMeasurable.mk f ⋯ a - AEStronglyMeasurable.mk f ⋯ x‖ₑ) x_1 = (fun a ↦ ‖f a - f x‖ₑ) x_1

Tactic:
filter_upwards [hf.1.ae_eq_mk] with y hy

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 μ
I : Integrable (AEStronglyMeasurable.mk f ⋯) μ
x : α
hx :
  Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ) / μ a)
    (v.filterAt x) (𝓝 0)
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
a : Set α
y : α
hy : f y = AEStronglyMeasurable.mk f ⋯ y
⊢ ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ = ‖f y - 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
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
ha : IsBot a
x : α
⊢ x ∈ Iic a ↔ x ∈ {a}

Tactic:
grind [ha x]

Goal state after:
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

Goal state after:
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
this : ContinuousFunctionalCalculus R A p
⊢ IsClosedEmbedding ⇑(cfcHom ha)
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
S : Type u_3
inst✝⁴ : SMul S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f ((fun x ↦ s • x) '' spectrum R a)
ha : p a
⊢ cfc (fun x ↦ f (s • x)) a = cfc f (s • a)

Tactic:
by
  rw [cfc_comp' .., cfc_smul_id ..]

Goal state after:
Module: Mathlib.Topology.Algebra.StarSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Semiring A
inst✝¹² : StarRing A
inst✝¹¹ : IsSemitopologicalSemiring A
inst✝¹⁰ : ContinuousStar A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : StarRing B
inst✝⁴ : Algebra R B
inst✝³ : T2Space B
F : Type u_4
a : A
inst✝² : FunLike F (↥(elemental R a)) B
inst✝¹ : AlgHomClass F R (↥(elemental R a)) B
inst✝ : StarHomClass F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst✝⁷] ⇑φ
hψ : Continuous[instTopologicalSpaceSubtype, inst✝⁷] ⇑ψ
h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
x✝ x y : ↥(adjoin R {a})
hx : φ ((inclusion ⋯) x) = ψ ((inclusion ⋯) x)
hy : φ ((inclusion ⋯) y) = ψ ((inclusion ⋯) y)
⊢ φ ((inclusion ⋯) (x * y)) = ψ ((inclusion ⋯) (x * y))

Tactic:
simp only [map_mul, hx, hy]

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✝¹⁹ : CommRing R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalRing R
inst✝¹³ : ContinuousStar R
inst✝¹² : ContinuousSqrt R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NoZeroDivisors R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ cfcₙ f a ≤ 0 ↔ ∀ x ∈ σₙ R a, f x ≤ 0

Tactic:
by
  simp_rw [← neg_nonneg, ← cfcₙ_neg]
  exact cfcₙ_nonneg_iff (fun x ↦ -f x) a

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
⊢ Continuous toNNReal

Tactic:
by
  rw [continuous_induced_rng]
  convert_to! Continuous (ContinuousMap.toNNReal ∘ ((↑) : C(X, ℝ)₀ → C(X, ℝ))) using 1
  exact ContinuousMap.continuous_postcomp _ |>.comp continuous_induced_dom

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
⊢ LowerHemicontinuous f ↔ ∀ (u : Set β), IsOpen[inst✝] u → IsOpen[inst✝¹] {x | (f x ∩ u).Nonempty}

Tactic:
simp_rw [lowerHemicontinuous_iff, lowerHemicontinuousAt_iff, isOpen_iff_mem_nhds,
    forall_comm (α := α), mem_ofPred, Filter.Eventually]

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
t : Set α
ht : IsOpen[inst✝] t
hne : ((fun x ↦ {x}) x ∩ t).Nonempty
x' : α
⊢ x' ∈ t → IsOpen[inst✝] t ∧ ({x'} ∩ t).Nonempty

Tactic:
hx'

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
t : Set α
ht : IsOpen[inst✝] t
hne : ((fun x ↦ {x}) x ∩ t).Nonempty
x' : α
hx' : x' ∈ t
⊢ IsOpen[inst✝] t ∧ ({x'} ∩ t).Nonempty
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
t : Set α
ht : IsOpen[inst✝] t
hne : ((fun x ↦ {x}) x ∩ t).Nonempty
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x t ↦ IsOpen[inst✝] t ∧ ((fun x ↦ {x}) x ∩ t).Nonempty) x' t

Tactic:
filter_upwards [ht.mem_nhds (Set.singleton_inter_nonempty.mp hne)] with x' hx'

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
t : Set α
ht : IsOpen[inst✝] t
hne : ((fun x ↦ {x}) x ∩ t).Nonempty
x' : α
hx' : x' ∈ t
⊢ IsOpen[inst✝] t ∧ ({x'} ∩ t).Nonempty
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝¹³ : NormedField 𝕜
inst✝¹² : NormedRing A
inst✝¹¹ : NormedAlgebra 𝕜 A
inst✝¹⁰ : CompleteSpace A
B : Type u_3
inst✝⁹ : NonUnitalNormedRing B
inst✝⁸ : NormedSpace 𝕜 B
inst✝⁷ : CompleteSpace B
inst✝⁶ : IsScalarTower 𝕜 B B
inst✝⁵ : SMulCommClass 𝕜 B B
inst✝⁴ : ProperSpace 𝕜
inst✝³ : NormedSpace ℝ B
inst✝² : IsScalarTower ℝ B B
inst✝¹ : SMulCommClass ℝ B B
a : B
inst✝ : CompactSpace ↑(quasispectrum ℝ a)
⊢ CompactSpace ↑(quasispectrum ℝ≥0 a)

Tactic:
rw [← isCompact_iff_compactSpace] at *
  rw [← quasispectrum.preimage_algebraMap ℝ]
  exact isClosed_nonneg.isClosedEmbedding_subtypeVal.isCompact_preimage <| by assumption

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
a : A
ha : (σ a).Nonempty
k : 𝕜
hk : k ∈ σ a
h : IsMaxOn (fun a ↦ ‖a‖₊) (σ a) k
⊢ ∃ k ∈ σ a, ↑‖k‖₊ = spectralRadius 𝕜 a

Tactic:
exact ⟨k, hk, le_antisymm (le_iSup₂ (α := ℝ≥0∞) k hk) (iSup₂_le <| mod_cast h)⟩

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n ↦ (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
⊢ exp z ∈ spectrum 𝕜 (exp a)

Tactic:
have h₀ : (∑' n : ℕ, ((n + 1).factorial⁻¹ : 𝕜) • (a - ↑ₐ z) ^ (n + 1)) = (a - ↑ₐ z) * b := by
    simpa only [mul_smul_comm, pow_succ'] using hb.tsum_mul_left (a - ↑ₐ z)

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n ↦ (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
⊢ exp z ∈ spectrum 𝕜 (exp a)
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
a : A
ha : p a
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ :
  (cfcₙAux ⋯ a ha) f ∈
    closure[Unitization.instUniformSpace.toTopologicalSpace]
      (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id (σₙ 𝕜 a)}))
⊢ (cfcₙAux ⋯ a ha) f ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)

Tactic:
rw [← SetLike.mem_coe]

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
a : A
ha : p a
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ :
  (cfcₙAux ⋯ a ha) f ∈
    closure[Unitization.instUniformSpace.toTopologicalSpace]
      (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id (σₙ 𝕜 a)}))
⊢ (cfcₙAux ⋯ a ha) f ∈ ↑(NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A))
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

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✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
⊢ Isometry ⇑(cfcHom ha)

Tactic:
have := SpectrumRestricts.cfc f halg.isClosedEmbedding h0 h

Goal state after:
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✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
this : ContinuousFunctionalCalculus R A p
⊢ Isometry ⇑(cfcHom ha)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x ≤ c
⊢ ‖cfcₙ f a‖₊ ≤ c

Tactic:
by
  refine cfcₙ_cases (‖·‖₊ ≤ c) a f (by simp) fun hf hf0 ha ↦ ?_
  simp only [← cfcₙ_apply f a, isLUB_le_iff (IsGreatest.nnnorm_cfcₙ_nnreal f a hf hf0 ha |>.isLUB)]
  rintro - ⟨x, hx, rfl⟩
  exact h x hx

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✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
U : Set (Compacts α)
hU :
  U ∈
    (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}}
this : IsPreconnected (U ∩ {K | (↑K).Finite})
⊢ IsPreconnected U

Tactic:
refine this.subset_closure inter_subset_left ?_
    grw [← (basis.isOpen hU).inter_closure, dense_setOfPred_finite.closure_eq, inter_univ]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
key : ∀ (z : ℂ), x * NormedSpace.exp (z • star a) = NormedSpace.exp (z • star b) * x
⊢ SemiconjBy x (star a) (star b)

Tactic:
by
    have (a : A) : HasDerivAt (fun z : ℂ ↦ exp (z • a)) a 0 := by
      simpa using hasDerivAt_exp_smul_const a (0 : ℂ)
    apply (this (star a)).const_mul x |>.unique
    simpa [key] using (this (star b)).mul_const x

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
⊢ B.polar Set.univ = {0}

Tactic:
rw [Set.eq_singleton_iff_unique_mem]
  refine ⟨by simp only [zero_mem_polar], fun y hy => h _ fun x => ?_⟩
  refine norm_le_zero_iff.mp (le_of_forall_gt_imp_ge_of_dense fun ε hε => ?_)
  rcases NormedField.exists_norm_lt 𝕜 hε with ⟨c, hc, hcε⟩
  calc
    ‖B x y‖ = ‖c‖ * ‖B (c⁻¹ • x) y‖ := by
      rw [B.map_smul, LinearMap.smul_apply, smul_eq_mul, norm_mul, norm_inv,
        mul_inv_cancel_left₀ hc.ne']
    _ ≤ ε * 1 := by gcongr; exact hy _ trivial
    _ = ε := mul_one _

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
⊢ x' ∈ polar 𝕜 (ball 0 r) → x' ∈ closedBall 0 (‖c‖ / r)

Tactic:
hx'

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
hx' : x' ∈ polar 𝕜 (ball 0 r)
⊢ x' ∈ closedBall 0 (‖c‖ / r)
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:
by
  conv_rhs => rw [← inv_inv r]
  rw [← polar_closedBall (inv_pos_of_pos hr), StrongDual.polar,
    (topDualPairing 𝕜 E).flip.sInter_polar_finite_subset_eq_polar (closedBall (0 : E) r⁻¹)]

Goal state after: