-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem PProd.chain.chain_fst [CCPO α] [CCPO β] {c : α ×' β → Prop} (hchain : chain c) :
    chain (chain.fst c)

Proof state:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
⊢ chain (fst c)

Tactic:
intro a₁ a₂ ⟨b₁, h₁⟩ ⟨b₂, h₂⟩

Result:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
a₁ a₂ : α
b₁ : β
h₁ : c ⟨a₁, b₁⟩
b₂ : β
h₂ : c ⟨a₂, b₂⟩
⊢ a₁ ⊑ a₂ ∨ a₂ ⊑ a₁

Proof state:
case inl
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
a₁ a₂ : α
b₁ : β
h₁ : c ⟨a₁, b₁⟩
b₂ : β
h₂ : c ⟨a₂, b₂⟩
h✝ : ⟨a₁, b₁⟩ ⊑ ⟨a₂, b₂⟩
⊢ a₁ ⊑ a₂ ∨ a₂ ⊑ a₁

case inr
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
a₁ a₂ : α
b₁ : β
h₁ : c ⟨a₁, b₁⟩
b₂ : β
h₂ : c ⟨a₂, b₂⟩
h✝ : ⟨a₂, b₂⟩ ⊑ ⟨a₁, b₁⟩
⊢ a₁ ⊑ a₂ ∨ a₂ ⊑ a₁

Tactic:
case inl h => left; exact h.1

Result:
case inr
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
a₁ a₂ : α
b₁ : β
h₁ : c ⟨a₁, b₁⟩
b₂ : β
h₂ : c ⟨a₂, b₂⟩
h✝ : ⟨a₂, b₂⟩ ⊑ ⟨a₁, b₁⟩
⊢ a₁ ⊑ a₂ ∨ a₂ ⊑ a₁

Proof state:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
a₁ a₂ : α
b₁ : β
h₁ : c ⟨a₁, b₁⟩
b₂ : β
h₂ : c ⟨a₂, b₂⟩
⊢ a₁ ⊑ a₂ ∨ a₂ ⊑ a₁

Tactic:
cases hchain ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h₁ h₂

Result:
case inl
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
a₁ a₂ : α
b₁ : β
h₁ : c ⟨a₁, b₁⟩
b₂ : β
h₂ : c ⟨a₂, b₂⟩
h✝ : ⟨a₁, b₁⟩ ⊑ ⟨a₂, b₂⟩
⊢ a₁ ⊑ a₂ ∨ a₂ ⊑ a₁

case inr
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
a₁ a₂ : α
b₁ : β
h₁ : c ⟨a₁, b₁⟩
b₂ : β
h₂ : c ⟨a₂, b₂⟩
h✝ : ⟨a₂, b₂⟩ ⊑ ⟨a₁, b₁⟩
⊢ a₁ ⊑ a₂ ∨ a₂ ⊑ a₁

Proof state:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
a₁ a₂ : α
b₁ : β
h₁ : c ⟨a₁, b₁⟩
b₂ : β
h₂ : c ⟨a₂, b₂⟩
h : ⟨a₁, b₁⟩ ⊑ ⟨a₂, b₂⟩
⊢ a₁ ⊑ a₂ ∨ a₂ ⊑ a₁

Tactic:
left

Result:
case h
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
a₁ a₂ : α
b₁ : β
h₁ : c ⟨a₁, b₁⟩
b₂ : β
h₂ : c ⟨a₂, b₂⟩
h : ⟨a₁, b₁⟩ ⊑ ⟨a₂, b₂⟩
⊢ a₁ ⊑ a₂

Proof state:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
a₁ a₂ : α
b₁ : β
h₁ : c ⟨a₁, b₁⟩
b₂ : β
h₂ : c ⟨a₂, b₂⟩
h : ⟨a₂, b₂⟩ ⊑ ⟨a₁, b₁⟩
⊢ a₁ ⊑ a₂ ∨ a₂ ⊑ a₁

Tactic:
right

Result:
case h
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
a₁ a₂ : α
b₁ : β
h₁ : c ⟨a₁, b₁⟩
b₂ : β
h₂ : c ⟨a₂, b₂⟩
h : ⟨a₂, b₂⟩ ⊑ ⟨a₁, b₁⟩
⊢ a₂ ⊑ a₁

Proof state:
case h
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
a₁ a₂ : α
b₁ : β
h₁ : c ⟨a₁, b₁⟩
b₂ : β
h₂ : c ⟨a₂, b₂⟩
h : ⟨a₁, b₁⟩ ⊑ ⟨a₂, b₂⟩
⊢ a₁ ⊑ a₂

Tactic:
exact h.1

Result:
no goals

Proof state:
case inr
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
a₁ a₂ : α
b₁ : β
h₁ : c ⟨a₁, b₁⟩
b₂ : β
h₂ : c ⟨a₂, b₂⟩
h✝ : ⟨a₂, b₂⟩ ⊑ ⟨a₁, b₁⟩
⊢ a₁ ⊑ a₂ ∨ a₂ ⊑ a₁

Tactic:
case inr h => right; exact h.1

Result:
no goals

Proof state:
case h
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
c : α ×' β → Prop
hchain : chain c
a₁ a₂ : α
b₁ : β
h₁ : c ⟨a₁, b₁⟩
b₂ : β
h₂ : c ⟨a₂, b₂⟩
h : ⟨a₂, b₂⟩ ⊑ ⟨a₁, b₁⟩
⊢ a₂ ⊑ a₁

Tactic:
exact h.1

Result:
no goals