-- Mathlib/Order/SuccPred/Archimedean.lean
lemma BddAbove.exists_isGreatest_of_nonempty {X : Type*} [LinearOrder X] [SuccOrder X]
    [IsSuccArchimedean X] {S : Set X} (hS : BddAbove S) (hS' : S.Nonempty) :
    ∃ x, IsGreatest S x

Proof state:
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
x : X
hx : x ∈ S
⊢ ¬x = succ m

Tactic:
rintro rfl

Result:
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
hx : succ m ∈ S
⊢ False

Proof state:
case pos
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∈ S
⊢ ∃ x, IsGreatest S x

Tactic:
exact ⟨_, hm', hm⟩

Result:
no goals

Proof state:
case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
⊢ ∀ (n_1 : X),
    n ≤ n_1 →
      (n_1 ∈ upperBounds S → n ∈ S → n_1 ∉ S → ∃ x, IsGreatest S x) →
        succ n_1 ∈ upperBounds S → n ∈ S → succ n_1 ∉ S → ∃ x, IsGreatest S x

Tactic:
intro m _ IH hm hn hm'

Result:
case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : m ∈ upperBounds S → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hm : succ m ∈ upperBounds S
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∃ x, IsGreatest S x

Proof state:
case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : m ∈ upperBounds S → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hm : succ m ∈ upperBounds S
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∃ x, IsGreatest S x

Tactic:
rw [mem_upperBounds] at IH hm

Result:
case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hm : ∀ x ∈ S, x ≤ succ m
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∃ x, IsGreatest S x

Proof state:
case neg.refine_1
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
⊢ n ∈ upperBounds S → n ∈ S → n ∉ S → ∃ x, IsGreatest S x

Tactic:
simp (config := {contextual := true})

Result:
no goals

Proof state:
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
hx : succ m ∈ S
⊢ False

Tactic:
exact hm' hx

Result:
no goals

Proof state:
case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∉ S
⊢ ∃ x, IsGreatest S x

Tactic:
have hn' := hm hn

Result:
case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∉ S
hn' : n ≤ m
⊢ ∃ x, IsGreatest S x

Proof state:
case intro.intro
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
⊢ ∃ x, IsGreatest S x

Tactic:
by_cases hm' : m ∈ S

Result:
case pos
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∈ S
⊢ ∃ x, IsGreatest S x

case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∉ S
⊢ ∃ x, IsGreatest S x

Proof state:
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
x : X
hx : x ∈ S
⊢ x ≤ m

Tactic:
refine (hm x hx).resolve_left ?_

Result:
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
x : X
hx : x ∈ S
⊢ ¬x = succ m

Proof state:
case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
⊢ ∃ x, IsGreatest S x

Tactic:
replace hm : ∀ x ∈ S, x ≤ m := by
  intro x hx
  refine (hm x hx).resolve_left ?_
  rintro rfl
  exact hm' hx

Result:
case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
⊢ ∃ x, IsGreatest S x

Proof state:
case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
⊢ ∃ x, IsGreatest S x

Tactic:
by_cases hmS : m ∈ S

Result:
case pos
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
hmS : m ∈ S
⊢ ∃ x, IsGreatest S x

case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
hmS : m ∉ S
⊢ ∃ x, IsGreatest S x

Proof state:
case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
⊢ m ∈ upperBounds S → n ∈ S → m ∉ S → ∃ x, IsGreatest S x

Tactic:
refine Succ.rec ?_ ?_ hn'

Result:
case neg.refine_1
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
⊢ n ∈ upperBounds S → n ∈ S → n ∉ S → ∃ x, IsGreatest S x

case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
⊢ ∀ (n_1 : X),
    n ≤ n_1 →
      (n_1 ∈ upperBounds S → n ∈ S → n_1 ∉ S → ∃ x, IsGreatest S x) →
        succ n_1 ∈ upperBounds S → n ∈ S → succ n_1 ∉ S → ∃ x, IsGreatest S x

Proof state:
case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∉ S
hn' : n ≤ m
⊢ ∃ x, IsGreatest S x

Tactic:
revert hn hm hm'

Result:
case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
⊢ m ∈ upperBounds S → n ∈ S → m ∉ S → ∃ x, IsGreatest S x