mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
⊢ spectralRadius 𝕜 a < (↑‖↑(Units.mk0 z hz)‖₊)⁻¹

Tactic:
lt_inv_iff_lt_inv

Goal state after:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
⊢ ↑‖↑(Units.mk0 z hz)‖₊ < (spectralRadius 𝕜 a)⁻¹
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
⊢ IsUnit (1 - z • a)

Tactic:
let u := Units.mk0 z hz
    suffices hu : IsUnit (u⁻¹ • (1 : A) - a) by
      rwa [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv u] at hu
    rw [Units.smul_def, ← Algebra.algebraMap_eq_smul_one, ← mem_resolventSet_iff]
    refine mem_resolventSet_of_spectralRadius_lt ?_
    rwa [Units.val_inv_eq_inv_val, nnnorm_inv,
      coe_inv (nnnorm_ne_zero_iff.mpr (Units.val_mk0 hz ▸ hz : (u : 𝕜) ≠ 0)), lt_inv_iff_lt_inv]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_4
inst✝ : Finite ι
⊢ (∀ (U : Set α), IsOpen[inst✝¹] U → IsOpen[Pi.topologicalSpace] (range ⁻¹' {t | t ⊆ U})) ∧
    ∀ (F : Set α), IsClosed[inst✝¹] F → IsClosed[Pi.topologicalSpace] (range ⁻¹' {t | t ⊆ F})

Tactic:
preimage_ofPred_eq,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_4
inst✝ : Finite ι
⊢ (∀ (U : Set α), IsOpen[inst✝¹] U → IsOpen[Pi.topologicalSpace] {a | range a ⊆ U}) ∧
    ∀ (F : Set α), IsClosed[inst✝¹] F → IsClosed[Pi.topologicalSpace] {a | range a ⊆ F}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
⊢ (∀ (U : Set β), IsOpen[inst✝] U → IsOpen[TopologicalSpace.vietoris α] ((fun x ↦ f '' x) ⁻¹' {t | t ⊆ U})) ∧
    ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[TopologicalSpace.vietoris α] ((fun x ↦ f '' x) ⁻¹' {t | t ⊆ F})

Tactic:
preimage_ofPred_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
⊢ (∀ (U : Set β), IsOpen[inst✝] U → IsOpen[TopologicalSpace.vietoris α] {a | f '' a ⊆ U}) ∧
    ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[TopologicalSpace.vietoris α] {a | f '' a ⊆ F}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
this : {U | IsOpen[inst✝¹] U} = (fun x ↦ f ⁻¹' x) '' {V | IsOpen[inst✝] V}
⊢ generateFrom
      ((fun x ↦ {t | t ⊆ f ⁻¹' x}) '' {V | IsOpen[inst✝] V} ∪
        (fun x ↦ {s | (s ∩ f ⁻¹' x).Nonempty}) '' {V | IsOpen[inst✝] V}) =
    generateFrom
      ((fun x ↦ (fun x ↦ f '' x) ⁻¹' {t | t ⊆ x}) '' {V | IsOpen[inst✝] V} ∪
        (fun x ↦ (fun x ↦ f '' x) ⁻¹' {s | (s ∩ x).Nonempty}) '' {V | IsOpen[inst✝] V})

Tactic:
preimage_ofPred_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
this : {U | IsOpen[inst✝¹] U} = (fun x ↦ f ⁻¹' x) '' {V | IsOpen[inst✝] V}
⊢ generateFrom
      ((fun x ↦ {t | t ⊆ f ⁻¹' x}) '' {V | IsOpen[inst✝] V} ∪
        (fun x ↦ {s | (s ∩ f ⁻¹' x).Nonempty}) '' {V | IsOpen[inst✝] V}) =
    generateFrom
      ((fun a ↦ {a_1 | f '' a_1 ⊆ a}) '' {V | IsOpen[inst✝] V} ∪
        (fun a ↦ {a_1 | (f '' a_1 ∩ a).Nonempty}) '' {V | IsOpen[inst✝] V})
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
⊢ U ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] U →
    (fun y ↦ (y, L)) ⁻¹' Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id U) ∈ f

Tactic:
⟨hU₁, hU₂⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
⊢ (fun y ↦ (y, L)) ⁻¹' Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id U) ∈ f
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsClosed {K | (↑K ∩ F).Nonempty}

Tactic:
simp_rw +singlePass [← compl_compl F, Set.inter_compl_nonempty_iff, ← Set.compl_ofPred]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsClosed {a | ↑a ⊆ Fᶜ}ᶜ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inr
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h✝ : Nontrivial A
⊢ ‖cfc f a‖ < c

Tactic:
· refine cfc_cases (‖·‖ < c) a f (by simpa) fun hf ha ↦ ?_
    simp only [← cfc_apply f a, (IsGreatest.norm_cfc f a hf ha |>.lt_iff)]
    rintro - ⟨x, hx, rfl⟩
    exact h x hx

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

Goal state before:
pp: case a
𝕜₁ : 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‖₊
⊢ ⨆ k ∈ spectrum 𝕜₁ a, ↑‖k‖₊ ≤ ⨆ k ∈ spectrum 𝕜₂ a, ↑‖k‖₊

Tactic:
apply iSup₂_le fun x hx ↦ ?_

Goal state after:
𝕜₁ : 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‖₊
x : 𝕜₁
hx : x ∈ spectrum 𝕜₁ a
⊢ ↑‖x‖₊ ≤ ⨆ k ∈ spectrum 𝕜₂ a, ↑‖k‖₊
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case a
𝕜₁ : 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‖₊
⊢ ⨆ k ∈ spectrum 𝕜₂ a, ↑‖k‖₊ ≤ ⨆ k ∈ spectrum 𝕜₁ a, ↑‖k‖₊

Tactic:
apply iSup₂_le fun x hx ↦ ?_

Goal state after:
𝕜₁ : 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‖₊
x : 𝕜₂
hx : x ∈ spectrum 𝕜₂ a
⊢ ↑‖x‖₊ ≤ ⨆ k ∈ spectrum 𝕜₁ a, ↑‖k‖₊
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case e'_3
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✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
this : ContinuousFunctionalCalculus R A p
g₁ g₂ : C(↑(σ R a), R)
x : ↑(σ R a)
x' : ↑(σ S a) := ⋯
⊢ ↑x = ↑(Subtype.map ⇑f ⋯ (Subtype.map ⇑(algebraMap R S) ⋯ x))

Tactic:
exact haf.left_inv _ |>.symm

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

Goal state before:
pp: case e'_4
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✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
this : ContinuousFunctionalCalculus R A p
g₁ g₂ : C(↑(σ R a), R)
x : ↑(σ R a)
x' : ↑(σ S a) := ⋯
⊢ ↑x = ↑(Subtype.map ⇑f ⋯ (Subtype.map ⇑(algebraMap R S) ⋯ x))

Tactic:
exact haf.left_inv _ |>.symm

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

Goal state before:
pp: case e'_3
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✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : MetricSpace A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts a ⇑f
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a)) R
x : ↑(σₙ R a)
x' : ↑(σₙ S a) := ⋯
⊢ ↑x = ↑(Subtype.map ⇑f ⋯ (Subtype.map ⇑(algebraMap R S) ⋯ x))

Tactic:
exact haf.left_inv _ |>.symm

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

Goal state before:
pp: case e'_4
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✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : MetricSpace A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts a ⇑f
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a)) R
x : ↑(σₙ R a)
x' : ↑(σₙ S a) := ⋯
⊢ ↑x = ↑(Subtype.map ⇑f ⋯ (Subtype.map ⇑(algebraMap R S) ⋯ x))

Tactic:
exact haf.left_inv _ |>.symm

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {V | IsOpen[instTopologicalSpaceProd] V}
K : Compacts α
L : Compacts β
x : α
y : β
hx : x ∈ K
hy : y ∈ L
hxy : (x, y) ∈ U
V : Set α
W : Set β
hV : IsOpen[inst✝¹] V
hW : IsOpen[inst✝] W
hxV : x ∈ V
hyW : y ∈ W
hVW : V ×ˢ W ⊆ U
⊢ ∃ t ⊆ (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' (fun V ↦ {s | (s ∩ V).Nonempty}) U, IsOpen t ∧ (K, L) ∈ t

Tactic:
preimage_ofPred_eq,

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {V | IsOpen[instTopologicalSpaceProd] V}
K : Compacts α
L : Compacts β
x : α
y : β
hx : x ∈ K
hy : y ∈ L
hxy : (x, y) ∈ U
V : Set α
W : Set β
hV : IsOpen[inst✝¹] V
hW : IsOpen[inst✝] W
hxV : x ∈ V
hyW : y ∈ W
hVW : V ×ˢ W ⊆ U
⊢ ∃ t ⊆ {a | ((SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) a ∩ U).Nonempty}, IsOpen t ∧ (K, L) ∈ t
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✝ : RegularSpace α
⊢ ∀
    t ∈
      (fun x ↦ SetLike.coe ⁻¹' {t | t ⊆ x}) '' {U | IsOpen[inst✝³] U} ∪
        (fun x ↦ SetLike.coe ⁻¹' {s | (s ∩ x).Nonempty}) '' {U | IsOpen[inst✝³] U},
    ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
preimage_ofPred_eq,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
⊢ ∀
    t ∈
      (fun a ↦ {a_1 | ↑a_1 ⊆ a}) '' {U | IsOpen[inst✝³] U} ∪
        (fun a ↦ {a_1 | (↑a_1 ∩ a).Nonempty}) '' {U | IsOpen[inst✝³] U},
    ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
hK : K ∈ (fun a ↦ {a_1 | ↑a_1 ⊆ a}) U
⊢ ∃ s ∈ 𝓝ˢ ((fun a ↦ {a_1 | ↑a_1 ⊆ a}) U)ᶜ, ∃ t ∈ 𝓝 K, Disjoint s t

Tactic:
obtain ⟨V, W, hV, hW, hKV, hUW, hVW⟩ :=
      SeparatedNhds.of_isCompact_isClosed K.isCompact hU.isClosed_compl
        (disjoint_compl_right_iff_subset.mpr hK)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
hK : K ∈ (fun a ↦ {a_1 | ↑a_1 ⊆ a}) U
V W : Set α
hV : IsOpen[inst✝³] V
hW : IsOpen[inst✝³] W
hKV : ↑K ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ ∃ s ∈ 𝓝ˢ ((fun a ↦ {a_1 | ↑a_1 ⊆ a}) U)ᶜ, ∃ t ∈ 𝓝 K, Disjoint s t
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
⊢ IsCompact (SetLike.coe '' {L | ↑L ⊆ K})

Tactic:
refine .of_subset_of_specializes hK.powerset_vietoris (by grind) (fun s hs => ?_)

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set α
hs : s ∈ 𝒫 K
⊢ ∃ y ∈ SetLike.coe '' {L | ↑L ⊆ K}, s ⤳ y
Module: Mathlib.Topology.Sets.VietorisTopology

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

Tactic:
preimage_ofPred_eq,

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L : NonemptyCompacts α
hL : IsPreconnected ↑L
⊢ IsPreconnected (Icc (toCompactsOrderEmbedding K) (toCompactsOrderEmbedding L))

Tactic:
exact Compacts.isPreconnected_Icc (Compacts.coe_nonempty.mp K.nonempty) hL

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𝕜
this✝ : IsTopologicalAddGroup E
this : WithSeminorms fun i ↦ (f i).toSeminorm
⊢ φ ∈ Submodule.span 𝕜 (Set.range f) ↔ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm

Tactic:
LinearMap.mem_span_iff_continuous

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𝕜
this✝ : IsTopologicalAddGroup E
this : WithSeminorms fun i ↦ (f i).toSeminorm
⊢ Continuous[⨅ i, induced (⇑(f i)) inferInstance, inferInstance] ⇑φ ↔
    ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ AbsConvex 𝕜 (B.polar s)

Tactic:
rw [polar_eq_biInter_preimage]
  exact AbsConvex.iInter₂ fun i hi =>
    ⟨balanced_closedBall_zero.mulActionHom_preimage (f := (B i : (F →ₑ[(RingHom.id 𝕜)] 𝕜))),
      (convex_RCLike_iff_convex_real.mpr (convex_closedBall 0 1)).linear_preimage _⟩

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

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

Tactic:
simpa [p.closedBall_zero_eq] using! hp.isClosed_preimage n

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ b ∈ ↑I, nndist f b < ε

Tactic:
set t := {x : X | ε / 2 ≤ ‖f x‖₊}

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
⊢ ∃ b ∈ ↑I, nndist f b < ε
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
hd : Disjoint s t
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
by
  -- The actual proof is in the code above. Here we just repack it into the expected format.
  let P : Set X → Set X → Prop := fun _ _ ↦ True
  set c : Urysohns.CU P :=
  { C := s
    U := tᶜ
    P_C_U := trivial
    closed_C := hs
    open_U := ht.isOpen_compl
    subset := disjoint_left.1 hd
    hP := by
      rintro c u c_closed - u_open cu
      rcases normal_exists_closure_subset c_closed u_open cu with ⟨v, v_open, cv, hv⟩
      exact ⟨v, v_open, cv, hv, trivial, trivial⟩ }
  exact ⟨⟨c.lim, c.continuous_lim⟩, c.lim_of_mem_C, fun x hx => c.lim_of_notMem_U _ fun h => h hx,
    c.lim_mem_Icc⟩

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case h.refine_1
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
⊢ EqOn (⇑(1 - g)) 0 t

Tactic:
intro x hx
    simp only [ContinuousMap.sub_apply, ContinuousMap.one_apply, Pi.zero_apply]
    exact sub_eq_zero_of_eq (hgt.symm hx)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case pos
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
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁺) a * cfcₙ (fun x ↦ x⁻) a = 0

Tactic:
← cfcₙ_mul _ _,

Goal state after:
case pos
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
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁺ * x⁻) a = 0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case pos
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
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁻) a * cfcₙ (fun x ↦ x⁺) a = 0

Tactic:
← cfcₙ_mul _ _,

Goal state after:
case pos
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
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁻ * x⁺) a = 0
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
⊢ Bornology.IsBounded Set.univ

Tactic:
by
    rw [Metric.isBounded_iff_ediam_ne_top, ← lt_top_iff_ne_top]
    refine lt_of_le_of_lt ?_ <| BoundedSpace.bounded_univ (α := β) |>.ediam_ne_top.lt_top
    simp only [Metric.ediam_le_iff, Set.mem_univ, edist_le, forall_const]
    exact fun f g x ↦ Metric.edist_le_ediam_of_mem (Set.mem_univ _) (Set.mem_univ _)

Goal state after: