no goals
α : Type u_1
β : Type ?u.6442
r : α → α → Prop
c : Set α
inst✝ : Preorder α
a : α
ih :
  ∀ (c : Set α),
    c ⊆ Ici a → IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, a ≤ ub ∧ ∀ (z : α), z ∈ c → z ≤ ub
x : α
hax : a ≤ x
⊢ ∀ (c : Set α),
    c ⊆ Ici a → IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ Ici a ∧ ∀ (z : α), z ∈ c → z ≤ ub
simpa using ih