-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem IsSupClosedCompact.wellFoundedGT (h : IsSupClosedCompact α) :
    WellFoundedGT α where
  wf

Proof state:
case intro
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
this : sSup (range ⇑a) ∈ range ⇑a
n : ℕ
hn : a n = sSup (range ⇑a)
h' : sSup (range ⇑a) < a (n + 1)
⊢ False

Tactic:
apply lt_irrefl (a (n + 1))

Result:
case intro
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
this : sSup (range ⇑a) ∈ range ⇑a
n : ℕ
hn : a n = sSup (range ⇑a)
h' : sSup (range ⇑a) < a (n + 1)
⊢ a (n + 1) < a (n + 1)

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
this : sSup (range ⇑a) ∈ range ⇑a
⊢ False

Tactic:
obtain ⟨n, hn⟩ := Set.mem_range.mp this

Result:
case intro
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
this : sSup (range ⇑a) ∈ range ⇑a
n : ℕ
hn : a n = sSup (range ⇑a)
⊢ False

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
this : sSup (range ⇑a) ∈ range ⇑a
n : ℕ
hn : a n = sSup (range ⇑a)
⊢ a (n + 1) > sSup (range ⇑a)

Tactic:
simp [← hn, a.map_rel_iff]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
this : sSup (range ⇑a) ∈ range ⇑a
n : ℕ
hn : a n = sSup (range ⇑a)
⊢ sSup (range ⇑a) < a (n + 1)

Tactic:
change _ > _

Result:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
this : sSup (range ⇑a) ∈ range ⇑a
n : ℕ
hn : a n = sSup (range ⇑a)
⊢ a (n + 1) > sSup (range ⇑a)

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ sSup (range ⇑a) ∈ range ⇑a

Tactic:
apply h (Set.range a)

Result:
case x
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ (range ⇑a).Nonempty

case a
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ SupClosed (range ⇑a)

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
this : sSup (range ⇑a) ∈ range ⇑a
n : ℕ
hn : a n = sSup (range ⇑a)
h' : sSup (range ⇑a) < a (n + 1)
⊢ a (n + 1) ≤ sSup (range ⇑a)

Tactic:
apply le_sSup

Result:
case a
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
this : sSup (range ⇑a) ∈ range ⇑a
n : ℕ
hn : a n = sSup (range ⇑a)
h' : sSup (range ⇑a) < a (n + 1)
⊢ a (n + 1) ∈ range ⇑a

Proof state:
case a
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ SupClosed (range ⇑a)

Tactic:
rintro x ⟨m, hm⟩ y ⟨n, hn⟩

Result:
case a.intro.intro
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
x : α
m : ℕ
hm : a m = x
y : α
n : ℕ
hn : a n = y
⊢ x ⊔ y ∈ range ⇑a

Proof state:
case intro
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
this : sSup (range ⇑a) ∈ range ⇑a
n : ℕ
hn : a n = sSup (range ⇑a)
h' : sSup (range ⇑a) < a (n + 1)
⊢ a (n + 1) < a (n + 1)

Tactic:
apply lt_of_le_of_lt _ h'

Result:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
this : sSup (range ⇑a) ∈ range ⇑a
n : ℕ
hn : a n = sSup (range ⇑a)
h' : sSup (range ⇑a) < a (n + 1)
⊢ a (n + 1) ≤ sSup (range ⇑a)

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ False

Tactic:
suffices sSup (Set.range a) ∈ Set.range a by
  obtain ⟨n, hn⟩ := Set.mem_range.mp this
  have h' : sSup (Set.range a) < a (n + 1) := by
    change _ > _
    simp [← hn, a.map_rel_iff]
  apply lt_irrefl (a (n + 1))
  apply lt_of_le_of_lt _ h'
  apply le_sSup
  apply Set.mem_range_self

Result:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ sSup (range ⇑a) ∈ range ⇑a

Proof state:
case intro
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
this : sSup (range ⇑a) ∈ range ⇑a
n : ℕ
hn : a n = sSup (range ⇑a)
⊢ False

Tactic:
have h' : sSup (Set.range a) < a (n + 1) := by
  change _ > _
  simp [← hn, a.map_rel_iff]

Result:
case intro
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
this : sSup (range ⇑a) ∈ range ⇑a
n : ℕ
hn : a n = sSup (range ⇑a)
h' : sSup (range ⇑a) < a (n + 1)
⊢ False

Proof state:
case a.intro.intro
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
x : α
m : ℕ
hm : a m = x
y : α
n : ℕ
hn : a n = y
⊢ x ⊔ y ∈ range ⇑a

Tactic:
use m ⊔ n

Result:
case h
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
x : α
m : ℕ
hm : a m = x
y : α
n : ℕ
hn : a n = y
⊢ a (m ⊔ n) = x ⊔ y

Proof state:
case h
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
x : α
m : ℕ
hm : a m = x
y : α
n : ℕ
hn : a n = y
⊢ a (m ⊔ n) = x ⊔ y

Tactic:
rw [← hm, ← hn]

Result:
case h
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
x : α
m : ℕ
hm : a m = x
y : α
n : ℕ
hn : a n = y
⊢ a (m ⊔ n) = a m ⊔ a n

Proof state:
case x
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ (range ⇑a).Nonempty

Tactic:
use a 37

Result:
case h
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ a 37 ∈ range ⇑a

Proof state:
case h
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ a 37 ∈ range ⇑a

Tactic:
apply Set.mem_range_self

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
⊢ WellFounded fun x1 x2 => x1 > x2

Tactic:
refine RelEmbedding.wellFounded_iff_no_descending_seq.mpr ⟨fun a => ?_⟩

Result:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ False

Proof state:
case h
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
x : α
m : ℕ
hm : a m = x
y : α
n : ℕ
hn : a n = y
⊢ a (m ⊔ n) = a m ⊔ a n

Tactic:
apply RelHomClass.map_sup a

Result:
no goals

Proof state:
case a
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
this : sSup (range ⇑a) ∈ range ⇑a
n : ℕ
hn : a n = sSup (range ⇑a)
h' : sSup (range ⇑a) < a (n + 1)
⊢ a (n + 1) ∈ range ⇑a

Tactic:
apply Set.mem_range_self

Result:
no goals