α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort ?u.9479
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
⊢ IsSuccLimit a → a ≤ b
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort ?u.9479
inst✝ : IsSuccArchimedean α
h : IsSuccLimit a
b : α
hb : b ≤ a
⊢ a ≤ b
revert h
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort ?u.9479
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccLimit c → c ≤ b
hc : IsSuccLimit (succ c)
⊢ succ c ≤ b
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort ?u.9479
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
⊢ IsSuccLimit a → a ≤ b
refine' Succ.rec (fun _ => le_rfl) (fun c _ H hc => _) hb
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort ?u.9479
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccLimit c → c ≤ b
hc : IsSuccLimit (succ c)
this : succ c = c
⊢ succ c ≤ b
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort ?u.9479
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccLimit c → c ≤ b
hc : IsSuccLimit (succ c)
⊢ succ c ≤ b
have := hc.isMax.succ_eq
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort ?u.9479
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccLimit c → c ≤ b
hc : IsSuccLimit c
this : succ c = c
⊢ c ≤ b
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort ?u.9479
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccLimit c → c ≤ b
hc : IsSuccLimit (succ c)
this : succ c = c
⊢ succ c ≤ b
rw [this] at hc⊢
no goals
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort ?u.9479
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccLimit c → c ≤ b
hc : IsSuccLimit c
this : succ c = c
⊢ c ≤ b
exact H hc