-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem mem_ωSup (x : α) (c : Chain (Part α)) : x ∈ ωSup c ↔ some x ∈ c

Proof state:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
hh : some (Classical.choose h') ∈ c
⊢ x ∈ some x

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_2
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
⊢ x ∈ some (Classical.choose h) → some x ∈ c

case neg
α : Type u_2
x : α
c : Chain (Part α)
h : ¬∃ a, some a ∈ c
⊢ x ∈ none → some x ∈ c

Tactic:
swap

Result:
case neg
α : Type u_2
x : α
c : Chain (Part α)
h : ¬∃ a, some a ∈ c
⊢ x ∈ none → some x ∈ c

case pos
α : Type u_2
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
⊢ x ∈ some (Classical.choose h) → some x ∈ c

Proof state:
α : Type u_2
x : α
c : Chain (Part α)
⊢ (x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none) ↔ some x ∈ c

Tactic:
constructor

Result:
case mp
α : Type u_2
x : α
c : Chain (Part α)
⊢ (x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none) → some x ∈ c

case mpr
α : Type u_2
x : α
c : Chain (Part α)
⊢ some x ∈ c → x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none

Proof state:
case pos
α : Type u_2
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
hh : some (Classical.choose h) ∈ c
h' : x = Classical.choose h
⊢ some x ∈ c

Tactic:
subst x

Result:
case pos
α : Type u_2
c : Chain (Part α)
h : ∃ a, some a ∈ c
hh : some (Classical.choose h) ∈ c
⊢ some (Classical.choose h) ∈ c

Proof state:
case neg
α : Type u_2
x : α
c : Chain (Part α)
h : ¬∃ a, some a ∈ c
⊢ x ∈ none → some x ∈ c

Tactic:
rintro ⟨⟨⟩⟩

Result:
no goals

Proof state:
case pos
α : Type u_2
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
h' : x ∈ some (Classical.choose h)
⊢ some x ∈ c

Tactic:
have hh := Classical.choose_spec h

Result:
case pos
α : Type u_2
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
h' : x ∈ some (Classical.choose h)
hh : some (Classical.choose h) ∈ c
⊢ some x ∈ c

Proof state:
case pos
α : Type u_2
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
h' : x ∈ some (Classical.choose h)
hh : some (Classical.choose h) ∈ c
⊢ some x ∈ c

Tactic:
simp only [mem_some_iff] at h'

Result:
case pos
α : Type u_2
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
hh : some (Classical.choose h) ∈ c
h' : x = Classical.choose h
⊢ some x ∈ c

Proof state:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none

Tactic:
rw [dif_pos h']

Result:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ some (Classical.choose h')

Proof state:
case pos
α : Type u_2
c : Chain (Part α)
h : ∃ a, some a ∈ c
hh : some (Classical.choose h) ∈ c
⊢ some (Classical.choose h) ∈ c

Tactic:
exact hh

Result:
no goals

Proof state:
α : Type u_2
x : α
c : Chain (Part α)
⊢ x ∈ ωSup c ↔ some x ∈ c

Tactic:
simp only [ωSup, Part.ωSup]

Result:
α : Type u_2
x : α
c : Chain (Part α)
⊢ (x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none) ↔ some x ∈ c

Proof state:
case pos
α : Type u_2
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
⊢ x ∈ some (Classical.choose h) → some x ∈ c

Tactic:
intro h'

Result:
case pos
α : Type u_2
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
h' : x ∈ some (Classical.choose h)
⊢ some x ∈ c

Proof state:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
hh : some (Classical.choose h') ∈ c
⊢ x ∈ some (Classical.choose h')

Tactic:
rw [eq_of_chain hh h]

Result:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
hh : some (Classical.choose h') ∈ c
⊢ x ∈ some x

Proof state:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ some (Classical.choose h')

Tactic:
have hh := Classical.choose_spec h'

Result:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
hh : some (Classical.choose h') ∈ c
⊢ x ∈ some (Classical.choose h')

Proof state:
case mp
α : Type u_2
x : α
c : Chain (Part α)
⊢ (x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none) → some x ∈ c

Tactic:
split_ifs with h

Result:
case pos
α : Type u_2
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
⊢ x ∈ some (Classical.choose h) → some x ∈ c

case neg
α : Type u_2
x : α
c : Chain (Part α)
h : ¬∃ a, some a ∈ c
⊢ x ∈ none → some x ∈ c

Proof state:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
⊢ x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none

Tactic:
have h' : ∃ a : α, some a ∈ c := ⟨_, h⟩

Result:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none

Proof state:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
⊢ some x ∈ c → x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none

Tactic:
intro h

Result:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
⊢ x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none