internlm/Lean-Github huggingface dataset:
Theorem: UpperLowerContinuous.real_induction
Proof state before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : ¬y ≤ a
⊢ False
Tactic:
push_neg at H'
Proof state after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
⊢ False
Theorem: UpperLowerContinuous.real_induction
Proof state before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
⊢ False
Tactic:
apply ha.2
Proof state after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
⊢ a ∈ S
Theorem: UpperLowerContinuous.real_induction
Proof state before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
⊢ a ∈ S
Tactic:
obtain hlt | hle := lt_or_le a w₀
Proof state after:
case inl
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
hlt : a < w₀
⊢ a ∈ S

case inr
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
hle : w₀ ≤ a
⊢ a ∈ S
Theorem: UpperLowerContinuous.real_induction
Proof state before:
case inl
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
hlt : a < w₀
⊢ a ∈ S
Tactic:
exact h7 ⟨ha.1, hlt⟩
Proof state after:
no goals
Theorem: UpperLowerContinuous.real_induction
Proof state before:
case inr
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
hle : w₀ ≤ a
⊢ a ∈ S
Tactic:
exact hy ⟨hle, H'⟩
Proof state after:
no goals
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
⊢ TopologicalSpace.IsTopologicalBasis lower_intervals
Tactic:
refine
 @TopologicalSpace.IsTopologicalBasis.mk ℝ tₗ lower_intervals ?_ ?_ rfl
Proof state after:
case refine_1

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

case refine_2

⊢ ⋃₀ lower_intervals = Set.univ
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case refine_1

⊢ ∀ t₁ ∈ lower_intervals, ∀ t₂ ∈ lower_intervals, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
Tactic:
intro I1 hI1 I2 hI2 x hx
Proof state after:
case refine_1
I1 : Set ℝ
hI1 : I1 ∈ lower_intervals
I2 : Set ℝ
hI2 : I2 ∈ lower_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
⊢ ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case refine_1
I1 : Set ℝ
hI1 : I1 ∈ lower_intervals
I2 : Set ℝ
hI2 : I2 ∈ lower_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
⊢ ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
Tactic:
obtain ⟨a, b, hab⟩ := hI1
Proof state after:
case refine_1.intro.intro
I1 I2 : Set ℝ
hI2 : I2 ∈ lower_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
⊢ ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case refine_1.intro.intro
I1 I2 : Set ℝ
hI2 : I2 ∈ lower_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
⊢ ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
Tactic:
obtain ⟨c, d, hcd⟩ := hI2
Proof state after:
case refine_1.intro.intro.intro.intro
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case refine_1.intro.intro.intro.intro
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
Tactic:
use Set.Ico (Sup.sup a c) (Inf.inf b d)
Proof state after:
case h
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ Set.Ico (a ⊔ c) (b ⊓ d) ∈ lower_intervals ∧ x ∈ Set.Ico (a ⊔ c) (b ⊓ d) ∧ Set.Ico (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case h
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ Set.Ico (a ⊔ c) (b ⊓ d) ∈ lower_intervals ∧ x ∈ Set.Ico (a ⊔ c) (b ⊓ d) ∧ Set.Ico (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2
Tactic:
constructor
Proof state after:
case h.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ Set.Ico (a ⊔ c) (b ⊓ d) ∈ lower_intervals

case h.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ x ∈ Set.Ico (a ⊔ c) (b ⊓ d) ∧ Set.Ico (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case h.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ Set.Ico (a ⊔ c) (b ⊓ d) ∈ lower_intervals
Tactic:
exact ⟨Sup.sup a c, Inf.inf b d, rfl ⟩
Proof state after:
no goals
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case h.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ x ∈ Set.Ico (a ⊔ c) (b ⊓ d) ∧ Set.Ico (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2
Tactic:
constructor
Proof state after:
case h.right.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ x ∈ Set.Ico (a ⊔ c) (b ⊓ d)

case h.right.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ Set.Ico (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case h.right.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ x ∈ Set.Ico (a ⊔ c) (b ⊓ d)
Tactic:
aesop
Proof state after:
no goals
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case h.right.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ Set.Ico (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2
Tactic:
intro y hy
Proof state after:
case h.right.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
y : ℝ
hy : y ∈ Set.Ico (a ⊔ c) (b ⊓ d)
⊢ y ∈ I1 ∩ I2
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case h.right.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
y : ℝ
hy : y ∈ Set.Ico (a ⊔ c) (b ⊓ d)
⊢ y ∈ I1 ∩ I2
Tactic:
aesop
Proof state after:
no goals
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case refine_2

⊢ ⋃₀ lower_intervals = Set.univ
Tactic:
ext x
Proof state after:
case refine_2.h
x : ℝ
⊢ x ∈ ⋃₀ lower_intervals ↔ x ∈ Set.univ
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case refine_2.h
x : ℝ
⊢ x ∈ ⋃₀ lower_intervals ↔ x ∈ Set.univ
Tactic:
constructor
Proof state after:
case refine_2.h.mp
x : ℝ
⊢ x ∈ ⋃₀ lower_intervals → x ∈ Set.univ

case refine_2.h.mpr
x : ℝ
⊢ x ∈ Set.univ → x ∈ ⋃₀ lower_intervals
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case refine_2.h.mp
x : ℝ
⊢ x ∈ ⋃₀ lower_intervals → x ∈ Set.univ
Tactic:
aesop
Proof state after:
no goals
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case refine_2.h.mpr
x : ℝ
⊢ x ∈ Set.univ → x ∈ ⋃₀ lower_intervals
Tactic:
intro _
Proof state after:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ ⋃₀ lower_intervals
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ ⋃₀ lower_intervals
Tactic:
apply Set.mem_sUnion.mpr
Proof state after:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ ∃ t ∈ lower_intervals, x ∈ t
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ ∃ t ∈ lower_intervals, x ∈ t
Tactic:
use Set.Ico x (x+1)
Proof state after:
case h
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ico x (x + 1) ∈ lower_intervals ∧ x ∈ Set.Ico x (x + 1)
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case h
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ico x (x + 1) ∈ lower_intervals ∧ x ∈ Set.Ico x (x + 1)
Tactic:
constructor
Proof state after:
case h.left
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ico x (x + 1) ∈ lower_intervals

case h.right
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ Set.Ico x (x + 1)
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case h.left
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ico x (x + 1) ∈ lower_intervals
Tactic:
exact ⟨x, x+1, rfl⟩
Proof state after:
no goals
Theorem: UpperLowerContinuous.lower_basis
Proof state before:
case h.right
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ Set.Ico x (x + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: UpperLowerContinuous.upper_basis
Proof state before:
⊢ TopologicalSpace.IsTopologicalBasis upper_intervals
Tactic:
refine
 @TopologicalSpace.IsTopologicalBasis.mk ℝ tᵤ upper_intervals ?_ ?_ rfl
Proof 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
Theorem: UpperLowerContinuous.upper_basis
Proof 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
Proof 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
Theorem: UpperLowerContinuous.upper_basis
Proof 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
Proof 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
Theorem: UpperLowerContinuous.upper_basis
Proof 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
Proof 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
Theorem: UpperLowerContinuous.upper_basis
Proof 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)
Proof 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
Theorem: UpperLowerContinuous.upper_basis
Proof 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
Proof 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
Theorem: UpperLowerContinuous.upper_basis
Proof 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⟩
Proof state after:
no goals
Theorem: UpperLowerContinuous.upper_basis
Proof 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
Proof 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
Theorem: UpperLowerContinuous.upper_basis
Proof 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
Proof state after:
no goals
Theorem: UpperLowerContinuous.upper_basis
Proof 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
Proof 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
Theorem: UpperLowerContinuous.upper_basis
Proof 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
Proof state after:
no goals
Theorem: UpperLowerContinuous.upper_basis
Proof state before:
case refine_2

⊢ ⋃₀ upper_intervals = Set.univ
Tactic:
ext x
Proof state after:
case refine_2.h
x : ℝ
⊢ x ∈ ⋃₀ upper_intervals ↔ x ∈ Set.univ
Theorem: UpperLowerContinuous.upper_basis
Proof state before:
case refine_2.h
x : ℝ
⊢ x ∈ ⋃₀ upper_intervals ↔ x ∈ Set.univ
Tactic:
constructor
Proof 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
Theorem: UpperLowerContinuous.upper_basis
Proof state before:
case refine_2.h.mp
x : ℝ
⊢ x ∈ ⋃₀ upper_intervals → x ∈ Set.univ
Tactic:
aesop
Proof state after:
no goals
Theorem: UpperLowerContinuous.upper_basis
Proof state before:
case refine_2.h.mpr
x : ℝ
⊢ x ∈ Set.univ → x ∈ ⋃₀ upper_intervals
Tactic:
intro _
Proof state after:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ ⋃₀ upper_intervals
Theorem: UpperLowerContinuous.upper_basis
Proof state before:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ ⋃₀ upper_intervals
Tactic:
apply Set.mem_sUnion.mpr
Proof state after:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ ∃ t ∈ upper_intervals, x ∈ t
Theorem: UpperLowerContinuous.upper_basis
Proof state before:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ ∃ t ∈ upper_intervals, x ∈ t
Tactic:
use Set.Ioc (x-1) x
Proof state after:
case h
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ioc (x - 1) x ∈ upper_intervals ∧ x ∈ Set.Ioc (x - 1) x
Theorem: UpperLowerContinuous.upper_basis
Proof state before:
case h
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ioc (x - 1) x ∈ upper_intervals ∧ x ∈ Set.Ioc (x - 1) x
Tactic:
constructor
Proof 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
Theorem: UpperLowerContinuous.upper_basis
Proof state before:
case h.left
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ioc (x - 1) x ∈ upper_intervals
Tactic:
exact ⟨x-1, x, rfl⟩
Proof state after:
no goals
Theorem: UpperLowerContinuous.upper_basis
Proof state before:
case h.right
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ Set.Ioc (x - 1) x
Tactic:
simp
Proof state after:
no goals
Theorem: UpperLowerContinuous.open_basis
Proof state before:
⊢ TopologicalSpace.IsTopologicalBasis open_intervals
Tactic:
refine
  @TopologicalSpace.IsTopologicalBasis.mk ℝ tₛ open_intervals ?_ ?_ rfl
Proof 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
Theorem: UpperLowerContinuous.open_basis
Proof 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
Proof 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
Theorem: UpperLowerContinuous.open_basis
Proof 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
Proof 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
Theorem: UpperLowerContinuous.open_basis
Proof 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
Proof 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
Theorem: UpperLowerContinuous.open_basis
Proof 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)
Proof 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
Theorem: UpperLowerContinuous.open_basis
Proof 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
Proof 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
Theorem: UpperLowerContinuous.open_basis
Proof 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⟩
Proof state after:
no goals
Theorem: UpperLowerContinuous.open_basis
Proof 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
Proof 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
Theorem: UpperLowerContinuous.open_basis
Proof 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
Proof state after:
no goals
Theorem: UpperLowerContinuous.open_basis
Proof 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
Proof 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
Theorem: UpperLowerContinuous.open_basis
Proof 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
Proof state after:
no goals
Theorem: UpperLowerContinuous.open_basis
Proof state before:
case refine_2

⊢ ⋃₀ open_intervals = Set.univ
Tactic:
ext x
Proof state after:
case refine_2.h
x : ℝ
⊢ x ∈ ⋃₀ open_intervals ↔ x ∈ Set.univ
Theorem: UpperLowerContinuous.open_basis
Proof state before:
case refine_2.h
x : ℝ
⊢ x ∈ ⋃₀ open_intervals ↔ x ∈ Set.univ
Tactic:
constructor
Proof 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
Theorem: UpperLowerContinuous.open_basis
Proof state before:
case refine_2.h.mp
x : ℝ
⊢ x ∈ ⋃₀ open_intervals → x ∈ Set.univ
Tactic:
aesop
Proof state after:
no goals
Theorem: UpperLowerContinuous.open_basis
Proof state before:
case refine_2.h.mpr
x : ℝ
⊢ x ∈ Set.univ → x ∈ ⋃₀ open_intervals
Tactic:
intro _
Proof state after:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ ⋃₀ open_intervals
Theorem: UpperLowerContinuous.open_basis
Proof state before:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ ⋃₀ open_intervals
Tactic:
apply Set.mem_sUnion.mpr
Proof state after:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ ∃ t ∈ open_intervals, x ∈ t