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

State before:
x : ℝ
⊢ IsOpen (Set.Ici x)
Tactic:
rw [@TopologicalSpace.IsTopologicalBasis.isOpen_iff
        ℝ tₗ _ lower_intervals lower_basis]
State after:
x : ℝ
⊢ ∀ a ∈ Set.Ici x, ∃ t ∈ lower_intervals, a ∈ t ∧ t ⊆ Set.Ici x

State before:
x : ℝ
⊢ ∀ a ∈ Set.Ici x, ∃ t ∈ lower_intervals, a ∈ t ∧ t ⊆ Set.Ici x
Tactic:
intro a ha
State after:
x a : ℝ
ha : a ∈ Set.Ici x
⊢ ∃ t ∈ lower_intervals, a ∈ t ∧ t ⊆ Set.Ici x

State before:
x a : ℝ
ha : a ∈ Set.Ici x
⊢ ∃ t ∈ lower_intervals, a ∈ t ∧ t ⊆ Set.Ici x
Tactic:
use Set.Ico a (a + 1)
State after:
case h
x a : ℝ
ha : a ∈ Set.Ici x
⊢ Set.Ico a (a + 1) ∈ lower_intervals ∧ a ∈ Set.Ico a (a + 1) ∧ Set.Ico a (a + 1) ⊆ Set.Ici x

State before:
case h
x a : ℝ
ha : a ∈ Set.Ici x
⊢ Set.Ico a (a + 1) ∈ lower_intervals ∧ a ∈ Set.Ico a (a + 1) ∧ Set.Ico a (a + 1) ⊆ Set.Ici x
Tactic:
constructor
State after:
case h.left
x a : ℝ
ha : a ∈ Set.Ici x
⊢ Set.Ico a (a + 1) ∈ lower_intervals

case h.right
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a ∈ Set.Ico a (a + 1) ∧ Set.Ico a (a + 1) ⊆ Set.Ici x

State before:
case h.left
x a : ℝ
ha : a ∈ Set.Ici x
⊢ Set.Ico a (a + 1) ∈ lower_intervals
Tactic:
exact ⟨a, a + 1, rfl⟩
State after:
no goals

State before:
case h.right
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a ∈ Set.Ico a (a + 1) ∧ Set.Ico a (a + 1) ⊆ Set.Ici x
Tactic:
constructor
State after:
case h.right.left
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a ∈ Set.Ico a (a + 1)

case h.right.right
x a : ℝ
ha : a ∈ Set.Ici x
⊢ Set.Ico a (a + 1) ⊆ Set.Ici x

State before:
case h.right.left
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a ∈ Set.Ico a (a + 1)
Tactic:
constructor
State after:
case h.right.left.left
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a ≤ a

case h.right.left.right
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a < a + 1

State before:
case h.right.left.left
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a ≤ a
Tactic:
exact Eq.le rfl
State after:
no goals

State before:
case h.right.left.right
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a < a + 1
Tactic:
exact lt_add_one a
State after:
no goals

State before:
case h.right.right
x a : ℝ
ha : a ∈ Set.Ici x
⊢ Set.Ico a (a + 1) ⊆ Set.Ici x
Tactic:
intro y hy
State after:
case h.right.right
x a : ℝ
ha : a ∈ Set.Ici x
y : ℝ
hy : y ∈ Set.Ico a (a + 1)
⊢ y ∈ Set.Ici x

State before:
case h.right.right
x a : ℝ
ha : a ∈ Set.Ici x
y : ℝ
hy : y ∈ Set.Ico a (a + 1)
⊢ y ∈ Set.Ici x
Tactic:
rw[Set.mem_Ici] at ha
State after:
case h.right.right
x a : ℝ
ha : x ≤ a
y : ℝ
hy : y ∈ Set.Ico a (a + 1)
⊢ y ∈ Set.Ici x

State before:
case h.right.right
x a : ℝ
ha : x ≤ a
y : ℝ
hy : y ∈ Set.Ico a (a + 1)
⊢ y ∈ Set.Ici x
Tactic:
exact ha.trans hy.1
State after:
no goals