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

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : ¬IsFiniteMeasure ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
rw [not_isFiniteMeasure_iff] at hν

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : ν univ = ∞
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hs₀ : μ s = 0
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hs₀ : ¬μ s = 0
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]

Tactic:
· rw [← ae_eq_empty] at hs₀
    rw [restrict_congr_set (hs₀.union EventuallyEq.rfl), empty_union]
    exact right_mem_segment _ _ _

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hs₀ : ¬μ s = 0
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
⊢ ∃ p, Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2

Tactic:
by
    obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν
    by_cases hr : r = 0
    · exact ⟨⟨μ, 0⟩, measurable_const, by simp [hr], by simp⟩
    refine ⟨⟨μ.singularPart ν, r⁻¹ • μ.rnDeriv ν⟩, hmeas.const_smul _,
      hsing.mono_ac AbsolutelyContinuous.rfl smul_absolutelyContinuous, ?_⟩
    have : r⁻¹ • rnDeriv μ ν = ((r⁻¹ : ℝ≥0) : ℝ≥0∞) • rnDeriv μ ν := by simp [ENNReal.smul_def]
    rw [this, withDensity_smul _ hmeas, ENNReal.smul_def r, withDensity_smul_measure,
      ← smul_assoc, smul_eq_mul, ENNReal.coe_inv hr, ENNReal.inv_mul_cancel, one_smul]
    · exact hadd
    · simp [hr]
    · exact ENNReal.coe_ne_top

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
| μ

Tactic:
haveLebesgueDecomposition_add μ ν

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
| μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}
hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}
f : α → Set (Set α) := fun x ↦ {a | μ a = 0}
x : α
ε : ℝ
εpos : ε > 0
hx : ∀ (ε : ℝ), 0 < ε → ∃ t ∈ v.setsAt x, t ⊆ closedBall x ε ∧ μ t = 0
a : Set α
a_sets : a ∈ v.setsAt x
ax : a ⊆ closedBall x ε
μa : μ a = 0
⊢ ∃ t ∈ v.setsAt x ∩ f x, t ⊆ closedBall x ε

Tactic:
exact ⟨a, ⟨a_sets, μa⟩, ax⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ ν₁ + ν₂ = ν₁.singularPart μ + (ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ)))

Tactic:
add_comm (ν₂.singularPart μ),

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
n : ℕ
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)

Tactic:
specialize hf₃ n (t ∩ A) (ht.inter hAmeas)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
n : ℕ
t : Set α
hf₃ : μ (t ∩ A ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A ∩ (f n)ᶜ)
ht : MeasurableSet t
⊢ μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
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 μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ AEMeasurable (v.limRatio ρ) μ

Tactic:
by
  apply ENNReal.aemeasurable_of_exist_almost_disjoint_supersets _ _ fun p q hpq => ?_
  exact v.exists_measurable_supersets_limRatio hρ hpq

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

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this✝¹ : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ (μ - ν.withDensity ξ) (A ∩ E)
hε₂ : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν ≤ μ (A ∩ E)
hξε : (ξ + E.indicator fun x ↦ ↑ε) ∈ measurableLE ν μ
this✝ : ∫⁻ (a : α), ξ a + E.indicator (fun x ↦ ↑ε) a ∂ν ≤ sSup (measurableLEEval ν μ)
this : (ν.withDensity ξ) univ ≠ ∞
⊢ ∫⁻ (a : α), ξ a ∂ν ≠ ∞

Tactic:
rwa [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ] at this

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
⊢ (eVariationOn (f ∘ φ) (t ∩ Icc x y)).toReal = variationOnFromTo f (φ '' t) (φ x) (φ y)

Tactic:
variationOnFromTo.eq_of_le _ _ (hφ hx hy h),

Goal state after:
case inl
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
⊢ (eVariationOn (f ∘ φ) (t ∩ Icc x y)).toReal = (eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))).toReal
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝² : SigmaFinite ν₁
inst✝¹ : SigmaFinite ν₂
inst✝ : SigmaFinite μ
⊢ ν₁ + ν₂ = ν₁.singularPart μ + (ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ)))

Tactic:
add_comm (ν₂.singularPart μ),

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝² : SigmaFinite ν₁
inst✝¹ : SigmaFinite ν₂
inst✝ : SigmaFinite μ
⊢ ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
L : Filter α
hf : BoundedVariationOn f ∅
hL : ∀ y ∈ ∅, ∅ ∩ Ici y ∈ L
⊢ Tendsto (fun y ↦ eVariationOn f (∅ ∩ Ici y)) L (𝓝 0)

Tactic:
simpa using tendsto_const_nhds

Goal state after:
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 : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
this : Tendsto (ENNReal.toReal ∘ fun a ↦ (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 (ENNReal.toReal 0))
⊢ Tendsto (fun a ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)

Tactic:
simp only [ENNReal.toReal_zero] at this

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 : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
this : Tendsto (ENNReal.toReal ∘ fun a ↦ (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
⊢ Tendsto (fun a ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : 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 : α
A : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
a : α
ha : a ∈ s ∩ Ici x
⊢ 0 = eVariationOn f (s ∩ Ico a x)

Tactic:
simp [show Ico a x = ∅ by grind]

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

Goal state before:
pp: case pos
α : 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
A : Iic a = {a}
B : Iio a = ∅
⊢ eVariationOn f (Iic a) = eVariationOn f (Iio a) + edist (f a) (Function.leftLim f a)

Tactic:
simp [A, B, leftLim_eq_of_isBot ha]

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✝¹⁰ : Semifield 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
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousInv₀ R
f g : R → R
a : A
hg' : ∀ x ∈ spectrum R a, g x ≠ 0
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ cfc (fun x ↦ f x * (g x)⁻¹) a = cfc f a * (cfc g a)⁻¹ʳ

Tactic:
cfc_mul ..,

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✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousInv₀ R
f g : R → R
a : A
hg' : ∀ x ∈ spectrum R a, g x ≠ 0
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ cfc f a * cfc (fun x ↦ (g x)⁻¹) a = cfc f a * (cfc g a)⁻¹ʳ
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
inst✝ : CompleteSpace E
hE : Nonempty E
f : α → E
s : Set α
hf : BoundedVariationOn f s
⊢ ∃ l, Tendsto f (𝓟 s ⊓ atTop) (𝓝 l)

Tactic:
rcases eq_empty_or_nonempty s with rfl | hs

Goal state after:
case inl
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
inst✝ : CompleteSpace E
hE : Nonempty E
f : α → E
hf : BoundedVariationOn f ∅
⊢ ∃ l, Tendsto f (𝓟 ∅ ⊓ atTop) (𝓝 l)

case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
inst✝ : CompleteSpace E
hE : Nonempty E
f : α → E
s : Set α
hf : BoundedVariationOn f s
hs : s.Nonempty
⊢ ∃ l, Tendsto f (𝓟 s ⊓ atTop) (𝓝 l)
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ m ∈ Finset.range (n + 1), X ^ m * (1 - X) ^ (n - m) * ↑(n.choose m)

Tactic:
simp only [bernsteinPolynomial, mul_comm, mul_assoc]

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
inst✝ : ContinuousMapZero.UniqueHom R A
a : A
ha : p a
⊢ (cfcₙHom_of_cfcHom R ha) (ContinuousMapZero.id (σₙ R a)) = a

Tactic:
by
    simpa only [cfcₙHom_id ha] using! cfcHom_id ha

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

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
⊢ ∃ x, dist x f < ε ∧ x ∈ L

Tactic:
have lt_h : ∀ x z, f z - ε < (h x : X → ℝ) z := by
    intro x z
    obtain ⟨y, ym, zm⟩ := Set.exists_set_mem_of_union_eq_top _ _ (ys_w x) z
    dsimp [h]
    simp only [coe_sup', Finset.sup'_apply, Finset.lt_sup'_iff]
    exact ⟨y, ym, zm⟩

Goal state after:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
⊢ ∃ x, dist x f < ε ∧ x ∈ L
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
⊢ A.topologicalClosure = ⊤

Tactic:
rw [StarSubalgebra.eq_top_iff]
  -- Let `I` be the natural inclusion of `C(X, ℝ)` into `C(X, 𝕜)`
  let I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ofRealCLM.compLeftContinuous ℝ X
  -- The main point of the proof is that its range (i.e., every real-valued function) is contained
  -- in the closure of `A`
  have key : I.range ≤ (A.toSubmodule.restrictScalars ℝ).topologicalClosure := by
    -- Let `A₀` be the subalgebra of `C(X, ℝ)` consisting of `A`'s purely real elements; it is the
    -- preimage of `A` under `I`.  In this argument we only need its submodule structure.
    let A₀ : Submodule ℝ C(X, ℝ) := (A.toSubmodule.restrictScalars ℝ).comap I.toLinearMap
    -- By `Subalgebra.SeparatesPoints.rclike_to_real`, this subalgebra also separates points, so
    -- we may apply the real Stone-Weierstrass result to it.
    have SW : A₀.topologicalClosure = ⊤ :=
      haveI := subalgebra_topologicalClosure_eq_top_of_separatesPoints _ hA.rclike_to_real
      congr_arg Subalgebra.toSubmodule this
    rw [← Submodule.map_top, ← SW]
    -- So it suffices to prove that the image under `I` of the closure of `A₀` is contained in the
    -- closure of `A`, which follows by abstract nonsense
    have h₁ := A₀.topologicalClosure_map I
    have h₂ := (A.toSubmodule.restrictScalars ℝ).map_comap_le I.toLinearMap
    exact h₁.trans (Submodule.topologicalClosure_mono h₂)
  -- In particular, for a function `f` in `C(X, 𝕜)`, the real and imaginary parts of `f` are in the
  -- closure of `A`
  intro f
  let f_re : C(X, ℝ) := (⟨RCLike.re, RCLike.reCLM.continuous⟩ : C(𝕜, ℝ)).comp f
  let f_im : C(X, ℝ) := (⟨RCLike.im, RCLike.imCLM.continuous⟩ : C(𝕜, ℝ)).comp f
  have h_f_re : I f_re ∈ A.topologicalClosure := key ⟨f_re, rfl⟩
  have h_f_im : I f_im ∈ A.topologicalClosure := key ⟨f_im, rfl⟩
  -- So `f_re + I • f_im` is in the closure of `A`
  have := A.topologicalClosure.add_mem h_f_re (A.topologicalClosure.smul_mem h_f_im RCLike.I)
  rw [StarSubalgebra.mem_toSubalgebra] at this
  convert! this
  -- And this, of course, is just `f`
  ext
  apply Eq.symm
  simp [I, f_re, f_im, mul_comm RCLike.I _]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
V : Set E
hV : IsOpen (⇑(toWeakSpaceCLM 𝕜 E) '' V)
⊢ IsOpen[inst✝] V

Tactic:
simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁴ : CommSemiring 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✝¹⁵ : Ring B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Algebra R B
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : ContinuousFunctionalCalculus R A p
inst✝⁴ : ContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMap.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst✝¹⁷, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R ↑φ
this✝ : Continuous[inst✝¹⁷, inst✝¹³] ⇑ψ
h_spec : spectrum R (ψ a) ⊆ spectrum R a
hψa : q (ψ a)
ι : C(↑(spectrum R (ψ a)), ↑(spectrum R a)) := { toFun := Set.inclusion h_spec, continuous_toFun := ⋯ }
this : ψ.comp (cfcHom ha) = (cfcHom hψa).comp (ContinuousMap.compStarAlgHom' R R ι)
hf' : ContinuousOn f (spectrum R (ψ a))
⊢ φ ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }) =
    (cfcHom hψa) { toFun := (spectrum R (φ a)).domRestrict f, continuous_toFun := ⋯ }

Tactic:
congrm($(this) ⟨_, hf.domRestrict⟩)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ∀ (u : Set β), IsOpen[inst✝] u → f x ∈ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∈ u
t : Set β
ht : t ∈ 𝓝 (f x)
⊢ ∀ᶠ (x : α) in 𝓝[s] x, f x ∈ t

Tactic:
obtain ⟨u, hut, huo, hux⟩ := mem_nhds_iff.mp ht

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ∀ (u : Set β), IsOpen[inst✝] u → f x ∈ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∈ u
t : Set β
ht : t ∈ 𝓝 (f x)
u : Set β
hut : u ⊆ t
huo : IsOpen[inst✝] u
hux : f x ∈ u
⊢ ∀ᶠ (x : α) in 𝓝[s] x, f x ∈ t
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
U V : SetRel α α
⊢ hausdorffEntourage (U ○ V) = hausdorffEntourage U ○ hausdorffEntourage V

Tactic:
by
  apply subset_antisymm
  · intro ⟨s, t⟩ ⟨hst, hts⟩
    simp only [mem_comp, mem_hausdorffEntourage] at *
    refine ⟨U.image s ∩ V.preimage t, ⟨?_, Set.inter_subset_left⟩, ⟨Set.inter_subset_right, ?_⟩⟩
    · intro x hx
      obtain ⟨z, hz, y, hxy, hyz⟩ := hst hx
      exact ⟨y, ⟨⟨x, hx, hxy⟩, ⟨z, hz, hyz⟩⟩, hxy⟩
    · intro z hz
      obtain ⟨x, hx, y, hxy, hyz⟩ := hts hz
      exact ⟨y, ⟨⟨x, hx, hxy⟩, ⟨z, hz, hyz⟩⟩, hyz⟩
  · intro ⟨s₁, s₃⟩ ⟨s₂, ⟨h₁₂, h₂₁⟩, ⟨h₂₃, h₃₂⟩⟩
    simp only at *
    grw [mem_hausdorffEntourage, preimage_comp, ← h₂₃, ← h₁₂, image_comp, ← h₂₁, ← h₃₂]
    exact ⟨subset_rfl, subset_rfl⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
⊢ s ⤳ t

Tactic:
simp_rw [Specializes, nhds_generateFrom, le_iInf₂_iff]

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
⊢ ∀ i ∈ {s | t ∈ s ∧ s ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}},
    ⨅
        s_1 ∈
          {s_2 |
            s ∈ s_2 ∧
              s_2 ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}},
        Filter.principal s_1 ≤
      Filter.principal i
Module: Mathlib.Analysis.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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
⊢ ‖cfc f a‖ < c

Tactic:
by
  obtain (_ | _) := subsingleton_or_nontrivial A
  · simpa [Subsingleton.elim (cfc f a) 0]
  · refine cfc_cases (‖·‖ < c) a f (by simpa) fun hf ha ↦ ?_
    simp only [← cfc_apply f a, (IsGreatest.norm_cfc f a hf ha |>.lt_iff)]
    rintro - ⟨x, hx, rfl⟩
    exact h x hx

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

Goal state before:
pp: case e'_9
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
⊢ resolvent a k ^ 2 =
    (((ContinuousLinearMap.mulLeftRight A A) (resolvent a ((↑↑(algebraMap 𝕜 A)).1 k)))
        (resolvent a ((↑↑(algebraMap 𝕜 A)).1 k)))
      1

Tactic:
simp [resolvent, pow_two]

Goal state after: