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✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
⊢ cfc (fun x ↦ -f x) a = -cfc f a

Tactic:
by_cases h : p a ∧ ContinuousOn f (spectrum R a)

Goal state after:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : p a ∧ ContinuousOn f (spectrum R a)
⊢ cfc (fun x ↦ -f x) a = -cfc f a

case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
⊢ cfc (fun x ↦ -f x) a = -cfc f a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case pos
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ₙHom ⋯) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ⋯) { toFun := (σₙ R a).domRestrict g, continuous_toFun := ⋯, map_zero' := ⋯ }

Tactic:
congr 3

Goal state after:
case pos.e_6
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
⊢ (σₙ R a).domRestrict f = (σₙ R a).domRestrict g
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
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Set.Icc a b
⊢ ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) = ENNReal.ofReal (f (u n) - f (u 0))

Tactic:
rw [sum_range_sub (f <| u ·)]

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

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

Tactic:
nth_rw 2 [← cfcₙ_zero R 0]
    apply cfcₙ_congr
    simpa [CFC.quasispectrum_zero_eq]

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

Goal state before:
pp: case pos.right
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 := ⋯
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := ⋯
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := ⋯
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := ⋯
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯
xs_w : ⋃ x ∈ xs, W x = ⊤ := ⋯
xs_nonempty : xs.Nonempty
k : ↑L := ⋯
z : X
⊢ f z - ε < ↑k z

Tactic:
simp only [k, Finset.lt_inf'_iff, ContinuousMap.inf'_apply]

Goal state after:
case pos.right
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, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := fun x ↦ {z | ↑(h x) z < f z + ε}
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯.choose
xs_w : ⋃ x ∈ xs, W x = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhds)
xs_nonempty : xs.Nonempty
k : ↑L := ⟨xs.inf' xs_nonempty fun x ↦ ↑(h x), ⋯⟩
z : X
⊢ ∀ i ∈ xs, f z - ε < ↑(h i) z
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: case neg
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
r : ℝ
f : C(X, ℝ)₀
hr : r < 0
⊢ φ (r • f).toNNReal - φ (-(r • f)).toNNReal = r • (φ f.toNNReal - φ (-f).toNNReal)

Tactic:
← neg_pos

Goal state after:
case neg
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
r : ℝ
f : C(X, ℝ)₀
hr : 0 < -r
⊢ φ (r • f).toNNReal - φ (-(r • f)).toNNReal = r • (φ f.toNNReal - φ (-f).toNNReal)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁹ : TopologicalSpace X
inst✝⁸ : Zero X
A : Type u_2
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsSemitopologicalRing A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this : Fact (0 ∈ s')
e0 : e 0 = 0
⊢ φ = ψ

Tactic:
have e0' : e.symm 0 = 0 := e.symm_apply_eq.mpr e0

Goal state after:
X : Type u_1
inst✝⁹ : TopologicalSpace X
inst✝⁸ : Zero X
A : Type u_2
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsSemitopologicalRing A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this : Fact (0 ∈ s')
e0 : e 0 = 0
e0' : e.symm 0 = 0
⊢ φ = ψ
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
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖

Tactic:
simp_rw [unitization_norm_def, add_mul, mul_add, unitization_mul, fst_mul, snd_mul]

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
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.1 * y.ofLp.toProd.1‖ +
      ‖x.ofLp.toProd.1 • y.ofLp.toProd.2 + y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
      (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case mem
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f✝¹ f✝ f : C(↑s, 𝕜)
hf : f ∈ {(toContinuousMapOnAlgHom s) X} ∪ star {(toContinuousMapOnAlgHom s) X}
⊢ p f

Tactic:
| mem f hf =>

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

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

Tactic:
| mem f hf =>

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

Goal state before:
pp: case mem
𝕜 : 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✝ f : C(↑s, 𝕜)₀
hf : f ∈ {ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s}
⊢ p f

Tactic:
| mem f hf =>

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

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

Tactic:
rw [← inter_eq_left, inter_union_distrib_left] at ht₂

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ : t ∩ powerset '' {U | IsOpen[inst✝] U} ∪ t ∩ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V} = t
s : Set α
hs : s ∈ ⋂₀ t
h✝ : s.Nonempty
⊢ ∃ u v,
    u ⊆ powerset '' {U | IsOpen[inst✝] U} ∧ v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U} ∧ u ∪ v = t
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
⊢ t ⊆ V.image (U.image s ∩ V.preimage t)

Tactic:
intro z hz

Goal state after:
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
⊢ z ∈ V.image (U.image s ∩ V.preimage t)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ ↑t, {x | (x, y) ∈ Prod.swap ⁻¹' U}
⊢ ∃ t, (↑t, s) ∈ hausdorffEntourage U

Tactic:
refine ⟨{x ∈ t | ∃ y ∈ s, (x, y) ∈ U}, ?_⟩
  rw [Finset.coe_filter]
  refine ⟨fun _ h => h.2, fun x hx => ?_⟩
  obtain ⟨y, hy, hxy⟩ := Set.mem_iUnion₂.mp (ht₂ hx)
  exact ⟨y, ⟨hy, x, hx, hxy⟩, hxy⟩

Goal state after:
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✝ : DiscreteUniformity α
⊢ SetRel.id ∈ 𝓤 (Set α)

Tactic:
convert! Filter.mem_lift' (DiscreteUniformity.relId_mem_uniformity α)

Goal state after:
case e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : DiscreteUniformity α
⊢ SetRel.id = hausdorffEntourage SetRel.id
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
⊢ (↑‖a‖₊)⁻¹ ≤ radius fun n ↦ ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)

Tactic:
refine le_of_forall_nnreal_lt fun r hr =>
        le_radius_of_bound_nnreal _ (max 1 ‖(1 : A)‖₊) fun n => ?_
      rw [← norm_toNNReal, norm_mkPiRing, norm_toNNReal]
      rcases n with - | n
      · simp
      · grw [nnnorm_pow_le' a n.succ_pos, ← le_max_left]
        by_cases h : ‖a‖₊ = 0
        · simp [h, pow_succ']
        · rw [← coe_inv h, coe_lt_coe, NNReal.lt_inv_iff_mul_lt h] at hr
          simpa only [← mul_pow, mul_comm] using! pow_le_one' hr.le n.succ

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : IsCompact s
⊢ ∀
    i ∈
      {s_1 |
        s ∈ s_1 ∧
          s_1 ∈
            Set.powerset '' {U | IsOpen[inst✝.toTopologicalSpace] U} ∪
              (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝.toTopologicalSpace] U}},
    i ∈ 𝓝 s

Tactic:
rintro _ ⟨hs', (⟨U, hU, rfl⟩ | ⟨U, hU, rfl⟩)⟩

Goal state after:
case inl
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : U ∈ {U | IsOpen[inst✝.toTopologicalSpace] U}
hs' : s ∈ 𝒫 U
⊢ 𝒫 U ∈ 𝓝 s

case inr
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : U ∈ {U | IsOpen[inst✝.toTopologicalSpace] U}
hs' : s ∈ (fun V ↦ {s | (s ∩ V).Nonempty}) U
⊢ (fun V ↦ {s | (s ∩ V).Nonempty}) U ∈ 𝓝 s
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n ↦ (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
h₃ : exp (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b
⊢ ¬IsUnit (↑ₐ (exp z) - exp a)

Tactic:
IsUnit.sub_iff,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n ↦ (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
h₃ : exp (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b
⊢ ¬IsUnit (exp a - ↑ₐ (exp z))
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
⊢ s ⤳ t

Tactic:
· simp_rw [Specializes, nhds_generateFrom, le_iInf₂_iff]
    rintro _ ⟨hs, ⟨U, hU, rfl⟩ | ⟨U, hU, rfl⟩⟩
    · refine iInf₂_le U.powerset ⟨fun x hx => ?_, .inl <| mem_image_of_mem _ hU⟩
      obtain ⟨y, hyt, hxy⟩ := hst x hx
      exact hxy.mem_open hU <| hs hyt
    · obtain ⟨x, hxt, hxU⟩ := hs
      obtain ⟨y, hyU, hys⟩ := mem_closure_iff.mp (hts hxt) U hU hxU
      exact iInf₂_le {t | (t ∩ U).Nonempty} ⟨⟨y, hys, hyU⟩, .inr <| mem_image_of_mem _ hU⟩

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

Goal state before:
pp: case refine_2
𝕜 : 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
this : CompleteSpace ↥S
μ : 𝕜
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ ∀ᶠ (x : ↥S) in map (fun x_1 ↦ (algebraMap 𝕜 ↥S) x_1 - x) (𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ), IsUnit x

Tactic:
rw [eventually_map]
    apply Eventually.filter_mono inf_le_right
    simp [spectrum.notMem_iff]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
⊢ ∃ φ,
    Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑φ ∧
      Function.Injective ⇑φ ∧
        φ { toContinuousMap := ContinuousMap.restrict (σₙ 𝕜 a) (ContinuousMap.id 𝕜), map_zero' := ⋯ } = a ∧
          (∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), σₙ 𝕜 (φ f) = Set.range ⇑f) ∧ ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), p (φ f)

Tactic:
have coe_ψ (f : C(σₙ 𝕜 a, 𝕜)₀) : ψ f = cfcₙAux hp₁ a ha f :=
      congr_arg Subtype.val <| (inrRangeEquiv 𝕜 A).apply_symm_apply
        ⟨cfcₙAux hp₁ a ha f, cfcₙAux_mem_range_inr hp₁ a ha f⟩

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
⊢ ∃ φ,
    Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑φ ∧
      Function.Injective ⇑φ ∧
        φ { toContinuousMap := ContinuousMap.restrict (σₙ 𝕜 a) (ContinuousMap.id 𝕜), map_zero' := ⋯ } = a ∧
          (∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), σₙ 𝕜 (φ f) = Set.range ⇑f) ∧ ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), p (φ f)
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
⊢ CompactSpace ↑(σₙ 𝕜 a)

Tactic:
have h_cpct : CompactSpace (spectrum 𝕜 a) := inferInstance

Goal state after:
𝕜 : 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
h_cpct : CompactSpace ↑(σ 𝕜 a)
⊢ CompactSpace ↑(σₙ 𝕜 a)
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: case e'_2
A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A
x : ℝ
u : ↥(unitary A) := ⟨NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a), ⋯⟩
⊢ NormedSpace.exp (-x • a) * NormedSpace.exp (x • star a) = ↑(star u)

pp: case e'_3
A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A
x : ℝ
u : ↥(unitary A) := ⟨NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a), ⋯⟩
⊢ NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a) = ↑u⁻¹

Tactic:
· simp [u, star_exp]

Goal state after:
case e'_3
A : Type u_1
inst✝ : CStarAlgebra A
a : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A
x : ℝ
u : ↥(unitary A) := ⟨NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a), ⋯⟩
⊢ NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a) = ↑u⁻¹
Module: Mathlib.Analysis.LocallyConvex.WeakDual

Goal state before:
pp: ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
⊢ φ ∈ Submodule.span 𝕜 (Set.range f) ↔ Continuous[⨅ i, induced (⇑(f i)) inferInstance, inferInstance] ⇑φ

Tactic:
let t𝕜 : TopologicalSpace 𝕜 := inferInstance

Goal state after:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
⊢ φ ∈ Submodule.span 𝕜 (Set.range f) ↔ Continuous[⨅ i, induced (⇑(f i)) inferInstance, inferInstance] ⇑φ
Module: Mathlib.Analysis.Normed.Module.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
fr : Dual ℝ E
p : Seminorm 𝕜 E
hp : ∀ (x : E), |fr x| ≤ p x
x : E
hx : ¬fr.extendRCLike x = 0
hsq : ‖fr.extendRCLike x‖ ^ 2 ≤ ‖fr.extendRCLike x‖ * p x
⊢ ‖fr.extendRCLike x‖ * ‖fr.extendRCLike x‖ ≤ p x * ‖fr.extendRCLike x‖

Tactic:
simpa [pow_two, mul_comm] using hsq

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

Goal state before:
pp: ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
⊢ φ ∈ Submodule.span 𝕜 (Set.range f) ↔ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm

Tactic:
let t𝕜 : TopologicalSpace 𝕜 := inferInstance

Goal state after:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
⊢ φ ∈ Submodule.span 𝕜 (Set.range f) ↔ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm
Module: Mathlib.Analysis.Normed.Module.WeakDual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ ContinuousLinearMap.uniformSpace.toTopologicalSpace ≤ instTopologicalSpaceWeakDual 𝕜 E

Tactic:
convert! (@toWeakDual_continuous _ _ _ _ (by assumption)).le_induced
  exact induced_id.symm

Goal state after: