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

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

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

case refine_2

⊢ ⋃₀ upper_intervals = Set.univ

State before:
case refine_1

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

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

State before:
case refine_1.intro.intro
I1 I2 : Set ℝ
hI2 : I2 ∈ upper_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioc a b = I1
⊢ ∃ t₃ ∈ upper_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.Ioc a b = I1
c d : ℝ
hcd : Set.Ioc c d = I2
⊢ ∃ t₃ ∈ upper_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.Ioc a b = I1
c d : ℝ
hcd : Set.Ioc c d = I2
⊢ ∃ t₃ ∈ upper_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
Tactic:
use Set.Ioc (Sup.sup a c) (Inf.inf b d)
State after:
case h
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioc a b = I1
c d : ℝ
hcd : Set.Ioc c d = I2
⊢ Set.Ioc (a ⊔ c) (b ⊓ d) ∈ upper_intervals ∧ x ∈ Set.Ioc (a ⊔ c) (b ⊓ d) ∧ Set.Ioc (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2

State before:
case h
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioc a b = I1
c d : ℝ
hcd : Set.Ioc c d = I2
⊢ Set.Ioc (a ⊔ c) (b ⊓ d) ∈ upper_intervals ∧ x ∈ Set.Ioc (a ⊔ c) (b ⊓ d) ∧ Set.Ioc (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.Ioc a b = I1
c d : ℝ
hcd : Set.Ioc c d = I2
⊢ Set.Ioc (a ⊔ c) (b ⊓ d) ∈ upper_intervals

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

State before:
case h.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioc a b = I1
c d : ℝ
hcd : Set.Ioc c d = I2
⊢ Set.Ioc (a ⊔ c) (b ⊓ d) ∈ upper_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.Ioc a b = I1
c d : ℝ
hcd : Set.Ioc c d = I2
⊢ x ∈ Set.Ioc (a ⊔ c) (b ⊓ d) ∧ Set.Ioc (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.Ioc a b = I1
c d : ℝ
hcd : Set.Ioc c d = I2
⊢ x ∈ Set.Ioc (a ⊔ c) (b ⊓ d)

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

State before:
case h.right.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioc a b = I1
c d : ℝ
hcd : Set.Ioc c d = I2
⊢ x ∈ Set.Ioc (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.Ioc a b = I1
c d : ℝ
hcd : Set.Ioc c d = I2
⊢ Set.Ioc (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.Ioc a b = I1
c d : ℝ
hcd : Set.Ioc c d = I2
y : ℝ
hy : y ∈ Set.Ioc (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.Ioc a b = I1
c d : ℝ
hcd : Set.Ioc c d = I2
y : ℝ
hy : y ∈ Set.Ioc (a ⊔ c) (b ⊓ d)
⊢ y ∈ I1 ∩ I2
Tactic:
aesop
State after:
no goals

State before:
case refine_2

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

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

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

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

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

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

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

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

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

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

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