Theorem: IsPreconnected.relative_clopen (Ray/Misc/Connected.lean)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
⊢ s ⊆ interior t
Tactic:
generalize hu : (fun x : s ↦ (x : X)) ⁻¹' t = u
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
⊢ s ⊆ interior t

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
⊢ s ⊆ interior t
Tactic:
have uo : IsOpen u := by
  rw [← subset_interior_iff_isOpen]; intro ⟨x, m⟩ h
  simp only [mem_preimage, Subtype.coe_mk, ← hu] at h
  have n := op ⟨m, h⟩
  simp only [mem_interior_iff_mem_nhds, preimage_coe_mem_nhds_subtype, Subtype.coe_mk,
    ← hu] at n ⊢
  exact nhdsWithin_le_nhds n
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ s ⊆ interior t

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ s ⊆ interior t
Tactic:
have uc : IsClosed u := by
  rw [← closure_eq_iff_isClosed]; refine subset_antisymm ?_ subset_closure
  rw [← hu]
  refine _root_.trans (continuous_subtype_val.closure_preimage_subset _) ?_
  intro ⟨x, m⟩ h; exact cl ⟨m, h⟩
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
⊢ s ⊆ interior t

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
⊢ s ⊆ interior t
Tactic:
have p : IsPreconnected (univ : Set s) := (Subtype.preconnectedSpace sp).isPreconnected_univ
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
⊢ s ⊆ interior t

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
⊢ s ⊆ interior t
Tactic:
cases' disjoint_or_subset_of_isClopen p ⟨uc, uo⟩ with h h
State after:
case inl
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Disjoint univ u
⊢ s ⊆ interior t

case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : univ ⊆ u
⊢ s ⊆ interior t

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
⊢ IsOpen u
Tactic:
rw [← subset_interior_iff_isOpen]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
⊢ u ⊆ interior u

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
⊢ u ⊆ interior u
Tactic:
intro ⟨x, m⟩ h
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : ⟨x, m⟩ ∈ u
⊢ ⟨x, m⟩ ∈ interior u

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : ⟨x, m⟩ ∈ u
⊢ ⟨x, m⟩ ∈ interior u
Tactic:
simp only [mem_preimage, Subtype.coe_mk, ← hu] at h
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : x ∈ t
⊢ ⟨x, m⟩ ∈ interior u

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : x ∈ t
⊢ ⟨x, m⟩ ∈ interior u
Tactic:
have n := op ⟨m, h⟩
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : x ∈ t
n : x ∈ interior t
⊢ ⟨x, m⟩ ∈ interior u

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : x ∈ t
n : x ∈ interior t
⊢ ⟨x, m⟩ ∈ interior u
Tactic:
simp only [mem_interior_iff_mem_nhds, preimage_coe_mem_nhds_subtype, Subtype.coe_mk,
  ← hu] at n ⊢
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : x ∈ t
n : t ∈ 𝓝 x
⊢ t ∈ 𝓝[s] x

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : x ∈ t
n : t ∈ 𝓝 x
⊢ t ∈ 𝓝[s] x
Tactic:
exact nhdsWithin_le_nhds n
State after:
no goals

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ IsClosed u
Tactic:
rw [← closure_eq_iff_isClosed]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ closure u = u

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ closure u = u
Tactic:
refine subset_antisymm ?_ subset_closure
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ closure u ⊆ u

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ closure u ⊆ u
Tactic:
rw [← hu]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ closure ((fun x => ↑x) ⁻¹' t) ⊆ (fun x => ↑x) ⁻¹' t

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ closure ((fun x => ↑x) ⁻¹' t) ⊆ (fun x => ↑x) ⁻¹' t
Tactic:
refine _root_.trans (continuous_subtype_val.closure_preimage_subset _) ?_
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ Subtype.val ⁻¹' closure t ⊆ (fun x => ↑x) ⁻¹' t

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ Subtype.val ⁻¹' closure t ⊆ (fun x => ↑x) ⁻¹' t
Tactic:
intro ⟨x, m⟩ h
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
x : X
m : x ∈ s
h : ⟨x, m⟩ ∈ Subtype.val ⁻¹' closure t
⊢ ⟨x, m⟩ ∈ (fun x => ↑x) ⁻¹' t

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
x : X
m : x ∈ s
h : ⟨x, m⟩ ∈ Subtype.val ⁻¹' closure t
⊢ ⟨x, m⟩ ∈ (fun x => ↑x) ⁻¹' t
Tactic:
exact cl ⟨m, h⟩
State after:
no goals

State before:
case inl
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Disjoint univ u
⊢ s ⊆ interior t
Tactic:
simp only [univ_disjoint, preimage_eq_empty_iff, Subtype.range_coe, ← hu] at h
State after:
case inl
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Disjoint t s
⊢ s ⊆ interior t

State before:
case inl
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Disjoint t s
⊢ s ⊆ interior t
Tactic:
exfalso
State after:
case inl
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Disjoint t s
⊢ False

State before:
case inl
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Disjoint t s
⊢ False
Tactic:
exact ne.not_disjoint h.symm
State after:
no goals

State before:
case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : univ ⊆ u
⊢ s ⊆ interior t
Tactic:
rw [← Subtype.coe_preimage_self, ← hu, preimage_subset_preimage_iff] at h
State after:
case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : s ⊆ t
⊢ s ⊆ interior t

case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Subtype.val ⁻¹' s ⊆ (fun x => ↑x) ⁻¹' t
⊢ s ⊆ range Subtype.val

State before:
case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : s ⊆ t
⊢ s ⊆ interior t

case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Subtype.val ⁻¹' s ⊆ (fun x => ↑x) ⁻¹' t
⊢ s ⊆ range Subtype.val
Tactic:
exact _root_.trans (subset_inter (subset_refl _) h) op
State after:
case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Subtype.val ⁻¹' s ⊆ (fun x => ↑x) ⁻¹' t
⊢ s ⊆ range Subtype.val

State before:
case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Subtype.val ⁻¹' s ⊆ (fun x => ↑x) ⁻¹' t
⊢ s ⊆ range Subtype.val
Tactic:
simp only [Subtype.range_coe, subset_refl]
State after:
no goals