[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
hφ : StrictMonoOn φ (Iic n)
⊢ ∀ (m : α), m ≤ n → m ≤ φ m
[PROOFSTEP]
revert hφ
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
⊢ StrictMonoOn φ (Iic n) → ∀ (m : α), m ≤ n → m ≤ φ m
[PROOFSTEP]
refine' Succ.rec_bot (fun n => StrictMonoOn φ (Set.Iic n) → ∀ m ≤ n, m ≤ φ m) (fun _ _ hm => hm.trans bot_le) _ _
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
⊢ ∀ (a : α),
    (fun n => StrictMonoOn φ (Iic n) → ∀ (m : α), m ≤ n → m ≤ φ m) a →
      (fun n => StrictMonoOn φ (Iic n) → ∀ (m : α), m ≤ n → m ≤ φ m) (succ a)
[PROOFSTEP]
rintro k ih hφ m hm
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ (m : α), m ≤ k → m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
⊢ m ≤ φ m
[PROOFSTEP]
by_cases hk : IsMax k
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ (m : α), m ≤ k → m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : IsMax k
⊢ m ≤ φ m
[PROOFSTEP]
rw [succ_eq_iff_isMax.2 hk] at hm
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ (m : α), m ≤ k → m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ k
hk : IsMax k
⊢ m ≤ φ m
[PROOFSTEP]
exact ih (hφ.mono <| Iic_subset_Iic.2 (le_succ _)) _ hm
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ (m : α), m ≤ k → m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : ¬IsMax k
⊢ m ≤ φ m
[PROOFSTEP]
obtain rfl | h := le_succ_iff_eq_or_le.1 hm
[GOAL]
case neg.inl
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ (m : α), m ≤ k → m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
⊢ succ k ≤ φ (succ k)
[PROOFSTEP]
specialize ih (StrictMonoOn.mono hφ fun x hx => le_trans hx (le_succ _)) k le_rfl
[GOAL]
case neg.inl
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
ih : k ≤ φ k
⊢ succ k ≤ φ (succ k)
[PROOFSTEP]
refine' le_trans (succ_mono ih) (succ_le_of_lt (hφ (le_succ _) le_rfl _))
[GOAL]
case neg.inl
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
ih : k ≤ φ k
⊢ k < succ k
[PROOFSTEP]
rw [lt_succ_iff_eq_or_lt_of_not_isMax hk]
[GOAL]
case neg.inl
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
ih : k ≤ φ k
⊢ k = k ∨ k < k
[PROOFSTEP]
exact Or.inl rfl
[GOAL]
case neg.inr
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ (m : α), m ≤ k → m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : ¬IsMax k
h : m ≤ k
⊢ m ≤ φ m
[PROOFSTEP]
exact ih (StrictMonoOn.mono hφ fun x hx => le_trans hx (le_succ _)) _ h
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
⊢ StrictMonoOn ψ (Iic n)
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ∈ Iic n
y : α
hy : y ∈ Iic n
hxy : x < y
⊢ ψ x < ψ y
[PROOFSTEP]
obtain ⟨i, rfl⟩ := hxy.le.exists_succ_iterate
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ∈ Iic n
i : ℕ
hy : succ^[i] x ∈ Iic n
hxy : x < succ^[i] x
⊢ ψ x < ψ (succ^[i] x)
[PROOFSTEP]
induction' i with k ih
[GOAL]
case intro.zero
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ∈ Iic n
i : ℕ
hy✝ : succ^[i] x ∈ Iic n
hxy✝ : x < succ^[i] x
hy : succ^[Nat.zero] x ∈ Iic n
hxy : x < succ^[Nat.zero] x
⊢ ψ x < ψ (succ^[Nat.zero] x)
[PROOFSTEP]
simp at hxy
[GOAL]
case intro.succ
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ∈ Iic n
i : ℕ
hy✝ : succ^[i] x ∈ Iic n
hxy✝ : x < succ^[i] x
k : ℕ
ih : succ^[k] x ∈ Iic n → x < succ^[k] x → ψ x < ψ (succ^[k] x)
hy : succ^[Nat.succ k] x ∈ Iic n
hxy : x < succ^[Nat.succ k] x
⊢ ψ x < ψ (succ^[Nat.succ k] x)
[PROOFSTEP]
cases' k with k
[GOAL]
case intro.succ.zero
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ∈ Iic n
i : ℕ
hy✝ : succ^[i] x ∈ Iic n
hxy✝ : x < succ^[i] x
ih : succ^[Nat.zero] x ∈ Iic n → x < succ^[Nat.zero] x → ψ x < ψ (succ^[Nat.zero] x)
hy : succ^[Nat.succ Nat.zero] x ∈ Iic n
hxy : x < succ^[Nat.succ Nat.zero] x
⊢ ψ x < ψ (succ^[Nat.succ Nat.zero] x)
[PROOFSTEP]
exact hψ _ (lt_of_lt_of_le hxy hy)
[GOAL]
case intro.succ.succ
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ∈ Iic n
i : ℕ
hy✝ : succ^[i] x ∈ Iic n
hxy✝ : x < succ^[i] x
k : ℕ
ih : succ^[Nat.succ k] x ∈ Iic n → x < succ^[Nat.succ k] x → ψ x < ψ (succ^[Nat.succ k] x)
hy : succ^[Nat.succ (Nat.succ k)] x ∈ Iic n
hxy : x < succ^[Nat.succ (Nat.succ k)] x
⊢ ψ x < ψ (succ^[Nat.succ (Nat.succ k)] x)
[PROOFSTEP]
rw [Set.mem_Iic] at *
[GOAL]
case intro.succ.succ
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ≤ n
i : ℕ
hy✝ : succ^[i] x ≤ n
hxy✝ : x < succ^[i] x
k : ℕ
ih : succ^[Nat.succ k] x ≤ n → x < succ^[Nat.succ k] x → ψ x < ψ (succ^[Nat.succ k] x)
hy : succ^[Nat.succ (Nat.succ k)] x ≤ n
hxy : x < succ^[Nat.succ (Nat.succ k)] x
⊢ ψ x < ψ (succ^[Nat.succ (Nat.succ k)] x)
[PROOFSTEP]
simp only [Function.iterate_succ', Function.comp_apply] at ih hxy hy ⊢
[GOAL]
case intro.succ.succ
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ≤ n
i : ℕ
hy✝ : succ^[i] x ≤ n
hxy✝ : x < succ^[i] x
k : ℕ
ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))
hxy : x < succ (succ (succ^[k] x))
hy : succ (succ (succ^[k] x)) ≤ n
⊢ ψ x < ψ (succ (succ (succ^[k] x)))
[PROOFSTEP]
by_cases hmax : IsMax (succ^[k] x)
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ≤ n
i : ℕ
hy✝ : succ^[i] x ≤ n
hxy✝ : x < succ^[i] x
k : ℕ
ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))
hxy : x < succ (succ (succ^[k] x))
hy : succ (succ (succ^[k] x)) ≤ n
hmax : IsMax (succ^[k] x)
⊢ ψ x < ψ (succ (succ (succ^[k] x)))
[PROOFSTEP]
rw [succ_eq_iff_isMax.2 hmax] at hxy ⊢
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ≤ n
i : ℕ
hy✝ : succ^[i] x ≤ n
hxy✝ : x < succ^[i] x
k : ℕ
ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))
hxy : x < succ (succ^[k] x)
hy : succ (succ (succ^[k] x)) ≤ n
hmax : IsMax (succ^[k] x)
⊢ ψ x < ψ (succ (succ^[k] x))
[PROOFSTEP]
exact ih (le_trans (le_succ _) hy) hxy
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ≤ n
i : ℕ
hy✝ : succ^[i] x ≤ n
hxy✝ : x < succ^[i] x
k : ℕ
ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))
hxy : x < succ (succ (succ^[k] x))
hy : succ (succ (succ^[k] x)) ≤ n
hmax : ¬IsMax (succ^[k] x)
⊢ ψ x < ψ (succ (succ (succ^[k] x)))
[PROOFSTEP]
by_cases hmax' : IsMax (succ (succ^[k] x))
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ≤ n
i : ℕ
hy✝ : succ^[i] x ≤ n
hxy✝ : x < succ^[i] x
k : ℕ
ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))
hxy : x < succ (succ (succ^[k] x))
hy : succ (succ (succ^[k] x)) ≤ n
hmax : ¬IsMax (succ^[k] x)
hmax' : IsMax (succ (succ^[k] x))
⊢ ψ x < ψ (succ (succ (succ^[k] x)))
[PROOFSTEP]
rw [succ_eq_iff_isMax.2 hmax'] at hxy ⊢
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ≤ n
i : ℕ
hy✝ : succ^[i] x ≤ n
hxy✝ : x < succ^[i] x
k : ℕ
ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))
hxy : x < succ (succ^[k] x)
hy : succ (succ (succ^[k] x)) ≤ n
hmax : ¬IsMax (succ^[k] x)
hmax' : IsMax (succ (succ^[k] x))
⊢ ψ x < ψ (succ (succ^[k] x))
[PROOFSTEP]
exact ih (le_trans (le_succ _) hy) hxy
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ≤ n
i : ℕ
hy✝ : succ^[i] x ≤ n
hxy✝ : x < succ^[i] x
k : ℕ
ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))
hxy : x < succ (succ (succ^[k] x))
hy : succ (succ (succ^[k] x)) ≤ n
hmax : ¬IsMax (succ^[k] x)
hmax' : ¬IsMax (succ (succ^[k] x))
⊢ ψ x < ψ (succ (succ (succ^[k] x)))
[PROOFSTEP]
refine' lt_trans (ih (le_trans (le_succ _) hy) (lt_of_le_of_lt (le_succ_iterate k _) (lt_succ_iff_not_isMax.2 hmax))) _
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ≤ n
i : ℕ
hy✝ : succ^[i] x ≤ n
hxy✝ : x < succ^[i] x
k : ℕ
ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))
hxy : x < succ (succ (succ^[k] x))
hy : succ (succ (succ^[k] x)) ≤ n
hmax : ¬IsMax (succ^[k] x)
hmax' : ¬IsMax (succ (succ^[k] x))
⊢ ψ (succ (succ^[k] x)) < ψ (succ (succ (succ^[k] x)))
[PROOFSTEP]
rw [← Function.comp_apply (f := succ), ← Function.iterate_succ']
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ≤ n
i : ℕ
hy✝ : succ^[i] x ≤ n
hxy✝ : x < succ^[i] x
k : ℕ
ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))
hxy : x < succ (succ (succ^[k] x))
hy : succ (succ (succ^[k] x)) ≤ n
hmax : ¬IsMax (succ^[k] x)
hmax' : ¬IsMax (succ (succ^[k] x))
⊢ ψ (succ^[Nat.succ k] x) < ψ (succ (succ^[Nat.succ k] x))
[PROOFSTEP]
refine' hψ _ (lt_of_lt_of_le _ hy)
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : Preorder β
ψ : α → β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
n : α
hψ : ∀ (m : α), m < n → ψ m < ψ (succ m)
x : α
hx : x ≤ n
i : ℕ
hy✝ : succ^[i] x ≤ n
hxy✝ : x < succ^[i] x
k : ℕ
ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))
hxy : x < succ (succ (succ^[k] x))
hy : succ (succ (succ^[k] x)) ≤ n
hmax : ¬IsMax (succ^[k] x)
hmax' : ¬IsMax (succ (succ^[k] x))
⊢ succ^[Nat.succ k] x < succ (succ (succ^[k] x))
[PROOFSTEP]
rwa [Function.iterate_succ', Function.comp_apply, lt_succ_iff_not_isMax]