import Mathlib

-- https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/API.2Ftactic.20for.20subspace.20topology

example: ∀ (s t : Set ℝ), IsClosed s → closure (s ∩ t) ∩ t ⊆ s ∩ t
example (
s: Set ℝ
s 
t: Set ℝ
t : 
Set: Type → Type
Set 
ℝ: Type
ℝ) (
hs: IsClosed s
hs : 
IsClosed: {X : Type} → [inst : TopologicalSpace X] → Set X → Prop
IsClosed 
s: Set ℝ
s) : 
closure: {X : Type} → [inst : TopologicalSpace X] → Set X → Set X
closure (
s: Set ℝ
s ∩ 
t: Set ℝ
t) ∩ 
t: Set ℝ
t ⊆ 
s: Set ℝ
s ∩ 
t: Set ℝ
t := by
Goals accomplished! 🐙
  simp only [
Set.subset_inter_iff: ∀ {α : Type ?u.694} {s t r : Set α}, r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t
Set.subset_inter_iff, 
Set.inter_subset_right: ∀ {α : Type ?u.719} {s t : Set α}, s ∩ t ⊆ t
Set.inter_subset_right, 
and_true: ∀ (p : Prop), (p ∧ True) = p
and_true]
s, t: Set ℝ
hs: IsClosed s
closure (s ∩ t) ∩ t ⊆ s
  intro 
x: ℝ
x 
hx: x ∈ closure (s ∩ t) ∩ t
hx
s, t: Set ℝ
hs: IsClosed s
x: ℝ
hx: x ∈ closure (s ∩ t) ∩ t
x ∈ s
  obtain 
⟨hxst, _hxt⟩: x ∈ closure (s ∩ t) ∩ t
⟨
hxst: x ∈ closure (s ∩ t)
hxst
⟨hxst, _hxt⟩: x ∈ closure (s ∩ t) ∩ t
, 
_hxt: x ∈ t
_hxt
⟨hxst, _hxt⟩: x ∈ closure (s ∩ t) ∩ t
⟩ := 
hx: x ∈ closure (s ∩ t) ∩ t
hx
s, t: Set ℝ
hs: IsClosed s
x: ℝ
hxst: x ∈ closure (s ∩ t)
_hxt: x ∈ t
intro
x ∈ s
  have 
hsub: closure (s ∩ t) ⊆ s
hsub : 
closure: {X : Type} → [inst : TopologicalSpace X] → Set X → Set X
closure (
s: Set ℝ
s ∩ 
t: Set ℝ
t) ⊆ 
s: Set ℝ
s :=
s, t: Set ℝ
hs: IsClosed s
x: ℝ
hxst: x ∈ closure (s ∩ t)
_hxt: x ∈ t
intro
x ∈ s by
Goals accomplished! 🐙
    rw [
s, t: Set ℝ
hs: IsClosed s
x: ℝ
hxst: x ∈ closure (s ∩ t)
_hxt: x ∈ t
closure (s ∩ t) ⊆ s
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
IsClosed.closure_subset_iff: ∀ {X : Type} {s t : Set X} [inst : TopologicalSpace X], IsClosed t → (closure s ⊆ t ↔ s ⊆ t)
IsClosed.closure_subset_iff 
hs: IsClosed s
hs)
s, t: Set ℝ
hs: IsClosed s
x: ℝ
hxst: x ∈ closure (s ∩ t)
_hxt: x ∈ t
s ∩ t ⊆ s]
s, t: Set ℝ
hs: IsClosed s
x: ℝ
hxst: x ∈ closure (s ∩ t)
_hxt: x ∈ t
s ∩ t ⊆ s
    exact 
Set.inter_subset_left: ∀ {α : Type} {s t : Set α}, s ∩ t ⊆ s
Set.inter_subset_left
Goals accomplished! 🐙
  exact 
hsub: closure (s ∩ t) ⊆ s
hsub 
hxst: x ∈ closure (s ∩ t)
hxst
Goals accomplished! 🐙

example: ∀ (s t : Set ℝ), IsClosed (s ∩ t) → closure (s ∩ t) ∩ t ⊆ s ∩ t
example (
s: Set ℝ
s 
t: Set ℝ
t : 
Set: Type → Type
Set 
ℝ: Type
ℝ) (
hst: IsClosed (s ∩ t)
hst: 
IsClosed: {X : Type} → [inst : TopologicalSpace X] → Set X → Prop
IsClosed (
s: Set ℝ
s ∩ 
t: Set ℝ
t)) : 
closure: {X : Type} → [inst : TopologicalSpace X] → Set X → Set X
closure (
s: Set ℝ
s ∩ 
t: Set ℝ
t) ∩ 
t: Set ℝ
t ⊆ 
s: Set ℝ
s ∩ 
t: Set ℝ
t := by
Goals accomplished! 🐙
  simp only [
Set.subset_inter_iff: ∀ {α : Type ?u.2189} {s t r : Set α}, r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t
Set.subset_inter_iff, 
Set.inter_subset_right: ∀ {α : Type ?u.2214} {s t : Set α}, s ∩ t ⊆ t
Set.inter_subset_right, 
and_true: ∀ (p : Prop), (p ∧ True) = p
and_true]
s, t: Set ℝ
hst: IsClosed (s ∩ t)
closure (s ∩ t) ∩ t ⊆ s
  intro 
x: ℝ
x 
hx: x ∈ closure (s ∩ t) ∩ t
hx
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hx: x ∈ closure (s ∩ t) ∩ t
x ∈ s
  obtain 
⟨hxst, _hxt⟩: x ∈ closure (s ∩ t) ∩ t
⟨
hxst: x ∈ closure (s ∩ t)
hxst
⟨hxst, _hxt⟩: x ∈ closure (s ∩ t) ∩ t
, 
_hxt: x ∈ t
_hxt
⟨hxst, _hxt⟩: x ∈ closure (s ∩ t) ∩ t
⟩ := 
hx: x ∈ closure (s ∩ t) ∩ t
hx
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
_hxt: x ∈ t
intro
x ∈ s
  have 
_hclosed: IsClosed (closure (s ∩ t))
_hclosed : 
IsClosed: {X : Type} → [inst : TopologicalSpace X] → Set X → Prop
IsClosed (
closure: {X : Type} → [inst : TopologicalSpace X] → Set X → Set X
closure (
s: Set ℝ
s ∩ 
t: Set ℝ
t)) :=
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
_hxt: x ∈ t
intro
x ∈ s by
Goals accomplished! 🐙
    exact 
isClosed_closure: ∀ {X : Type} {s : Set X} [inst : TopologicalSpace X], IsClosed (closure s)
isClosed_closure
Goals accomplished! 🐙
  have 
hsub: s ∩ t ⊆ s
hsub : (
s: Set ℝ
s ∩ 
t: Set ℝ
t) ⊆ 
s: Set ℝ
s :=
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
_hxt: x ∈ t
_hclosed: IsClosed (closure (s ∩ t))
intro
x ∈ s by
Goals accomplished! 🐙 exact 
Set.inter_subset_left: ∀ {α : Type} {s t : Set α}, s ∩ t ⊆ s
Set.inter_subset_left
Goals accomplished! 🐙
  have 
hsub'': closure (s ∩ t) ⊆ s ∩ t
hsub'' : 
closure: {X : Type} → [inst : TopologicalSpace X] → Set X → Set X
closure (
s: Set ℝ
s ∩ 
t: Set ℝ
t) ⊆ (
s: Set ℝ
s ∩ 
t: Set ℝ
t) :=
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
_hxt: x ∈ t
_hclosed: IsClosed (closure (s ∩ t))
hsub: s ∩ t ⊆ s
intro
x ∈ s by
Goals accomplished! 🐙
    rw [
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
_hxt: x ∈ t
_hclosed: IsClosed (closure (s ∩ t))
hsub: s ∩ t ⊆ s
closure (s ∩ t) ⊆ s ∩ t
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
IsClosed.closure_subset_iff: ∀ {X : Type} {s t : Set X} [inst : TopologicalSpace X], IsClosed t → (closure s ⊆ t ↔ s ⊆ t)
IsClosed.closure_subset_iff 
hst: IsClosed (s ∩ t)
hst)
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
_hxt: x ∈ t
_hclosed: IsClosed (closure (s ∩ t))
hsub: s ∩ t ⊆ s
s ∩ t ⊆ s ∩ t]
Goals accomplished! 🐙
  exact 
hsub: s ∩ t ⊆ s
hsub (
hsub'': closure (s ∩ t) ⊆ s ∩ t
hsub'' 
hxst: x ∈ closure (s ∩ t)
hxst)
Goals accomplished! 🐙
  done
Warning: 'done' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
Goals accomplished! 🐙

example: ∀ (s t : Set ℝ), IsClosed (s ∩ t) → closure (s ∩ t) ∩ t ⊆ s ∩ t
example (
s: Set ℝ
s 
t: Set ℝ
t : 
Set: Type → Type
Set 
ℝ: Type
ℝ) (
hst: IsClosed (s ∩ t)
hst: 
IsClosed: {X : Type} → [inst : TopologicalSpace X] → Set X → Prop
IsClosed (
s: Set ℝ
s ∩ 
t: Set ℝ
t)) : 
closure: {X : Type} → [inst : TopologicalSpace X] → Set X → Set X
closure (
s: Set ℝ
s ∩ 
t: Set ℝ
t) ∩ 
t: Set ℝ
t ⊆ 
s: Set ℝ
s ∩ 
t: Set ℝ
t := by
Goals accomplished! 🐙
  simp only [
Set.subset_inter_iff: ∀ {α : Type ?u.4483} {s t r : Set α}, r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t
Set.subset_inter_iff, 
Set.inter_subset_right: ∀ {α : Type ?u.4508} {s t : Set α}, s ∩ t ⊆ t
Set.inter_subset_right, 
and_true: ∀ (p : Prop), (p ∧ True) = p
and_true]
s, t: Set ℝ
hst: IsClosed (s ∩ t)
closure (s ∩ t) ∩ t ⊆ s
  intro 
x: ℝ
x 
hx: x ∈ closure (s ∩ t) ∩ t
hx
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hx: x ∈ closure (s ∩ t) ∩ t
x ∈ s
  obtain 
⟨hxst, _⟩: x ∈ closure (s ∩ t) ∩ t
⟨
hxst: x ∈ closure (s ∩ t)
hxst
⟨hxst, _⟩: x ∈ closure (s ∩ t) ∩ t
, 
_: x ∈ t
_
⟨hxst, _⟩: x ∈ closure (s ∩ t) ∩ t
⟩ := 
hx: x ∈ closure (s ∩ t) ∩ t
hx
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
intro
x ∈ s
  have 
h: s ∩ t ⊆ s
h : (
s: Set ℝ
s ∩ 
t: Set ℝ
t) ⊆ 
s: Set ℝ
s :=
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
intro
x ∈ s by
Goals accomplished! 🐙 exact 
Set.inter_subset_left: ∀ {α : Type} {s t : Set α}, s ∩ t ⊆ s
Set.inter_subset_left
Goals accomplished! 🐙
  have 
hsub: closure (s ∩ t) ⊆ s ∩ t
hsub : 
closure: {X : Type} → [inst : TopologicalSpace X] → Set X → Set X
closure (
s: Set ℝ
s ∩ 
t: Set ℝ
t) ⊆ (
s: Set ℝ
s ∩ 
t: Set ℝ
t) :=
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
h: s ∩ t ⊆ s
intro
x ∈ s by
Goals accomplished! 🐙
    rw [
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
h: s ∩ t ⊆ s
closure (s ∩ t) ⊆ s ∩ t
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
IsClosed.closure_subset_iff: ∀ {X : Type} {s t : Set X} [inst : TopologicalSpace X], IsClosed t → (closure s ⊆ t ↔ s ⊆ t)
IsClosed.closure_subset_iff 
hst: IsClosed (s ∩ t)
hst)
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
h: s ∩ t ⊆ s
s ∩ t ⊆ s ∩ t]
Goals accomplished! 🐙
  exact 
h: s ∩ t ⊆ s
h (
hsub: closure (s ∩ t) ⊆ s ∩ t
hsub 
hxst: x ∈ closure (s ∩ t)
hxst)
Goals accomplished! 🐙
  done
Warning: 'done' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
Goals accomplished! 🐙

variable {
X: Type ?u.8991
X} [
TopologicalSpace: Type u_1 → Type u_1
TopologicalSpace 
X: Type ?u.8991
X]

def 
restrict: (A : Set X) → Set X → Set ↑A
restrict (
A: Set X
A : 
Set: Type u_1 → Type u_1
Set 
X: Type u_1
X) : 
Set: Type u_1 → Type u_1
Set 
X: Type u_1
X → 
Set: Type u_1 → Type u_1
Set 
A: Set X
A := fun 
B: Set X
B ↦ {
x: ↑A
x | ↑
x: ↑A
x ∈ 
B: Set X
B}

-- @[simp]
-- lemma restrict_coe {A : Set X} ( C : Set X) : (Subtype.val ⁻¹' C : Set A) = (restrict A C) := rfl

example: ∀ {X : Type u_1} (s t : Set X), restrict t s = Subtype.val ⁻¹' s
example (
s: Set X
s 
t: Set X
t : 
Set: Type u_1 → Type u_1
Set 
X: Type u_1
X) : 
restrict: {X : Type u_1} → (A : Set X) → Set X → Set ↑A
restrict 
t: Set X
t 
s: Set X
s = (
Subtype.val: {α : Type u_1} → {p : α → Prop} → Subtype p → α
Subtype.val ⁻¹' 
s: Set X
s : 
Set: Type u_1 → Type u_1
Set 
t: Set X
t) := by
Goals accomplished! 🐙
  ext 
x: ↑t
x
X: Type u_1
inst✝: TopologicalSpace X
s, t: Set X
x: ↑t
h
x ∈ restrict t s ↔ x ∈ Subtype.val ⁻¹' s
  simp [
restrict: {X : Type ?u.5837} → (A : Set X) → Set X → Set ↑A
restrict]
Goals accomplished! 🐙


example: ∀ {X : Type u_1} [inst : TopologicalSpace X] (s t : Set X), IsClosed (restrict t s) → closure (s ∩ t) ∩ t ⊆ s ∩ t
example
Warning: declaration uses 'sorry' (
s: Set X
s 
t: Set X
t : 
Set: Type u_1 → Type u_1
Set 
X: Type u_1
X) (
hs: IsClosed (restrict t s)
hs : 
IsClosed: {X : Type u_1} → [inst : TopologicalSpace X] → Set X → Prop
IsClosed (
restrict: {X : Type u_1} → (A : Set X) → Set X → Set ↑A
restrict 
t: Set X
t 
s: Set X
s)) : 
closure: {X : Type u_1} → [inst : TopologicalSpace X] → Set X → Set X
closure (
s: Set X
s ∩ 
t: Set X
t) ∩ 
t: Set X
t ⊆ 
s: Set X
s ∩ 
t: Set X
t := by
Goals accomplished! 🐙
  simp only [
Set.subset_inter_iff: ∀ {α : Type ?u.7071} {s t r : Set α}, r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t
Set.subset_inter_iff, 
Set.inter_subset_right: ∀ {α : Type ?u.7096} {s t : Set α}, s ∩ t ⊆ t
Set.inter_subset_right, 
and_true: ∀ (p : Prop), (p ∧ True) = p
and_true]
X: Type u_1
inst✝: TopologicalSpace X
s, t: Set X
hs: IsClosed (restrict t s)
closure (s ∩ t) ∩ t ⊆ s
  intro 
x: X
x 
hx: x ∈ closure (s ∩ t) ∩ t
hx
X: Type u_1
inst✝: TopologicalSpace X
s, t: Set X
hs: IsClosed (restrict t s)
x: X
hx: x ∈ closure (s ∩ t) ∩ t
x ∈ s
  obtain 
⟨hxst, _⟩: x ∈ closure (s ∩ t) ∩ t
⟨
hxst: x ∈ closure (s ∩ t)
hxst
⟨hxst, _⟩: x ∈ closure (s ∩ t) ∩ t
, 
_: x ∈ t
_
⟨hxst, _⟩: x ∈ closure (s ∩ t) ∩ t
⟩ := 
hx: x ∈ closure (s ∩ t) ∩ t
hx
X: Type u_1
inst✝: TopologicalSpace X
s, t: Set X
hs: IsClosed (restrict t s)
x: X
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
intro
x ∈ s
  have 
h: s ∩ t ⊆ s
h : (
s: Set X
s ∩ 
t: Set X
t) ⊆ 
s: Set X
s :=
X: Type u_1
inst✝: TopologicalSpace X
s, t: Set X
hs: IsClosed (restrict t s)
x: X
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
intro
x ∈ s by
Goals accomplished! 🐙 exact 
Set.inter_subset_left: ∀ {α : Type u_1} {s t : Set α}, s ∩ t ⊆ s
Set.inter_subset_left
Goals accomplished! 🐙
  have 
hsub: closure (restrict t s) ⊆ restrict t s
hsub : 
closure: {X : Type u_1} → [inst : TopologicalSpace X] → Set X → Set X
closure (
restrict: {X : Type u_1} → (A : Set X) → Set X → Set ↑A
restrict 
t: Set X
t 
s: Set X
s) ⊆ (
restrict: {X : Type u_1} → (A : Set X) → Set X → Set ↑A
restrict 
t: Set X
t 
s: Set X
s) :=
X: Type u_1
inst✝: TopologicalSpace X
s, t: Set X
hs: IsClosed (restrict t s)
x: X
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
h: s ∩ t ⊆ s
intro
x ∈ s by
Goals accomplished! 🐙 rwa [
X: Type u_1
inst✝: TopologicalSpace X
s, t: Set X
hs: IsClosed (restrict t s)
x: X
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
h: s ∩ t ⊆ s
closure (restrict t s) ⊆ restrict t s
IsClosed.closure_subset_iff: ∀ {X : Type u_1} {s t : Set X} [inst : TopologicalSpace X], IsClosed t → (closure s ⊆ t ↔ s ⊆ t)
IsClosed.closure_subset_iff
X: Type u_1
inst✝: TopologicalSpace X
s, t: Set X
hs: IsClosed (restrict t s)
x: X
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
h: s ∩ t ⊆ s
restrict t s ⊆ restrict t s
X: Type u_1
inst✝: TopologicalSpace X
s, t: Set X
hs: IsClosed (restrict t s)
x: X
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
h: s ∩ t ⊆ s
IsClosed (restrict t s)]
X: Type u_1
inst✝: TopologicalSpace X
s, t: Set X
hs: IsClosed (restrict t s)
x: X
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
h: s ∩ t ⊆ s
IsClosed (restrict t s)
  have 
hsub': restrict t s ⊆ closure (restrict t s)
hsub' : (
restrict: {X : Type u_1} → (A : Set X) → Set X → Set ↑A
restrict 
t: Set X
t 
s: Set X
s) ⊆ 
closure: {X : Type u_1} → [inst : TopologicalSpace X] → Set X → Set X
closure (
restrict: {X : Type u_1} → (A : Set X) → Set X → Set ↑A
restrict 
t: Set X
t 
s: Set X
s) :=
X: Type u_1
inst✝: TopologicalSpace X
s, t: Set X
hs: IsClosed (restrict t s)
x: X
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
h: s ∩ t ⊆ s
hsub: closure (restrict t s) ⊆ restrict t s
intro
x ∈ s by
Goals accomplished! 🐙 exact 
subset_closure: ∀ {X : Type u_1} {s : Set X} [inst : TopologicalSpace X], s ⊆ closure s
subset_closure
Goals accomplished! 🐙
  have 
hsub'': s ∩ t ⊆ closure (s ∩ t)
hsub'' : (
s: Set X
s ∩ 
t: Set X
t) ⊆ 
closure: {X : Type u_1} → [inst : TopologicalSpace X] → Set X → Set X
closure (
s: Set X
s ∩ 
t: Set X
t) :=
X: Type u_1
inst✝: TopologicalSpace X
s, t: Set X
hs: IsClosed (restrict t s)
x: X
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
h: s ∩ t ⊆ s
hsub: closure (restrict t s) ⊆ restrict t s
hsub': restrict t s ⊆ closure (restrict t s)
intro
x ∈ s by
Goals accomplished! 🐙 exact 
subset_closure: ∀ {X : Type u_1} {s : Set X} [inst : TopologicalSpace X], s ⊆ closure s
subset_closure
Goals accomplished! 🐙
  have 
he: restrict t s = closure (restrict t s)
he : (
restrict: {X : Type u_1} → (A : Set X) → Set X → Set ↑A
restrict 
t: Set X
t 
s: Set X
s) = 
closure: {X : Type u_1} → [inst : TopologicalSpace X] → Set X → Set X
closure (
restrict: {X : Type u_1} → (A : Set X) → Set X → Set ↑A
restrict 
t: Set X
t 
s: Set X
s) :=
X: Type u_1
inst✝: TopologicalSpace X
s, t: Set X
hs: IsClosed (restrict t s)
x: X
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
h: s ∩ t ⊆ s
hsub: closure (restrict t s) ⊆ restrict t s
hsub': restrict t s ⊆ closure (restrict t s)
hsub'': s ∩ t ⊆ closure (s ∩ t)
intro
x ∈ s by
Goals accomplished! 🐙 exact 
Set.Subset.antisymm: ∀ {α : Type u_1} {a b : Set α}, a ⊆ b → b ⊆ a → a = b
Set.Subset.antisymm 
hsub': restrict t s ⊆ closure (restrict t s)
hsub' 
hsub: closure (restrict t s) ⊆ restrict t s
hsub
Goals accomplished! 🐙
  -- have hq : (restrict t s) ⊆ t := sorry
  obtain 
⟨y, ⟨hy, hy'⟩⟩: IsOpen (restrict t s)ᶜ
⟨
y: Set X
y
⟨y, ⟨hy, hy'⟩⟩: IsOpen (restrict t s)ᶜ
, 
⟨hy, hy'⟩: IsOpen y ∧ Subtype.val ⁻¹' y = (restrict t s)ᶜ
⟨
hy: IsOpen y
hy
⟨hy, hy'⟩: IsOpen y ∧ Subtype.val ⁻¹' y = (restrict t s)ᶜ
, 
hy': Subtype.val ⁻¹' y = (restrict t s)ᶜ
hy'
⟨hy, hy'⟩: IsOpen y ∧ Subtype.val ⁻¹' y = (restrict t s)ᶜ
⟩
⟨y, ⟨hy, hy'⟩⟩: IsOpen (restrict t s)ᶜ
⟩ := 
hs: IsClosed (restrict t s)
hs
X: Type u_1
inst✝: TopologicalSpace X
s, t: Set X
x: X
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
h: s ∩ t ⊆ s
hsub: closure (restrict t s) ⊆ restrict t s
hsub': restrict t s ⊆ closure (restrict t s)
hsub'': s ∩ t ⊆ closure (s ∩ t)
he: restrict t s = closure (restrict t s)
y: Set X
hy: IsOpen y
hy': Subtype.val ⁻¹' y = (restrict t s)ᶜ
intro.mk.intro.intro
x ∈ s
  -- have h' : (s ∩ t) ⊆ (restrict t s) := by
  --   rw?
  sorry
Goals accomplished! 🐙
  done
Warning: 'done' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
Goals accomplished! 🐙

-- example (s t : Set X) (hs : IsClosed (Subtype.val ⁻¹' s : Set t)) : closure (s ∩ t) ∩ t ⊆ s ∩ t := by
--   suffices : closure (Subtype.val ⁻¹' s : Set t) ⊆ (Subtype.val ⁻¹' s : Set t)
--   · convert Set.image_subset Subtype.val this <;> simp [embedding_subtype_val.closure_eq_preimage_closure_image]
--   rwa [IsClosed.closure_subset_iff]

variable {α : Type u} {β : Type v}

def image    (f : α → β) (s : Set α) : Set β := {f x | x ∈ s}
def preimage (f : α → β) (s : Set β) : Set α := { x | f x ∈ s }


variable  (s t : Set X) in
#check
IsClosed (Subtype.val ⁻¹' s) : Prop 
IsClosed: {X : Type u_1} → [inst : TopologicalSpace X] → Set X → Prop
IsClosed (
Set.preimage: {α β : Type u_1} → (α → β) → Set β → Set α
Set.preimage 
Subtype.val: {α : Type u_1} → {p : α → Prop} → Subtype p → α
Subtype.val 
s: Set X
s)

example: ∀ {X : Type u_1} [inst : TopologicalSpace X] (s t : Set X), IsClosed (Subtype.val ⁻¹' s) → closure (s ∩ t) ∩ t ⊆ s ∩ t
example
Warning: declaration uses 'sorry' (
s: Set X
s 
t: Set X
t : 
Set: Type u_1 → Type u_1
Set 
X: Type u_1
X) (
hs: IsClosed (Subtype.val ⁻¹' s)
hs : 
IsClosed: {X : Type u_1} → [inst : TopologicalSpace X] → Set X → Prop
IsClosed (
Subtype.val: {α : Type u_1} → {p : α → Prop} → Subtype p → α
Subtype.val ⁻¹' 
s: Set X
s : 
Set: Type u_1 → Type u_1
Set 
t: Set X
t)) : 
closure: {X : Type u_1} → [inst : TopologicalSpace X] → Set X → Set X
closure (
s: Set X
s ∩ 
t: Set X
t) ∩ 
t: Set X
t ⊆ 
s: Set X
s ∩ 
t: Set X
t := by
Goals accomplished! 🐙
  sorry
Goals accomplished! 🐙
  done
Warning: 'done' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
Goals accomplished! 🐙


-- example (s t : Set ℝ) (hs : IsOpen s): closure (s ∩ t) ∩ t ⊆ s ∩ t := by
--   simp only [Set.subset_inter_iff, Set.inter_subset_right, and_true]
--   intro x hx
--   obtain ⟨hxst, hxt⟩ := hx
--   rw [mem_closure_iff] at hxst
--   have h := hxst s hs
--   have he : (s ∩ (s ∩ t)) = s ∩ t := by
--     simp only [Set.inter_eq_right, Set.inter_subset_left]
--   have hne (hu: Set.Nonempty (s ∩ t)) : Set.Nonempty (s ∩ (s ∩ t)) := by
--     rw [he]
--     exact hu

--   done

-- open Set

-- example (s t : Set ℝ) : closure (s ∩ t) ∩ t ⊆ s ∩ t := by
--   rw [← Subtype.image_preimage_val, ← Subtype.image_preimage_val,
--     image_subset_image_iff Subtype.val_injective]
--   intros t ht
--   rw [mem_preimage, ← closure_subtype] at ht
--   revert ht t
--   apply IsClosed.closure_subset