[GOAL]
α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ¬Acc r a
⊢ ∃ b, ¬Acc r b ∧ r b a
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
⊢ Acc r a
[PROOFSTEP]
refine' ⟨_, fun b hr => _⟩
[GOAL]
α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
b : α
hr : r b a
⊢ Acc r b
[PROOFSTEP]
by_contra hb
[GOAL]
α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
b : α
hr : r b a
hb : ¬Acc r b
⊢ False
[PROOFSTEP]
exact h b hb hr
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
⊢ Acc r x ↔ IsEmpty { f // x ∈ Set.range ↑f }
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
⊢ Acc r x → IsEmpty { f // x ∈ Set.range ↑f }
[PROOFSTEP]
refine' fun h => h.recOn fun x _ IH => _
[GOAL]
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝¹ : α
h : Acc r x✝¹
x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → IsEmpty { f // y ∈ Set.range ↑f }
⊢ IsEmpty { f // x ∈ Set.range ↑f }
[PROOFSTEP]
constructor
[GOAL]
case mp.false
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝¹ : α
h : Acc r x✝¹
x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → IsEmpty { f // y ∈ Set.range ↑f }
⊢ { f // x ∈ Set.range ↑f } → False
[PROOFSTEP]
rintro ⟨f, k, hf⟩
[GOAL]
case mp.false.mk.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝¹ : α
h : Acc r x✝¹
x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → IsEmpty { f // y ∈ Set.range ↑f }
f : (fun x x_1 => x > x_1) ↪r r
k : ℕ
hf : ↑f k = x
⊢ False
[PROOFSTEP]
exact IsEmpty.elim' (IH (f (k + 1)) (hf ▸ f.map_rel_iff.2 (lt_add_one k))) ⟨f, _, rfl⟩
[GOAL]
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
⊢ IsEmpty { f // x ∈ Set.range ↑f } → Acc r x
[PROOFSTEP]
have : ∀ x : { a // ¬Acc r a }, ∃ y : { a // ¬Acc r a }, r y.1 x.1 :=
  by
  rintro ⟨x, hx⟩
  cases exists_not_acc_lt_of_not_acc hx with
  | intro w h => exact ⟨⟨w, h.1⟩, h.2⟩
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
⊢ ∀ (x : { a // ¬Acc r a }), ∃ y, r ↑y ↑x
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mk
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝ x : α
hx : ¬Acc r x
⊢ ∃ y, r ↑y ↑{ val := x, property := hx }
[PROOFSTEP]
cases exists_not_acc_lt_of_not_acc hx with
| intro w h => exact ⟨⟨w, h.1⟩, h.2⟩
[GOAL]
case mk
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝¹ x : α
hx : ¬Acc r x
x✝ : ∃ b, ¬Acc r b ∧ r b x
⊢ ∃ y, r ↑y ↑{ val := x, property := hx }
[PROOFSTEP]
cases exists_not_acc_lt_of_not_acc hx with
| intro w h => exact ⟨⟨w, h.1⟩, h.2⟩
[GOAL]
case mk.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝ x : α
hx : ¬Acc r x
w : α
h : ¬Acc r w ∧ r w x
⊢ ∃ y, r ↑y ↑{ val := x, property := hx }
[PROOFSTEP]

| intro w h => exact ⟨⟨w, h.1⟩, h.2⟩
[GOAL]
case mk.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝ x : α
hx : ¬Acc r x
w : α
h : ¬Acc r w ∧ r w x
⊢ ∃ y, r ↑y ↑{ val := x, property := hx }
[PROOFSTEP]
exact ⟨⟨w, h.1⟩, h.2⟩
[GOAL]
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
this : ∀ (x : { a // ¬Acc r a }), ∃ y, r ↑y ↑x
⊢ IsEmpty { f // x ∈ Set.range ↑f } → Acc r x
[PROOFSTEP]
obtain ⟨f, h⟩ := Classical.axiom_of_choice this
[GOAL]
case mpr.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
this : ∀ (x : { a // ¬Acc r a }), ∃ y, r ↑y ↑x
f : { a // ¬Acc r a } → { a // ¬Acc r a }
h : ∀ (x : { a // ¬Acc r a }), r ↑(f x) ↑x
⊢ IsEmpty { f // x ∈ Set.range ↑f } → Acc r x
[PROOFSTEP]
refine' fun E => by_contradiction fun hx => E.elim' ⟨natGT (fun n => (f^[n] ⟨x, hx⟩).1) fun n => _, 0, rfl⟩
[GOAL]
case mpr.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
this : ∀ (x : { a // ¬Acc r a }), ∃ y, r ↑y ↑x
f : { a // ¬Acc r a } → { a // ¬Acc r a }
h : ∀ (x : { a // ¬Acc r a }), r ↑(f x) ↑x
E : IsEmpty { f // x ∈ Set.range ↑f }
hx : ¬Acc r x
n : ℕ
⊢ r ((fun n => ↑(f^[n] { val := x, property := hx })) (n + 1)) ((fun n => ↑(f^[n] { val := x, property := hx })) n)
[PROOFSTEP]
simp only [Function.iterate_succ']
[GOAL]
case mpr.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
this : ∀ (x : { a // ¬Acc r a }), ∃ y, r ↑y ↑x
f : { a // ¬Acc r a } → { a // ¬Acc r a }
h : ∀ (x : { a // ¬Acc r a }), r ↑(f x) ↑x
E : IsEmpty { f // x ∈ Set.range ↑f }
hx : ¬Acc r x
n : ℕ
⊢ r ↑((f ∘ f^[n]) { val := x, property := hx }) ↑(f^[n] { val := x, property := hx })
[PROOFSTEP]
apply h
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x x_1 => x > x_1) ↪r r
k : ℕ
⊢ ¬Acc r (↑f k)
[PROOFSTEP]
rw [acc_iff_no_decreasing_seq, not_isEmpty_iff]
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x x_1 => x > x_1) ↪r r
k : ℕ
⊢ Nonempty { f_1 // ↑f k ∈ Set.range ↑f_1 }
[PROOFSTEP]
exact ⟨⟨f, k, rfl⟩⟩
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
⊢ WellFounded r ↔ IsEmpty ((fun x x_1 => x > x_1) ↪r r)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
⊢ WellFounded r → IsEmpty ((fun x x_1 => x > x_1) ↪r r)
[PROOFSTEP]
rintro ⟨h⟩
[GOAL]
case mp.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
h : ∀ (a : α), Acc r a
⊢ IsEmpty ((fun x x_1 => x > x_1) ↪r r)
[PROOFSTEP]
exact ⟨fun f => not_acc_of_decreasing_seq f 0 (h _)⟩
[GOAL]
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
⊢ IsEmpty ((fun x x_1 => x > x_1) ↪r r) → WellFounded r
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
h : IsEmpty ((fun x x_1 => x > x_1) ↪r r)
⊢ WellFounded r
[PROOFSTEP]
exact ⟨fun x => acc_iff_no_decreasing_seq.2 inferInstance⟩
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x x_1 => x > x_1) ↪r r
⊢ ¬WellFounded r
[PROOFSTEP]
rw [wellFounded_iff_no_descending_seq, not_isEmpty_iff]
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x x_1 => x > x_1) ↪r r
⊢ Nonempty ((fun x x_1 => x > x_1) ↪r r)
[PROOFSTEP]
exact ⟨f⟩
[GOAL]
α : Type u_1
s : Set ℕ
inst✝ : Infinite ↑s
⊢ ℕ ≃o ↑s
[PROOFSTEP]
classical exact
  RelIso.ofSurjective
    (RelEmbedding.orderEmbeddingOfLTEmbedding
      (RelEmbedding.natLT (Nat.Subtype.ofNat s) fun n => Nat.Subtype.lt_succ_self _))
    Nat.Subtype.ofNat_surjective
[GOAL]
α : Type u_1
s : Set ℕ
inst✝ : Infinite ↑s
⊢ ℕ ≃o ↑s
[PROOFSTEP]
exact
  RelIso.ofSurjective
    (RelEmbedding.orderEmbeddingOfLTEmbedding
      (RelEmbedding.natLT (Nat.Subtype.ofNat s) fun n => Nat.Subtype.lt_succ_self _))
    Nat.Subtype.ofNat_surjective
[GOAL]
α : Type u_1
s : Set ℕ
inst✝ : Infinite ↑s
dP : DecidablePred fun x => x ∈ s
n : ℕ
⊢ ↑(orderIsoOfNat s) n = ofNat s n
[PROOFSTEP]
simp [orderIsoOfNat]
[GOAL]
α : Type u_1
s : Set ℕ
inst✝ : Infinite ↑s
dP : DecidablePred fun x => x ∈ s
n : ℕ
⊢ ofNat s n = ofNat s n
[PROOFSTEP]
congr!
[GOAL]
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
[PROOFSTEP]
classical
have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
  simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
    Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
cases this
exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
  ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]
[GOAL]
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
[PROOFSTEP]
have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
  simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
    Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
[GOAL]
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ Infinite ↑(e ⁻¹' s) ∨ Infinite ↑(e ⁻¹' t)
[PROOFSTEP]
simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
  Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
[GOAL]
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
this : Infinite ↑(e ⁻¹' s) ∨ Infinite ↑(e ⁻¹' t)
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
[PROOFSTEP]
cases this
[GOAL]
case inl
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h✝ : Infinite ↑(e ⁻¹' s)
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
case inr
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h✝ : Infinite ↑(e ⁻¹' t)
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
[PROOFSTEP]
exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
  ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
classical
let bad : Set ℕ := {m | ∀ n, m < n → ¬r (f m) (f n)}
by_cases hbad : Infinite bad
· haveI := hbad
  refine' ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => _⟩
  have h := @Set.mem_range_self _ _ (↑(Nat.orderEmbeddingOfSet bad)) m
  rw [Nat.orderEmbeddingOfSet_range bad] at h 
  exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn)
· rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad 
  obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → ¬n ∈ bad :=
    by
    by_cases he : hbad.toFinset.Nonempty
    ·
      refine'
        ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
          Nat.not_succ_le_self _ (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
    · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
  have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) :=
    by
    intro n
    have h := hm _ (le_add_of_nonneg_left n.zero_le)
    simp only [exists_prop, not_not, Set.mem_setOf_eq, not_forall] at h 
    obtain ⟨n', hn1, hn2⟩ := h
    obtain ⟨x, hpos, rfl⟩ := exists_pos_add_of_lt hn1
    refine' ⟨n + x, add_lt_add_left hpos n, _⟩
    rw [add_assoc, add_comm x m, ← add_assoc]
    exact hn2
  let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn)
  exact
    ⟨(RelEmbedding.natLT (fun n => g' n + m) fun n =>
          Nat.add_lt_add_right (Nat.find_spec (h (g' n))).1 m).orderEmbeddingOfLTEmbedding,
      Or.intro_left _ fun n => (Nat.find_spec (h (g' n))).2⟩
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
let bad : Set ℕ := {m | ∀ n, m < n → ¬r (f m) (f n)}
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
by_cases hbad : Infinite bad
[GOAL]
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite ↑bad
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
haveI := hbad
[GOAL]
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad this : Infinite ↑bad
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
refine' ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => _⟩
[GOAL]
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad this : Infinite ↑bad
m n : ℕ
mn : m < n
⊢ ¬r (f (↑(Nat.orderEmbeddingOfSet bad) m)) (f (↑(Nat.orderEmbeddingOfSet bad) n))
[PROOFSTEP]
have h := @Set.mem_range_self _ _ (↑(Nat.orderEmbeddingOfSet bad)) m
[GOAL]
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad this : Infinite ↑bad
m n : ℕ
mn : m < n
h : ↑(Nat.orderEmbeddingOfSet bad) m ∈ Set.range ↑(Nat.orderEmbeddingOfSet bad)
⊢ ¬r (f (↑(Nat.orderEmbeddingOfSet bad) m)) (f (↑(Nat.orderEmbeddingOfSet bad) n))
[PROOFSTEP]
rw [Nat.orderEmbeddingOfSet_range bad] at h 
[GOAL]
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad this : Infinite ↑bad
m n : ℕ
mn : m < n
h : ↑(Nat.orderEmbeddingOfSet bad) m ∈ bad
⊢ ¬r (f (↑(Nat.orderEmbeddingOfSet bad) m)) (f (↑(Nat.orderEmbeddingOfSet bad) n))
[PROOFSTEP]
exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn)
[GOAL]
case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : ¬Infinite ↑bad
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad 
[GOAL]
case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → ¬n ∈ bad :=
  by
  by_cases he : hbad.toFinset.Nonempty
  ·
    refine'
      ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
        Nat.not_succ_le_self _ (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
  · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
[PROOFSTEP]
by_cases he : hbad.toFinset.Nonempty
[GOAL]
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
he : Finset.Nonempty (Set.Finite.toFinset hbad)
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
[PROOFSTEP]
refine'
  ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
    Nat.not_succ_le_self _ (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
[GOAL]
case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
he : ¬Finset.Nonempty (Set.Finite.toFinset hbad)
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
[PROOFSTEP]
exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
[GOAL]
case neg.intro
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) :=
  by
  intro n
  have h := hm _ (le_add_of_nonneg_left n.zero_le)
  simp only [exists_prop, not_not, Set.mem_setOf_eq, not_forall] at h 
  obtain ⟨n', hn1, hn2⟩ := h
  obtain ⟨x, hpos, rfl⟩ := exists_pos_add_of_lt hn1
  refine' ⟨n + x, add_lt_add_left hpos n, _⟩
  rw [add_assoc, add_comm x m, ← add_assoc]
  exact hn2
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
⊢ ∀ (n : ℕ), ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
n : ℕ
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
[PROOFSTEP]
have h := hm _ (le_add_of_nonneg_left n.zero_le)
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
n : ℕ
h : ¬n + m ∈ bad
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
[PROOFSTEP]
simp only [exists_prop, not_not, Set.mem_setOf_eq, not_forall] at h 
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
n : ℕ
h : ∃ x, n + m < x ∧ r (f (n + m)) (f x)
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
[PROOFSTEP]
obtain ⟨n', hn1, hn2⟩ := h
[GOAL]
case intro.intro
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
[PROOFSTEP]
obtain ⟨x, hpos, rfl⟩ := exists_pos_add_of_lt hn1
[GOAL]
case intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
n x : ℕ
hpos : 0 < x
hn1 : n + m < n + m + x
hn2 : r (f (n + m)) (f (n + m + x))
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
[PROOFSTEP]
refine' ⟨n + x, add_lt_add_left hpos n, _⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
n x : ℕ
hpos : 0 < x
hn1 : n + m < n + m + x
hn2 : r (f (n + m)) (f (n + m + x))
⊢ r (f (n + m)) (f (n + x + m))
[PROOFSTEP]
rw [add_assoc, add_comm x m, ← add_assoc]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
n x : ℕ
hpos : 0 < x
hn1 : n + m < n + m + x
hn2 : r (f (n + m)) (f (n + m + x))
⊢ r (f (n + m)) (f (n + m + x))
[PROOFSTEP]
exact hn2
[GOAL]
case neg.intro
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
h : ∀ (n : ℕ), ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn)
[GOAL]
case neg.intro
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
h : ∀ (n : ℕ), ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
g' : ℕ → ℕ := Nat.rec m fun n gn => Nat.find (_ : ∃ n', gn < n' ∧ r (f (gn + m)) (f (n' + m)))
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
exact
  ⟨(RelEmbedding.natLT (fun n => g' n + m) fun n =>
        Nat.add_lt_add_right (Nat.find_spec (h (g' n))).1 m).orderEmbeddingOfLTEmbedding,
    Or.intro_left _ fun n => (Nat.find_spec (h (g' n))).2⟩
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (↑g m)) (f (↑g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
obtain ⟨g, hr | hnr⟩ := exists_increasing_or_nonincreasing_subseq' r f
[GOAL]
case intro.inl
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (↑g m)) (f (↑g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
refine' ⟨g, Or.intro_left _ fun m n mn => _⟩
[GOAL]
case intro.inl
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))
m n : ℕ
mn : m < n
⊢ r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
obtain ⟨x, rfl⟩ := exists_add_of_le (Nat.succ_le_iff.2 mn)
[GOAL]
case intro.inl.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))
m x : ℕ
mn : m < Nat.succ m + x
⊢ r (f (↑g m)) (f (↑g (Nat.succ m + x)))
[PROOFSTEP]
induction' x with x ih
[GOAL]
case intro.inl.intro.zero
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))
m x : ℕ
mn✝ : m < Nat.succ m + x
mn : m < Nat.succ m + Nat.zero
⊢ r (f (↑g m)) (f (↑g (Nat.succ m + Nat.zero)))
[PROOFSTEP]
apply hr
[GOAL]
case intro.inl.intro.succ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))
m x✝ : ℕ
mn✝ : m < Nat.succ m + x✝
x : ℕ
ih : m < Nat.succ m + x → r (f (↑g m)) (f (↑g (Nat.succ m + x)))
mn : m < Nat.succ m + Nat.succ x
⊢ r (f (↑g m)) (f (↑g (Nat.succ m + Nat.succ x)))
[PROOFSTEP]
apply IsTrans.trans _ _ _ _ (hr _)
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))
m x✝ : ℕ
mn✝ : m < Nat.succ m + x✝
x : ℕ
ih : m < Nat.succ m + x → r (f (↑g m)) (f (↑g (Nat.succ m + x)))
mn : m < Nat.succ m + Nat.succ x
⊢ r (f (↑g m)) (f (↑g (Nat.add (Nat.succ m) x)))
[PROOFSTEP]
exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))
[GOAL]
case intro.inr
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hnr : ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (↑g m)) (f (↑g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
exact ⟨g, Or.intro_right _ hnr⟩
[GOAL]
α : Type u_1
inst✝ : Preorder α
⊢ (WellFounded fun x x_1 => x > x_1) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
[PROOFSTEP]
refine' ⟨fun h a => _, fun h => _⟩
[GOAL]
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
[PROOFSTEP]
have hne : (Set.range a).Nonempty := ⟨a 0, by simp⟩
[GOAL]
α : Type u_1
inst✝ : Preorder α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
⊢ ↑a 0 ∈ Set.range ↑a
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.has_min _ hne
[GOAL]
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
[PROOFSTEP]
exact ⟨n, fun m _ => H _ (Set.mem_range_self _)⟩
[GOAL]
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
[PROOFSTEP]
refine' RelEmbedding.wellFounded_iff_no_descending_seq.2 ⟨fun a => _⟩
[GOAL]
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
[PROOFSTEP]
obtain ⟨n, hn⟩ := h (a.swap : ((· < ·) : ℕ → ℕ → Prop) →r ((· < ·) : α → α → Prop)).toOrderHom
[GOAL]
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
[PROOFSTEP]
exact hn n.succ n.lt_succ_self.le ((RelEmbedding.map_rel_iff _).2 n.lt_succ_self)
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
⊢ (∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ↑a n = ↑a m
[PROOFSTEP]
congr! 4
[GOAL]
case a.h.h.e'_2.h.h.a
α : Type u_1
inst✝ : PartialOrder α
a✝¹ : ℕ →o α
x✝ a✝ : ℕ
⊢ x✝ ≤ a✝ → ¬↑a✝¹ x✝ < ↑a✝¹ a✝ ↔ x✝ ≤ a✝ → ↑a✝¹ x✝ = ↑a✝¹ a✝
[PROOFSTEP]
rename_i a n m
[GOAL]
case a.h.h.e'_2.h.h.a
α : Type u_1
inst✝ : PartialOrder α
a : ℕ →o α
n m : ℕ
⊢ n ≤ m → ¬↑a n < ↑a m ↔ n ≤ m → ↑a n = ↑a m
[PROOFSTEP]
simp (config := { contextual := true }) [lt_iff_le_and_ne, fun h => a.mono h]
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
⊢ iSup ↑a = monotonicSequenceLimit a
[PROOFSTEP]
refine' (iSup_le fun m => _).antisymm (le_iSup a _)
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
⊢ ↑a m ≤ monotonicSequenceLimit a
[PROOFSTEP]
cases' le_or_lt m (monotonicSequenceLimitIndex a) with hm hm
[GOAL]
case inl
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : m ≤ monotonicSequenceLimitIndex a
⊢ ↑a m ≤ monotonicSequenceLimit a
[PROOFSTEP]
exact a.monotone hm
[GOAL]
case inr
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
⊢ ↑a m ≤ monotonicSequenceLimit a
[PROOFSTEP]
cases' WellFounded.monotone_chain_condition'.1 h a with n hn
[GOAL]
case inr.intro
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
⊢ ↑a m ≤ monotonicSequenceLimit a
[PROOFSTEP]
have : n ∈ {n | ∀ m, n ≤ m → a n = a m} := fun k hk => (a.mono hk).eq_of_not_lt (hn k hk)
[GOAL]
case inr.intro
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
this : n ∈ {n | ∀ (m : ℕ), n ≤ m → ↑a n = ↑a m}
⊢ ↑a m ≤ monotonicSequenceLimit a
[PROOFSTEP]
exact (Nat.sInf_mem ⟨n, this⟩ m hm.le).ge
