mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Surjective ⇑f
x✝¹ x✝ : PrimeSpectrum S
h : { asIdeal := Ideal.comap f x✝¹.asIdeal, isPrime := ⋯ } = { asIdeal := Ideal.comap f x✝.asIdeal, isPrime := ⋯ }
⊢ Ideal.comap f x✝¹.asIdeal = Ideal.comap f x✝.asIdeal

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Surjective ⇑f
x✝¹ x✝ : PrimeSpectrum S
h : { asIdeal := Ideal.comap f x✝¹.asIdeal, isPrime := ⋯ } = { asIdeal := Ideal.comap f x✝.asIdeal, isPrime := ⋯ }
⊢ Ideal.comap f x✝¹.asIdeal = Ideal.comap f x✝.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
⊢ ∃ i, e i ∈ p.asIdeal

Tactic:
simpa using

Goal state after:
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
⊢ ∃ i, e i ∈ p.asIdeal
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Ring.KrullDimLE 1 R
a : R
ha : Prime a
⊢ Ideal.span {a} ≠ ⊥

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Ring.KrullDimLE 1 R
a : R
ha : Prime a
⊢ ¬a = 0
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
⊢ ∃ p ∈ I.minimalPrimes, y ∉ p

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
⊢ ∃ p, I.IsMinimalPrime p ∧ y ∉ p
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ ↑(a ⊔ ⟨1 - ↑a, ⋯⟩) = ↑⊤

Tactic:
by
    simp_rw [(· ⊔ ·), SemilatticeSup.sup, add_sub_cancel, mul_sub, mul_one]
    rw [a.2, sub_self, sub_zero]; rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
h : Nat.find H = 0
⊢ y ^ n ∈ I

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
h : Nat.find H = 0
⊢ y ^ n ∈ I
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: case refine_1
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : Y → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
i : Y
hi : i ∈ t
⊢ (b ∘ f') i ⊆ ⋃ i ∈ ↑(Finset.image f' t), b i

Tactic:
simpa using

Goal state after:
case refine_1
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : Y → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
i : Y
hi : i ∈ t
⊢ b (f' i) ⊆ ⋃ y ∈ t, b (f' y)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : x ∉ range ⇑(algebraMap R K)
hlocal : ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K x) 1
⊢ 1 ∉ denom

Tactic:
simpa using

Goal state after:
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : x ∉ range ⇑(algebraMap R K)
hlocal : ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K x) 1
⊢ ∀ (x_1 : R), ¬(algebraMap R K) x_1 = x
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : K
⊢ x✝ ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ →
    x✝ ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯

Tactic:
simpa using

Goal state after:
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : K
⊢ (∀ (i : PrimeSpectrum R), x✝ ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) →
    ∀ (i : MaximalSpectrum R), x✝ ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ Function.Surjective ⇑(piLocalizationToMaximal R)

Tactic:
classical
  exact fun r ↦ ⟨fun I ↦ if h : I.1.IsMaximal then r ⟨_, h⟩ else 0, funext fun _ ↦ dif_pos _⟩

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
⊢ ⋃ i, ↑(u i) = univ

Tactic:
simpa using

Goal state after:
ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
⊢ ⋃ i, ↑(u i) = univ
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
a : X
⊢ ∃ i, a ∈ u i

Tactic:
simpa using

Goal state after:
ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
a : X
⊢ ∃ i, a ∈ u i
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: ι : Type u_1
X : Type u_3
inst✝¹ : TopologicalSpace X
u : ι → Opens X
hu : ↑⊤ ⊆ ↑(iSup u)
inst✝ : CompactSpace X
⊢ univ ⊆ ⋃ i, (u i).carrier

Tactic:
simpa using

Goal state after:
ι : Type u_1
X : Type u_3
inst✝¹ : TopologicalSpace X
u : ι → Opens X
hu : ↑⊤ ⊆ ↑(iSup u)
inst✝ : CompactSpace X
⊢ ⋃ i, ↑(u i) = univ
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: case h
ι : Type u_1
X : Type u_3
inst✝¹ : TopologicalSpace X
u : ι → Opens X
hu : ↑⊤ ⊆ ↑(iSup u)
inst✝ : CompactSpace X
s : Finset ι
hs : univ ⊆ ⋃ i ∈ s, (u i).carrier
⊢ IsOpenCover fun i ↦ u ↑i

Tactic:
simpa using

Goal state after:
case h
ι : Type u_1
X : Type u_3
inst✝¹ : TopologicalSpace X
u : ι → Opens X
hu : ↑⊤ ⊆ ↑(iSup u)
inst✝ : CompactSpace X
s : Finset ι
hs : univ ⊆ ⋃ i ∈ s, (u i).carrier
⊢ ⋃ x ∈ s, ↑(u x) = univ
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
x : X
hx : x ∈ s
i : ι
hi : x ∈ ↑(U i)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst✝] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ ↑(U j)
hji : j ≠ i
⊢ ¬Disjoint ↑(U j) ↑(U i)

Tactic:
simpa using

Goal state after:
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
x : X
hx : x ∈ s
i : ι
hi : x ∈ ↑(U i)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst✝] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ ↑(U j)
hji : j ≠ i
⊢ ¬Disjoint (U j) (U i)
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
hU : IsOpenCover U
h : ∀ (i : ι), PreirreducibleSpace ↥(U i)
h' : ∀ (i : ι), IsPreirreducible (U i).carrier
⊢ univ ⊆ ⋃ i, ↑(U i)

Tactic:
simpa using

Goal state after:
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
hU : IsOpenCover U
h : ∀ (i : ι), PreirreducibleSpace ↥(U i)
h' : ∀ (i : ι), IsPreirreducible (U i).carrier
⊢ ⋃ i, ↑(U i) = univ
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case mpr
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpen[inst✝] (s ∩ ↑(U i))
⊢ IsOpen[inst✝] s

Tactic:
simpa using

Goal state after:
case mpr
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpen[inst✝] (s ∩ ↑(U i))
⊢ IsOpen[inst✝] s
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
s : Set β
⊢ IsClosed[inst✝] s ↔ ∀ (i : ι), IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)

Tactic:
simpa using

Goal state after:
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
s : Set β
⊢ IsClosed[inst✝] s ↔ ∀ (i : ι), IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
a : α
ha : aᶜ ∈ L
⊢ a ∈ L

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
a : α
ha : aᶜ ∈ L
⊢ a ∈ L
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ ⊤ ∈ L

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ ⊤ ∈ L
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
p : (g : α) → g ∈ closure s → Prop
mem : ∀ (x : α) (hx : x ∈ s), p x ⋯
bot : p ⊥ ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
compl : ∀ (x : α) (hx : x ∈ closure s), p x hx → p xᶜ ⋯
x✝ : α
hx✝ : x✝ ∈ closure s
x : α
hx : x ∈ closure s
y : α
hy : y ∈ closure s
hx' : p x hx
hy' : p y hy
⊢ p (x ⊓ y) ⋯

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
p : (g : α) → g ∈ closure s → Prop
mem : ∀ (x : α) (hx : x ∈ s), p x ⋯
bot : p ⊥ ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
compl : ∀ (x : α) (hx : x ∈ closure s), p x hx → p xᶜ ⋯
x✝ : α
hx✝ : x✝ ∈ closure s
x : α
hx : x ∈ closure s
y : α
hy : y ∈ closure s
hx' : p x hx
hy' : p y hy
⊢ p (x ⊓ y) ⋯
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
H : ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)), 𝓝 x = Filter.comap Subtype.val (Filter.comap f (𝓝 ((f ∘ Subtype.val) x)))
x : α
i : ι
hi : f x ∈ U i
⊢ 𝓝 x = Filter.comap f (𝓝 (f x))

Tactic:
simpa using

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
H : ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)), 𝓝 x = Filter.comap Subtype.val (Filter.comap f (𝓝 ((f ∘ Subtype.val) x)))
x : α
i : ι
hi : f x ∈ U i
⊢ ∃ t ∈ 𝓝 (f x), f ⁻¹' t ⊆ f ⁻¹' ↑(U i)
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsEmbedding f ↔ ∀ (i : ι), IsEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsInducing f ∧ Function.Injective f ↔
    (∀ (x : ι), IsInducing ((↑(U x)).restrictPreimage f)) ∧ ∀ (x : ι), Function.Injective ((↑(U x)).restrictPreimage f)
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen[inst✝] (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
⊢ ↑s ⊆ ⋃ i, ↑(U i)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen[inst✝] (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
⊢ ↑s ⊆ ⋃ i, ↑(U i)
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen[inst✝] (coborder s)
tfae_2_to_3 : IsOpen[inst✝] (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)) →
    ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
tfae_4_to_5 :
  (∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s) →
    IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)
x✝ : IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)
H : IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s) := x✝
⊢ IsLocallyClosed (range Subtype.val)

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen[inst✝] (coborder s)
tfae_2_to_3 : IsOpen[inst✝] (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)) →
    ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
tfae_4_to_5 :
  (∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s) →
    IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)
x✝ : IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)
H : IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s) := x✝
⊢ IsLocallyClosed (closure[inst✝] s)
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen[inst✝] (coborder s)
tfae_2_to_3 : IsOpen[inst✝] (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)) →
    ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
tfae_4_to_5 :
  (∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s) →
    IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)
x✝ : IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)
H : IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s) := x✝
⊢ s = ↑(closure[inst✝] s ↓∩ s)

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen[inst✝] (coborder s)
tfae_2_to_3 : IsOpen[inst✝] (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)) →
    ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
tfae_4_to_5 :
  (∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s) →
    IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)
x✝ : IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)
H : IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s) := x✝
⊢ s ⊆ closure[inst✝] s
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
⊢ ⊤ ≤ ⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i)

Tactic:
simpa using

Goal state after:
X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
⊢ ∀ (a : X), ∃ i, f a ∈ U i
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
a b : IrreducibleCloseds β
hle :
  { toFun := fun T ↦ ⟨map f ⋯ T, ⋯⟩, invFun := fun V ↦ { carrier := f ⁻¹' ↑↑V, isIrreducible' := ⋯, isClosed' := ⋯ },
        left_inv := ⋯, right_inv := ⋯ }
      a ≤
    { toFun := fun T ↦ ⟨map f ⋯ T, ⋯⟩, invFun := fun V ↦ { carrier := f ⁻¹' ↑↑V, isIrreducible' := ⋯, isClosed' := ⋯ },
        left_inv := ⋯, right_inv := ⋯ }
      b
⊢ a ≤ b

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
a b : IrreducibleCloseds β
hle :
  { toFun := fun T ↦ ⟨map f ⋯ T, ⋯⟩, invFun := fun V ↦ { carrier := f ⁻¹' ↑↑V, isIrreducible' := ⋯, isClosed' := ⋯ },
        left_inv := ⋯, right_inv := ⋯ }
      a ≤
    { toFun := fun T ↦ ⟨map f ⋯ T, ⋯⟩, invFun := fun V ↦ { carrier := f ⁻¹' ↑↑V, isIrreducible' := ⋯, isClosed' := ⋯ },
        left_inv := ⋯, right_inv := ⋯ }
      b
⊢ a ≤ b
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset (↑s × ↑s)
⊢ ∀ (hx : (∅.sup fun x ↦ ↑x.1 \ ↑x.2) ∈ closure s), p (∅.sup fun x ↦ ↑x.1 \ ↑x.2) hx

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset (↑s × ↑s)
⊢ p ⊥ ⋯
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∃ S, (∀ (k : ↥S), IsIrreducible ↑↑k) ∧ s = S.sup id

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∃ S, (∀ a ∈ S, IsIrreducible ↑a) ∧ s = sSup ↑S
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) → X := Subtype.val ∘ (f ⁻¹' ↑(U i)).restrictPreimage (iV i)
this : IsEmbedding f'
⊢ range f' = f ⁻¹' ↑(U i)

Tactic:
simpa using

Goal state after:
X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) → X := Subtype.val ∘ (f ⁻¹' ↑(U i)).restrictPreimage (iV i)
this : IsEmbedding f'
⊢ f ⁻¹' ↑(U i) ⊆ range (iV i)
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
U V : Set α
hUopen : IsOpen[inst✝] U
hUcomp : IsCompact U
hVopen : IsOpen[inst✝] V
hVcomp : IsCompact V
i : ι
⊢ IsCompact (b i)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
U V : Set α
hUopen : IsOpen[inst✝] U
hUcomp : IsCompact U
hVopen : IsOpen[inst✝] V
hVcomp : IsCompact V
i : ι
⊢ IsCompact (b i)
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsCodirectedOrder P
x : P
I : Ideal P
hx : x ∉ I
h : I = I ⊔ principal x
⊢ x ∈ I

Tactic:
simpa using

Goal state after:
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsCodirectedOrder P
x : P
I : Ideal P
hx : x ∉ I
h : I = I ⊔ principal x
⊢ x ∈ I
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : CompleteLattice P
I : Ideal P
α : Sort u_2
inst✝ : Finite α
f : α → P
⊢ ⨆ i, f i ∈ I ↔ ∀ (i : α), f i ∈ I

Tactic:
simpa using

Goal state after:
P : Type u_1
inst✝¹ : CompleteLattice P
I : Ideal P
α : Sort u_2
inst✝ : Finite α
f : α → P
⊢ ⨆ i, f i ∈ I ↔ ∀ (i : α), f i ∈ I
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : ∀ a ∈ U₁, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₁
hU₂ : ∀ a ∈ U₂, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : W₁ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : W₂ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
⊢ IsClosed[inst✝¹] W₁ᶜ

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : ∀ a ∈ U₁, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₁
hU₂ : ∀ a ∈ U₂, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : W₁ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : W₂ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
⊢ IsOpen[inst✝¹] W₁