Theorem: sup_segment (LeanTeaching/TutoLib.lean)

State before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
⊢ ∃ x ∈ Icc a b, is_sup A x
Tactic:
have b_maj :  ∀ (y : ℝ), y ∈ A → y ≤ b := fun y y_in ↦ (h y_in).2
State after:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
⊢ ∃ x ∈ Icc a b, is_sup A x

State before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
⊢ ∃ x ∈ Icc a b, is_sup A x
Tactic:
have Sup_maj : upper_bound A (sSup A) := by
  intro x
  apply le_csSup
  exact ⟨b, b_maj⟩
State after:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ ∃ x ∈ Icc a b, is_sup A x

State before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ ∃ x ∈ Icc a b, is_sup A x
Tactic:
refine ⟨sSup A, ?_, ?_⟩
State after:
case refine_1
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ sSup A ∈ Icc a b

case refine_2
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ is_sup A (sSup A)

State before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
⊢ upper_bound A (sSup A)
Tactic:
intro x
State after:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
x : ℝ
⊢ x ∈ A → x ≤ sSup A

State before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
x : ℝ
⊢ x ∈ A → x ≤ sSup A
Tactic:
apply le_csSup
State after:
case h₁
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
x : ℝ
⊢ BddAbove A

State before:
case h₁
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
x : ℝ
⊢ BddAbove A
Tactic:
exact ⟨b, b_maj⟩
State after:
no goals

State before:
case refine_1
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ sSup A ∈ Icc a b
Tactic:
constructor
State after:
case refine_1.left
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ a ≤ sSup A

case refine_1.right
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ sSup A ≤ b

State before:
case refine_1.left
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ a ≤ sSup A
Tactic:
cases' hnonvide with x x_in
State after:
case refine_1.left.intro
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
x : ℝ
x_in : x ∈ A
⊢ a ≤ sSup A

State before:
case refine_1.left.intro
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
x : ℝ
x_in : x ∈ A
⊢ a ≤ sSup A
Tactic:
exact le_trans (h x_in).1 (Sup_maj _ x_in)
State after:
no goals

State before:
case refine_1.right
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ sSup A ≤ b
Tactic:
apply csSup_le hnonvide b_maj
State after:
no goals

State before:
case refine_2
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ is_sup A (sSup A)
Tactic:
exact ⟨Sup_maj, fun y ↦ csSup_le hnonvide⟩
State after:
no goals