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 : α → β
H : IsOpenMap f
s : Set β
⊢ IsOpenMap (s.restrictPreimage f)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B ↔ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : ↑(f ⁻¹' s)
y : ↑s
h : y ⤳ s.restrictPreimage f x
a : α
ha : a ⤳ ↑x
hy : f a = ↑y
⊢ a ∈ f ⁻¹' 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 : α → β
H : GeneralizingMap f
s : Set β
⊢ GeneralizingMap (s.restrictPreimage f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
⊢ IsProperMap (s.restrictPreimage f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

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

Tactic:
by

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

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ IsLocallyClosed s ↔ ∃ s', IsLocallyClosed s' ∧ f ⁻¹' s' = s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B ↔ ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us

Tactic:
by

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 : α
L M : BooleanSubalgebra α
h : (fun L ↦ L.carrier) L = (fun L ↦ L.carrier) M
⊢ L = M

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsEmbedding f
⊢ IsLocallyClosed s ↔ ∃ s', IsLocallyClosed s' ∧ s' ∩ range f = f '' s

Tactic:
by

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

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

Tactic:
by simpa using compl_mem L.bot_mem

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

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
⊢ ∃ κ a, W = ⨆ k, U (a k)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsLocallyClosed s
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
⊢ IsLocallyClosed (f '' s)

Tactic:
by

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

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 : α
L : BooleanSubalgebra α
s : Set α
hs : s = ↑L
⊢ s = ↑L.toSublattice

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
hW : IsCompact W.carrier
κ : Type u
a : κ → ι
heq : W = ⨆ k, U (a k)
⊢ W.carrier ⊆ ⋃ i, (U (a i)).carrier

Tactic:
by

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 : α
L : BooleanSubalgebra α
s : Set α
hs : s = ↑L
⊢ ∀ {a : α}, a ∈ (L.copy s ⋯).carrier → aᶜ ∈ (L.copy s ⋯).carrier

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
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst✝¹] s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
x : β
hx : x ∈ U i
this : (∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' f '' s ↔ ⟨x, hx⟩ ∈ (U i).carrier.restrictPreimage f '' Subtype.val ⁻¹' s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst✝] U
hZ : IsClosed[inst✝] Z
⊢ Z ∪ (frontier (U ∩ Z))ᶜ = univ

Tactic:
by

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 : α
L : BooleanSubalgebra α
s : Set α
hs : s = ↑L
⊢ ⊥ ∈ (L.copy s ⋯).carrier

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
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst✝¹] s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
x : β
hx : x ∈ U i
⊢ (∃ y ∈ s, f y ∈ U i ∧ f y = x) → ∃ y ∈ s, f y = x

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
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)

Tactic:
by

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 x✝ : α
⊢ x✝ ∈ {⊥, ⊤} → ∀ ⦃b : α⦄, b ∈ {⊥, ⊤} → x✝ ⊔ b ∈ {⊥, ⊤}

Tactic:
by

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 x✝ : α
⊢ x✝ ∈ {⊥, ⊤} → ∀ ⦃b : α⦄, b ∈ {⊥, ⊤} → x✝ ⊓ b ∈ {⊥, ⊤}

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)

Tactic:
by

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 : α
⊢ ∀ {a : α}, a ∈ {⊥, ⊤} → aᶜ ∈ {⊥, ⊤}

Tactic:
by

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 : α
⊢ ⊥ ∈ {⊥, ⊤}

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
H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsClosed[inst✝¹] s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
x : β
hx : x ∈ U i
this : (∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' f '' s ↔ ⟨x, hx⟩ ∈ (U i).carrier.restrictPreimage f '' (Subtype.val ⁻¹' sᶜ)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

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

Tactic:
by simp [iInf]

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ ↑L = univ ↔ L = ⊤

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
H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsClosed[inst✝¹] s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
x : β
hx : x ∈ U i
⊢ (∃ y ∈ s, f y ∈ U i ∧ f y = x) → ∃ y ∈ s, f y = x

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
⊢ IsClosedMap f ↔ ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)

Tactic:
by

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

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

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 : α
_S : BooleanSubalgebra α
_a : α
⊢ _a ∈ ⊥ → _a ∈ _S

Tactic:
by

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 : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra β
⊢ ∀ {a : α}, a ∈ ⇑f ⁻¹' ↑L → aᶜ ∈ ⇑f ⁻¹' ↑L

Tactic:
by

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 : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra β
⊢ ⊥ ∈ ⇑f ⁻¹' ↑L

Tactic:
by

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 : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra α
a : α
ha : a ∈ ↑L
⊢ aᶜ ∈ ↑L ∧ f aᶜ = (f a)ᶜ

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
hW : IsCompact W.carrier
⊢ ∃ κ, ∃ (_ : Finite κ), ∃ a, W = ⨆ k, U (a k)

Tactic:
by

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 : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra α
⊢ ∀ {a : β}, a ∈ ⇑f '' ↑L → aᶜ ∈ ⇑f '' ↑L

Tactic:
by

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 : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra α
⊢ ⊥ ∈ ↑L ∧ f ⊥ = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsCompact U ∧ IsOpen[inst✝] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, ↑(b i)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
⊢ U.carrier ⊆ ⋃ i, ↑↑i

Tactic:
by

Goal state after:
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
        (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
        L =
      M ↔
    L =
      map
        (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
        M

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
t : Finset ↑Us'
ht : U.carrier ⊆ ⋃ i ∈ t, ↑↑i
⊢ ↑(Finset.image Subtype.val t) ⊆ Us'

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)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
x : X
hx : x ∈ s
⊢ ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
hf : Injective ⇑f
⊢ map f (L ⊓ M) = map f L ⊓ map f M

Tactic:
by

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
f : BoundedLatticeHom α β
h : Surjective ⇑f
⊢ ↑(map f ⊤) = ↑⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
t : Finset ↑Us'
ht : U.carrier ⊆ ⋃ i ∈ t, ↑↑i
⊢ ⋃ i ∈ t, ↑↑i ⊆ ↑(sSup ↑(Finset.image Subtype.val t))

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
h : Continuous[inst✝¹, inst✝] f
⊢ IsInducing f ↔ ∀ (i : ι), IsInducing ((U i).carrier.restrictPreimage f)

Tactic:
by

Goal state after:
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:
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
h : Continuous[inst✝¹, inst✝] f
⊢ IsEmbedding f ↔ ∀ (i : ι), IsEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
⊢ ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us

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 x : α
h : x ∈ s
⊢ x = {(⟨x, h⟩, ⟨⊥, bot_mem⟩)}.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
a : α
⊢ ⊥ = ∅.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
by

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

Goal state before:
pp: α : Type u_5
t₁ t₂ : TopologicalSpace α
Us : Set (Opens α)
hUs : IsBasis Us
⊢ t₁ ≤ t₂ ↔ ∀ U ∈ Us, IsOpen[t₁] ↑U

Tactic:
by

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

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
B : (i : ι) → Set (Opens (α i))
hB : ∀ (i : ι), IsBasis (B i)
⊢ IsBasis (⋃ i, (fun U ↦ { carrier := Sigma.mk i '' U.carrier, is_open' := ⋯ }) '' B i)

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
h : Continuous[inst✝¹, inst✝] f
⊢ IsOpenEmbedding f ↔ ∀ (i : ι), IsOpenEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
hU' : ↑s ⊆ ⋃ i, U i
⊢ s ≤ ⨆ i, { carrier := U i, is_open' := ⋯ }

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
h : Continuous[inst✝¹, inst✝] f
⊢ IsClosedEmbedding f ↔ ∀ (i : ι), IsClosedEmbedding ((U i).carrier.restrictPreimage f)

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
h : Continuous[inst✝¹, inst✝] f
⊢ IsHomeomorph f ↔ ∀ (i : ι), IsHomeomorph ((U i).carrier.restrictPreimage f)

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₁ t₂ : Finset (↑s × ↑s)
⊢ ((t₁.sup fun x ↦ ↑x.1 \ ↑x.2) ⊔ t₂.sup fun x ↦ ↑x.1 \ ↑x.2) = (t₁ ∪ t₂).sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
by

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

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
⊢ IsCompactElement s ↔ IsCompact ↑s

Tactic:
by

Goal state after:
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 : C(α, β)
s : Set (Opens β)
⊢ ↑{ carrier := ⇑f ⁻¹' ↑(sSup s), is_open' := ⋯ } = ↑(sSup ((fun s ↦ { carrier := ⇑f ⁻¹' ↑s, is_open' := ⋯ }) '' s))

Tactic:
by

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

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

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

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
hf : ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)
x : α
y : β
h : (fun x1 x2 ↦ x1 ⤳ x2) y (f x)
i : ι
hx : f x ∈ U i
⊢ ⟨y, ⋯⟩ ⤳ (U i).carrier.restrictPreimage f ⟨x, hx⟩

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)
⊢ (∅.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = {(⟨⊤, top_mem⟩, ⟨⊥, bot_mem⟩)}.sup fun x ↦ ↑x.1 \ ↑x.2

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 ((U i).carrier.restrictPreimage f)

Tactic:
by

Goal state after: