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))

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))
α : 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))
obtain ⟨g, hr | hnr⟩ := exists_increasing_or_nonincreasing_subseq' r f
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))
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))
refine' ⟨g, Or.intro_left _ fun m n mn => _⟩
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)))
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))
obtain ⟨x, rfl⟩ := exists_add_of_le (Nat.succ_le_iff.2 mn)
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)))

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)))
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)))
induction' x with x ih
no goals
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)))
apply hr
α : 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)))
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)))
apply IsTrans.trans _ _ _ _ (hr _)
no goals
α : 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)))
exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))
no goals
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))
exact ⟨g, Or.intro_right _ hnr⟩