α : 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
α : 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)
intro x hx y hy hxy
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)
α : 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
obtain ⟨i, rfl⟩ := hxy.le.exists_succ_iterate
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)

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)
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)
induction' i with k ih
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)

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)
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)
cases' k with k
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)
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)
rw [Set.mem_Iic] at *
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)))
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)
simp only [Function.iterate_succ', Function.comp_apply] at ih hxy hy⊢
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)))

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)))
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)))
by_cases hmax : IsMax ((succ^[k]) x)
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)))

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)))
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)))
by_cases hmax' : IsMax (succ ((succ^[k]) x))
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)))
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)))
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)))
    _
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))
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)))
rw [← Function.comp_apply (f := succ), ← Function.iterate_succ']
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))
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))
refine' hψ _ (lt_of_lt_of_le _ hy)
no goals
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))
rwa [Function.iterate_succ', Function.comp_apply, lt_succ_iff_not_isMax]
no goals
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)
simp at hxy
no goals
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)
exact hψ _ (lt_of_lt_of_le hxy hy)
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))
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)))
rw [succ_eq_iff_isMax.2 hmax] at hxy ⊢
no goals
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))
exact ih (le_trans (le_succ _) hy) hxy
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))
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)))
rw [succ_eq_iff_isMax.2 hmax'] at hxy ⊢
no goals
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))
exact ih (le_trans (le_succ _) hy) hxy