P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ (match Encodable.decode (Encodable.encode i) with
    | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
    | some i_1 => Cofinal.above (𝒟 i_1) (sequenceOfCofinals p 𝒟 (Encodable.encode i))) ∈
    𝒟 i
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) ∈ 𝒟 i
dsimp only [sequenceOfCofinals, Nat.add]
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ (match some i with
    | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
    | some i_1 => Cofinal.above (𝒟 i_1) (sequenceOfCofinals p 𝒟 (Encodable.encode i))) ∈
    𝒟 i
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ (match Encodable.decode (Encodable.encode i) with
    | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
    | some i_1 => Cofinal.above (𝒟 i_1) (sequenceOfCofinals p 𝒟 (Encodable.encode i))) ∈
    𝒟 i
rw [Encodable.encodek]
no goals
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ (match some i with
    | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
    | some i_1 => Cofinal.above (𝒟 i_1) (sequenceOfCofinals p 𝒟 (Encodable.encode i))) ∈
    𝒟 i
apply Cofinal.above_mem