mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ : α
⊢ bot ≤ a✝

Tactic:
;

Goal state after:
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ : α
⊢ bot ≤ a✝
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : ConditionallyCompleteLattice α
__Lattice✝ : Lattice α := c.copy LE.le ⋯ max ⋯ min ⋯
⊢ ∀ (s : Set α), s.Nonempty → BddAbove s → IsLUB s (sSup s)

Tactic:
;

Goal state after:
α : Type u
c : ConditionallyCompleteLattice α
__Lattice✝ : Lattice α := c.copy LE.le ⋯ max ⋯ min ⋯
⊢ ∀ (s : Set α), s.Nonempty → BddAbove s → IsLUB s (sSup s)
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : ConditionallyCompleteLattice α
__Lattice✝ : Lattice α := c.copy LE.le ⋯ max ⋯ min ⋯
⊢ ∀ (s : Set α), s.Nonempty → BddBelow s → IsGLB s (sInf s)

Tactic:
;

Goal state after:
α : Type u
c : ConditionallyCompleteLattice α
__Lattice✝ : Lattice α := c.copy LE.le ⋯ max ⋯ min ⋯
⊢ ∀ (s : Set α), s.Nonempty → BddBelow s → IsGLB s (sInf s)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI✝ : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
hI : 1 = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
eq : I = { asIdeal := J, isPrime := ⋯ }
⊢ False

Tactic:
;

Goal state after:
case h
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI✝ : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
hI : 1 = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
eq : I = { asIdeal := J, isPrime := ⋯ }
⊢ False
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI✝ : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
hI : 1 = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
eq : I = { asIdeal := J, isPrime := ⋯ }
this : I.asIdeal = J
⊢ False

Tactic:
;

Goal state after:
case h
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI✝ : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
hI : 1 = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
eq : I = { asIdeal := J, isPrime := ⋯ }
this : I.asIdeal = J
⊢ False
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: case inl
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)
he : s = ∅
⊢ IsPreirreducible ∅

Tactic:
;

Goal state after:
case inl
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)
he : s = ∅
⊢ IsPreirreducible ∅
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x✝¹ : PiLocalization R
x✝ : PrimeSpectrum R
⊢ (mapPiLocalization (RingHom.id R)) x✝¹ x✝ = (RingHom.id (PiLocalization R)) x✝¹ x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
x✝¹ : PiLocalization R
x✝ : PrimeSpectrum R
⊢ (mapPiLocalization (RingHom.id R)) x✝¹ x✝ = (RingHom.id (PiLocalization R)) x✝¹ x✝
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring P
f : R →+* S
g : S →+* P
x✝¹ : PiLocalization R
x✝ : PrimeSpectrum P
⊢ (mapPiLocalization (g.comp f)) x✝¹ x✝ = ((mapPiLocalization g).comp (mapPiLocalization f)) x✝¹ x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
P : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring P
f : R →+* S
g : S →+* P
x✝¹ : PiLocalization R
x✝ : PrimeSpectrum P
⊢ (mapPiLocalization (g.comp f)) x✝¹ x✝ = ((mapPiLocalization g).comp (mapPiLocalization f)) x✝¹ x✝
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ Function.Bijective ⇑(mapPiLocalization f)

Tactic:
by
  let f := RingEquiv.ofBijective f hf
  let e := RingEquiv.ofRingHom (mapPiLocalization (f : R →+* S)) (mapPiLocalization f.symm) ?_ ?_
  · exact e.bijective
  · rw [← mapPiLocalization_comp, RingEquiv.comp_symm, mapPiLocalization_id]
  · rw [← mapPiLocalization_comp, RingEquiv.symm_comp, mapPiLocalization_id]

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

Goal state before:
pp: case neg
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
x : X
hx₁ : x ∈ ↑(U i)
hx₂ : x ∈ uᶜ
⊢ False

Tactic:
;

Goal state after:
case neg
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
x : X
hx₁ : x ∈ ↑(U i)
hx₂ : x ∈ uᶜ
⊢ False
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
U : Set Y
hU : IsOpen[inst✝] U
Z : Set Y
hZ : IsClosed[inst✝] Z
⊢ ∃ s', (∃ U Z, IsOpen[inst✝] U ∧ IsClosed[inst✝] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = f ⁻¹' U ∩ f ⁻¹' Z

Tactic:
exact ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L M✝ : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
M : BooleanSubalgebra α
carrier✝ : Set α
supClosed'✝ : SupClosed carrier✝
infClosed'✝ : InfClosed carrier✝
compl_mem'✝ :
  ∀ {a : α},
    a ∈ { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝ }.carrier →
      aᶜ ∈ { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝ }.carrier
bot_mem'✝ : ⊥ ∈ { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝ }.carrier
h :
  (fun L ↦ L.carrier)
      { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝, compl_mem' := compl_mem'✝,
        bot_mem' := bot_mem'✝ } =
    (fun L ↦ L.carrier) M
⊢ { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝, compl_mem' := compl_mem'✝,
      bot_mem' := bot_mem'✝ } =
    M

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L M✝ : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
M : BooleanSubalgebra α
carrier✝ : Set α
supClosed'✝ : SupClosed carrier✝
infClosed'✝ : InfClosed carrier✝
compl_mem'✝ :
  ∀ {a : α},
    a ∈ { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝ }.carrier →
      aᶜ ∈ { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝ }.carrier
bot_mem'✝ : ⊥ ∈ { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝ }.carrier
h :
  (fun L ↦ L.carrier)
      { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝, compl_mem' := compl_mem'✝,
        bot_mem' := bot_mem'✝ } =
    (fun L ↦ L.carrier) M
⊢ { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝, compl_mem' := compl_mem'✝,
      bot_mem' := bot_mem'✝ } =
    M
Module: Mathlib.Order.BooleanSubalgebra

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

Tactic:
;

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

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

Tactic:
;

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L : BooleanSubalgebra α
⊢ ↑L = ↑L.toSublattice

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L : BooleanSubalgebra α
⊢ ↑L = ↑L.toSublattice
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L : BooleanSubalgebra α
__Sublattice✝ : Sublattice α := L.copy ↑L ⋯
⊢ ∀ {a : α}, a ∈ (L.copy ↑L ⋯).carrier → aᶜ ∈ (L.copy ↑L ⋯).carrier

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L : BooleanSubalgebra α
__Sublattice✝ : Sublattice α := L.copy ↑L ⋯
⊢ ∀ {a : α}, a ∈ (L.copy ↑L ⋯).carrier → aᶜ ∈ (L.copy ↑L ⋯).carrier
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L : BooleanSubalgebra α
__Sublattice✝ : Sublattice α := L.copy ↑L ⋯
⊢ ⊥ ∈ (L.copy ↑L ⋯).carrier

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L : BooleanSubalgebra α
__Sublattice✝ : Sublattice α := L.copy ↑L ⋯
⊢ ⊥ ∈ (L.copy ↑L ⋯).carrier
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a : α
S : Set (BooleanSubalgebra α)
⊢ a ∈ ↑(sInf S) ↔ ∀ L ∈ S, a ∈ L

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a : α
S : Set (BooleanSubalgebra α)
⊢ a ∈ ↑(sInf S) ↔ ∀ L ∈ S, a ∈ L
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : BooleanAlgebra α
a : α
f : ι → BooleanSubalgebra α
⊢ a ∈ ↑(⨅ i, f i) ↔ ∀ (i : ι), a ∈ f i

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝ : BooleanAlgebra α
a : α
f : ι → BooleanSubalgebra α
⊢ a ∈ ↑(⨅ i, f i) ↔ ∀ (i : ι), a ∈ f i
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f✝ : BoundedLatticeHom α β
s t : Set α
a✝ b : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra α
a : α
ha : a ∈ ↑L
⊢ (f a)ᶜ ∈ ⇑f '' ↑L

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f✝ : BoundedLatticeHom α β
s t : Set α
a✝ b : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra α
a : α
ha : a ∈ ↑L
⊢ (f a)ᶜ ∈ ⇑f '' ↑L
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L : BooleanSubalgebra α
M : BooleanSubalgebra β
e : β ≃o α
⊢ ↑(map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ } L) = ↑M ↔
    ↑L = ↑(map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ } M)

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L : BooleanSubalgebra α
M : BooleanSubalgebra β
e : β ≃o α
⊢ ↑(map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ } L) = ↑M ↔
    ↑L = ↑(map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ } M)
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Opens β)
H : IsTopologicalBasis (SetLike.coe '' B)
f : α → β
h : IsInducing f
x✝ : Set α
⊢ x✝ ∈ SetLike.coe '' {x | ∃ U ∈ B, { carrier := f ⁻¹' ↑U, is_open' := ⋯ } = x} ↔ x✝ ∈ preimage f '' SetLike.coe '' B

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Opens β)
H : IsTopologicalBasis (SetLike.coe '' B)
f : α → β
h : IsInducing f
x✝ : Set α
⊢ x✝ ∈ SetLike.coe '' {x | ∃ U ∈ B, { carrier := f ⁻¹' ↑U, is_open' := ⋯ } = x} ↔ x✝ ∈ preimage f '' SetLike.coe '' B
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
⊢ ∀ {a b : Opens α},
    ↑({ toFun := ⇑(comap ↑f.symm), invFun := ⇑(comap ↑f), left_inv := ⋯, right_inv := ⋯ } a) ⊆
        ↑({ toFun := ⇑(comap ↑f.symm), invFun := ⇑(comap ↑f), left_inv := ⋯, right_inv := ⋯ } b) ↔
      ↑a ⊆ ↑b

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
⊢ ∀ {a b : Opens α},
    ↑({ toFun := ⇑(comap ↑f.symm), invFun := ⇑(comap ↑f), left_inv := ⋯, right_inv := ⋯ } a) ⊆
        ↑({ toFun := ⇑(comap ↑f.symm), invFun := ⇑(comap ↑f), left_inv := ⋯, right_inv := ⋯ } b) ↔
      ↑a ⊆ ↑b
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: case refine_1
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
x✝ : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst✝] (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst✝] s ⊆ s
x : { x // x ∈ closure[inst✝] s }
⊢ x ∈ Subtype.val ⁻¹' ⋃ x, ⋃ (h : x ∈ s), U x h → x ∈ closure[inst✝] s ↓∩ s

pp: case refine_2
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
x✝ : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst✝] (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst✝] s ⊆ s
x : { x // x ∈ closure[inst✝] s }
⊢ x ∈ closure[inst✝] s ↓∩ s → x ∈ Subtype.val ⁻¹' ⋃ x, ⋃ (h : x ∈ s), U x h

Tactic:
· rintro ⟨_, ⟨⟨y, rfl⟩, ⟨_, ⟨hy, rfl⟩, hxU⟩⟩⟩
      exact e y hy ⟨hxU, x.2⟩

Goal state after:
case refine_2
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
x✝ : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst✝] (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst✝] s ⊆ s
x : { x // x ∈ closure[inst✝] s }
⊢ x ∈ closure[inst✝] s ↓∩ s → x ∈ Subtype.val ⁻¹' ⋃ x, ⋃ (h : x ∈ s), U x h
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∀ (x : Closeds α),
    (∀ y < x, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S) →
      ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ x = sSup S

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∀ (x : Closeds α),
    (∀ y < x, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S) →
      ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ x = sSup S
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
H : ∀ y < ⊥, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
⊢ ∅.Finite ∧ (∀ t ∈ ∅, IsIrreducible ↑t) ∧ ⊥ = sSup ∅

Tactic:
;

Goal state after:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
H : ∀ y < ⊥, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
⊢ ∅.Finite ∧ (∀ t ∈ ∅, IsIrreducible ↑t) ∧ ⊥ = sSup ∅
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : IsIrreducible ↑s
⊢ {s}.Finite ∧ (∀ t ∈ {s}, IsIrreducible ↑t) ∧ s = sSup {s}

Tactic:
;

Goal state after:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : IsIrreducible ↑s
⊢ {s}.Finite ∧ (∀ t ∈ {s}, IsIrreducible ↑t) ∧ s = sSup {s}
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Closeds α
carrier✝ : Set α
isClosed'✝ : IsClosed[inst✝¹] carrier✝
h : { carrier := carrier✝, isClosed' := isClosed'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, isClosed' := isClosed'✝ } = t

Tactic:
;

Goal state after:
case mk
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Closeds α
carrier✝ : Set α
isClosed'✝ : IsClosed[inst✝¹] carrier✝
h : { carrier := carrier✝, isClosed' := isClosed'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, isClosed' := isClosed'✝ } = t
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
carrier✝¹ : Set α
isClosed'✝¹ : IsClosed[inst✝¹] carrier✝¹
carrier✝ : Set α
isClosed'✝ : IsClosed[inst✝¹] carrier✝
h :
  { carrier := carrier✝¹, isClosed' := isClosed'✝¹ }.carrier = { carrier := carrier✝, isClosed' := isClosed'✝ }.carrier
⊢ { carrier := carrier✝¹, isClosed' := isClosed'✝¹ } = { carrier := carrier✝, isClosed' := isClosed'✝ }

Tactic:
;

Goal state after:
case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
carrier✝¹ : Set α
isClosed'✝¹ : IsClosed[inst✝¹] carrier✝¹
carrier✝ : Set α
isClosed'✝ : IsClosed[inst✝¹] carrier✝
h :
  { carrier := carrier✝¹, isClosed' := isClosed'✝¹ }.carrier = { carrier := carrier✝, isClosed' := isClosed'✝ }.carrier
⊢ { carrier := carrier✝¹, isClosed' := isClosed'✝¹ } = { carrier := carrier✝, isClosed' := isClosed'✝ }
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
x✝ : α
⊢ x✝ ∈ ↑(⨅ i, s i) ↔ x✝ ∈ ⋂ i, ↑(s i)

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
x✝ : α
⊢ x✝ ∈ ↑(⨅ i, s i) ↔ x✝ ∈ ⋂ i, ↑(s i)
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
⊢ ↑(⨅ i, s i) = ↑{ carrier := ⋂ i, ↑(s i), isClosed' := ⋯ }

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
⊢ ↑(⨅ i, s i) = ↑{ carrier := ⋂ i, ↑(s i), isClosed' := ⋯ }
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Closeds α
x : α
ht : IsAtom {x}
⊢ ↑(Closeds.closure {x}) = {x}

Tactic:
;

Goal state after:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Closeds α
x : α
ht : IsAtom {x}
⊢ ↑(Closeds.closure {x}) = {x}
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Clopens α
carrier✝ : Set α
isClopen'✝ : IsClopen carrier✝
h : (fun s ↦ s.carrier) { carrier := carrier✝, isClopen' := isClopen'✝ } = (fun s ↦ s.carrier) t
⊢ { carrier := carrier✝, isClopen' := isClopen'✝ } = t

Tactic:
;

Goal state after:
case mk
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Clopens α
carrier✝ : Set α
isClopen'✝ : IsClopen carrier✝
h : (fun s ↦ s.carrier) { carrier := carrier✝, isClopen' := isClopen'✝ } = (fun s ↦ s.carrier) t
⊢ { carrier := carrier✝, isClopen' := isClopen'✝ } = t