mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case refine_2
α : 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)
b : α
hb : b ∈ s ∩ Iio a
this : Nonempty ((n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iio a })
⊢ ⨆ i, ∑ i_1 ∈ Finset.range i.fst, edist (f (↑i.snd (i_1 + 1))) (f (↑i.snd i_1)) + edist (f a) l ≤
    eVariationOn f (s ∩ Iic a)

Tactic:
apply iSup_le

Goal state after:
case refine_2
α : 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)
b : α
hb : b ∈ s ∩ Iio a
this : Nonempty ((n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iio a })
⊢ ∀ (i : (n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iio a }),
    ∑ i_1 ∈ Finset.range i.fst, edist (f (↑i.snd (i_1 + 1))) (f (↑i.snd i_1)) + edist (f a) l ≤
      eVariationOn f (s ∩ Iic 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
f : R → R
a : A
hf : ¬ContinuousOn f (spectrum R a)
⊢ cfc f a = 0

Tactic:
by
  rw [cfc_def, dif_neg (not_and_of_not_right _ hf)]

Goal state after:
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)
⊢ cfc f a = cfc g a

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

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 := ⋯ } = cfc g a
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : CompleteSpace E
inst✝ : DenselyOrdered α
f : α → E
a : α
hf : BoundedVariationOn f univ
⊢ eVariationOn f (Iic a) = eVariationOn f (Iio a) + edist (f a) (Function.leftLim f a)

Tactic:
let : TopologicalSpace α := Preorder.topology α
  have : OrderTopology α := ⟨rfl⟩
  by_cases ha : IsBot a
  · have A : Iic a = {a} := by ext x; grind [ha x]
    have B : Iio a = ∅ := by simp [ha.isMin]
    simp [A, B, leftLim_eq_of_isBot ha]
  have : (𝓝[<] a).NeBot := nhdsLT_neBot_of_exists_lt (by simpa [IsBot] using ha)
  have : eVariationOn f (univ ∩ Iic a) = eVariationOn f (univ ∩ Iio a)
      + edist (f a) (f.leftLim a) := by
    apply eVariationOn_on_inter_Iic_eq_Iio_add_edist (by simpa) (mem_univ _)
    simpa only [univ_inter] using hf.tendsto_leftLim _
  simpa using this

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 g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
⊢ ⨆ p, ∑ i ∈ Finset.range p.fst, edist (g (↑p.snd (i + 1))) (g (↑p.snd i)) ≤ eVariationOn f s

Tactic:
apply iSup_le

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
⊢ ∀ (i : (n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
    ∑ i_1 ∈ Finset.range i.fst, edist (g (↑i.snd (i_1 + 1))) (g (↑i.snd i_1)) ≤ eVariationOn f s
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 g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
h : ¬p a ∨ ¬ContinuousOn g (σₙ R a) ∨ ¬g 0 = 0
⊢ cfcₙ f a = cfcₙ g a

Tactic:
obtain (ha | hg | h0) := h

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

case neg.inr.inl
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 g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
hg : ¬ContinuousOn g (σₙ R a)
⊢ cfcₙ f a = cfcₙ g a

case neg.inr.inr
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 g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
h0 : ¬g 0 = 0
⊢ cfcₙ f a = cfcₙ g a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg.inr.inr
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 g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
h0 : ¬g 0 = 0
⊢ cfcₙ f a = cfcₙ g a

Tactic:
rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero]
      exact fun hf ↦ h0 (hfg (quasispectrum.zero_mem R a) ▸ hf)

Goal state after:
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
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Iic y)) (𝓟 s ⊓ atBot) (𝓝 0)

Tactic:
have : (fun y ↦ eVariationOn f (s ∩ Iic y)) =
      (fun y ↦ eVariationOn (f ∘ ofDual) (ofDual ⁻¹' s ∩ Ici (toDual y))) := by
    ext y
    rw [Ici_toDual, ← preimage_inter, comp_ofDual]
  rw [this]
  exact hf.ofDual.tendsto_eVariationOn_Ici_zero

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n ν : ℕ
| ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν) - ↑(n.choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))

Tactic:
mul_sub

Goal state after:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
| ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) -
    ↑(n + 1) * (↑(n.choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ Function.Injective ⇑(cfcₙHom_of_cfcHom R ha)

Tactic:
by
  refine (cfcHom_injective ha).comp fun f g h ↦ ?_
  ext x
  obtain rfl | hx := eq_or_ne x 0
  · simp
  · have := by simpa [quasispectrum_eq_spectrum_union_zero] using x.prop
    replace := this.resolve_left (Subtype.val_injective.ne_iff.mpr hx)
    congrm($h ⟨x, this⟩)

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

Goal state before:
pp: case calc_1.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
k : ℕ
m : k ∈ Finset.range (n + 1)
⊢ (n • X - ↑k) ^ 2 = ↑(k * (k - 1)) + (1 - ↑(2 * n) * X) * ↑k + ↑(n ^ 2) * X ^ 2

Tactic:
simp only [← natCast_mul, push_cast]

Goal state after:
case calc_1.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
k : ℕ
m : k ∈ Finset.range (n + 1)
⊢ (↑n * X - ↑k) ^ 2 = ↑k * ↑(k - 1) + (1 - 2 * ↑n * X) * ↑k + ↑n ^ 2 * X ^ 2
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case calc_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
⊢ ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1 = n • X * (1 - X)

Tactic:
simp only [← natCast_mul, push_cast]

Goal state after:
case calc_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
⊢ ↑n * ↑(n - 1) * X ^ 2 + (1 - 2 * ↑n * X) * (↑n * X) + ↑n ^ 2 * X ^ 2 * 1 = ↑n * X * (1 - X)
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case star
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f = 0
⊢ (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) (star f) = 0

Tactic:
map_star,

Goal state after:
case star
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f = 0
⊢ star ((evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f) = 0
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✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
⊢ { toFun := fun φ ↦ φ 1, continuous_toFun := ⋯ } = 1

Tactic:
by ext a; simp only [coe_mk, coe_one, Pi.one_apply, map_one a]

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

Goal state before:
pp: case refine_1
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁹ : CommSemiring R
inst✝²⁸ : Nontrivial R
inst✝²⁷ : StarRing R
inst✝²⁶ : MetricSpace R
inst✝²⁵ : IsTopologicalSemiring R
inst✝²⁴ : ContinuousStar R
inst✝²³ : CommRing S
inst✝²² : Algebra R S
inst✝²¹ : NonUnitalRing A
inst✝²⁰ : StarRing A
inst✝¹⁹ : TopologicalSpace A
inst✝¹⁸ : Module R A
inst✝¹⁷ : IsScalarTower R A A
inst✝¹⁶ : SMulCommClass R A A
inst✝¹⁵ : NonUnitalRing B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Module R B
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : SMulCommClass R B B
inst✝⁹ : Module S A
inst✝⁸ : Module S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus R A p
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMapZero.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst✝¹⁹, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R ↑φ
this : Continuous[inst✝¹⁹, inst✝¹³] ⇑ψ
h_spec : quasispectrum R (φ a) ⊆ quasispectrum R a
hψa : q (ψ a)
ι : C(↑(quasispectrum R (ψ a)), ↑(quasispectrum R a))₀ :=
  { toFun := Set.inclusion h_spec, continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Continuous[_, inst✝¹³] ⇑(ψ.comp (cfcₙHom ha))

Tactic:
dsimp [ContinuousMapZero.nonUnitalStarAlgHom_precomp]
    fun_prop

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

Goal state before:
pp: case refine_2
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁹ : CommSemiring R
inst✝²⁸ : Nontrivial R
inst✝²⁷ : StarRing R
inst✝²⁶ : MetricSpace R
inst✝²⁵ : IsTopologicalSemiring R
inst✝²⁴ : ContinuousStar R
inst✝²³ : CommRing S
inst✝²² : Algebra R S
inst✝²¹ : NonUnitalRing A
inst✝²⁰ : StarRing A
inst✝¹⁹ : TopologicalSpace A
inst✝¹⁸ : Module R A
inst✝¹⁷ : IsScalarTower R A A
inst✝¹⁶ : SMulCommClass R A A
inst✝¹⁵ : NonUnitalRing B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Module R B
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : SMulCommClass R B B
inst✝⁹ : Module S A
inst✝⁸ : Module S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus R A p
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMapZero.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst✝¹⁹, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R ↑φ
this : Continuous[inst✝¹⁹, inst✝¹³] ⇑ψ
h_spec : quasispectrum R (φ a) ⊆ quasispectrum R a
hψa : q (ψ a)
ι : C(↑(quasispectrum R (ψ a)), ↑(quasispectrum R a))₀ :=
  { toFun := Set.inclusion h_spec, continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Continuous[_, inst✝¹³] ⇑((cfcₙHom hψa).comp (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι))

Tactic:
dsimp [ContinuousMapZero.nonUnitalStarAlgHom_precomp]
    fun_prop

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

Goal state before:
pp: F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst✝¹³ : CommRing K
inst✝¹² : Ring A
inst✝¹¹ : Algebra K A
inst✝¹⁰ : TopologicalSpace K
inst✝⁹ : T1Space K
inst✝⁸ : TopologicalSpace A
inst✝⁷ : ContinuousSub A
inst✝⁶ : ContinuousSMul K A
inst✝⁵ : FunLike F A K
inst✝⁴ : AlgHomClass F K A K
inst✝³ : SetLike S A
inst✝² : OneMemClass S A
inst✝¹ : AddSubgroupClass S A
inst✝ : SMulMemClass S K A
φ : F
hφ : Continuous[inst✝⁸, inst✝¹⁰] ⇑φ
s : S
⊢ closure[inst✝⁸] (↑s ∩ ↑(RingHom.ker φ)) = closure[inst✝⁸] ↑s ∩ ↑(RingHom.ker φ)

Tactic:
by
  refine subset_antisymm ?_ ?_
  · simpa only [ker_eq, (isClosed_singleton.preimage hφ).closure_eq]
      using closure_inter_subset_inter_closure s (ker φ : Set A)
  · intro x ⟨hxs, (hxφ : φ x = 0)⟩
    rw [mem_closure_iff_clusterPt, ClusterPt] at hxs
    have : Tendsto (fun y ↦ y - φ y • 1) (𝓝 x ⊓ 𝓟 s) (𝓝 x) := by
      conv => congr; rfl; rfl; rw [← sub_zero x, ← zero_smul K 1, ← hxφ]
      exact Filter.tendsto_inf_left (Continuous.tendsto (by fun_prop) x)
    refine mem_closure_of_tendsto this <| eventually_inf_principal.mpr ?_
    filter_upwards [] with g hg using
      ⟨sub_mem hg (SMulMemClass.smul_mem _ <| one_mem _), by simp [RingHom.mem_ker]⟩

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

Goal state before:
pp: case smul
𝕜 : 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 ⇑φ
r✝ : 𝕜
f✝ : C(↑s, 𝕜)₀
h : φ f✝ * a = 0
⊢ φ (r✝ • f✝) * a = 0

Tactic:
| smul _ _ h =>

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

Goal state before:
pp: case smul
𝕜 : 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 ⇑φ
r✝ : 𝕜
f✝ : C(↑s, 𝕜)₀
h : a * φ f✝ = 0
⊢ a * φ (r✝ • f✝) = 0

Tactic:
| smul _ _ h =>

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

Goal state before:
pp: case a
α : Type u_1
U V : SetRel α α
s₁ s₃ : Set α
⊢ (s₁, s₃) ∈ hausdorffEntourage U ○ hausdorffEntourage V → (s₁, s₃) ∈ hausdorffEntourage (U ○ V)

Tactic:
⟨s₂, ⟨h₁₂, h₂₁⟩, ⟨h₂₃, h₃₂⟩⟩

Goal state after:
case a
α : Type u_1
U V : SetRel α α
s₁ s₃ s₂ : Set α
h₁₂ : (s₁, s₂).1 ⊆ U.preimage (s₁, s₂).2
h₂₁ : (s₁, s₂).2 ⊆ U.image (s₁, s₂).1
h₂₃ : (s₂, s₃).1 ⊆ V.preimage (s₂, s₃).2
h₃₂ : (s₂, s₃).2 ⊆ V.image (s₂, s₃).1
⊢ (s₁, s₃) ∈ hausdorffEntourage (U ○ V)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
⊢ 𝓝 (closure[inst✝.toTopologicalSpace] s) = 𝓝 s

Tactic:
simp_rw +singlePass [isUniformInducing_closure.isInducing.nhds_eq_comap, closure_closure]

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : T2Space α
inst✝ : CompleteSpace α
⊢ IsClosed (Set.range toCloseds)

Tactic:
convert! Closeds.isClosed_setOfPred_totallyBounded

Goal state after:
case e'_3
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : T2Space α
inst✝ : CompleteSpace α
⊢ Set.range toCloseds = {s | TotallyBounded ↑s}
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
⊢ frontier (σ 𝕜 x) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 ↑x)ᶜ

Tactic:
frontier_eq_closure_inter_closure

Goal state after:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∩
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 ↑x)ᶜ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: 𝕜 : 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
a : A
ha : p a
this : CompactSpace ↑(σₙ 𝕜 a)
f : ContinuousMapZero (↑(σₙ 𝕜 a)) 𝕜
ι : C(↑(σ 𝕜 a), ↑(σₙ 𝕜 a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
⊢ ∀ (x : ↑(σ 𝕜 a)), ‖((↑f).comp ι) x‖ ≤ ‖↑f‖

Tactic:
rintro ⟨x, hx⟩
      exact (f : C(σₙ 𝕜 a, 𝕜)).norm_coe_le_norm ⟨x, spectrum_subset_quasispectrum 𝕜 a hx⟩

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
⊢ ‖φ a‖₊ ≤ ‖a‖₊

Tactic:
have h (ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B) (x : Unitization ℂ A) :
      ‖ψ x‖₊ ≤ ‖x‖₊ := by
    suffices ∀ {s}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊ by
      refine nonneg_le_nonneg_of_sq_le_sq zero_le ?_
      simp_rw [← nnnorm_star_mul_self, ← map_star, ← map_mul]
      exact this <| .star_mul_self x
    intro s hs
    suffices this : spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s by
      rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
        at this
    exact iSup_le_iSup_of_subset (AlgHom.spectrum_apply_subset ψ s)

Goal state after:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
h : ∀ (ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B) (x : Unitization ℂ A), ‖ψ x‖₊ ≤ ‖x‖₊
⊢ ‖φ a‖₊ ≤ ‖a‖₊
Module: Mathlib.Analysis.LocallyConvex.Polar

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ B.polar s = ⋂ x ∈ s, {y | ‖(B x) y‖ ≤ 1}

Tactic:
by
  ext
  simp only [polar_mem_iff, Set.mem_iInter, Set.mem_ofPred_eq]

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
x : E
⊢ x ∈ ⋂ t, ⋂ (_ : s ⊆ t), ⋂ (_ : AbsConvex 𝕜 t), t ↔ ∀ (t : Set E), s ⊆ t → AbsConvex 𝕜 t → x ∈ t

Tactic:
mem_iInter

Goal state after:
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
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ZeroLEOneClass 𝕜
⊢ (𝓝 0).HasBasis (fun s ↦ s ∈ 𝓝 0 ∧ IsClosed[inst✝⁴] s ∧ AbsConvex 𝕜 s) id

Tactic:
by
  refine (nhds_basis_opens 0).to_hasBasis ?_
    fun s ⟨hs_nhds, _, _⟩ ↦ ⟨interior s,
      by simp [interior_subset, mem_interior_iff_mem_nhds.mpr hs_nhds]⟩
  intro s ⟨hs_zero, hs_open⟩
  obtain ⟨W, hW_open, hW_zero, hW_add⟩ :=
    exists_open_nhds_zero_add_subset (hs_open.mem_nhds hs_zero)
  obtain ⟨V, ⟨hV_zero, hV_open, hV_abs⟩, hVW⟩ :=
    (nhds_hasBasis_absConvex_open 𝕜 E).mem_iff.mp (hW_open.mem_nhds hW_zero)
  exact ⟨closure V,
    ⟨Filter.mem_of_superset (hV_open.mem_nhds hV_zero) subset_closure, isClosed_closure,
     hV_abs.closure⟩,
    (closure_subset_add_self_of_mem_nhds_zero (hV_open.mem_nhds hV_zero)).trans
      ((add_subset_add hVW hVW).trans hW_add)⟩

Goal state after: