mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ

Tactic:
by
  refine (absolutelyContinuous_smul <| ENNReal.coe_ne_zero.2 hr).ae_le
    (?_ : ν.rnDeriv (r • μ) =ᵐ[r • μ] r⁻¹ • ν.rnDeriv μ)
  rw [← withDensity_eq_iff_of_sigmaFinite]
  · simp_rw [ENNReal.smul_def]
    rw [withDensity_smul _ (measurable_rnDeriv _ _)]
    suffices ν.singularPart (r • μ) + withDensity (r • μ) (rnDeriv ν (r • μ))
        = ν.singularPart (r • μ) + r⁻¹ • withDensity (r • μ) (rnDeriv ν μ) by
      rwa [add_right_inj] at this
    rw [← ν.haveLebesgueDecomposition_add (r • μ), singularPart_smul_right _ _ _ hr,
      ENNReal.smul_def r, withDensity_smul_measure, ← ENNReal.smul_def, ← smul_assoc,
      smul_eq_mul, inv_mul_cancel₀ hr, one_smul]
    exact ν.haveLebesgueDecomposition_add μ
  · exact (measurable_rnDeriv _ _).aemeasurable
  · exact (measurable_rnDeriv _ _).aemeasurable.const_smul _

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : LinearOrder α
E : Type u_3
inst✝¹ : PseudoMetricSpace E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
hb : 𝓝[<] b = ⊥
⊢ Function.leftLim (variationOnFromTo f univ a) b = variationOnFromTo f univ a b - dist (f b) (Function.leftLim f b)

Tactic:
simp [leftLim_eq_of_eq_bot _ hb]

Goal state after:
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: α : Type u_2
inst✝⁶ : LinearOrder α
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set α
f : α → E
g : α → F
C D : ℝ≥0∞
hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C
hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D
B : E →L[ℝ] F →L[ℝ] G
n : ℕ
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ ∑ i ∈ Finset.range n, edist ((B (f (u (i + 1)))) (g (u (i + 1)))) ((B (f (u i))) (g (u i))) ≤
    ∑ i ∈ Finset.range n, edist ((B (f (u (i + 1)))) (g (u (i + 1)))) ((B (f (u i))) (g (u (i + 1)))) +
      ∑ i ∈ Finset.range n, edist ((B (f (u i))) (g (u (i + 1)))) ((B (f (u i))) (g (u i)))

Tactic:
by
    rw [← Finset.sum_add_distrib]
    gcongr with i hi
    apply edist_triangle

Goal state after:
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ρ : ρ ≪ μ
x : α
x✝ : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : μ o < ∞
s : Set α := ⋯
μs : μ s ≠ ∞
q : ℝ≥0
hq : 0 < q
⊢ s ⊆ {x | v.limRatioMeas hρ x < ↑q}

Tactic:
intro y hy

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : μ o < ∞
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ∞
q : ℝ≥0
hq : 0 < q
y : α
hy : y ∈ s
⊢ y ∈ {x | v.limRatioMeas hρ x < ↑q}
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 : α
hy : y ∈ s
y' : α
hy' : ε ≤ eVariationOn f (s ∩ Ici y')
y'_mem : y' ∈ s ∩ Ici y
a : α
ha : a ∈ s ∩ Ici y'
b : α
hb : b ∈ s ∩ Ici y'
hab : a < b
h : δ < eVariationOn f (s ∩ Icc a b)
this : Ici y' ∩ Icc a b = Icc a b
⊢ δ ≤ eVariationOn f (s ∩ Icc y b)

Tactic:
exact h.le.trans (mono _ (by grind))

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 : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc f a * cfc (fun x ↦ (f x)⁻¹) a = 1

Tactic:
by
    rw [← cfc_mul .., ← cfc_one R a]
    exact cfc_congr fun _ _ ↦ by aesop

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 : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (fun x ↦ (f x)⁻¹) a * cfc f a = 1

Tactic:
by
    rw [← cfc_mul .., ← cfc_one R a]
    exact cfc_congr fun _ _ ↦ by aesop

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
a b : α
hf : MonotoneOn f s
as : a ∈ s
bs : b ∈ s
hab : a ≤ b
hle : eVariationOn f (s ∩ Set.Icc a b) ≤ ENNReal.ofReal (f b - f a)
h : BoundedVariationOn f (s ∩ Set.Icc a b)
⊢ eVariationOn f (s ∩ Set.Icc a b) = ENNReal.ofReal (f b - f a)

Tactic:
apply eq_of_le_of_ge hle (ofReal_le_of_le_toReal _)

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
a b : α
hf : MonotoneOn f s
as : a ∈ s
bs : b ∈ s
hab : a ≤ b
hle : eVariationOn f (s ∩ Set.Icc a b) ≤ ENNReal.ofReal (f b - f a)
h : BoundedVariationOn f (s ∩ Set.Icc a b)
⊢ f b - f a ≤ (eVariationOn f (s ∩ Set.Icc a b)).toReal
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]

Tactic:
rw [map_add]

Goal state after:
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 + (toContinuousMapOnAlgHom s) g ∈ R[(toContinuousMapOnAlgHom s) X]
Module: Mathlib.Topology.ContinuousMap.Weierstrass

Goal state before:
pp: a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ (polynomialFunctions (Set.Icc a b)).topologicalClosure

Tactic:
rw [polynomialFunctions_closure_eq_top _ _]

Goal state after:
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ ⊤
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: n ν : ℕ
x : ↑I
⊢ 0 ≤ (bernstein n ν) x

Tactic:
by
  simp only [bernstein_apply]
  have h₁ : (0 : ℝ) ≤ x := by unit_interval
  have h₂ : (0 : ℝ) ≤ 1 - x := by unit_interval
  positivity

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

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

Tactic:
· apply Or.inr
      push _ ∈ _ at hx ⊢
      rw [show x = 0 from Subtype.val_injective hx, map_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
⊢ elemental 𝕜 (restrict s (ContinuousMap.id 𝕜)) = ⊤

Tactic:
rw [StarAlgebra.elemental, ← polynomialFunctions.starClosure_topologicalClosure,
    polynomialFunctions.starClosure_eq_adjoin_X]
  congr
  exact Polynomial.toContinuousMap_X_eq_id.symm

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

Goal state before:
pp: case mem
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f✝¹ f✝ f : C(↑s, 𝕜)
hf : f = (toContinuousMapOnAlgHom s) X ∨ star ((toContinuousMapOnAlgHom s) X) = f
⊢ p f

Tactic:
eq_comm (b := f)

Goal state after:
case mem
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f✝¹ f✝ f : C(↑s, 𝕜)
hf : f = (toContinuousMapOnAlgHom s) X ∨ f = star ((toContinuousMapOnAlgHom s) X)
⊢ p f
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case algebraMap
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f✝ f : C(↑s, 𝕜)
r : 𝕜
⊢ p ((algebraMap 𝕜 C(↑s, 𝕜)) r)

Tactic:
exact const r

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ LowerHemicontinuous fun x ↦ {x}

Tactic:
intro x t ⟨ht, hne⟩
  filter_upwards [ht.mem_nhds (Set.singleton_inter_nonempty.mp hne)] with x' hx'
  exact ⟨ht, Set.singleton_inter_nonempty.mpr hx'⟩

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
n : ℕ
hn : n ≠ 0
⊢ ⨆ i ∈ σ a, ↑‖i‖₊ ^ n ≤ ⨆ k ∈ σ (a ^ n), ↑‖k‖₊

Tactic:
refine iSup₂_le fun x hx ↦ ?_

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
n : ℕ
hn : n ≠ 0
x : 𝕜
hx : x ∈ σ a
⊢ ↑‖x‖₊ ^ n ≤ ⨆ k ∈ σ (a ^ n), ↑‖k‖₊
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hf_compact : ∀ x ∈ s, IsCompact (f x)
x₀ : α
hx₀s : x₀ ∈ s
u : Set β
hu : IsOpen[inst✝.toTopologicalSpace] u
hx₀u : f x₀ ⊆ u
W : Set (β × β)
hW : W ∈ uniformity β
left✝ : IsOpen[instTopologicalSpaceProd] W
hWu : ∀ x ∈ f x₀, ball x W ⊆ u
V : Set (β × β)
hV : V ∈ uniformity β
hVsym : SetRel.IsSymm V
hVcomp : SetRel.comp V V ⊆ W
U : SetRel β β
hUsub : id U ⊆ V
hUmem : U ∈ uniformity β
hUopen : IsOpen[instTopologicalSpaceProd] U
hHU : hausdorffEntourage U ∈ uniformity (Set β)
N : ι
hN : ∀ x ∈ s, (f x, F N x) ∈ hausdorffEntourage U
hFN_image : F N x₀ ⊆ U.image (f x₀)
hF : ∀ (n : ι), ∀ x ∈ s, UpperHemicontinuousWithinAt (F n) s x
hFN_uhc : ∀ᶠ (x : α) in 𝓝[s] x₀, F N x ⊆ U.image (f x₀)
x : α
hFNx : F N x ⊆ U.image (f x₀)
hx_s : x ∈ s
⊢ f x ⊆ u

Tactic:
intro y hy

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hf_compact : ∀ x ∈ s, IsCompact (f x)
x₀ : α
hx₀s : x₀ ∈ s
u : Set β
hu : IsOpen[inst✝.toTopologicalSpace] u
hx₀u : f x₀ ⊆ u
W : Set (β × β)
hW : W ∈ uniformity β
left✝ : IsOpen[instTopologicalSpaceProd] W
hWu : ∀ x ∈ f x₀, ball x W ⊆ u
V : Set (β × β)
hV : V ∈ uniformity β
hVsym : SetRel.IsSymm V
hVcomp : SetRel.comp V V ⊆ W
U : SetRel β β
hUsub : id U ⊆ V
hUmem : U ∈ uniformity β
hUopen : IsOpen[instTopologicalSpaceProd] U
hHU : hausdorffEntourage U ∈ uniformity (Set β)
N : ι
hN : ∀ x ∈ s, (f x, F N x) ∈ hausdorffEntourage U
hFN_image : F N x₀ ⊆ U.image (f x₀)
hF : ∀ (n : ι), ∀ x ∈ s, UpperHemicontinuousWithinAt (F n) s x
hFN_uhc : ∀ᶠ (x : α) in 𝓝[s] x₀, F N x ⊆ U.image (f x₀)
x : α
hFNx : F N x ⊆ U.image (f x₀)
hx_s : x ∈ s
y : β
hy : y ∈ f x
⊢ y ∈ u
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : ∀ i ∈ 𝓤 α, ∃ x ∈ Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i, x ∈ {s | TotallyBounded s}
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Tactic:
obtain ⟨t, ⟨hst : s ⊆ V.preimage t, -⟩, ht⟩ := hs V hV

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : ∀ i ∈ 𝓤 α, ∃ x ∈ Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i, x ∈ {s | TotallyBounded s}
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
t : Set α
ht : t ∈ {s | TotallyBounded s}
hst : s ⊆ V.preimage t
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x✝ :
  (∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
U : Set β
hU : U ∈ {V | IsOpen[inst✝] V}
⊢ IsOpen[inst✝¹] {a | ¬Disjoint (f a) U}

Tactic:
← compl_ofPred,

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x✝ :
  (∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
U : Set β
hU : U ∈ {V | IsOpen[inst✝] V}
⊢ IsOpen[inst✝¹] {a | Disjoint (f a) U}ᶜ
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.vietoris α] fun x ↦ x.1 ∪ x.2

Tactic:
continuous_iff,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ (∀ (U : Set α), IsOpen[inst✝] U → IsOpen[instTopologicalSpaceProd] ((fun x ↦ x.1 ∪ x.2) ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set α), IsClosed[inst✝] F → IsClosed[instTopologicalSpaceProd] ((fun x ↦ x.1 ∪ x.2) ⁻¹' 𝒫 F)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_4
inst✝ : Finite ι
⊢ Continuous[Pi.topologicalSpace, TopologicalSpace.vietoris α] range

Tactic:
continuous_iff,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_4
inst✝ : Finite ι
⊢ (∀ (U : Set α), IsOpen[inst✝¹] U → IsOpen[Pi.topologicalSpace] (range ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set α), IsClosed[inst✝¹] F → IsClosed[Pi.topologicalSpace] (range ⁻¹' 𝒫 F)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
⊢ Continuous[TopologicalSpace.vietoris α, TopologicalSpace.vietoris β] fun x ↦ f '' x

Tactic:
continuous_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
⊢ (∀ (U : Set β), IsOpen[inst✝] U → IsOpen[TopologicalSpace.vietoris α] ((fun x ↦ f '' x) ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[TopologicalSpace.vietoris α] ((fun x ↦ f '' x) ⁻¹' 𝒫 F)
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case h
𝕜 : 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 : ℕ
hn : n ≠ 0
⊢ n ≤ n + 1

Tactic:
exact n.le_succ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ i' ∈ 𝓤 α, Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id i') ∈ f.curry f
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
change ∀ {U} (hU : U ∈ 𝓤 α), ∀ᶠ K in f, ∀ᶠ K' in f, (↑K, ↑K') ∈ hausdorffEntourage U at hf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
⊢ ∃ x, f ≤ 𝓝 x
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
⊢ IsOpen ({a | ↑a ⊆ ⋃₀ u} ∩ ⋂ i ∈ u, {x | (↑x ∩ i).Nonempty})

Tactic:
exact .inter
      (isOpen_subsets_of_isOpen <| isOpen_sUnion fun U hU => hB.isOpen <| huB hU)
      (hu.isOpen_biInter fun U hU => isOpen_inter_nonempty_of_isOpen <| hB.isOpen <| huB hU)

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

Goal state before:
pp: case refine_2
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
g₁ g₂ : C(↑(σ R a), R)
x : ↑(σ R a)
⊢ dist (g₁ x) (g₂ x) ≤
    dist
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g₁.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g₂.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))

Tactic:
· let x' : σ S a := Subtype.map (algebraMap R S) (fun _ ↦ spectrum.algebraMap_mem S) x
      apply le_of_eq_of_le ?_ <| ContinuousMap.dist_apply_le_dist x'
      simp only [ContinuousMap.comp_apply, ContinuousMap.coe_mk, StarAlgHom.ofId_apply,
        halg.dist_eq, x']
      congr!
      all_goals ext; exact haf.left_inv _ |>.symm

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (σ ℝ a)

Tactic:
exact continuous_subtype_val.comp_continuousOn <|
    ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image ..

Goal state after:
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
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (σₙ ℝ a)

Tactic:
exact continuous_subtype_val.comp_continuousOn <|
    ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image ..

Goal state after:
Module: Mathlib.Analysis.Convex.TotallyBounded

Goal state before:
pp: E : Type u_1
s : Set E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ TotallyBounded ((convexHull ℝ) s)

Tactic:
by
  rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at ⊢ hs
  intro U hU
  obtain ⟨W, hW₁, hW₂⟩ := exists_nhds_zero_half hU
  obtain ⟨V, hV₁,hV₂, hV₃⟩ := (locallyConvexSpace_iff_exists_convex_subset_zero ℝ E).mp ‹_› W hW₁
  obtain ⟨t, htf, hts⟩ := hs _ hV₁
  obtain ⟨t', htf', hts'⟩ := totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp
    (htf.isCompact_convexHull ℝ).totallyBounded _ hV₁
  use t', htf'
  simp only [iUnion_vadd_set, vadd_eq_add] at hts hts' ⊢
  grw [hts, convexHull_add_subset, hV₂.convexHull_eq, hts', add_assoc, hV₃, add_subset_iff.mpr hW₂]

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

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ (convexHull ℝ) (balancedHull ℝ s) ⊆ (convexHull ℝ) (s ∪ -s)

Tactic:
← Convex.convexHull_eq (convex_convexHull ℝ (s ∪ -s))

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ (convexHull ℝ) (balancedHull ℝ s) ⊆ (convexHull ℝ) ((convexHull ℝ) (s ∪ -s))
Module: Mathlib.Analysis.LocallyConvex.HahnBanach

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : NormedField 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : Module 𝕜 E
S : Submodule 𝕜 E
f : Dual 𝕜 ↥S
p : Seminorm 𝕜 E
hp : ∀ (x : ↥S), ‖f x‖ ≤ p ↑x
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ : Module ℝ E := restrictScalars ℝ 𝕜 E
this : IsScalarTower ℝ 𝕜 E := IsScalarTower.restrictScalars ℝ 𝕜 E
⊢ ∃ g, (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), ‖g x‖ ≤ p x

Tactic:
let fr : Dual ℝ S := reLm.comp (f.restrictScalars ℝ)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : NormedField 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : Module 𝕜 E
S : Submodule 𝕜 E
f : Dual 𝕜 ↥S
p : Seminorm 𝕜 E
hp : ∀ (x : ↥S), ‖f x‖ ≤ p ↑x
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ : Module ℝ E := restrictScalars ℝ 𝕜 E
this : IsScalarTower ℝ 𝕜 E := IsScalarTower.restrictScalars ℝ 𝕜 E
fr : Dual ℝ ↥S := reLm ∘ₗ ↑ℝ f
⊢ ∃ g, (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), ‖g x‖ ≤ p x