-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem admissible_or (P Q : α → Prop)
  (hadm₁ : admissible P) (hadm₂ : admissible Q) : admissible (fun x => P x ∨ Q x)

Proof state:
case inl.h
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
hP : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ P (csup c)

Tactic:
rw [csup_conj (h := hP) (hchain := hchain)]

Result:
case inl.h
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
hP : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ P (csup fun x => c x ∧ P x)

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

Tactic:
apply Decidable.or_iff_not_imp_left.mpr

Result:
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
⊢ (¬∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y) → ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y

Proof state:
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
h' : ∃ x h, ∀ (x_1 : α), c x_1 → x ⊑ x_1 → ¬P x_1
⊢ ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y

Tactic:
obtain ⟨x, hcx, hx⟩ := h'

Result:
case intro.intro
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
x : α
hcx : c x
hx : ∀ (x_1 : α), c x_1 → x ⊑ x_1 → ¬P x_1
⊢ ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y

Proof state:
case intro.intro.inl.inr
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
x : α
hcx : c x
hx : ∀ (x_1 : α), c x_1 → x ⊑ x_1 → ¬P x_1
y : α
hcy : c y
hxy : x ⊑ y
hQy : Q y
⊢ Q y

Tactic:
assumption

Result:
no goals

Proof state:
case intro.intro
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
x : α
hcx : c x
hx : ∀ (x_1 : α), c x_1 → x ⊑ x_1 → ¬P x_1
⊢ ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y

Tactic:
intro y hcy

Result:
case intro.intro
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
x : α
hcx : c x
hx : ∀ (x_1 : α), c x_1 → x ⊑ x_1 → ¬P x_1
y : α
hcy : c y
⊢ ∃ y_1, c y_1 ∧ y ⊑ y_1 ∧ Q y_1

Proof state:
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
⊢ admissible fun x => P x ∨ Q x

Tactic:
intro c hchain h

Result:
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
⊢ P (csup c) ∨ Q (csup c)

Proof state:
case inr.h
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
hQ : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y
⊢ ∀ (x : α), c x ∧ Q x → Q x

Tactic:
intro x ⟨hcx, hQx⟩

Result:
case inr.h
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
hQ : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y
x : α
hcx : c x
hQx : Q x
⊢ Q x

Proof state:
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
⊢ P (csup c) ∨ Q (csup c)

Tactic:
have : (∀ x, c x → ∃ y, c y ∧ x ⊑ y ∧ P y) ∨ (∀ x, c x → ∃ y, c y ∧ x ⊑ y ∧ Q y) := by
  open Classical in
  apply Decidable.or_iff_not_imp_left.mpr
  intro h'
  simp only [not_forall, not_imp, not_exists, not_and] at h'
  obtain ⟨x, hcx, hx⟩ := h'
  intro y hcy
  cases hchain x y hcx hcy  with
  | inl hxy =>
    refine ⟨y, hcy, rel_refl, ?_⟩
    cases h y hcy with
    | inl hPy => exfalso; apply hx y hcy hxy hPy
    | inr hQy => assumption
  | inr hyx =>
    refine ⟨x, hcx, hyx , ?_⟩
    cases h x hcx with
    | inl hPx => exfalso; apply hx x hcx rel_refl hPx
    | inr hQx => assumption

Result:
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
this : (∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y) ∨ ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y
⊢ P (csup c) ∨ Q (csup c)

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

Tactic:
open Classical in
apply Decidable.or_iff_not_imp_left.mpr
intro h'
simp only [not_forall, not_imp, not_exists, not_and] at h'
obtain ⟨x, hcx, hx⟩ := h'
intro y hcy
cases hchain x y hcx hcy  with
| inl hxy =>
  refine ⟨y, hcy, rel_refl, ?_⟩
  cases h y hcy with
  | inl hPy => exfalso; apply hx y hcy hxy hPy
  | inr hQy => assumption
| inr hyx =>
  refine ⟨x, hcx, hyx , ?_⟩
  cases h x hcx with
  | inl hPx => exfalso; apply hx x hcx rel_refl hPx
  | inr hQx => assumption

Result:
no goals

Proof state:
case inr.h
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
hQ : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y
⊢ Q (csup fun x => c x ∧ Q x)

Tactic:
apply hadm₂ _ (chain_conj _ _ hchain)

Result:
case inr.h
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
hQ : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y
⊢ ∀ (x : α), c x ∧ Q x → Q x

Proof state:
case inr.h
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
hQ : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y
⊢ Q (csup c)

Tactic:
rw [csup_conj (h := hQ) (hchain := hchain)]

Result:
case inr.h
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
hQ : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y
⊢ Q (csup fun x => c x ∧ Q x)

Proof state:
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
⊢ (¬∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y) → ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y

Tactic:
intro h'

Result:
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
h' : ¬∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y

Proof state:
case intro.intro.inl.inl
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
x : α
hcx : c x
hx : ∀ (x_1 : α), c x_1 → x ⊑ x_1 → ¬P x_1
y : α
hcy : c y
hxy : x ⊑ y
hPy : P y
⊢ Q y

Tactic:
exfalso

Result:
case intro.intro.inl.inl
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
x : α
hcx : c x
hx : ∀ (x_1 : α), c x_1 → x ⊑ x_1 → ¬P x_1
y : α
hcy : c y
hxy : x ⊑ y
hPy : P y
⊢ False