α : Type u_1
β : Type ?u.12805
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
⊢ StrictMonoOn φ (Iic n) → ∀ (m : α), m ≤ n → m ≤ φ m
α : Type u_1
β : Type ?u.12805
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
hφ : StrictMonoOn φ (Iic n)
⊢ ∀ (m : α), m ≤ n → m ≤ φ m
revert hφ
α : Type u_1
β : Type ?u.12805
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)
α : Type u_1
β : Type ?u.12805
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
⊢ StrictMonoOn φ (Iic n) → ∀ (m : α), m ≤ n → m ≤ φ m
refine'
  Succ.rec_bot (fun n => StrictMonoOn φ (Set.Iic n) → ∀ m ≤ n, m ≤ φ m)
    (fun _ _ hm => hm.trans bot_le) _ _
α : Type u_1
β : Type ?u.12805
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
α : Type u_1
β : Type ?u.12805
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)
rintro k ih hφ m hm
case pos
α : Type u_1
β : Type ?u.12805
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

case neg
α : Type u_1
β : Type ?u.12805
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
α : Type u_1
β : Type ?u.12805
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
by_cases hk : IsMax k
case neg.inl
α : Type u_1
β : Type ?u.12805
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)

case neg.inr
α : Type u_1
β : Type ?u.12805
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
case neg
α : Type u_1
β : Type ?u.12805
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
obtain rfl | h := le_succ_iff_eq_or_le.1 hm
case pos
α : Type u_1
β : Type ?u.12805
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
case pos
α : Type u_1
β : Type ?u.12805
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
rw [succ_eq_iff_isMax.2 hk] at hm
no goals
case pos
α : Type u_1
β : Type ?u.12805
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
exact ih (hφ.mono <| Iic_subset_Iic.2 (le_succ _)) _ hm
case neg.inl
α : Type u_1
β : Type ?u.12805
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)
case neg.inl
α : Type u_1
β : Type ?u.12805
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)
specialize ih (StrictMonoOn.mono hφ fun x hx => le_trans hx (le_succ _)) k le_rfl
case neg.inl
α : Type u_1
β : Type ?u.12805
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
case neg.inl
α : Type u_1
β : Type ?u.12805
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)
refine' le_trans (succ_mono ih) (succ_le_of_lt (hφ (le_succ _) le_rfl _))
case neg.inl
α : Type u_1
β : Type ?u.12805
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
case neg.inl
α : Type u_1
β : Type ?u.12805
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
rw [lt_succ_iff_eq_or_lt_of_not_isMax hk]
no goals
case neg.inl
α : Type u_1
β : Type ?u.12805
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
exact Or.inl rfl
no goals
case neg.inr
α : Type u_1
β : Type ?u.12805
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
exact ih (StrictMonoOn.mono hφ fun x hx => le_trans hx (le_succ _)) _ h