mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁴ : CommRing R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalRing R
inst✝⁹ : ContinuousStar R
inst✝⁸ : ContinuousSqrt R
inst✝⁷ : StarOrderedRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
r : R
a : A
ha : p a
⊢ a ≤ (algebraMap R A) r ↔ ∀ x ∈ spectrum R a, x ≤ r

Tactic:
nth_rw 1 [← cfc_id R a]

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁴ : CommRing R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalRing R
inst✝⁹ : ContinuousStar R
inst✝⁸ : ContinuousSqrt R
inst✝⁷ : StarOrderedRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
r : R
a : A
ha : p a
⊢ cfc id a ≤ (algebraMap R A) r ↔ ∀ x ∈ spectrum R a, x ≤ r
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁴ : CommRing R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalRing R
inst✝⁹ : ContinuousStar R
inst✝⁸ : ContinuousSqrt R
inst✝⁷ : StarOrderedRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
r : R
a : A
ha : p a
⊢ (algebraMap R A) r ≤ a ↔ ∀ x ∈ spectrum R a, r ≤ x

Tactic:
nth_rw 1 [← cfc_id R a]

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁴ : CommRing R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalRing R
inst✝⁹ : ContinuousStar R
inst✝⁸ : ContinuousSqrt R
inst✝⁷ : StarOrderedRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
r : R
a : A
ha : p a
⊢ (algebraMap R A) r ≤ cfc id a ↔ ∀ x ∈ spectrum R a, r ≤ x
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
this : (fun y ↦ eVariationOn f (s ∩ Iic y)) = fun y ↦ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Ici (toDual y))
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Iic y)) (𝓟 s ⊓ atBot) (𝓝 0)

Tactic:
rw [this]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
this : (fun y ↦ eVariationOn f (s ∩ Iic y)) = fun y ↦ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Ici (toDual y))
⊢ Tendsto (fun y ↦ eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Ici (toDual y))) (𝓟 s ⊓ atBot) (𝓝 0)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : 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

Tactic:
← h.dist_le (x := a) (y := b)

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 ≤ dist (f a) (f b)

case hx
α : 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)
⊢ a ∈ s ∩ Set.Icc a b

case hy
α : 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)
⊢ b ∈ s ∩ Set.Icc a b
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
this : eval 1 ((⇑derivative)^[n - k] p) = 0
⊢ eval 1 ((⇑derivative)^[n - k] p) ≠ eval 1 ((⇑derivative)^[n - k] (bernsteinPolynomial ℚ n k))

Tactic:
rw [this]

Goal state after:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
this : eval 1 ((⇑derivative)^[n - k] p) = 0
⊢ 0 ≠ eval 1 ((⇑derivative)^[n - k] (bernsteinPolynomial ℚ n k))
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set R
φ ψ : C(↑s, R) →ₐ[R] A
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ polynomialFunctions s ≤ φ.equalizer ψ

Tactic:
by
  rw [polynomialFunctions.eq_adjoin_X s]
  exact φ.adjoin_le_equalizer ψ fun x hx => (Set.mem_singleton_iff.1 hx).symm ▸ h

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalSemiring R
inst✝¹ : StarRing R
inst✝ : ContinuousStar R
s : Set R
⊢ (polynomialFunctions s).starClosure = adjoin R {(toContinuousMapOnAlgHom s) X}

Tactic:
by
  rw [polynomialFunctions.eq_adjoin_X s, adjoin_eq_starClosure_adjoin]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
⊢ p.comp (↑f).attachBound ∈ A.topologicalClosure

Tactic:
have mem_closure : p ∈ (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).topologicalClosure :=
    continuousMap_mem_polynomialFunctions_closure _ _ p
  -- and so there are polynomials arbitrarily close.
  have frequently_mem_polynomials := mem_closure_iff_frequently.mp mem_closure
  -- To prove `p.comp (attachBound f)` is in the closure of `A`,
  -- we show there are elements of `A` arbitrarily close.
  apply mem_closure_iff_frequently.mpr
  -- To show that, we pull back the polynomials close to `p`,
  refine
    ((compRightContinuousMap ℝ (attachBound (f : C(X, ℝ)))).continuousAt
            p).tendsto.frequently_map
      _ ?_ frequently_mem_polynomials
  -- but need to show that those pullbacks are actually in `A`.
  rintro _ ⟨g, ⟨-, rfl⟩⟩
  simp only [SetLike.mem_coe, AlgHom.coe_toRingHom,
    Polynomial.toContinuousMapOnAlgHom_apply]
  apply polynomial_comp_attachBound_mem

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

Goal state before:
pp: case star_id
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id s) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id s)) * a = 0
hφ : Continuous ⇑φ
⊢ φ (star (ContinuousMapZero.id s)) * a = 0

Tactic:
| star_id =>

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

Goal state before:
pp: case star_id
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id s) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id s)) = 0
hφ : Continuous ⇑φ
⊢ a * φ (star (ContinuousMapZero.id s)) = 0

Tactic:
| star_id =>

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
s : Set α
x : α
γ : Type u_5
inst✝ : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousWithinAt f s x
hi : IsInducing i
h_cl : IsClosed[inst✝¹] (range i)
v : Set β
hv : IsOpen[inst✝¹] v
hu : IsOpen[inst✝] (i ⁻¹' v)
hifu : i ⁻¹' (f x ∩ range i) ⊆ i ⁻¹' v
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, i ⁻¹' (f x' ∩ range i) ⊆ i ⁻¹' v

Tactic:
preimage_subset_preimage_iff inter_subset_right

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
s : Set α
x : α
γ : Type u_5
inst✝ : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousWithinAt f s x
hi : IsInducing i
h_cl : IsClosed[inst✝¹] (range i)
v : Set β
hv : IsOpen[inst✝¹] v
hu : IsOpen[inst✝] (i ⁻¹' v)
hifu : f x ∩ range i ⊆ v
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ range i ⊆ v
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
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : ↑K ⊆ V.preimage t
K' : Compacts α
left✝ : (↑K, ↑K').1 ⊆ SetRel.preimage (Prod.swap ⁻¹' V) (↑K, ↑K').2
hK' : ↑K' ⊆ V.preimage ↑K
⊢ ↑K' ⊆ V.preimage ↑K

Tactic:
hK'

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 α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : ↑K ⊆ V.preimage t
K' : Compacts α
left✝ : (↑K, ↑K').1 ⊆ SetRel.preimage (Prod.swap ⁻¹' V) (↑K, ↑K').2
hK' : ↑K' ⊆ V.preimage ↑K
⊢ V.preimage ↑K ⊆ V.preimage ↑K
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
x : α
hx : x ∈ s
this : {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s} = ⋃ n, range '' univ.pi fun x ↦ s
⊢ IsPreconnected {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s}

Tactic:
rw [this]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
x : α
hx : x ∈ s
this : {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s} = ⋃ n, range '' univ.pi fun x ↦ s
⊢ IsPreconnected (⋃ n, range '' univ.pi fun x ↦ s)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inr
𝕜 : 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
h✝ : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx : x ∈ σ 𝕜 a
⊢ (fun x ↦ ‖f x‖) x ≤ c

Tactic:
exact h x hx

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

Goal state before:
pp: case inr
𝕜 : 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
h✝ : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx : x ∈ σ 𝕜 a
⊢ (fun x ↦ ‖f x‖) x < c

Tactic:
exact h x hx

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 : { toFun := (σₙ 𝕜 a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
x : 𝕜
hx : x ∈ σₙ 𝕜 a
⊢ (fun x ↦ ‖f x‖) x ≤ c

Tactic:
exact h x hx

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 : { toFun := (σₙ 𝕜 a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
x : 𝕜
hx : x ∈ σₙ 𝕜 a
⊢ (fun x ↦ ‖f x‖) x < c

Tactic:
exact h x hx

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

Goal state before:
pp: case inr
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
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h✝ : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
x : ℝ≥0
hx : x ∈ σ ℝ≥0 a
⊢ f x ≤ c

Tactic:
exact h x hx

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

Goal state before:
pp: case inr
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
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h✝ : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
x : ℝ≥0
hx : x ∈ σ ℝ≥0 a
⊢ f x < c

Tactic:
exact h x hx

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
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x ≤ c
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : { toFun := (σₙ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : 0 ≤ a
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
⊢ f x ≤ c

Tactic:
exact h x hx

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

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : { toFun := (σₙ ℝ≥0 a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : 0 ≤ a
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
⊢ f x < c

Tactic:
exact h x hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : DiscreteTopology α
K : Compacts α
⊢ IsOpen {K}

Tactic:
convert!
    (isOpen_subsets_of_isOpen (isOpen_discrete (K : Set α))).inter
      (K.isCompact.finite_of_discrete.isOpen_biInter fun x hx =>
        isOpen_inter_nonempty_of_isOpen (isOpen_discrete { x }))

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : DiscreteTopology α
K : Compacts α
⊢ {K} = {K_1 | ↑K_1 ⊆ ↑K} ∩ ⋂ i ∈ ↑K, {K | (↑K ∩ {i}).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this✝ : Fintype ↑u := hu'.fintype
this :
  {K | ↑K ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑K ∩ U).Nonempty) ∧ (↑K).Finite} =
    Finset.univ.sup '' univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}
⊢ IsPreconnected {a | ↑a ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑a ∩ U).Nonempty) ∧ (↑a).Finite}

Tactic:
rw [this]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this✝ : Fintype ↑u := hu'.fintype
this :
  {K | ↑K ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑K ∩ U).Nonempty) ∧ (↑K).Finite} =
    Finset.univ.sup '' univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}
⊢ IsPreconnected (Finset.univ.sup '' univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U})
Module: Mathlib.Analysis.LocallyConvex.Polar

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : y ∈ B.polar Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖(B x) y‖ = ‖c‖ * ‖(B (c⁻¹ • x)) y‖

Tactic:
by
      rw [B.map_smul, LinearMap.smul_apply, smul_eq_mul, norm_mul, norm_inv,
        mul_inv_cancel_left₀ hc.ne']

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
⊢ ((absConvexHull 𝕜) s).Nonempty ↔ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty, nonempty_iff_ne_empty, Ne, Ne]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
⊢ ¬(absConvexHull 𝕜) s = ∅ ↔ ¬s = ∅
Module: Mathlib.Analysis.LocallyConvex.Polar

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝³ : SeminormedCommRing R
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (topDualPairing R M).SeparatingLeft

Tactic:
rw [LinearMap.separatingLeft_iff_ker_eq_bot, LinearMap.ker_eq_bot]

Goal state after:
R : Type u_4
M : Type u_5
inst✝³ : SeminormedCommRing R
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Function.Injective ⇑(topDualPairing R M)
Module: Mathlib.Analysis.LocallyConvex.Barrelled

Goal state before:
pp: α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ⇑p
h₁ : ∀ (n : ℕ), IsClosed[inst✝³] (p.closedBall 0 ↑n)
h₂ : ⋃ n, p.closedBall 0 ↑n = univ
n : ℕ
x : E
hxn : x ∈ interior (p.closedBall 0 ↑n)
⊢ p.closedBall 0 (↑n + ↑n) ∈ 𝓝 0

Tactic:
rw [p.closedBall_zero_eq] at hxn ⊢

Goal state after:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ⇑p
h₁ : ∀ (n : ℕ), IsClosed[inst✝³] (p.closedBall 0 ↑n)
h₂ : ⋃ n, p.closedBall 0 ↑n = univ
n : ℕ
x : E
hxn : x ∈ interior {y | p y ≤ ↑n}
⊢ {y | p y ≤ ↑n + ↑n} ∈ 𝓝 0
Module: Mathlib.Analysis.LocallyConvex.Barrelled

Goal state before:
pp: ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : IsUniformAddGroup E
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst✝ : PolynormableSpace 𝕜₂ F
H : ∀ (x : E), IsVonNBounded 𝕜₂ (range fun i ↦ (𝓕 i) x)
hp : WithSeminorms fun p ↦ ↑p
⊢ ∀ (k : { p // Continuous[inst✝⁵.toTopologicalSpace, _] ⇑p }) (x : E), BddAbove (range fun i ↦ ↑k ((𝓕 i) x))

Tactic:
simp_rw [hp.isVonNBounded_iff_seminorm_bddAbove, ← range_comp] at H

Goal state after:
ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : IsUniformAddGroup E
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst✝ : PolynormableSpace 𝕜₂ F
hp : WithSeminorms fun p ↦ ↑p
H : ∀ (x : E) (i : { p // Continuous[inst✝⁵.toTopologicalSpace, _] ⇑p }), BddAbove (range (⇑↑i ∘ fun i ↦ (𝓕 i) x))
⊢ ∀ (k : { p // Continuous[inst✝⁵.toTopologicalSpace, _] ⇑p }) (x : E), BddAbove (range fun i ↦ ↑k ((𝓕 i) x))
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
c : CU P
y : X
hxl : x ∉ c.left.left.U
hyl : y ∉ c.left.left.U
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ r
hydl : dist (c.left.right.lim y) (c.left.right.lim x) ≤ r
hydr : dist (c.right.lim y) (c.right.lim x) ≤ r
⊢ (dist (c.left.right.lim y) (c.left.right.lim x) / 2 + dist (c.right.lim y) (c.right.lim x)) / 2 ≤ r * (3 / 4)

Tactic:
calc _ ≤ (r / 2 + r) / 2 := by gcongr
        _ = _ := by ring

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

Goal state before:
pp: A : Type u_1
inst✝ : CommCStarAlgebra A
⊢ ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
    a ∈ (gelfandTransform ℂ A).range.carrier → star a ∈ (gelfandTransform ℂ A).range.carrier

Tactic:
rintro - ⟨a, rfl⟩

Goal state after:
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
⊢ star ((gelfandTransform ℂ A).toRingHom a) ∈ (gelfandTransform ℂ A).range.carrier