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 μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞
x : α
hx : Tendsto (fun a ↦ (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
⊢ Tendsto (fun a ↦ (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))

Tactic:
rw [h'x]

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

Goal state before:
pp: case refine_1.inl.succ
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this✝ : u (n + 1) ≤ a
hn : u (n + 1) = a
this :
  Tendsto (fun y ↦ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (eVariationOn f (s ∩ Iio a) + edist (f a) l))
⊢ ∑ i ∈ Finset.range ⟨n + 1, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨n + 1, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨n + 1, ⟨u, ⋯⟩⟩.snd i)) ≤
    eVariationOn f (s ∩ Iio a) + edist (f a) l

Tactic:
apply ge_of_tendsto this

Goal state after:
case refine_1.inl.succ
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this✝ : u (n + 1) ≤ a
hn : u (n + 1) = a
this :
  Tendsto (fun y ↦ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (eVariationOn f (s ∩ Iio a) + edist (f a) l))
⊢ ∀ᶠ (c : α) in 𝓝[s ∩ Iio a] a,
    ∑ i ∈ Finset.range ⟨n + 1, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨n + 1, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨n + 1, ⟨u, ⋯⟩⟩.snd i)) ≤
      eVariationOn f (s ∩ Iio a) + edist (f a) (f c)
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
ι : Type u_3
f : ι → R → R
a : A
ha : p a
hf : ∀ (i : ι), ContinuousOn (f i) (spectrum R a)
⊢ (fun i ↦ cfc (f i) a) = fun i ↦ (cfcHom ha) { toFun := (spectrum R a).domRestrict (f i), continuous_toFun := ⋯ }

Tactic:
ext i

Goal state after:
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
ι : Type u_3
f : ι → R → R
a : A
ha : p a
hf : ∀ (i : ι), ContinuousOn (f i) (spectrum R a)
i : ι
⊢ cfc (f i) a = (cfcHom ha) { toFun := (spectrum R a).domRestrict (f i), continuous_toFun := ⋯ }
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case neg
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
f g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : ¬(p a ∧ ContinuousOn g (spectrum R a))
⊢ cfc f a = cfc g a

Tactic:
obtain (ha | hg) := not_and_or.mp h

Goal state after:
case neg.inl
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
f g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : ¬(p a ∧ ContinuousOn g (spectrum R a))
ha : ¬p a
⊢ cfc f a = cfc g a

case neg.inr
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
f g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : ¬(p a ∧ ContinuousOn g (spectrum R a))
hg : ¬ContinuousOn g (spectrum R a)
⊢ cfc f a = cfc g a
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
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (fun x ↦ r + f x) a = (algebraMap R A) r + cfc f a

Tactic:
have : (fun z => r + f z) = (fun z => (fun _ => r) z + f z) := by ext; simp

Goal state after:
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
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
this : (fun z ↦ r + f z) = fun z ↦ (fun x ↦ r) z + f z
⊢ cfc (fun x ↦ r + f x) a = (algebraMap R A) r + cfc f a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case pos
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
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ cfc (fun x ↦ star (f x)) a = star (cfc f a)

Tactic:
rw [cfc_apply f a, ← map_star, cfc_apply _ a]

Goal state after:
case pos
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
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ (cfcHom ha) { toFun := (spectrum R a).domRestrict fun x ↦ star (f x), continuous_toFun := ⋯ } =
    (cfcHom ha) (star { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : LinearOrder α
E : Type u_2
inst✝³ : PseudoEMetricSpace E
inst✝² : CompleteSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
hs : (s ∩ Iio x).Nonempty
⊢ ∃ l, Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)

Tactic:
exact BoundedVariationOn.exists_tendsto_left_of_filter (s := s ∩ Iio x)
    (hf.mono inter_subset_left) _ (fun y hy ↦ inter_mem_nhdsWithin _ (Ici_mem_nhds hy.2)) hs

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

Goal state before:
pp: case neg
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
f✝ g : R → R
a✝ : A
ha : p a✝
hf : ContinuousOn f✝ (spectrum R a✝)
hg : ContinuousOn g (spectrum R a✝)
f : R → R
a : A
h : ¬ContinuousOn f (spectrum R a)
⊢ star (cfc f a) * cfc f a = cfc f a * star (cfc f a)

Tactic:
simp [cfc_apply_of_not_continuousOn a h]

Goal state after:
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 : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)

Tactic:
rcases le_or_gt x y with hy | hy

Goal state after:
case inl
α : 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 : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : x ≤ y
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)

case inr
α : 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 : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
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
ι : Type u_3
f : ι → R → R
a : A
ha : p a
hf : ∀ (i : ι), ContinuousOn (f i) (σₙ R a)
hf0 : ∀ (i : ι), f i 0 = 0
⊢ (fun i ↦ cfcₙ (f i) a) = fun i ↦
    (cfcₙHom ha) { toFun := (σₙ R a).domRestrict (f i), continuous_toFun := ⋯, map_zero' := ⋯ }

Tactic:
ext i

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
ι : Type u_3
f : ι → R → R
a : A
ha : p a
hf : ∀ (i : ι), ContinuousOn (f i) (σₙ R a)
hf0 : ∀ (i : ι), f i 0 = 0
i : ι
⊢ cfcₙ (f i) a = (cfcₙHom ha) { toFun := (σₙ R a).domRestrict (f i), continuous_toFun := ⋯, map_zero' := ⋯ }
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ¬f 0 = 0
⊢ cfcₙ f a = 0

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

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

Goal state before:
pp: case refine_2
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ ∀ (n : ℕ) (a : R), ((aeval f) ((monomial n) a)) x = eval (f x) ((monomial n) a)

Tactic:
· intro n a
    simp

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν.pred.succ ≤ n
h' : ν > 0
⊢ 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)

Tactic:
exact ascPochhammer_pos _ _ (tsub_pos_of_lt (Nat.lt_of_succ_le h))

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

Goal state before:
pp: case mp.refine_2.convert_2.right
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := ⋯
x : ↑(Set.Icc a b)
w₁ : 0 < (b - a)⁻¹
w₂ : 0 ≤ ↑x - a
w₃ : ↑x - a ≤ b - a
⊢ (↑x - a) * (b - a)⁻¹ ≤ 1

Tactic:
· rw [← div_eq_mul_inv, div_le_one (sub_pos.mpr h)]
          exact w₃

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

Goal state before:
pp: case neg
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
hf0 : ¬f 0 = 0
⊢ cfcₙ f 0 = 0

Tactic:
· exact cfcₙ_apply_of_not_map_zero _ hf0

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ ∀ U ∈ 𝓝 0, Convex ℝ U → ∀ᶠ (n : ℕ) in atTop, ∀ (x : ↑I), gauge U ((bernsteinApproximation n f) x - f x) < 1

Tactic:
intro U

Goal state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
⊢ U ∈ 𝓝 0 → Convex ℝ U → ∀ᶠ (n : ℕ) in atTop, ∀ (x : ↑I), gauge U ((bernsteinApproximation n f) x - f x) < 1
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ A = A.topologicalClosure

Tactic:
apply SetLike.ext'

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ ↑A = ↑A.topologicalClosure
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}
⊢ ∃ x, dist x f < ε ∧ x ∈ L

Tactic:
have U_nhds_y : ∀ x y, U x y ∈ 𝓝 y := by
    intro x y
    refine IsOpen.mem_nhds ?_ ?_
    · apply isOpen_lt <;> fun_prop
    · rw [Set.mem_ofPred_eq, w₂]
      exact sub_lt_self _ pos

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
⊢ ∃ x, dist x f < ε ∧ x ∈ L
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
⊢ A.topologicalClosure = ⊤

Tactic:
apply SetLike.ext'

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
⊢ ↑A.topologicalClosure = ↑⊤
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x✝ x : Unitization 𝕜 E
h : (algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2 = 0
⊢ ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1⋆ + (mul 𝕜 E) x.toProd.2⋆‖

Tactic:
simp only [h, norm_zero]

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x✝ x : Unitization 𝕜 E
h : (algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2 = 0
⊢ 0 ≤ ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1⋆ + (mul 𝕜 E) x.toProd.2⋆‖
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

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

pp: case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')

Tactic:
hasBasis_nhdsSet (f x) |>.forall_iff ?h₂

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ (∀ (i : Set β), IsOpen[inst✝] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (i : Set β), IsOpen[inst✝] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝[s] x

case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → f ⁻¹' Iic s_1 ∈ 𝓝[s] x → f ⁻¹' Iic t ∈ 𝓝[s] x

case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
h : ∀ (x : ℕ → α), Tendsto x atTop (𝓝 x₀) → ∀ y₀ ∈ f x₀, ∃ y, (∀ (n : ℕ), y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)
⊢ ∀ (u : Set β), IsOpen[inst✝¹] u → (f x₀ ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ u).Nonempty

Tactic:
intro U

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
h : ∀ (x : ℕ → α), Tendsto x atTop (𝓝 x₀) → ∀ y₀ ∈ f x₀, ∃ y, (∀ (n : ℕ), y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)
U : Set β
⊢ IsOpen[inst✝¹] U → (f x₀ ∩ U).Nonempty → ∀ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ U).Nonempty
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
⊢ ∀ U ∈ u, ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty

Tactic:
intro U

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
U : Set α
⊢ U ∈ u → ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ ∀ s ∈ 𝓤 α, hausdorffEntourage s ∈ ((𝓤 α).lift' hausdorffEntourage).lift' fun s ↦ SetRel.comp s s

Tactic:
intro U

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
U : Set (α × α)
⊢ U ∈ 𝓤 α → hausdorffEntourage U ∈ ((𝓤 α).lift' hausdorffEntourage).lift' fun s ↦ SetRel.comp s s
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
⊢ ∀ ib ∈ 𝓤 α,
    ∃ ia ∈ 𝓤 α,
      ∀ x ∈ hausdorffEntourage ia,
        closure[inst✝.toTopologicalSpace] x.1 ⊆ SetRel.preimage ib (closure[inst✝.toTopologicalSpace] x.2) ∧
          closure[inst✝.toTopologicalSpace] x.2 ⊆ SetRel.image ib (closure[inst✝.toTopologicalSpace] x.1)

Tactic:
intro U

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
⊢ U ∈ 𝓤 α →
    ∃ ia ∈ 𝓤 α,
      ∀ x ∈ hausdorffEntourage ia,
        closure[inst✝.toTopologicalSpace] x.1 ⊆ SetRel.preimage U (closure[inst✝.toTopologicalSpace] x.2) ∧
          closure[inst✝.toTopologicalSpace] x.2 ⊆ SetRel.image U (closure[inst✝.toTopologicalSpace] x.1)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
⊢ ∀ i' ∈ 𝓤 α,
    ∃ i ∈ 𝓤 α,
      (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹'
          hausdorffEntourage i ⊆
        hausdorffEntourage i'

Tactic:
intro U

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
⊢ U ∈ 𝓤 α →
    ∃ i ∈ 𝓤 α,
      (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹'
          hausdorffEntourage i ⊆
        hausdorffEntourage U
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
⊢ ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → {a | s ⊆ i'.preimage a} ∩ {a | a ⊆ i'.image s} ∈ 𝓝 s

Tactic:
intro U

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
⊢ U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U → {a | s ⊆ U.preimage a} ∩ {a | a ⊆ U.image s} ∈ 𝓝 s
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 : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
⊢ l.TotallyBounded

Tactic:
intro U

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
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
U : SetRel α α
⊢ U ∈ 𝓤 α → ∃ t, t.Finite ∧ U.preimage t ∈ l