Theorem: lt_sup (LeanTeaching/TutoLib.lean)

State before:
A : Set ℝ
x : ℝ
hx : is_sup A x
⊢ ∀ y < x, ∃ a ∈ A, y < a
Tactic:
intro y
State after:
A : Set ℝ
x : ℝ
hx : is_sup A x
y : ℝ
⊢ y < x → ∃ a ∈ A, y < a

State before:
A : Set ℝ
x : ℝ
hx : is_sup A x
y : ℝ
⊢ y < x → ∃ a ∈ A, y < a
Tactic:
contrapose!
State after:
A : Set ℝ
x : ℝ
hx : is_sup A x
y : ℝ
⊢ (∀ a ∈ A, a ≤ y) → x ≤ y

State before:
A : Set ℝ
x : ℝ
hx : is_sup A x
y : ℝ
⊢ (∀ a ∈ A, a ≤ y) → x ≤ y
Tactic:
exact hx.right y
State after:
no goals