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✝⁸ : 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 f a = (cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }

Tactic:
by
  rw [cfc_def, dif_pos ⟨ha, hf⟩]

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
f g : R → R
a : A
h : cfc f a = cfc g a
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ Set.EqOn f g (spectrum R a)

Tactic:
rw [cfc_apply f a, cfc_apply g a] at h
  exact fun x hx ↦ congr($(cfcHom_injective ha h) ⟨x, hx⟩)

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case hf
α : 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 : α
hx : Tendsto (fun a ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
a : Set α
ha : 0 < μ a
h'a : μ a < ∞
h''a : IntegrableOn f a μ
⊢ Integrable f ((μ a)⁻¹ • μ.restrict a)

Tactic:
exact (integrable_inv_smul_measure ha.ne' h'a.ne).2 h''a

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
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✝¹ : TopologicalSpace A
inst✝ : ContinuousFunctionalCalculus S A q
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
⊢ CompactSpace ↑(spectrum R a)

Tactic:
by
    have := ContinuousFunctionalCalculus.compactSpace_spectrum (R := S) a
    rw [← isCompact_iff_compactSpace] at this ⊢
    simpa using halg.isCompact_preimage this

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
a : A
ha : p a
f_cont : ContinuousOn f (σₙ R a)
f_zero : ¬f 0 = 0
⊢ (σₙ R a).domRestrict f 0 ≠ 0

Tactic:
exact f_zero

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
⊢ k < ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n ν)) = 0

Tactic:
by
  rcases ν with - | ν
  · rintro ⟨⟩
  · rw [Nat.lt_succ_iff]
    induction k generalizing n ν with
    | zero => simp [eval_at_0]
    | succ k ih =>
      simp only [derivative_succ, Function.comp_apply,
        Function.iterate_succ, Polynomial.iterate_derivative_sub,
        Polynomial.iterate_derivative_natCast_mul, Polynomial.eval_mul, Polynomial.eval_natCast,
        Polynomial.eval_sub]
      intro h
      apply mul_eq_zero_of_right
      rw [ih _ _ (Nat.le_of_succ_le h), sub_zero]
      convert! ih _ _ (Nat.pred_le_pred h)
      exact (Nat.succ_pred_eq_of_pos (k.succ_pos.trans_le h)).symm

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

Goal state before:
pp: case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
have w : (W : C(Set.Icc a b, ℝ) → C(I, ℝ)) = W' := rfl

Goal state after:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case calc_1
𝕜 : 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
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ BddAbove
    ((fun x_1 ↦ ‖((algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1 + (mul 𝕜 E) (x⋆ * x).toProd.2) x_1‖) ''
      Metric.closedBall 0 1)

Tactic:
refine ⟨‖(star x * x).fst‖ + ‖(star x * x).snd‖, ?_⟩

Goal state after:
case calc_1
𝕜 : 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
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖(x⋆ * x).toProd.1‖ + ‖(x⋆ * x).toProd.2‖ ∈
    upperBounds
      ((fun x_1 ↦ ‖((algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1 + (mul 𝕜 E) (x⋆ * x).toProd.2) x_1‖) ''
        Metric.closedBall 0 1)
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: 𝕜 : 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
⊢ ‖((splitMul 𝕜 E) (x⋆ * x)).2‖ ≤ ‖((splitMul 𝕜 E) x⋆).2‖ * ‖((splitMul 𝕜 E) x).2‖

Tactic:
rw [map_mul, Prod.snd_mul]
            exact norm_mul_le _ _

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
r : 𝕜
x : WithLp 1 (Unitization 𝕜 A)
⊢ ‖(r • x).ofLp.toProd.1‖ + ‖(r • x).ofLp.toProd.2‖ ≤ ‖r‖ * (‖x.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖)

Tactic:
ofLp_smul,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
r : 𝕜
x : WithLp 1 (Unitization 𝕜 A)
⊢ ‖(r • x.ofLp).toProd.1‖ + ‖(r • x.ofLp).toProd.2‖ ≤ ‖r‖ * (‖x.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖)
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : 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, 𝕜)₀
hf : f ∈ adjoin 𝕜 {ContinuousMapZero.id s}
⊢ p f

Tactic:
induction hf using NonUnitalAlgebra.adjoin_induction with

Goal state after:
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 : Set β), IsOpen[inst✝] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u

Tactic:
apply forall₂_congr

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ ∀ (a : Set β),
    IsOpen[inst✝] a → ((f x ⊆ a → ∀ᶠ (x' : α) in 𝓝[s] x, a ∈ 𝓝ˢ (f x')) ↔ f x ⊆ a → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ a)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case a.refine_2
α : Type u_1
U V : SetRel α α
s t : Set α
hst : s ⊆ (U ○ V).preimage t
hts : t ⊆ (U ○ V).image s
z : α
hz : z ∈ t
x : α
hx : x ∈ s
y : α
hxy : (x, y) ∈ U
hyz : (y, z) ∈ V
⊢ z ∈ V.image (U.image s ∩ V.preimage t)

Tactic:
exact ⟨y, ⟨⟨x, hx, hxy⟩, ⟨z, hz, hyz⟩⟩, hyz⟩

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 : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊
hn : 0 < ↑(n + 1)
⊢ ↑‖k‖₊ ≤ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1))

Tactic:
convert monotone_rpow_of_nonneg (one_div_pos.mpr hn).le nnnorm_pow_le

Goal state after:
case e'_3
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊
hn : 0 < ↑(n + 1)
⊢ ↑‖k‖₊ = (fun x ↦ x ^ (1 / ↑(n + 1))) ↑(‖k‖₊ ^ (n + 1))

case e'_4
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊
hn : 0 < ↑(n + 1)
⊢ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1)) = (fun x ↦ x ^ (1 / ↑(n + 1))) (↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊)
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 : ∀ (n : ι), UpperHemicontinuousOn (F n) s
hf_compact : ∀ x ∈ s, IsCompact (f x)
⊢ UpperHemicontinuousOn f s

Tactic:
by
  -- A function `f` is upper hemicontinuous at `x₀` if for all open `u` with `f x₀ ⊆ u`, then
  -- `f x ⊆ u` for all `x` near `x₀`
  rw [upperHemicontinuousOn_iff_forall_isOpen]
  intro x₀ hx₀s u hu hx₀u
  -- Find an open entourage `U` such that `U ○ U.symm ⊆ u`
  obtain ⟨W, hW, _, hWu⟩ := lebesgue_number_of_compact_open (hf_compact x₀ hx₀s) hu hx₀u
  obtain ⟨V, hV, hVsym, hVcomp⟩ := comp_symm_mem_uniformity_sets hW
  obtain ⟨U, ⟨hUmem, hUopen⟩, hUsub⟩ := uniformity_hasBasis_open.mem_iff.mp hV
  -- Then choose a sufficiently large `N` such that `⟨f x, F N x⟩ ∈ hausdorffEntourage U`
  -- for all `x ∈ s`
  have hHU : hausdorffEntourage U ∈ @uniformity _ (UniformSpace.hausdorff (α := β)) :=
    (mem_lift'_sets monotone_hausdorffEntourage).mpr ⟨U, hUmem, le_refl _⟩
  obtain ⟨N, hN⟩ := (htendsto (hausdorffEntourage U) hHU).exists
  have hFN_image : F N x₀ ⊆ U.image (f x₀) := ((mem_hausdorffEntourage ..).mp (hN x₀ hx₀s)).2
  -- Upper hemicontinuity implies `F N x ⊆ U.image (f x₀)` for `x` near `x₀`
  simp_rw [upperHemicontinuousOn_iff] at hF
  have hFN_uhc : ∀ᶠ x in 𝓝[s] x₀, F N x ⊆ U.image (f x₀) :=
    (hF N x₀ hx₀s).forall_isOpen _ hUopen.relImage hFN_image
  -- For such a nearby `x`, show `f x ⊆ u` by taking `y ∈ f x`,
  filter_upwards [hFN_uhc, self_mem_nhdsWithin] with x hFNx hx_s
  intro y hy
  -- finding a `z ∈ F N x` such that `(y, z) ∈ U` and then some `y₀ ∈ f x₀` such that `⟨y₀, z⟩ ∈ U`
  obtain ⟨z, hzFN, hyz⟩ := ((mem_hausdorffEntourage U (f x) (F N x)).mp (hN x hx_s)).1 hy
  obtain ⟨y₀, hy₀f, hy₀z⟩ := hFNx hzFN
  -- then use that `U ○ U.symm ⊆ u` to conclude
  exact hWu y₀ hy₀f (hVcomp ⟨z, hUsub hy₀z, hVsym.symm _ _ (hUsub hyz)⟩)

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ inst✝ = generateFrom {U | IsOpen[inst✝] U}

Tactic:
generateFrom_setOfPred_isOpen

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ inst✝ = induced (fun x ↦ {x}) (TopologicalSpace.vietoris α)

Tactic:
simp_rw [TopologicalSpace.vietoris, induced_generateFrom_eq, image_union, image_image,
      powerset, preimage_ofPred_eq, singleton_subset_iff, singleton_inter_nonempty, union_self,
      ofPred_mem_eq, image_id', generateFrom_setOfPred_isOpen]

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
hUV : ⋃₀ s ⊆ U ∪ V
ht' : t ⊆ U ∨ t ⊆ V
htU : t ⊆ U
u : Set α
hus : u ∈ s
huV : (u ∩ V).Nonempty
this : s ⊆ 𝒫 U ∪ {v | (v ∩ V).Nonempty}
⊢ (⋃₀ s ∩ (U ∩ V)).Nonempty

Tactic:
obtain ⟨v, hvs, hvU, hvV⟩ :=
      hs _ _ hU.powerset_vietoris (isOpen_inter_nonempty_of_isOpen hV) this
        ⟨t, hts, htU⟩ ⟨u, hus, huV⟩

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
hUV : ⋃₀ s ⊆ U ∪ V
ht' : t ⊆ U ∨ t ⊆ V
htU : t ⊆ U
u : Set α
hus : u ∈ s
huV : (u ∩ V).Nonempty
this : s ⊆ 𝒫 U ∪ {v | (v ∩ V).Nonempty}
v : Set α
hvs : v ∈ s
hvU : v ∈ 𝒫 U
hvV : v ∈ {s | (s ∩ V).Nonempty}
⊢ (⋃₀ s ∩ (U ∩ V)).Nonempty
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
⊢ B.polar Set.univ = {0}

Tactic:
Set.eq_singleton_iff_unique_mem

Goal state after:
𝕜 : 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
⊢ 0 ∈ B.polar Set.univ ∧ ∀ x ∈ B.polar Set.univ, x = 0
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex 𝕜 s
⊢ AbsConvex 𝕜 ((convexHull 𝕜) (balancedCore 𝕜 s))

Tactic:
refine ⟨(balancedCore_balanced s).convexHull, ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex 𝕜 s
⊢ Convex 𝕜 ((convexHull 𝕜) (balancedCore 𝕜 s))
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ IsPreconnected (toCompacts '' {K | (↑K).Finite ∧ ↑K ⊆ s})

Tactic:
convert Compacts.isPreconnected_nonempty_finite_subsets hs

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ toCompacts '' {K | (↑K).Finite ∧ ↑K ⊆ s} = {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ s}
Module: Mathlib.Analysis.Normed.Module.HahnBanach

Goal state before:
pp: case neg
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : ¬‖x‖ = 0
g : StrongDual 𝕜 E
hg : ‖g‖ = 1 ∧ g x = ↑‖x‖
⊢ ∃ g, ‖g‖ ≤ 1 ∧ g x = ↑‖x‖

Tactic:
exact ⟨g, hg.left.le, hg.right⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Module.WeakDual

Goal state before:
pp: α : Type u_4
𝕜 : Type u_5
E : Type u_6
F : Type u_7
inst✝⁵ : TopologicalSpace α
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
g : α → WeakBilin B
h : ∀ (y : F), Continuous[inst✝⁵, _] fun a ↦ re ((B (g a)) y)
⊢ Continuous[inst✝⁵, WeakBilin.instTopologicalSpace B] g

Tactic:
refine WeakBilin.continuous_of_continuous_eval _ fun x ↦ ?_

Goal state after:
α : Type u_4
𝕜 : Type u_5
E : Type u_6
F : Type u_7
inst✝⁵ : TopologicalSpace α
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
g : α → WeakBilin B
h : ∀ (y : F), Continuous[inst✝⁵, _] fun a ↦ re ((B (g a)) y)
x : F
⊢ Continuous[inst✝⁵, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun a ↦ (B (g a)) x
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
⊢ 0 < (1 - r) * (b - a) →
    (f ((lineMap b a) (1 - r)) ≤ (lineMap (f b) (f a)) (1 - r) ↔ slope f a b ≤ slope f ((lineMap b a) (1 - r)) b)

Tactic:
generalize 1 - r = r'

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r r' : k
⊢ 0 < r' * (b - a) → (f ((lineMap b a) r') ≤ (lineMap (f b) (f a)) r' ↔ slope f a b ≤ slope f ((lineMap b a) r') b)
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : ℕ → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s
fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)
f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : ∑' (i : ℕ), u i = 1
⊢ ∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
let g : X → ℝ := fun x ↦ ∑' n, u n * f n x

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : ℕ → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s
fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)
f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : ∑' (i : ℕ), u i = 1
g : X → ℝ := fun x ↦ ∑' (n : ℕ), u n * (f n) x
⊢ ∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : NonUnitalRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
a : A
ha : ¬IsSelfAdjoint a
h : IsSelfAdjoint (-a)
⊢ IsSelfAdjoint a

Tactic:
by simpa using h.neg

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
x : ℂ
⊢ x = 0 ∨ x ∈ spectrum ℂ a → 0 ≤ x

Tactic:
refine (Or.elim · ge_of_eq fun hx ↦ ?_)

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
x : ℂ
x✝ : x = 0 ∨ x ∈ spectrum ℂ a
hx : x ∈ spectrum ℂ a
⊢ 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : CStarRing A
inst✝⁵ : NormedSpace ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
⊢ ‖star b * a * b‖ = ‖star b * sqrt a * sqrt a * b‖

Tactic:
mul_assoc _ _ (CFC.sqrt a),

Goal state after:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : CStarRing A
inst✝⁵ : NormedSpace ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
⊢ ‖star b * a * b‖ = ‖star b * (sqrt a * sqrt a) * b‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : MetricSpace A
inst✝¹ : Algebra R A
inst✝ : IsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ LipschitzOnWith 1 (fun f ↦ cfc ((toFun {spectrum R a}) f) a)
    {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}

Tactic:
intro f hf g hg

Goal state after:
case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : MetricSpace A
inst✝¹ : Algebra R A
inst✝ : IsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{spectrum R a}] R
hf : f ∈ {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}
g : R →ᵤ[{spectrum R a}] R
hg : g ∈ {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}
⊢ edist ((fun f ↦ cfc ((toFun {spectrum R a}) f) a) f) ((fun f ↦ cfc ((toFun {spectrum R a}) f) a) g) ≤ ↑1 * edist f g
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
h : IsUnit (sqrt a)
ha : 0 ≤ a
⊢ IsUnit a

Tactic:
rwa [isUnit_sqrt_iff _ ha] at h

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

Goal state before:
pp: A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ (∃ r > 0, (algebraMap ℝ A) r ≤ a) ↔ ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
by
  have h_cpct : IsCompact (spectrum ℝ a) := isCompact_iff_compactSpace.mpr inferInstance
  simp_rw [algebraMap_le_iff_le_spectrum (a := a)]
  refine ⟨?_, fun h ↦ ?_⟩
  · rintro ⟨r, hr, hr_le⟩
    exact (hr.trans_le <| hr_le · ·)
  · obtain ⟨r, hr, hr_min⟩ := h_cpct.exists_isMinOn
      (ContinuousFunctionalCalculus.spectrum_nonempty a ha) continuousOn_id
    exact ⟨r, h _ hr, hr_min⟩

Goal state after: