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

State before:
x : ℝ
⊢ IsOpen (Set.Iio x)
Tactic:
rw [@TopologicalSpace.IsTopologicalBasis.isOpen_iff
        ℝ tᵤ _ upper_intervals upper_basis]
State after:
x : ℝ
⊢ ∀ a ∈ Set.Iio x, ∃ t ∈ upper_intervals, a ∈ t ∧ t ⊆ Set.Iio x

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

State before:
x a : ℝ
ha : a ∈ Set.Iio x
⊢ ∃ t ∈ upper_intervals, a ∈ t ∧ t ⊆ Set.Iio x
Tactic:
use Set.Ioc (a - 1) a
State after:
case h
x a : ℝ
ha : a ∈ Set.Iio x
⊢ Set.Ioc (a - 1) a ∈ upper_intervals ∧ a ∈ Set.Ioc (a - 1) a ∧ Set.Ioc (a - 1) a ⊆ Set.Iio x

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

case h.right
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a ∈ Set.Ioc (a - 1) a ∧ Set.Ioc (a - 1) a ⊆ Set.Iio x

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

State before:
case h.right
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a ∈ Set.Ioc (a - 1) a ∧ Set.Ioc (a - 1) a ⊆ Set.Iio x
Tactic:
constructor
State after:
case h.right.left
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a ∈ Set.Ioc (a - 1) a

case h.right.right
x a : ℝ
ha : a ∈ Set.Iio x
⊢ Set.Ioc (a - 1) a ⊆ Set.Iio x

State before:
case h.right.left
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a ∈ Set.Ioc (a - 1) a
Tactic:
constructor
State after:
case h.right.left.left
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a - 1 < a

case h.right.left.right
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a ≤ a

State before:
case h.right.left.left
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a - 1 < a
Tactic:
simp only [Set.mem_Iio, sub_lt_self_iff, zero_lt_one]
State after:
no goals

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

State before:
case h.right.right
x a : ℝ
ha : a ∈ Set.Iio x
⊢ Set.Ioc (a - 1) a ⊆ Set.Iio x
Tactic:
intro y hy
State after:
case h.right.right
x a : ℝ
ha : a ∈ Set.Iio x
y : ℝ
hy : y ∈ Set.Ioc (a - 1) a
⊢ y ∈ Set.Iio x

State before:
case h.right.right
x a : ℝ
ha : a ∈ Set.Iio x
y : ℝ
hy : y ∈ Set.Ioc (a - 1) a
⊢ y ∈ Set.Iio x
Tactic:
exact hy.2.trans_lt ha
State after:
no goals