Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within' (Ray/Misc/Topology.lean)

State before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
⊢ Icc a b ⊆ s
Tactic:
generalize hs' : ofDual ⁻¹' s = s'
State after:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ Icc a b ⊆ s

State before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
rev : Icc (toDual b) (toDual a) ⊆ s'
⊢ Icc a b ⊆ s
Tactic:
intro x m
State after:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
rev : Icc (toDual b) (toDual a) ⊆ s'
x : X
m : x ∈ Icc a b
⊢ x ∈ s

State before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
rev : Icc (toDual b) (toDual a) ⊆ s'
x : X
m : x ∈ Icc a b
⊢ x ∈ s
Tactic:
simp only [Set.mem_Icc] at m
State after:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
rev : Icc (toDual b) (toDual a) ⊆ s'
x : X
m : a ≤ x ∧ x ≤ b
⊢ x ∈ s

State before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
rev : Icc (toDual b) (toDual a) ⊆ s'
x : X
m : a ≤ x ∧ x ≤ b
⊢ x ∈ s
Tactic:
specialize @rev (toDual x)
State after:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : X
m : a ≤ x ∧ x ≤ b
rev : toDual x ∈ Icc (toDual b) (toDual a) → toDual x ∈ s'
⊢ x ∈ s

State before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : X
m : a ≤ x ∧ x ≤ b
rev : toDual x ∈ Icc (toDual b) (toDual a) → toDual x ∈ s'
⊢ x ∈ s
Tactic:
simp only [Set.dual_Icc, Set.mem_preimage, Set.mem_Icc, and_imp, OrderDual.ofDual_toDual,
  ← hs'] at rev
State after:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : X
m : a ≤ x ∧ x ≤ b
rev : a ≤ x → x ≤ b → x ∈ s
⊢ x ∈ s

State before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : X
m : a ≤ x ∧ x ≤ b
rev : a ≤ x → x ≤ b → x ∈ s
⊢ x ∈ s
Tactic:
exact rev m.1 m.2
State after:
no goals

State before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ Icc (toDual b) (toDual a) ⊆ s'
Tactic:
apply IsClosed.Icc_subset_of_forall_mem_nhdsWithin
State after:
case hs
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ IsClosed (s' ∩ Icc (toDual b) (toDual a))

case ha
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ toDual b ∈ s'

case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ ∀ x ∈ s' ∩ Ico (toDual b) (toDual a), s' ∈ 𝓝[>] x

State before:
case hs
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ IsClosed (s' ∩ Icc (toDual b) (toDual a))
Tactic:
have e : s' ∩ Icc (toDual b) (toDual a) = ofDual ⁻¹' (s ∩ Icc a b) := by
  apply Set.ext; intro x; simp only [Set.dual_Icc, Set.preimage_inter, ← hs']
State after:
case hs
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
e : s' ∩ Icc (toDual b) (toDual a) = ⇑ofDual ⁻¹' (s ∩ Icc a b)
⊢ IsClosed (s' ∩ Icc (toDual b) (toDual a))

State before:
case hs
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
e : s' ∩ Icc (toDual b) (toDual a) = ⇑ofDual ⁻¹' (s ∩ Icc a b)
⊢ IsClosed (s' ∩ Icc (toDual b) (toDual a))
Tactic:
rw [e]
State after:
case hs
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
e : s' ∩ Icc (toDual b) (toDual a) = ⇑ofDual ⁻¹' (s ∩ Icc a b)
⊢ IsClosed (⇑ofDual ⁻¹' (s ∩ Icc a b))

State before:
case hs
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
e : s' ∩ Icc (toDual b) (toDual a) = ⇑ofDual ⁻¹' (s ∩ Icc a b)
⊢ IsClosed (⇑ofDual ⁻¹' (s ∩ Icc a b))
Tactic:
exact IsClosed.preimage continuous_ofDual sc
State after:
no goals

State before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ s' ∩ Icc (toDual b) (toDual a) = ⇑ofDual ⁻¹' (s ∩ Icc a b)
Tactic:
apply Set.ext
State after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ ∀ (x : Xᵒᵈ), x ∈ s' ∩ Icc (toDual b) (toDual a) ↔ x ∈ ⇑ofDual ⁻¹' (s ∩ Icc a b)

State before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ ∀ (x : Xᵒᵈ), x ∈ s' ∩ Icc (toDual b) (toDual a) ↔ x ∈ ⇑ofDual ⁻¹' (s ∩ Icc a b)
Tactic:
intro x
State after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
⊢ x ∈ s' ∩ Icc (toDual b) (toDual a) ↔ x ∈ ⇑ofDual ⁻¹' (s ∩ Icc a b)

State before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
⊢ x ∈ s' ∩ Icc (toDual b) (toDual a) ↔ x ∈ ⇑ofDual ⁻¹' (s ∩ Icc a b)
Tactic:
simp only [Set.dual_Icc, Set.preimage_inter, ← hs']
State after:
no goals

State before:
case ha
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ toDual b ∈ s'
Tactic:
simp only [Set.mem_preimage, OrderDual.ofDual_toDual, sb, ← hs']
State after:
no goals

State before:
case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ ∀ x ∈ s' ∩ Ico (toDual b) (toDual a), s' ∈ 𝓝[>] x
Tactic:
intro x m
State after:
case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
m : x ∈ s' ∩ Ico (toDual b) (toDual a)
⊢ s' ∈ 𝓝[>] x

State before:
case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
m : x ∈ s' ∩ Ico (toDual b) (toDual a)
⊢ s' ∈ 𝓝[>] x
Tactic:
simp only [Set.mem_preimage, Set.mem_inter_iff, Set.mem_Ico, OrderDual.toDual_le,
  OrderDual.lt_toDual] at m
State after:
case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
m : x ∈ s' ∧ ofDual x ≤ b ∧ a < ofDual x
⊢ s' ∈ 𝓝[>] x

State before:
case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
m : x ∈ s' ∧ ofDual x ≤ b ∧ a < ofDual x
⊢ s' ∈ 𝓝[>] x
Tactic:
simp only [mem_nhdsWithin_iff_eventually, eventually_nhds_iff, Set.mem_inter_iff,
  Set.mem_Ioc, ← hs'] at so m ⊢
State after:
case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
⊢ ∃ t, (∀ x_1 ∈ t, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s) ∧ IsOpen t ∧ x ∈ t

State before:
case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
⊢ ∃ t, (∀ x_1 ∈ t, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s) ∧ IsOpen t ∧ x ∈ t
Tactic:
rcases so (ofDual x) ⟨m.1, m.2.2, m.2.1⟩ with ⟨n, h, o, nx⟩
State after:
case hgt.intro.intro.intro
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
⊢ ∃ t, (∀ x_1 ∈ t, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s) ∧ IsOpen t ∧ x ∈ t

State before:
case hgt.intro.intro.intro
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
⊢ ∃ t, (∀ x_1 ∈ t, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s) ∧ IsOpen t ∧ x ∈ t
Tactic:
use ofDual ⁻¹' n
State after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
⊢ (∀ x_1 ∈ ⇑ofDual ⁻¹' n, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s) ∧ IsOpen (⇑ofDual ⁻¹' n) ∧ x ∈ ⇑ofDual ⁻¹' n

State before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
⊢ (∀ x_1 ∈ ⇑ofDual ⁻¹' n, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s) ∧ IsOpen (⇑ofDual ⁻¹' n) ∧ x ∈ ⇑ofDual ⁻¹' n
Tactic:
refine ⟨?_, o.preimage continuous_ofDual, mem_preimage.mpr nx⟩
State after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
⊢ ∀ x_1 ∈ ⇑ofDual ⁻¹' n, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s

State before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
⊢ ∀ x_1 ∈ ⇑ofDual ⁻¹' n, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s
Tactic:
intro y m xy
State after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : y ∈ Ioi x
⊢ y ∈ ⇑ofDual ⁻¹' s

State before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : y ∈ Ioi x
⊢ y ∈ ⇑ofDual ⁻¹' s
Tactic:
simp only [Set.mem_Ioi] at xy
State after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : x < y
⊢ y ∈ ⇑ofDual ⁻¹' s

State before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : x < y
⊢ y ∈ ⇑ofDual ⁻¹' s
Tactic:
simp only [Set.mem_preimage]
State after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : x < y
⊢ ofDual y ∈ s

State before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : x < y
⊢ ofDual y ∈ s
Tactic:
simp only [Set.mem_Iio, Set.mem_preimage, OrderDual.ofDual_lt_ofDual] at h
State after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : x < y
h : ∀ x_1 ∈ n, x_1 < ofDual x → x_1 ∈ s
⊢ ofDual y ∈ s

State before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : x < y
h : ∀ x_1 ∈ n, x_1 < ofDual x → x_1 ∈ s
⊢ ofDual y ∈ s
Tactic:
exact h _ m xy
State after:
no goals