mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap (f ∘ Subtype.val)

Tactic:
by

Goal state after:
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
x✝ : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
H : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s := x✝
⊢ IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)

Tactic:
by

Goal state after:
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
⊢ GeneralizingMap f ↔ ∀ (i : ι), GeneralizingMap (f ∘ Subtype.val)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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 s

Tactic:
by

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝ : Finset (↑s × ↑s)
x✝² : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝¹ : ∃ t_1, (t.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t_1.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝ : (x, y) ∉ t
tc : Finset (↑s × ↑s)
eq : (t.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ((↑x \ ↑y)ᶜ ⊓ ∅.sup fun x ↦ ↑x.1 \ ↑x.2) = ∅.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ [IsLocallyClosed s, IsOpen[inst✝] (coborder s), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s,
      IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)].TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
⊢ IsCompact s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ NoetherianSpace α ↔ WellFoundedLT (Closeds α)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
⊢ NoetherianSpace (CofiniteTopology α)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ NoetherianSpace ↑s ↔ ∀ t ⊆ s, IsCompact t

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), NoetherianSpace ↑(f i)
⊢ NoetherianSpace ↑(⋃ i, f i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Closeds α
h : s.carrier = t.carrier
⊢ s = t

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
s t : Closeds α
⊢ ↑(s ⊔ t) = ↑s ∪ ↑t

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
S : Set (Closeds α)
⊢ ↑(sSup S) = closure[inst✝] (⋃₀ (SetLike.coe '' S))

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by simp [iInf]

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

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

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : Closeds α
s : Set (Closeds α)
⊢ ↑(⨅ b ∈ s, a ⊔ b) = ↑(a ⊔ sInf s)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Closeds α
⊢ (Opens.compl ∘ ⇑ofDual) ((⇑toDual ∘ compl) s) = s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : (Opens α)ᵒᵈ
⊢ (⇑toDual ∘ compl) ((Opens.compl ∘ ⇑ofDual) s) = s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Opens α
⊢ (Closeds.compl ∘ ⇑ofDual) ((⇑toDual ∘ compl) s) = s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : (Closeds α)ᵒᵈ
⊢ (⇑toDual ∘ compl) ((Closeds.compl ∘ ⇑ofDual) s) = s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Closeds α
hs : IsAtom s
⊢ ∃ a, ↑s = {a}

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Closeds α
⊢ IsAtom s ↔ ∃ x, s = {x}

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Opens α
⊢ IsCoatom s ↔ ∃ x, s = {x}.compl

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Clopens α
h : (fun s ↦ s.carrier) s = (fun s ↦ s.carrier) t
⊢ s = t

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : TopologicalSpace α
s : Finset ι
U : ι → Clopens α
⊢ ↑(s.sup U) = ⋃ i ∈ s, ↑(U i)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
s t : Clopens α
⊢ Disjoint ↑s ↑t ↔ Disjoint s t

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : IrreducibleCloseds α
h : s.carrier = t.carrier
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case inr.refine_2
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, ⋯⟩
hU'' : ⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i) = ⊤
⊢ range f₀ ⊆ ↑(⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i))

Tactic:
rw [hU'']; simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
⊢ Function.Injective (map f ⋯)

Tactic:
by

Goal state after:
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
V : IrreducibleCloseds β
⊢ (fun V ↦ { carrier := f ⁻¹' ↑↑V, isIrreducible' := ⋯, isClosed' := ⋯ }) ((fun T ↦ ⟨map f ⋯ T, ⋯⟩) V) = V

Tactic:
by

Goal state after:
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
V : ↑{V | (f ⁻¹' ↑V).Nonempty}
⊢ (fun T ↦ ⟨map f ⋯ T, ⋯⟩) ((fun V ↦ { carrier := f ⁻¹' ↑↑V, isIrreducible' := ⋯, isClosed' := ⋯ }) V) = V

Tactic:
by

Goal state after:
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 β
⊢ { 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:
by

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ a ∈ closure s ↔ ∃ t, a = t.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

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

Tactic:
by

Goal state after:
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, ⋯⟩
hU'' : ⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i) = ⊤
i : ι
⊢ Continuous[inst✝ i, instTopologicalSpaceSubtype] (f₀ ∘ iV i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
hs : IsClosed[inst✝¹] s
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsClosed[inst✝¹] t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ s = ⋃₀ S

Tactic:
by

Goal state after:
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:
by

Goal state after:
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) ⋯
x : α
hx : x ∈ closure s
⊢ p x hx

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
⊢ (irreducibleComponents α).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Spectral.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : SpectralMap α β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Spectral.Hom

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : SpectralMap β γ
f₁ f₂ : SpectralMap α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
⊢ ∃ o, IsOpen[inst✝¹] o ∧ o.Nonempty ∧ o ⊆ Z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
⊢ IsQuasiSeparated univ ↔ QuasiSeparatedSpace α

Tactic:
by

Goal state after:
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:
by

Goal state after:
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'
hf' : range f' = f ⁻¹' ↑(U i)
e : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) ≃ₜ ↑(f ⁻¹' ↑(U i)) := this.toHomeomorph.trans (Homeomorph.setCongr hf')
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] ((U i).carrier.restrictPreimage f)

Tactic:
by

Goal state after:
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)
⊢ IsEmbedding f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
⊢ IsQuasiSeparated (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
⊢ IsQuasiSeparated s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : QuasiSeparatedSpace β
h : IsOpenEmbedding f
⊢ QuasiSeparatedSpace α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsOpen[inst✝] s
⊢ IsQuasiSeparated s ↔ QuasiSeparatedSpace ↑s

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ IsCompact (U ∩ V)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
h : ¬∀ t ∈ s, IsOpen[inst✝¹] t
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
⊢ s ⊆ a ∪ b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
h : ¬∀ t ∈ s, IsOpen[inst✝¹] t
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
⊢ a ∪ b ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
b : ι → Set X
basis : IsTopologicalBasis (Set.range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
⊢ ∀ U ∈ Set.range b, IsCompact U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_3
U : ι → Opens X
hU : IsOpenCover U
inst✝ : ∀ (i : ι), PrespectralSpace ↥(U i)
⊢ PrespectralSpace X

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace Y
f : X → Y
hf : IsInducing f
hf' : IsSpectralMap f
⊢ ∀ U ∈ Set.preimage f '' {U | IsOpen[inst✝¹] U ∧ IsCompact U}, IsCompact U

Tactic:
by

Goal state after: