-- 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:
α : 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)

Tactic:
cases this with
| inl hP =>
  left
  rw [csup_conj (h := hP) (hchain := hchain)]
  apply hadm₁ _ (chain_conj _ _ hchain)
  intro x ⟨hcx, hPx⟩
  exact hPx
| inr hQ =>
  right
  rw [csup_conj (h := hQ) (hchain := hchain)]
  apply hadm₂ _ (chain_conj _ _ hchain)
  intro x ⟨hcx, hQx⟩
  exact hQx

Result:
no goals

Proof state:
case intro.intro.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
⊢ ∃ y_1, c y_1 ∧ y ⊑ y_1 ∧ Q y_1

Tactic:
refine ⟨y, hcy, rel_refl, ?_⟩

Result:
case intro.intro.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
⊢ Q y

Proof state:
case intro.intro.inr.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
hyx : y ⊑ x
hQx : Q x
⊢ Q x

Tactic:
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
x : α
hcx : c x
hQx : Q x
⊢ Q x

Tactic:
exact hQx

Result:
no goals

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 : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y

Tactic:
simp only [not_forall, not_imp, not_exists, not_and] at 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 h, ∀ (x_1 : α), c x_1 → x ⊑ x_1 → ¬P x_1
⊢ ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y

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
x : α
hcx : c x
hPx : P x
⊢ P x

Tactic:
exact hPx

Result:
no goals

Proof state:
case intro.intro.inr.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
hyx : y ⊑ x
hPx : P x
⊢ Q x

Tactic:
exfalso

Result:
case intro.intro.inr.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
hyx : y ⊑ x
hPx : P x
⊢ False

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
⊢ False

Tactic:
apply hx y hcy hxy hPy

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
y : α
hcy : c y
⊢ ∃ y_1, c y_1 ∧ y ⊑ y_1 ∧ Q y_1

Tactic:
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 intro.intro.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
⊢ Q y

Tactic:
cases h y hcy with
| inl hPy => exfalso; apply hx y hcy hxy hPy
| inr hQy => assumption

Result:
no goals

Proof state:
case 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
hQ : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ Q y
⊢ P (csup c) ∨ Q (csup c)

Tactic:
right

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 c)

Proof state:
case intro.intro.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
hyx : y ⊑ x
⊢ Q x

Tactic:
cases h x hcx with
| inl hPx => exfalso; apply hx x hcx rel_refl hPx
| inr hQx => assumption

Result:
no goals

Proof state:
case intro.intro.inr.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
hyx : y ⊑ x
hPx : P x
⊢ False

Tactic:
apply hx x hcx rel_refl hPx

Result:
no goals

Proof state:
case intro.intro.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
hyx : y ⊑ x
⊢ ∃ y_1, c y_1 ∧ y ⊑ y_1 ∧ Q y_1

Tactic:
refine ⟨x, hcx, hyx , ?_⟩

Result:
case intro.intro.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
hyx : y ⊑ 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
⊢ ∀ (x : α), c x ∧ P x → P x

Tactic:
intro x ⟨hcx, hPx⟩

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
x : α
hcx : c x
hPx : P x
⊢ P x

Proof state:
case 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
hP : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ P (csup c) ∨ Q (csup c)

Tactic:
left

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 c)