-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem closure_Ioo {a b : α} (hab : a ≠ b) : closure (Ioo a b) = Icc a b

Proof state:
case h₂.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ Icc a b ⊆ closure (Ioo a b)

Tactic:
rw [← diff_subset_closure_iff, Icc_diff_Ioo_same hab.le]

Result:
case h₂.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ {a, b} ⊆ closure (Ioo a b)

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure (Ioo a b) = Icc a b

Tactic:
apply Subset.antisymm

Result:
case h₁
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure (Ioo a b) ⊆ Icc a b

case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure (Ioo a b)

Proof state:
case h₂.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : a < b
hab' : (Ioo a b).Nonempty
⊢ {a, b} ⊆ closure (Ioo a b)

Tactic:
simp only [insert_subset_iff, singleton_subset_iff]

Result:
case h₂.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : a < b
hab' : (Ioo a b).Nonempty
⊢ a ∈ closure (Ioo a b) ∧ b ∈ closure (Ioo a b)

Proof state:
case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure (Ioo a b)

Tactic:
rcases hab.lt_or_lt with hab | hab

Result:
case h₂.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ Icc a b ⊆ closure (Ioo a b)

case h₂.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : b < a
⊢ Icc a b ⊆ closure (Ioo a b)

Proof state:
case h₂.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : a < b
hab' : (Ioo a b).Nonempty
⊢ a ∈ closure (Ioo a b) ∧ b ∈ closure (Ioo a b)

Tactic:
exact ⟨(isGLB_Ioo hab).mem_closure hab', (isLUB_Ioo hab).mem_closure hab'⟩

Result:
no goals

Proof state:
case h₂.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ {a, b} ⊆ closure (Ioo a b)

Tactic:
have hab' : (Ioo a b).Nonempty := nonempty_Ioo.2 hab

Result:
case h₂.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : a < b
hab' : (Ioo a b).Nonempty
⊢ {a, b} ⊆ closure (Ioo a b)

Proof state:
case h₂.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : b < a
⊢ Icc a b ⊆ closure (Ioo a b)

Tactic:
rw [Icc_eq_empty_of_lt hab]

Result:
case h₂.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : b < a
⊢ ∅ ⊆ closure (Ioo a b)

Proof state:
case h₂.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : b < a
⊢ ∅ ⊆ closure (Ioo a b)

Tactic:
exact empty_subset _

Result:
no goals

Proof state:
case h₁
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure (Ioo a b) ⊆ Icc a b

Tactic:
exact closure_minimal Ioo_subset_Icc_self isClosed_Icc

Result:
no goals