-- Mathlib/Order/Height.lean
theorem wellFoundedGT_of_chainHeight_ne_top (s : Set α) (hs : s.chainHeight ≠ ⊤) :
    WellFoundedGT s

Proof state:
case intro.refine_1
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
n : ℕ
hn : ↑n = s.chainHeight
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
i : α
h : i ∈ map Subtype.val (ofFn fun i => f ↑i)
⊢ i ∈ s

Tactic:
obtain ⟨a, -, rfl⟩ := mem_map.1 h

Result:
case intro.refine_1.intro.intro
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
n : ℕ
hn : ↑n = s.chainHeight
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
a : { x // x ∈ s }
h : ↑a ∈ map Subtype.val (ofFn fun i => f ↑i)
⊢ ↑a ∈ s

Proof state:
case intro
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
n : ℕ
hn : ↑n = s.chainHeight
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ ↑n.succ ≤ s.chainHeight

Tactic:
refine le_iSup₂_of_le ((ofFn (n := n.succ) fun i ↦ f i).map Subtype.val)
  ⟨chain'_map_of_chain' ((↑) : {x // x ∈ s} → α) (fun _ _ ↦ id)
    (chain'_iff_pairwise.2 <| pairwise_ofFn.2 fun i j ↦ f.map_rel_iff.2), fun i h ↦ ?_⟩ ?_

Result:
case intro.refine_1
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
n : ℕ
hn : ↑n = s.chainHeight
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
i : α
h : i ∈ map Subtype.val (ofFn fun i => f ↑i)
⊢ i ∈ s

case intro.refine_2
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
n : ℕ
hn : ↑n = s.chainHeight
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ ↑n.succ ≤ ↑(map Subtype.val (ofFn fun i => f ↑i)).length

Proof state:
case intro.refine_2
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
n : ℕ
hn : ↑n = s.chainHeight
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ ↑n.succ ≤ ↑n.succ

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case intro.refine_2
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
n : ℕ
hn : ↑n = s.chainHeight
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ ↑n.succ ≤ ↑(map Subtype.val (ofFn fun i => f ↑i)).length

Tactic:
rw [length_map, length_ofFn]

Result:
case intro.refine_2
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
n : ℕ
hn : ↑n = s.chainHeight
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ ↑n.succ ≤ ↑n.succ

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
⊢ WellFoundedGT ↑s

Tactic:
obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.1 hs

Result:
case intro
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
n : ℕ
hn : ↑n = s.chainHeight
⊢ WellFoundedGT ↑s

Proof state:
case intro
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
n : ℕ
hn : ↑n = s.chainHeight
⊢ WellFoundedGT ↑s

Tactic:
refine ⟨RelEmbedding.wellFounded_iff_no_descending_seq.2 ⟨fun f ↦ ?_⟩⟩

Result:
case intro
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
n : ℕ
hn : ↑n = s.chainHeight
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ False

Proof state:
case intro.refine_1.intro.intro
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
n : ℕ
hn : ↑n = s.chainHeight
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
a : { x // x ∈ s }
h : ↑a ∈ map Subtype.val (ofFn fun i => f ↑i)
⊢ ↑a ∈ s

Tactic:
exact a.prop

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
n : ℕ
hn : ↑n = s.chainHeight
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ False

Tactic:
refine n.lt_succ_self.not_le (WithTop.coe_le_coe.1 <| hn.symm ▸ ?_)

Result:
case intro
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
this : IsTrans { x // x ∈ s } fun x1 x2 => x1 < x2
n : ℕ
hn : ↑n = s.chainHeight
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ ↑n.succ ≤ s.chainHeight