mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖((((algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1) b)⋆ + (((mul 𝕜 E) x.toProd.2) b)⋆) *
        (((algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1) b + ((mul 𝕜 E) x.toProd.2) b)‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1 + (mul 𝕜 E) (x⋆ * x).toProd.2‖

Tactic:
mul_apply',

Goal state after:
𝕜 : 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
⊢ ‖((((algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1) b)⋆ + (x.toProd.2 * b)⋆) *
        (((algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1) b + x.toProd.2 * b)‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1 + (mul 𝕜 E) (x⋆ * x).toProd.2‖
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
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f g : C(X, ℝ)₀
⊢ φ (f * g).toNNReal - φ (-(f * g)).toNNReal = (φ f.toNNReal - φ (-f).toNNReal) * (φ g.toNNReal - φ (-g).toNNReal)

Tactic:
have := congr(φ $(f.toNNReal_mul_add_neg_mul_add_mul_neg_eq g))
    simp only [map_add, map_mul, sub_mul, mul_sub] at this ⊢
    rw [← sub_eq_zero] at this ⊢
    rw [← this]
    abel

Goal state after:
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
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖x.toProd.1⋆ • b⋆ * (x.toProd.1 • b + x.toProd.2 * b) + b⋆ * x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1 + (mul 𝕜 E) (x⋆ * x).toProd.2‖

Tactic:
smul_mul_assoc,

Goal state after:
𝕜 : 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.toProd.1⋆ • (b⋆ * (x.toProd.1 • b + x.toProd.2 * b)) + b⋆ * x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).toProd.1 + (mul 𝕜 E) (x⋆ * x).toProd.2‖
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
⊢ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ∩ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)) =
    ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})

Tactic:
ext f
  constructor
  · rintro ⟨hf₁, hf₂⟩
    rw [SetLike.mem_coe] at hf₂ ⊢
    simp_rw [adjoin_id_eq_span_one_add, Set.mem_add, SetLike.mem_coe, mem_span_singleton] at hf₁
    obtain ⟨-, ⟨r, rfl⟩, f, hf, rfl⟩ := hf₁
    have := nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom h0 hf
    simp only [SetLike.mem_coe, RingHom.mem_ker, evalStarAlgHom_apply] at hf₂ this
    rw [add_apply, this, add_zero, smul_apply, one_apply, smul_eq_mul, mul_one] at hf₂
    rwa [hf₂, zero_smul, zero_add]
  · simp only [Set.mem_inter_iff, SetLike.mem_coe]
    refine fun hf ↦ ⟨?_, nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom h0 hf⟩
    exact adjoin_le_starAlgebra_adjoin _ _ hf

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

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

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

Tactic:
all_goals assumption

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_mul_assoc,

Goal state after:
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
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
⊢ UpperHemicontinuousAt (fun x ↦ {f x}) x ↔ ContinuousAt f x

Tactic:
simp [← upperHemicontinuousWithinAt_univ_iff, continuousWithinAt_univ]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : UpperHemicontinuous f
hg : UpperHemicontinuous g
⊢ UpperHemicontinuous fun x ↦ f x ∪ g x

Tactic:
rw [upperHemicontinuous_iff] at hf hg ⊢

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : ∀ (x : α), UpperHemicontinuousAt f x
hg : ∀ (x : α), UpperHemicontinuousAt g x
⊢ ∀ (x : α), UpperHemicontinuousAt (fun x ↦ f x ∪ g x) x
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
⊢ NoncompactSpace (Closeds α) ↔ NoncompactSpace α

Tactic:
simp_rw [← not_compactSpace_iff, compactSpace_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → Set β
hs : IsPreconnected s
hf : ContinuousOn f s
h : ∃ x ∈ s, IsPreconnected (f x)
⊢ IsPreconnected (⋃ x ∈ s, f x)

Tactic:
rw [← sUnion_image]
  exact isPreconnected_sUnion (hs.image _ hf) (by grind)

Goal state after:
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
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ IsGreatest ((fun x ↦ ‖f x‖) '' σ 𝕜 a) ‖cfc f a‖

Tactic:
obtain ⟨x, hx⟩ := ContinuousFunctionalCalculus.isCompact_spectrum a
    |>.image_of_continuousOn hf.norm |>.exists_isGreatest <|
    (ContinuousFunctionalCalculus.spectrum_nonempty a ha).image _
  obtain ⟨x, hx', rfl⟩ := hx.1
  convert! hx
  rw [cfc_apply f a, norm_cfcHom a _]
  apply le_antisymm
  · apply ContinuousMap.norm_le _ (norm_nonneg _) |>.mpr
    rintro ⟨y, hy⟩
    exact hx.2 ⟨y, hy, rfl⟩
  · exact le_trans (by simp) <| ContinuousMap.norm_coe_le_norm _ (⟨x, hx'⟩ : σ 𝕜 a)

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
⊢ p 0

Tactic:
by
    rw [← hp₁, Unitization.inr_zero 𝕜]
    exact cfc_predicate_zero 𝕜

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

Goal state before:
pp: case inl
𝕜 : 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✝ : Subsingleton A
⊢ ‖cfc f a‖ ≤ c

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
⊢ ‖cfc f a‖ ≤ c

Tactic:
· simpa [Subsingleton.elim (cfc f a) 0]

Goal state after:
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
⊢ ‖cfc f a‖ ≤ c
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ SetLike.coe ⁻¹' closure[TopologicalSpace.vietoris α] (SetLike.coe '' SetLike.coe ⁻¹' {K | K.Finite ∧ K ⊆ s}) =
    SetLike.coe ⁻¹' 𝒫 closure[inst✝] s

Tactic:
image_preimage_eq_of_subset ?_,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ SetLike.coe ⁻¹' closure[TopologicalSpace.vietoris α] {K | K.Finite ∧ K ⊆ s} = SetLike.coe ⁻¹' 𝒫 closure[inst✝] s

α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ {K | K.Finite ∧ K ⊆ s} ⊆ range SetLike.coe
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inl
𝕜 : 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✝ : Subsingleton A
⊢ ‖cfc f a‖ < c

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
⊢ ‖cfc f a‖ < c

Tactic:
· simpa [Subsingleton.elim (cfc f a) 0]

Goal state after:
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
⊢ ‖cfc f a‖ < c
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst✝⁶ : NormedField 𝕜₁
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜₁ A
inst✝² : NormedAlgebra 𝕜₂ A
inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂
inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊
y : 𝕜₁
hy : y ∈ spectrum 𝕜₁ a
hx : (algebraMap 𝕜₁ 𝕜₂) y ∈ spectrum 𝕜₂ a
⊢ ↑‖(algebraMap 𝕜₁ 𝕜₂) y‖₊ ≤ ⨆ k ∈ spectrum 𝕜₁ a, ↑‖k‖₊

Tactic:
exact this y ▸ le_iSup₂ (α := ℝ≥0∞) y hy

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module ℝ A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx : x ∈ σₙ ℝ a
⊢ √x * √x = id x

Tactic:
rw [QuasispectrumRestricts.nnreal_iff] at ha₂

Goal state after:
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module ℝ A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : ∀ x ∈ σₙ ℝ a, 0 ≤ x
x : ℝ
hx : x ∈ σₙ ℝ a
⊢ √x * √x = id x
Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
⊢ HasFDerivAt (fun x ↦ resolvent x k) (((ContinuousLinearMap.mulLeftRight 𝕜 A) (resolvent a k)) (resolvent a k)) a

Tactic:
by
  have H₁ : HasFDerivAt Ring.inverse _ (algebraMap 𝕜 A k - a) :=
    hasFDerivAt_ringInverse (𝕜 := 𝕜) hk.unit
  have H₂ : HasFDerivAt (fun a => algebraMap 𝕜 A k - a) (- .id 𝕜 A) a := by
    simpa using! (hasFDerivAt_const _ a).sub (hasFDerivAt_id a)
  simpa [resolvent_eq hk] using! H₁.comp a H₂

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

Goal state before:
pp: A : Type u_2
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra ℂ A
hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0
a : A
z : ℂ
h : ¬(algebraMap ℂ A) z - a ≠ 0
⊢ (algebraMap ℂ A) z = a

Tactic:
Classical.not_not,

Goal state after:
A : Type u_2
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra ℂ A
hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0
a : A
z : ℂ
h : (algebraMap ℂ A) z - a = 0
⊢ (algebraMap ℂ A) z = a
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ NoncompactSpace (Compacts α) ↔ NoncompactSpace α

Tactic:
simp_rw [← not_compactSpace_iff, compactSpace_iff]

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✝ : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
hU : U ∈ 𝓝 K
⊢ ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s

Tactic:
isTopologicalBasis.mem_nhds_iff,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
hU :
  ∃ t ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝³] U},
    K ∈ t ∧ t ⊆ U
⊢ ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp (z • star b) * x * NormedSpace.exp (z • star (-a)) =
    ↑(expUnitary (2 • ℑ (z • star b))) * x * ↑(expUnitary (2 • ℑ (star z • a)))

Tactic:
← (h.smul_right (star z)).exp_neg_mul_mul_exp_eq_self

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp (z • star b) * (NormedSpace.exp (-(star z • b)) * x * NormedSpace.exp (star z • a)) *
      NormedSpace.exp (z • star (-a)) =
    ↑(expUnitary (2 • ℑ (z • star b))) * x * ↑(expUnitary (2 • ℑ (star z • a)))
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ NoncompactSpace (NonemptyCompacts α) ↔ NoncompactSpace α

Tactic:
simp_rw [← not_compactSpace_iff, compactSpace_iff]

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 →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
⊢ (∀ (i : Fin 1), Continuous[t₁, _] ⇑((normSeminorm 𝕜 𝕜).comp φ)) ↔
    ∃ s, ∀ (i : Fin 1), Continuous[t₂ s, _] ⇑((normSeminorm 𝕜 𝕜).comp φ)

Tactic:
forall_const

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
t₁ : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
⊢ Continuous[t₁, _] ⇑((normSeminorm 𝕜 𝕜).comp φ) ↔ ∃ s, Continuous[t₂ s, _] ⇑((normSeminorm 𝕜 𝕜).comp φ)
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
⊢ ‖fr.extendRCLike x‖ ≤ p x

Tactic:
by_cases hx : fr.extendRCLike (𝕜 := 𝕜) x = 0

Goal state after:
case pos
𝕜 : 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
⊢ ‖fr.extendRCLike x‖ ≤ p x

case neg
𝕜 : 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
⊢ ‖fr.extendRCLike x‖ ≤ p x
Module: Mathlib.Analysis.LocallyConvex.WeakDual

Goal state before:
pp: case mp
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
this✝ : IsTopologicalAddGroup E
this : WithSeminorms fun i ↦ (f i).toSeminorm
H : ∀ (i : Fin 1), Continuous[⨅ i, induced (⇑(f i)) inferInstance, _] ⇑((normSeminorm 𝕜 𝕜).comp φ)
⊢ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm

Tactic:
forall_const

Goal state after:
case mp
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
this✝ : IsTopologicalAddGroup E
this : WithSeminorms fun i ↦ (f i).toSeminorm
H : Continuous[⨅ i, induced (⇑(f i)) inferInstance, _] ⇑((normSeminorm 𝕜 𝕜).comp φ)
⊢ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm
Module: Mathlib.Analysis.LocallyConvex.WeakDual

Goal state before:
pp: 𝕜 : Type u_5
E : Type u_6
F : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
f : StrongDual 𝕜 (WeakBilin B)
⊢ ↑f ∈ Submodule.span 𝕜 ↑(ContinuousLinearMap.coeLM 𝕜 ∘ₗ WeakBilin.eval B).range

Tactic:
simpa [coe_range, mem_span_iff_continuous, continuous_iff_le_induced, ← induced_to_pi] using!
      f.continuous.le_induced

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ spectrum 𝕜 f = Set.range ⇑f

Tactic:
spectrum_eq_preimage_range,

Goal state after:
X : Type u_1
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ ⇑(algebraMap 𝕜 𝕜) ⁻¹' Set.range ⇑f = Set.range ⇑f
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx n c x
c : CU P
⊢ 0 ≤ ⅟2 • (approx n c.left x + approx n c.right x)

Tactic:
refine mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg ?_ ?_) <;> apply ihn

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

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : T2Space R
s : Set X
⊢ IsClosed ↑(idealOfSet R s)

Tactic:
simp only [idealOfSet, Submodule.coe_set_mk, Set.ofPred_forall]
  exact isClosed_iInter fun x => isClosed_iInter fun _ =>
    isClosed_eq (continuous_eval_const x) continuous_const

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (⇑g) 0 s
hgt : EqOn (⇑g) 1 t
hicc : ∀ (x : X), 0 ≤ g x ∧ g x ≤ 1
x : X
hx : x ∈ s
⊢ g x = 0

Tactic:
exact hgs hx

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] sᶜᶜ)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen[inst✝¹] u
hvIsOpen : IsOpen[inst✝¹] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst✝¹] u ⊆ vᶜ
P : Set X → Set X → Prop := fun C x ↦ sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed[inst✝¹] c
⊢ P c u0 →
    IsOpen[inst✝¹] u0 →
      c ⊆ u0 → ∃ v, IsOpen[inst✝¹] v ∧ c ⊆ v ∧ closure[inst✝¹] v ⊆ u0 ∧ P c v ∧ P (closure[inst✝¹] v) u0

Tactic:
Pc

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] sᶜᶜ)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen[inst✝¹] u
hvIsOpen : IsOpen[inst✝¹] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst✝¹] u ⊆ vᶜ
P : Set X → Set X → Prop := fun C x ↦ sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed[inst✝¹] c
Pc : P c u0
⊢ IsOpen[inst✝¹] u0 → c ⊆ u0 → ∃ v, IsOpen[inst✝¹] v ∧ c ⊆ v ∧ closure[inst✝¹] v ⊆ u0 ∧ P c v ∧ P (closure[inst✝¹] v) u0