case intro
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
⊢ WellFoundedGT ↑s
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
⊢ WellFoundedGT ↑s
obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.1 hs
case intro
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ False
case intro
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
⊢ WellFoundedGT ↑s
refine' ⟨RelEmbedding.wellFounded_iff_no_descending_seq.2 ⟨fun f ↦ _⟩⟩
case intro
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ↑(Nat.succ n) ≤ chainHeight s
case intro
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ False
refine' n.lt_succ_self.not_le (WithTop.coe_le_coe.1 <| hn.symm ▸ _)
case intro.refine'_1
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ℕ

case intro.refine'_2
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
i : α
h : i ∈ map Subtype.val (ofFn fun i => ↑f ↑i)
⊢ i ∈ s

case intro.refine'_3
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ↑(Nat.succ n) ≤ ↑(length (map Subtype.val (ofFn fun i => ↑f ↑i)))
case intro
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ↑(Nat.succ n) ≤ chainHeight s
refine'
  le_iSup₂_of_le _
    ⟨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 ↦ _⟩
    _
no goals
case intro.refine'_1
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ℕ
exact n.succ
case intro.refine'_2.intro.intro
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
a : { x // x ∈ s }
h : ↑a ∈ map Subtype.val (ofFn fun i => ↑f ↑i)
⊢ ↑a ∈ s
case intro.refine'_2
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
i : α
h : i ∈ map Subtype.val (ofFn fun i => ↑f ↑i)
⊢ i ∈ s
obtain ⟨a, -, rfl⟩ := mem_map.1 h
no goals
case intro.refine'_2.intro.intro
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
a : { x // x ∈ s }
h : ↑a ∈ map Subtype.val (ofFn fun i => ↑f ↑i)
⊢ ↑a ∈ s
exact a.prop
case intro.refine'_3
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ↑(Nat.succ n) ≤ ↑(Nat.succ n)
case intro.refine'_3
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ↑(Nat.succ n) ≤ ↑(length (map Subtype.val (ofFn fun i => ↑f ↑i)))
rw [length_map, length_ofFn]
no goals
case intro.refine'_3
α : Type u_1
β : Type ?u.50843
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ↑(Nat.succ n) ≤ ↑(Nat.succ n)
exact le_rfl