-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem csup_conj (c P : α → Prop) (hchain : chain c) (h : ∀ x, c x → ∃ y, c y ∧ x ⊑ y ∧ P y) :
    csup c = csup (fun x => c x ∧ P x)

Proof state:
case a.intro.intro.intro
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
x : α
hcx : c x
y : α
hcy : c y
hxy : x ⊑ y
hPy : P y
⊢ y ⊑ csup fun x => c x ∧ P x

Tactic:
clear x hcx hxy

Result:
case a.intro.intro.intro
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
y : α
hcy : c y
hPy : P y
⊢ y ⊑ csup fun x => c x ∧ P x

Proof state:
case a
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
x : α
hcx : c x
⊢ x ⊑ csup fun x => c x ∧ P x

Tactic:
obtain ⟨y, hcy, hxy, hPy⟩ := h x hcx

Result:
case a.intro.intro.intro
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
x : α
hcx : c x
y : α
hcy : c y
hxy : x ⊑ y
hPy : P y
⊢ x ⊑ csup fun x => c x ∧ P x

Proof state:
case a
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ (csup fun x => c x ∧ P x) ⊑ csup c

Tactic:
apply csup_le (chain_conj _ _ hchain)

Result:
case a
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ ∀ (y : α), c y ∧ P y → y ⊑ csup c

Proof state:
case a.intro.intro.intro
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
x : α
hcx : c x
y : α
hcy : c y
hxy : x ⊑ y
hPy : P y
⊢ x ⊑ csup fun x => c x ∧ P x

Tactic:
apply rel_trans hxy

Result:
case a.intro.intro.intro
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
x : α
hcx : c x
y : α
hcy : c y
hxy : x ⊑ y
hPy : P y
⊢ y ⊑ csup fun x => c x ∧ P x

Proof state:
case a
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
x : α
hcx : c x
hPx : P x
⊢ x ⊑ csup c

Tactic:
apply le_csup hchain hcx

Result:
no goals

Proof state:
case a
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ ∀ (y : α), c y ∧ P y → y ⊑ csup c

Tactic:
intro x ⟨hcx, hPx⟩

Result:
case a
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
x : α
hcx : c x
hPx : P x
⊢ x ⊑ csup c

Proof state:
case a
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ ∀ (y : α), c y → y ⊑ csup fun x => c x ∧ P x

Tactic:
intro x hcx

Result:
case a
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
x : α
hcx : c x
⊢ x ⊑ csup fun x => c x ∧ P x

Proof state:
case a
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ csup c ⊑ csup fun x => c x ∧ P x

Tactic:
apply csup_le hchain

Result:
case a
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ ∀ (y : α), c y → y ⊑ csup fun x => c x ∧ P x

Proof state:
case a.intro.intro.intro
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
y : α
hcy : c y
hPy : P y
⊢ y ⊑ csup fun x => c x ∧ P x

Tactic:
apply le_csup (chain_conj _ _ hchain) ⟨hcy, hPy⟩

Result:
no goals

Proof state:
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ csup c = csup fun x => c x ∧ P x

Tactic:
apply rel_antisymm

Result:
case a
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ csup c ⊑ csup fun x => c x ∧ P x

case a
α : Sort u
inst✝ : CCPO α
c P : α → Prop
hchain : chain c
h : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ (csup fun x => c x ∧ P x) ⊑ csup c