mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.StarOrdered

Goal state before:
pp: case mpr.add
α : Type u_1
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : Zero α
R : Type u_2
inst✝⁸ : TopologicalSpace R
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : NoZeroDivisors R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : IsTopologicalSemiring R
inst✝¹ : ContinuousStar R
inst✝ : StarOrderedRing C(α, R)
p g₁ g₂ : C(α, R)₀
hx✝ : g₁ ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hy✝ : g₂ ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
h₁ : ∀ (f : C(α, R)₀), f ≤ f + g₁
h₂ : ∀ (f : C(α, R)₀), f ≤ f + g₂
f : C(α, R)₀
⊢ f ≤ f + (g₁ + g₂)

Tactic:
calc
          f ≤ f + g₁ := h₁ f
          _ ≤ (f + g₁) + g₂ := h₂ (f + g₁)
          _ = f + (g₁ + g₂) := add_assoc _ _ _

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 μ
f : α → ℝ≥0∞
hf : Measurable f
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
ρ : Measure α := μ.withDensity f
this : IsFiniteMeasure ρ
x : α
hx : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
h'x : (μ.withDensity f).rnDeriv μ x = f x
⊢ Tendsto (fun a ↦ (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))

Tactic:
← h'x

Goal state after:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : Measurable f
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
ρ : Measure α := μ.withDensity f
this : IsFiniteMeasure ρ
x : α
hx : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
h'x : (μ.withDensity f).rnDeriv μ x = f x
⊢ Tendsto (fun a ↦ (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 ((μ.withDensity f).rnDeriv μ x))
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 α
a : α
l : E
h : (𝓝[s ∩ Ioi a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Ioi a] a) (𝓝 l)
⊢ eVariationOn f (s ∩ Ici a) = eVariationOn f (s ∩ Ioi a) + edist (f a) l

Tactic:
← comp_ofDual f,

Goal state after:
α : 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 ∩ Ioi a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Ioi a] a) (𝓝 l)
⊢ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' (s ∩ Ici a)) = eVariationOn f (s ∩ Ioi a) + edist (f a) l
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 α
a : α
h : (𝓝[s ∩ Ioi a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Ici a) a
⊢ eVariationOn f (s ∩ Ioi a) = eVariationOn f (s ∩ Ici a)

Tactic:
← comp_ofDual f,

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Ioi a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Ici a) a
⊢ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' (s ∩ Ioi a)) = eVariationOn f (s ∩ Ici a)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
a b : α
h : (𝓝[>] a).NeBot
h' : ContinuousWithinAt f (Ici a) a
hab : b ≤ a
⊢ eVariationOn f (Ioc a b) = eVariationOn f (Icc a b)

Tactic:
simp [hab]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : LinearOrder α
E : Type u_2
inst✝³ : PseudoEMetricSpace E
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : α → E
a b : α
h' : ContinuousWithinAt f (Ici a) a
hab : b ≤ a
⊢ eVariationOn f (Ioc a b) = eVariationOn f (Icc a b)

Tactic:
simp [hab]

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
a b : α
h : (𝓝[<] a).NeBot
h' : ContinuousWithinAt f (Iic a) a
⊢ eVariationOn f (Ico b a) = eVariationOn f (Icc b a)

Tactic:
← comp_ofDual f,

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
a b : α
h : (𝓝[<] a).NeBot
h' : ContinuousWithinAt f (Iic a) a
⊢ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Ico b a) = eVariationOn f (Icc b a)
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
a b : α
h : (𝓝[<] a).NeBot
h' : ContinuousWithinAt f (Iic a) a
⊢ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Ico b a) = eVariationOn f (Icc b a)

Tactic:
← comp_ofDual f,

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
a b : α
h : (𝓝[<] a).NeBot
h' : ContinuousWithinAt f (Iic a) a
⊢ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Ico b a) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Icc b a)
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 α
inst✝ : DenselyOrdered α
f : α → E
a b : α
h' : ContinuousWithinAt f (Iic a) a
⊢ eVariationOn f (Ico b a) = eVariationOn f (Icc b a)

Tactic:
← comp_ofDual f,

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
E : Type u_2
inst✝³ : PseudoEMetricSpace E
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : α → E
a b : α
h' : ContinuousWithinAt f (Iic a) a
⊢ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Ico b a) = eVariationOn f (Icc b a)
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 α
inst✝ : DenselyOrdered α
f : α → E
a b : α
h' : ContinuousWithinAt f (Iic a) a
⊢ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Ico b a) = eVariationOn f (Icc b a)

Tactic:
← comp_ofDual f,

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
E : Type u_2
inst✝³ : PseudoEMetricSpace E
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : α → E
a b : α
h' : ContinuousWithinAt f (Iic a) a
⊢ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Ico b a) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' Icc b 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 g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : p a ∧ ContinuousOn g (spectrum R a)
⊢ (cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ } = cfc g a

Tactic:
cfc_apply (ha := h.1) (hf := h.2)

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 g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : p a ∧ ContinuousOn g (spectrum R a)
⊢ (cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ } =
    (cfcHom ⋯) { toFun := (spectrum R a).domRestrict g, continuous_toFun := ⋯ }
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
inst✝ : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
⊢ ∃ l, Tendsto f L (𝓝 l)

Tactic:
rcases Filter.eq_or_neBot L with h | h

Goal state after:
case inl
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
inst✝ : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L = ⊥
⊢ ∃ l, Tendsto f L (𝓝 l)

case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
inst✝ : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
⊢ ∃ l, Tendsto f L (𝓝 l)
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 μ
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ ⨍ (y : α) in a, f y ∂μ) (v.filterAt x) (𝓝 (f x))

Tactic:
by
  filter_upwards [v.ae_tendsto_average_norm_sub hf, v.ae_eventually_measure_pos] with x hx h'x
  rw [tendsto_iff_norm_sub_tendsto_zero]
  refine squeeze_zero' (Eventually.of_forall fun a => norm_nonneg _) ?_ hx
  filter_upwards [h'x, v.eventually_measure_lt_top x, v.eventually_filterAt_integrableOn x hf]
    with a ha h'a h''a
  nth_rw 1 [← setAverage_const ha.ne' h'a.ne (f x)]
  simp_rw [setAverage_eq']
  rw [← integral_sub]
  · exact norm_integral_le_integral_norm _
  · exact (integrable_inv_smul_measure ha.ne' h'a.ne).2 h''a
  · exact (integrable_inv_smul_measure ha.ne' h'a.ne).2 (integrableOn_const h'a.ne)

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
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
a : A
φ : C(↑(spectrum S a), S) →⋆ₐ[S] A
f : C(S, R)
h : SpectrumRestricts a ⇑f
h_id : φ (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a
x : ↑(spectrum S a)
⊢ ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        ((ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)).comp
          { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
      x =
    (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) x

Tactic:
exact h.rightInvOn x.2

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✝⁹ : 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
q : R[X]
f : R → R
a : A
hf : ContinuousOn f ((fun x ↦ Polynomial.eval x q) '' spectrum R a)
ha : p a
⊢ cfc (fun x ↦ f (Polynomial.eval x q)) a = cfc f ((aeval a) q)

Tactic:
rw [cfc_comp' .., cfc_polynomial ..]

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
inst✝¹⁹ : Semifield R
inst✝¹⁸ : StarRing R
inst✝¹⁷ : MetricSpace R
inst✝¹⁶ : IsTopologicalSemiring R
inst✝¹⁵ : ContinuousStar R
inst✝¹⁴ : Field S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalRing S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : Module S A
inst✝⁶ : IsScalarTower S A A
inst✝⁵ : SMulCommClass S A A
inst✝⁴ : Algebra R S
inst✝³ : Module R A
inst✝² : IsScalarTower R S A
inst✝¹ : StarModule R S
inst✝ : ContinuousSMul R S
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_id : φ (ContinuousMapZero.id (σₙ S a)) = a
x : ↑(σₙ S a)
⊢ ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        ((ContinuousMapZero.id (σₙ R a)).comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
      x =
    (ContinuousMapZero.id (σₙ S a)) x

Tactic:
exact h.rightInvOn x.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
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : CompleteSpace E
inst✝ : T3Space E
f : α → E
hf : BoundedVariationOn f univ
x : α
this : Tendsto (Function.leftLim f) (𝓝[<] x) (𝓝 (Function.leftLim (Function.leftLim f) x))
⊢ ContinuousWithinAt (Function.leftLim f) (Iic x) x

Tactic:
rw [leftLim_leftLim (hf.tendsto_leftLim x)] at this

Goal state after:
α : Type u_1
inst✝⁵ : LinearOrder α
E : Type u_2
inst✝⁴ : PseudoEMetricSpace E
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : CompleteSpace E
inst✝ : T3Space E
f : α → E
hf : BoundedVariationOn f univ
x : α
this : Tendsto (Function.leftLim f) (𝓝[<] x) (𝓝 (Function.leftLim f x))
⊢ ContinuousWithinAt (Function.leftLim f) (Iic x) x
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: 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 : α
⊢ ((aeval f) g) x = eval (f x) g

Tactic:
refine Polynomial.induction_on' g ?_ ?_

Goal state after:
case refine_1
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 : α
⊢ ∀ (p q : R[X]),
    ((aeval f) p) x = eval (f x) p → ((aeval f) q) x = eval (f x) q → ((aeval f) (p + q)) x = eval (f x) (p + q)

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)
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: case refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
n : ℕ
r : R
hn : (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ n) ∈ R[(toContinuousMapOnAlgHom s) X]
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ n) * (toContinuousMapOnAlgHom s) X ∈
    R[(toContinuousMapOnAlgHom s) X]

Tactic:
exact mul_mem hn (Algebra.subset_adjoin <| Set.mem_singleton _)

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 : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
C : ℝ
hC : ∀ (x y : ↑I), gauge U (f x - f y) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ : ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2
nhds_zero : Tendsto (fun n ↦ C / δ ^ 2 / ↑n) atTop (𝓝 0)
n : ℕ
nh : C / δ ^ 2 / ↑n < 1 / 2
hn₀ : n ≠ 0
x : ↑I
S : Finset (Fin (n + 1)) := {k | dist k/ₙ x < δ}
⊢ gauge U ((bernsteinApproximation n f) x - f x) = gauge U (∑ k, (bernstein n ↑k) x • (f k/ₙ - f x))

Tactic:
simp [bernsteinApproximation.apply, smul_sub, ← Finset.sum_smul]

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

Goal state before:
pp: 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 z y : X
ym : y ∈ ↑(ys x)
zm : z ∈ U x y
⊢ f z - ε < ↑(h x) z

Tactic:
dsimp [h]

Goal state after:
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 z y : X
ym : y ∈ ↑(ys x)
zm : z ∈ U x y
⊢ f z - ε < ((ys x).sup' ⋯ fun y ↦ g x y) z
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NonUnitalNormedRing E
inst✝⁵ : StarRing E
inst✝⁴ : NormedStarGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : IsScalarTower 𝕜 E E
inst✝¹ : SMulCommClass 𝕜 E E
inst✝ : RegularNormedAlgebra 𝕜 E
a b : E
⊢ ‖((mul 𝕜 E) a⋆) b‖ = ‖((mul 𝕜 E).flip a) b⋆‖

Tactic:
simpa only [mul_apply', flip_apply, star_mul, star_star] using! norm_star (star b * a)

Goal state after:
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
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ⋯
key : (↑I).range ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
f_re : C(X, ℝ) := ⋯
f_im : C(X, ℝ) := ⋯
h_f_re : I f_re ∈ A.topologicalClosure
h_f_im : I f_im ∈ A.topologicalClosure
this : I f_re + RCLike.I • I f_im ∈ A.topologicalClosure
a✝ : X
⊢ (I f_re + RCLike.I • I f_im) a✝ = f a✝

Tactic:
simp [I, f_re, f_im, mul_comm RCLike.I _]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
⊢ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) =
    ↑(span 𝕜 ({1} ∪ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})))

Tactic:
by
  ext x
  rw [SetLike.mem_coe, SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra,
    ← StarSubalgebra.mem_toSubalgebra, ← Subalgebra.mem_toSubmodule,
    StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, span_union, span_eq_toSubmodule]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
⊢ φ 1 = 1

Tactic:
have h₁ : φ 1 * (1 - φ 1) = 0 := by rw [mul_sub, sub_eq_zero, mul_one, ← map_mul φ, one_mul]
    rcases mul_eq_zero.mp h₁ with (h₂ | h₂)
    · have : ∀ a, φ (a * 1) = 0 := fun a => by simp only [map_mul φ, h₂, mul_zero]
      exact False.elim (φ.prop.1 <| ContinuousLinearMap.ext <| by simpa only [mul_one] using! this)
    · exact (sub_eq_zero.mp h₂).symm

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

Goal state before:
pp: case mem.inl
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Fact (0 ∈ s)
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id s}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f : C(↑s, 𝕜)₀
⊢ p (ContinuousMapZero.id s)

Tactic:
assumption

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

Goal state before:
pp: case mem.inr
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Fact (0 ∈ s)
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id s}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f : C(↑s, 𝕜)₀
⊢ p (star (ContinuousMapZero.id s))

Tactic:
assumption

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 : α
⊢ (∀ t ∈ 𝓝 (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝 (f x')) → ∀ s_1 ∈ 𝓝 (f x), ∀ᶠ (x : α) in 𝓝[s] x, f x ∈ s_1

Tactic:
intro h t ht

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ∀ t ∈ 𝓝 (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝 (f x')
t : Set β
ht : t ∈ 𝓝 (f x)
⊢ ∀ᶠ (x : α) in 𝓝[s] x, f x ∈ t
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

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

Tactic:
intro h t 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)
⊢ ∀ᶠ (x : α) in 𝓝[s] x, f x ∈ t
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
hf : UpperHemicontinuous f
⊢ ∀ x ∈ {a | f a = ∅}, {a | f a = ∅} ∈ 𝓝 x

Tactic:
intro x (hx : f x = ∅)

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
hf : UpperHemicontinuous f
x : α
hx : f x = ∅
⊢ {a | f a = ∅} ∈ 𝓝 x
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h✝ : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U | IsOpen[inst✝] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U | IsOpen[inst✝] U}
v : Set (Set α)
hv₁ : v ⊆ {U | IsOpen[inst✝] U}
hv₂ : v.Finite
hv : (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}
ht₁ : (powerset '' u).Finite ∧ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' v).Finite
ht₂ :
  powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
U : Set α := ⋂₀ u
hU : IsOpen[inst✝] U
hs : s ∈ ⋂₀ (powerset '' u) ∩ ⋂₀ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' v)
x✝ : Set α
⊢ x✝ ∈ ⋂₀ (powerset '' u) ↔ x✝ ∈ 𝒫 U

Tactic:
simp [U]

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✝
A : Type u_3
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : A
inst✝ : IsCompact (spectrum ℝ a)
⊢ IsCompact (spectrum ℝ a)

Tactic:
assumption

Goal state after: