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 := byGoals accomplished! 🐙
  simp only [Set.subset_inter_iff: ∀ {α : Type ?u.659} {s t r : Set α}, r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t
Set.subset_inter_iff, Set.inter_subset_right: ∀ {α : Type ?u.684} (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
hxs, t: Set ℝ
hs: IsClosed s
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
,s, t: Set ℝ
hs: IsClosed s
x: ℝ
hx: x ∈ closure (s ∩ t) ∩ t
x ∈ s⟨hxst, : x ∈ closure (s ∩ t) ∩ t
 hxt: x ∈ t
hxtWarning: unused variable `hxt`
note: this linter can be disabled with `set_option linter.unusedVariables false`
s, t: Set ℝ
hs: IsClosed s
x: ℝ
hx: x ∈ closure (s ∩ t) ∩ t
x ∈ s⟩: x ∈ closure (s ∩ t) ∩ t
⟩ := hx: x ∈ closure (s ∩ t) ∩ t
hxs, t: Set ℝ
hs: IsClosed s
x: ℝ
hxst: x ∈ closure (s ∩ t)
hxt: x ∈ t
introx ∈ 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
introx ∈ s byGoals accomplished! 🐙
    rw [s, t: Set ℝ
hs: IsClosed s
x: ℝ
hxst: x ∈ closure (s ∩ t)
hxt: x ∈ t
closure (s ∩ t) ⊆ spropext: ∀ {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 s: Set ℝ
s t: Set ℝ
tGoals accomplished! 🐙
  exact hsub: closure (s ∩ t) ⊆ s
hsub hxst: x ∈ closure (s ∩ t)
hxstGoals 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 := byGoals accomplished! 🐙
  simp only [Set.subset_inter_iff: ∀ {α : Type ?u.2148} {s t r : Set α}, r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t
Set.subset_inter_iff, Set.inter_subset_right: ∀ {α : Type ?u.2173} (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
hxs, 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
,s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hx: x ∈ closure (s ∩ t) ∩ t
x ∈ s⟨hxst, : x ∈ closure (s ∩ t) ∩ t
 hxt: x ∈ t
hxtWarning: unused variable `hxt`
note: this linter can be disabled with `set_option linter.unusedVariables false`
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hx: x ∈ closure (s ∩ t) ∩ t
x ∈ s⟩: x ∈ closure (s ∩ t) ∩ t
⟩ := hx: x ∈ closure (s ∩ t) ∩ t
hxs, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
hxt: x ∈ t
introx ∈ s
  haves, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
hxt: x ∈ t
introx ∈ s hclosed: IsClosed (closure (s ∩ t))
hclosedWarning: unused variable `hclosed`
note: this linter can be disabled with `set_option linter.unusedVariables false`
s, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
hxt: x ∈ t
introx ∈ s : 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
introx ∈ s byGoals accomplished! 🐙
    exact isClosed_closure: ∀ {X : Type} {s : Set X} [inst : TopologicalSpace X], IsClosed (closure s)
isClosed_closureGoals 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))
introx ∈ s byGoals accomplished! 🐙 exact Set.inter_subset_left: ∀ {α : Type} (s t : Set α), s ∩ t ⊆ s
Set.inter_subset_left s: Set ℝ
s t: Set ℝ
tGoals accomplished! 🐙
  haves, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
hxt: x ∈ t
hclosed: IsClosed (closure (s ∩ t))
hsub: s ∩ t ⊆ s
introx ∈ s hsub': s ∩ t ⊆ closure (s ∩ t)
hsub'Warning: unused variable `hsub'`
note: this linter can be disabled with `set_option linter.unusedVariables false`
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
introx ∈ s : (s: Set ℝ
s ∩ t: Set ℝ
t) ⊆ 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
hclosed: IsClosed (closure (s ∩ t))
hsub: s ∩ t ⊆ s
introx ∈ s byGoals accomplished! 🐙 exact subset_closure: ∀ {X : Type} {s : Set X} [inst : TopologicalSpace X], s ⊆ closure s
subset_closureGoals 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
hsub': s ∩ t ⊆ closure (s ∩ t)
introx ∈ s byGoals 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
hsub': s ∩ t ⊆ closure (s ∩ t)
closure (s ∩ t) ⊆ s ∩ tpropext: ∀ {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
hsub': s ∩ t ⊆ closure (s ∩ t)
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! 🐙
  doneGoals 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 := byGoals accomplished! 🐙
  simp only [Set.subset_inter_iff: ∀ {α : Type ?u.4729} {s t r : Set α}, r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t
Set.subset_inter_iff, Set.inter_subset_right: ∀ {α : Type ?u.4754} (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
hxs, 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
hxs, t: Set ℝ
hst: IsClosed (s ∩ t)
x: ℝ
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
introx ∈ 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
introx ∈ s byGoals accomplished! 🐙 exact Set.inter_subset_left: ∀ {α : Type} (s t : Set α), s ∩ t ⊆ s
Set.inter_subset_left s: Set ℝ
s t: Set ℝ
tGoals 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
introx ∈ s byGoals 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 ∩ tpropext: ∀ {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! 🐙
  doneGoals accomplished! 🐙

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

def restrict: {X : Type u_1} → (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) := byGoals accomplished! 🐙
  ext x: ↑t
xX: Type ?u.5842
inst✝: TopologicalSpace X
s, t: Set X
x: ↑t
hx ∈ restrict t s ↔ x ∈ Subtype.val ⁻¹' s
  simp [restrict: {X : Type ?u.6040} → (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
exampleWarning: 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 := byGoals accomplished! 🐙
  simp only [Set.subset_inter_iff: ∀ {α : Type ?u.10454} {s t r : Set α}, r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t
Set.subset_inter_iff, Set.inter_subset_right: ∀ {α : Type ?u.10479} (s t : Set α), s ∩ t ⊆ t
Set.inter_subset_right, and_true: ∀ (p : Prop), (p ∧ True) = p
and_true]X: Type ?u.9951
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
hxX: Type ?u.9951
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
hxX: Type ?u.9951
inst✝: TopologicalSpace X
s, t: Set X
hs: IsClosed (restrict t s)
x: X
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
introx ∈ s
  have h: s ∩ t ⊆ s
h : (s: Set X
s ∩ t: Set X
t) ⊆ s: Set X
s :=X: Type ?u.9951
inst✝: TopologicalSpace X
s, t: Set X
hs: IsClosed (restrict t s)
x: X
hxst: x ∈ closure (s ∩ t)
right✝: x ∈ t
introx ∈ s byGoals accomplished! 🐙 exact Set.inter_subset_left: ∀ {α : Type ?u.9951} (s t : Set α), s ∩ t ⊆ s
Set.inter_subset_left s: Set X
s t: Set X
tGoals accomplished! 🐙
  have hsub: closure (restrict t s) ⊆ restrict t s
hsub : closure: {X : Type ?u.9951} → [inst : TopologicalSpace X] → Set X → Set X
closure (restrict: {X : Type ?u.9951} → (A : Set X) → Set X → Set ↑A
restrict t: Set X
t s: Set X
s) ⊆ (restrict: {X : Type ?u.9951} → (A : Set X) → Set X → Set ↑A
restrict t: Set X
t s: Set X
s) :=X: Type ?u.9951
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
introx ∈ s byGoals accomplished! 🐙 rwa [X: Type ?u.9951
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 sIsClosed.closure_subset_iff: ∀ {X : Type ?u.10936} {s t : Set X} [inst : TopologicalSpace X], IsClosed t → (closure s ⊆ t ↔ s ⊆ t)
IsClosed.closure_subset_iffX: Type ?u.9951
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.9951
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.9951
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.9951} → (A : Set X) → Set X → Set ↑A
restrict t: Set X
t s: Set X
s) ⊆ closure: {X : Type ?u.9951} → [inst : TopologicalSpace X] → Set X → Set X
closure (restrict: {X : Type ?u.9951} → (A : Set X) → Set X → Set ↑A
restrict t: Set X
t s: Set X
s) :=X: Type ?u.9951
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
introx ∈ s byGoals accomplished! 🐙 exact subset_closure: ∀ {X : Type ?u.9951} {s : Set X} [inst : TopologicalSpace X], s ⊆ closure s
subset_closureGoals accomplished! 🐙
  have hsub'': s ∩ t ⊆ closure (s ∩ t)
hsub'' : (s: Set X
s ∩ t: Set X
t) ⊆ closure: {X : Type ?u.9951} → [inst : TopologicalSpace X] → Set X → Set X
closure (s: Set X
s ∩ t: Set X
t) :=X: Type ?u.9951
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)
introx ∈ s byGoals accomplished! 🐙 exact subset_closure: ∀ {X : Type ?u.9951} {s : Set X} [inst : TopologicalSpace X], s ⊆ closure s
subset_closureGoals accomplished! 🐙
  have he: restrict t s = closure (restrict t s)
he : (restrict: {X : Type ?u.9951} → (A : Set X) → Set X → Set ↑A
restrict t: Set X
t s: Set X
s) = closure: {X : Type ?u.9951} → [inst : TopologicalSpace X] → Set X → Set X
closure (restrict: {X : Type ?u.9951} → (A : Set X) → Set X → Set ↑A
restrict t: Set X
t s: Set X
s) :=X: Type ?u.9951
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)
introx ∈ s byGoals accomplished! 🐙 exact Set.Subset.antisymm: ∀ {α : Type ?u.9951} {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
hsubGoals 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)
hsX: Type ?u.9951
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.introx ∈ s
  -- have h' : (s ∩ t) ⊆ (restrict t s) := by
  --   rw?
  sorryGoals accomplished! 🐙
  doneGoals 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
#checkIsClosed (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
exampleWarning: 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 := byGoals accomplished! 🐙
  sorryGoals accomplished! 🐙
  doneGoals 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