case refine'_1
α : Type u_1
inst✝ : Preorder α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m

case refine'_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
⊢ WellFounded fun x x_1 => x > x_1
α : Type u_1
inst✝ : Preorder α
⊢ (WellFounded fun x x_1 => x > x_1) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
refine' ⟨fun h a => _, fun h => _⟩
case refine'_1
α : Type u_1
inst✝ : Preorder α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
hne : Set.Nonempty (Set.range ↑a)
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
case refine'_1
α : Type u_1
inst✝ : Preorder α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
have hne : (Set.range a).Nonempty := ⟨a 0, by simp⟩
case refine'_1.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
hne : Set.Nonempty (Set.range ↑a)
n : ℕ
H : ∀ (x : α), x ∈ Set.range ↑a → ¬x > ↑a n
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
case refine'_1
α : Type u_1
inst✝ : Preorder α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
hne : Set.Nonempty (Set.range ↑a)
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.has_min _ hne
no goals
case refine'_1.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
hne : Set.Nonempty (Set.range ↑a)
n : ℕ
H : ∀ (x : α), x ∈ Set.range ↑a → ¬x > ↑a n
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
exact ⟨n, fun m _ => H _ (Set.mem_range_self _)⟩
no goals
α : Type u_1
inst✝ : Preorder α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
⊢ ↑a 0 ∈ Set.range ↑a
simp
case refine'_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ False
case refine'_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
⊢ WellFounded fun x x_1 => x > x_1
refine' RelEmbedding.wellFounded_iff_no_descending_seq.2 ⟨fun a => _⟩
no goals
case refine'_2.intro
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      ¬↑(RelHom.toOrderHom (RelEmbedding.toRelHom (RelEmbedding.swap a))) n <
          ↑(RelHom.toOrderHom (RelEmbedding.toRelHom (RelEmbedding.swap a))) m
⊢ False
exact hn n.succ n.lt_succ_self.le ((RelEmbedding.map_rel_iff _).2 n.lt_succ_self)