ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ False
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
⊢ WellFounded fun x x_1 => x > x_1
refine' RelEmbedding.wellFounded_iff_no_descending_seq.mpr ⟨fun a => _⟩
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ sSup (Set.range ↑a) ∈ Set.range ↑a
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ False
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
case x
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ Set.Nonempty (Set.range ↑a)

case a
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ∀ (a_1 : α), a_1 ∈ Set.range ↑a → ∀ (b : α), b ∈ Set.range ↑a → a_1 ⊔ b ∈ Set.range ↑a
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ sSup (Set.range ↑a) ∈ Set.range ↑a
apply h (Set.range a)
case intro
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
⊢ False
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
⊢ False
obtain ⟨n, hn⟩ := Set.mem_range.mp this
case intro
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
h' : sSup (Set.range ↑a) < ↑a (n + 1)
⊢ False
case intro
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
⊢ False
have h' : sSup (Set.range a) < a (n + 1) := by
  change _ > _
  simp [← hn, a.map_rel_iff]
case intro
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
h' : sSup (Set.range ↑a) < ↑a (n + 1)
⊢ ↑a (n + 1) < ↑a (n + 1)
case intro
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
h' : sSup (Set.range ↑a) < ↑a (n + 1)
⊢ False
apply lt_irrefl (a (n + 1))
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
h' : sSup (Set.range ↑a) < ↑a (n + 1)
⊢ ↑a (n + 1) ≤ sSup (Set.range ↑a)
case intro
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
h' : sSup (Set.range ↑a) < ↑a (n + 1)
⊢ ↑a (n + 1) < ↑a (n + 1)
apply lt_of_le_of_lt _ h'
case a
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
h' : sSup (Set.range ↑a) < ↑a (n + 1)
⊢ ↑a (n + 1) ∈ Set.range ↑a
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
h' : sSup (Set.range ↑a) < ↑a (n + 1)
⊢ ↑a (n + 1) ≤ sSup (Set.range ↑a)
apply le_sSup
no goals
case a
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
h' : sSup (Set.range ↑a) < ↑a (n + 1)
⊢ ↑a (n + 1) ∈ Set.range ↑a
apply Set.mem_range_self
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
⊢ ↑a (n + 1) > sSup (Set.range ↑a)
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
⊢ sSup (Set.range ↑a) < ↑a (n + 1)
change _ > _
no goals
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
⊢ ↑a (n + 1) > sSup (Set.range ↑a)
simp [← hn, a.map_rel_iff]
case x
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ↑a 37 ∈ Set.range ↑a
case x
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ Set.Nonempty (Set.range ↑a)
use a 37
no goals
case x
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ↑a 37 ∈ Set.range ↑a
apply Set.mem_range_self
case a.intro.intro
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
x : α
m : ℕ
hm : ↑a m = x
y : α
n : ℕ
hn : ↑a n = y
⊢ x ⊔ y ∈ Set.range ↑a
case a
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ∀ (a_1 : α), a_1 ∈ Set.range ↑a → ∀ (b : α), b ∈ Set.range ↑a → a_1 ⊔ b ∈ Set.range ↑a
rintro x ⟨m, hm⟩ y ⟨n, hn⟩
case a.intro.intro
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
x : α
m : ℕ
hm : ↑a m = x
y : α
n : ℕ
hn : ↑a n = y
⊢ ↑a (m ⊔ n) = x ⊔ y
case a.intro.intro
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
x : α
m : ℕ
hm : ↑a m = x
y : α
n : ℕ
hn : ↑a n = y
⊢ x ⊔ y ∈ Set.range ↑a
use m ⊔ n
case a.intro.intro
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
x : α
m : ℕ
hm : ↑a m = x
y : α
n : ℕ
hn : ↑a n = y
⊢ ↑a (m ⊔ n) = ↑a m ⊔ ↑a n
case a.intro.intro
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
x : α
m : ℕ
hm : ↑a m = x
y : α
n : ℕ
hn : ↑a n = y
⊢ ↑a (m ⊔ n) = x ⊔ y
rw [← hm, ← hn]
no goals
case a.intro.intro
ι : Sort ?u.27269
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
x : α
m : ℕ
hm : ↑a m = x
y : α
n : ℕ
hn : ↑a n = y
⊢ ↑a (m ⊔ n) = ↑a m ⊔ ↑a n
apply RelHomClass.map_sup a