α : Type ?u.41863
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))
α : Type ?u.41863
r : α → α → Prop
f : ℕ → α
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
let bad : Set ℕ := { m | ∀ n, m < n → ¬r (f m) (f n) }
case pos
α : Type ?u.41863
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))

case neg
α : Type ?u.41863
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))
α : Type ?u.41863
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))
by_cases hbad : Infinite bad
case pos
α : Type ?u.41863
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))
case pos
α : Type ?u.41863
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))
haveI := hbad
case pos
α : Type ?u.41863
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))
case pos
α : Type ?u.41863
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))
refine' ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => _⟩
case pos
α : Type ?u.41863
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))
case pos
α : Type ?u.41863
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))
have h := @Set.mem_range_self _ _ ↑(Nat.orderEmbeddingOfSet bad) m
case pos
α : Type ?u.41863
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))
case pos
α : Type ?u.41863
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))
rw [Nat.orderEmbeddingOfSet_range bad] at h
no goals
case pos
α : Type ?u.41863
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))
exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn)
case neg
α : Type ?u.41863
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))
case neg
α : Type ?u.41863
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))
rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad
case neg.intro
α : Type ?u.41863
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))
case neg.intro
α : Type ?u.41863
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))
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
case neg.intro
α : Type ?u.41863
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))
case neg.intro
α : Type ?u.41863
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))
let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn)
no goals
case neg.intro
α : Type ?u.41863
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))
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⟩
case pos
α : Type ?u.41863
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

case neg
α : Type ?u.41863
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
α : Type ?u.41863
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
by_cases he : hbad.toFinset.Nonempty
no goals
case pos
α : Type ?u.41863
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
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)))⟩
no goals
case neg
α : Type ?u.41863
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
exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
α : Type ?u.41863
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))
α : Type ?u.41863
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))
intro n
α : Type ?u.41863
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))
α : Type ?u.41863
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))
have h := hm _ (le_add_of_nonneg_left n.zero_le)
α : Type ?u.41863
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))
α : Type ?u.41863
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))
simp only [exists_prop, not_not, Set.mem_setOf_eq, not_forall] at h
case intro.intro
α : Type ?u.41863
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))
α : Type ?u.41863
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))
obtain ⟨n', hn1, hn2⟩ := h
case intro.intro.intro.intro
α : Type ?u.41863
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))
case intro.intro
α : Type ?u.41863
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))
obtain ⟨x, hpos, rfl⟩ := exists_pos_add_of_lt hn1
case intro.intro.intro.intro
α : Type ?u.41863
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))
case intro.intro.intro.intro
α : Type ?u.41863
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))
refine' ⟨n + x, add_lt_add_left hpos n, _⟩
case intro.intro.intro.intro
α : Type ?u.41863
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))
case intro.intro.intro.intro
α : Type ?u.41863
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))
rw [add_assoc, add_comm x m, ← add_assoc]
no goals
case intro.intro.intro.intro
α : Type ?u.41863
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))
exact hn2