Theorem: float_int_bounded (HOLFloat/Float_theorem.lean)

State before:
α✝ : Type u_1
s : Set α✝
S : ℤ → Prop
b : ℤ
⊢ Set.Nonempty s → (∀ (e : ℤ), e ∈ setOf S → e ≤ b) → ∃ e', is_sup_int S e'
Tactic:
intro hn ha
State after:
α✝ : Type u_1
s : Set α✝
S : ℤ → Prop
b : ℤ
hn : Set.Nonempty s
ha : ∀ (e : ℤ), e ∈ setOf S → e ≤ b
⊢ ∃ e', is_sup_int S e'

State before:
α✝ : Type u_1
s : Set α✝
S : ℤ → Prop
b : ℤ
hn : Set.Nonempty s
ha : ∀ (e : ℤ), e ∈ setOf S → e ≤ b
⊢ ∃ e', is_sup_int S e'
Tactic:
simp [setOf] at ha
State after:
α✝ : Type u_1
s : Set α✝
S : ℤ → Prop
b : ℤ
hn : Set.Nonempty s
ha : ∀ (e : ℤ), e ∈ S → e ≤ b
⊢ ∃ e', is_sup_int S e'

State before:
α✝ : Type u_1
s : Set α✝
S : ℤ → Prop
b : ℤ
hn : Set.Nonempty s
ha : ∀ (e : ℤ), e ∈ S → e ≤ b
⊢ ∃ e', is_sup_int S e'
Tactic:
simp [is_sup_int, IsLUB, IsLeast, lowerBounds, upperBounds]
State after:
α✝ : Type u_1
s : Set α✝
S : ℤ → Prop
b : ℤ
hn : Set.Nonempty s
ha : ∀ (e : ℤ), e ∈ S → e ≤ b
⊢ ∃ e', (∀ ⦃a : ℤ⦄, a ∈ S → a ≤ e') ∧ ∀ ⦃a : ℤ⦄, (∀ ⦃a_1 : ℤ⦄, a_1 ∈ S → a_1 ≤ a) → e' ≤ a

State before:
α✝ : Type u_1
s : Set α✝
S : ℤ → Prop
b : ℤ
hn : Set.Nonempty s
ha : ∀ (e : ℤ), e ∈ S → e ≤ b
⊢ ∃ e', (∀ ⦃a : ℤ⦄, a ∈ S → a ≤ e') ∧ ∀ ⦃a : ℤ⦄, (∀ ⦃a_1 : ℤ⦄, a_1 ∈ S → a_1 ≤ a) → e' ≤ a
Tactic:
sorry
State after:
no goals