α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
⊢ (x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none) ↔ some x ∈ c
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
⊢ x ∈ ωSup c ↔ some x ∈ c
simp [OmegaCompletePartialOrder.ωSup, Part.ωSup]
case mp
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
⊢ (x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none) → some x ∈ c

case mpr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
⊢ some x ∈ c → x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
⊢ (x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none) ↔ some x ∈ c
constructor
case mp.inl
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
⊢ x ∈ some (choose h) → some x ∈ c

case mp.inr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ¬∃ a, some a ∈ c
⊢ x ∈ none → some x ∈ c
case mp
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
⊢ (x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none) → some x ∈ c
split_ifs with h
case mp.inr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ¬∃ a, some a ∈ c
⊢ x ∈ none → some x ∈ c

case mp.inl
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
⊢ x ∈ some (choose h) → some x ∈ c
case mp.inl
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
⊢ x ∈ some (choose h) → some x ∈ c

case mp.inr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ¬∃ a, some a ∈ c
⊢ x ∈ none → some x ∈ c
swap
case mp.inl
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
⊢ x ∈ some (choose h) → some x ∈ c
case mp.inr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ¬∃ a, some a ∈ c
⊢ x ∈ none → some x ∈ c

case mp.inl
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
⊢ x ∈ some (choose h) → some x ∈ c
rintro ⟨⟨⟩⟩
case mp.inl
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
h' : x ∈ some (choose h)
⊢ some x ∈ c
case mp.inl
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
⊢ x ∈ some (choose h) → some x ∈ c
intro h'
case mp.inl
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
h' : x ∈ some (choose h)
hh : some (choose h) ∈ c
⊢ some x ∈ c
case mp.inl
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
h' : x ∈ some (choose h)
⊢ some x ∈ c
have hh := Classical.choose_spec h
case mp.inl
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
hh : some (choose h) ∈ c
h' : x = choose h
⊢ some x ∈ c
case mp.inl
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
h' : x ∈ some (choose h)
hh : some (choose h) ∈ c
⊢ some x ∈ c
simp at h'
case mp.inl
α : Type u
β : Type v
γ : Type ?u.16890
c : Chain (Part α)
h : ∃ a, some a ∈ c
hh : some (choose h) ∈ c
⊢ some (choose h) ∈ c
case mp.inl
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
hh : some (choose h) ∈ c
h' : x = choose h
⊢ some x ∈ c
subst x
no goals
case mp.inl
α : Type u
β : Type v
γ : Type ?u.16890
c : Chain (Part α)
h : ∃ a, some a ∈ c
hh : some (choose h) ∈ c
⊢ some (choose h) ∈ c
exact hh
case mpr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : some x ∈ c
⊢ x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none
case mpr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
⊢ some x ∈ c → x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none
intro h
case mpr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none
case mpr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : some x ∈ c
⊢ x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none
have h' : ∃ a : α, some a ∈ c := ⟨_, h⟩
case mpr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ some (choose h')
case mpr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none
rw [dif_pos h']
case mpr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
hh : some (choose h') ∈ c
⊢ x ∈ some (choose h')
case mpr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ some (choose h')
have hh := Classical.choose_spec h'
case mpr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
hh : some (choose h') ∈ c
⊢ x ∈ some x
case mpr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
hh : some (choose h') ∈ c
⊢ x ∈ some (choose h')
rw [eq_of_chain hh h]
no goals
case mpr
α : Type u
β : Type v
γ : Type ?u.16890
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
hh : some (choose h') ∈ c
⊢ x ∈ some x
simp