case intro.intro.intro.intro
α : Type u_1
β : Type ?u.3853
r : α → α → Prop
c✝ : Set α
inst✝ : Preorder α
s : Set α
ih : ∀ (c : Set α), c ⊆ s → IsChain (fun x x_1 => x ≤ x_1) c → ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
c : Set ↑s
hc : IsChain (fun x x_1 => x ≤ x_1) c
p : { x // x ∈ s }
hpc : p ∈ c
q : { x // x ∈ s }
hqc : q ∈ c
hpq : ↑p ≠ ↑q
⊢ (fun x x_1 => x ≤ x_1) ↑p ↑q ∨ (fun x x_1 => x ≤ x_1) ↑q ↑p
α : Type u_1
β : Type ?u.3853
r : α → α → Prop
c✝ : Set α
inst✝ : Preorder α
s : Set α
ih : ∀ (c : Set α), c ⊆ s → IsChain (fun x x_1 => x ≤ x_1) c → ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
c : Set ↑s
hc : IsChain (fun x x_1 => x ≤ x_1) c
⊢ IsChain (fun x x_1 => x ≤ x_1) (Subtype.val '' c)
rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq
no goals
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.3853
r : α → α → Prop
c✝ : Set α
inst✝ : Preorder α
s : Set α
ih : ∀ (c : Set α), c ⊆ s → IsChain (fun x x_1 => x ≤ x_1) c → ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
c : Set ↑s
hc : IsChain (fun x x_1 => x ≤ x_1) c
p : { x // x ∈ s }
hpc : p ∈ c
q : { x // x ∈ s }
hqc : q ∈ c
hpq : ↑p ≠ ↑q
⊢ (fun x x_1 => x ≤ x_1) ↑p ↑q ∨ (fun x x_1 => x ≤ x_1) ↑q ↑p
refine' hc hpc hqc fun t => hpq (Subtype.ext_iff.1 t)