Theorem: UpperLowerContinuous.open_basis (Compfiles/UpperLowerContinuous.lean)

State before:
⊢ TopologicalSpace.IsTopologicalBasis open_intervals
Tactic:
refine
  @TopologicalSpace.IsTopologicalBasis.mk ℝ tₛ open_intervals ?_ ?_ rfl
State after:
case refine_1

⊢ ∀ t₁ ∈ open_intervals, ∀ t₂ ∈ open_intervals, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ open_intervals, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

case refine_2

⊢ ⋃₀ open_intervals = Set.univ

State before:
case refine_1

⊢ ∀ t₁ ∈ open_intervals, ∀ t₂ ∈ open_intervals, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ open_intervals, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
Tactic:
intro I1 hI1 I2 hI2 x hx
State after:
case refine_1
I1 : Set ℝ
hI1 : I1 ∈ open_intervals
I2 : Set ℝ
hI2 : I2 ∈ open_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
⊢ ∃ t₃ ∈ open_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2

State before:
case refine_1
I1 : Set ℝ
hI1 : I1 ∈ open_intervals
I2 : Set ℝ
hI2 : I2 ∈ open_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
⊢ ∃ t₃ ∈ open_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
Tactic:
obtain ⟨a, b, hab⟩ := hI1
State after:
case refine_1.intro.intro
I1 I2 : Set ℝ
hI2 : I2 ∈ open_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
⊢ ∃ t₃ ∈ open_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2

State before:
case refine_1.intro.intro
I1 I2 : Set ℝ
hI2 : I2 ∈ open_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
⊢ ∃ t₃ ∈ open_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
Tactic:
obtain ⟨c, d, hcd⟩ := hI2
State after:
case refine_1.intro.intro.intro.intro
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
⊢ ∃ t₃ ∈ open_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2

State before:
case refine_1.intro.intro.intro.intro
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
⊢ ∃ t₃ ∈ open_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
Tactic:
use Set.Ioo (Sup.sup a c) (Inf.inf b d)
State after:
case h
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
⊢ Set.Ioo (a ⊔ c) (b ⊓ d) ∈ open_intervals ∧ x ∈ Set.Ioo (a ⊔ c) (b ⊓ d) ∧ Set.Ioo (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2

State before:
case h
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
⊢ Set.Ioo (a ⊔ c) (b ⊓ d) ∈ open_intervals ∧ x ∈ Set.Ioo (a ⊔ c) (b ⊓ d) ∧ Set.Ioo (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2
Tactic:
constructor
State after:
case h.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
⊢ Set.Ioo (a ⊔ c) (b ⊓ d) ∈ open_intervals

case h.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
⊢ x ∈ Set.Ioo (a ⊔ c) (b ⊓ d) ∧ Set.Ioo (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2

State before:
case h.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
⊢ Set.Ioo (a ⊔ c) (b ⊓ d) ∈ open_intervals
Tactic:
exact ⟨Sup.sup a c, Inf.inf b d, rfl⟩
State after:
no goals

State before:
case h.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
⊢ x ∈ Set.Ioo (a ⊔ c) (b ⊓ d) ∧ Set.Ioo (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2
Tactic:
constructor
State after:
case h.right.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
⊢ x ∈ Set.Ioo (a ⊔ c) (b ⊓ d)

case h.right.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
⊢ Set.Ioo (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2

State before:
case h.right.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
⊢ x ∈ Set.Ioo (a ⊔ c) (b ⊓ d)
Tactic:
aesop
State after:
no goals

State before:
case h.right.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
⊢ Set.Ioo (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2
Tactic:
intro y hy
State after:
case h.right.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
y : ℝ
hy : y ∈ Set.Ioo (a ⊔ c) (b ⊓ d)
⊢ y ∈ I1 ∩ I2

State before:
case h.right.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
y : ℝ
hy : y ∈ Set.Ioo (a ⊔ c) (b ⊓ d)
⊢ y ∈ I1 ∩ I2
Tactic:
aesop
State after:
no goals

State before:
case refine_2

⊢ ⋃₀ open_intervals = Set.univ
Tactic:
ext x
State after:
case refine_2.h
x : ℝ
⊢ x ∈ ⋃₀ open_intervals ↔ x ∈ Set.univ

State before:
case refine_2.h
x : ℝ
⊢ x ∈ ⋃₀ open_intervals ↔ x ∈ Set.univ
Tactic:
constructor
State after:
case refine_2.h.mp
x : ℝ
⊢ x ∈ ⋃₀ open_intervals → x ∈ Set.univ

case refine_2.h.mpr
x : ℝ
⊢ x ∈ Set.univ → x ∈ ⋃₀ open_intervals

State before:
case refine_2.h.mp
x : ℝ
⊢ x ∈ ⋃₀ open_intervals → x ∈ Set.univ
Tactic:
aesop
State after:
no goals

State before:
case refine_2.h.mpr
x : ℝ
⊢ x ∈ Set.univ → x ∈ ⋃₀ open_intervals
Tactic:
intro _
State after:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ ⋃₀ open_intervals

State before:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ ⋃₀ open_intervals
Tactic:
apply Set.mem_sUnion.mpr
State after:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ ∃ t ∈ open_intervals, x ∈ t

State before:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ ∃ t ∈ open_intervals, x ∈ t
Tactic:
use Set.Ioo (x-1) (x+1)
State after:
case h
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ioo (x - 1) (x + 1) ∈ open_intervals ∧ x ∈ Set.Ioo (x - 1) (x + 1)

State before:
case h
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ioo (x - 1) (x + 1) ∈ open_intervals ∧ x ∈ Set.Ioo (x - 1) (x + 1)
Tactic:
constructor
State after:
case h.left
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ioo (x - 1) (x + 1) ∈ open_intervals

case h.right
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ Set.Ioo (x - 1) (x + 1)

State before:
case h.left
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ioo (x - 1) (x + 1) ∈ open_intervals
Tactic:
exact ⟨x-1, x+1, rfl⟩
State after:
no goals

State before:
case h.right
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ Set.Ioo (x - 1) (x + 1)
Tactic:
simp
State after:
no goals