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

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

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

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

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

Tactic:
exact h.2

Result:
no goals

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

Tactic:
right

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

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

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
b₁ b₂ : β
a₁ : α
h₁ : c ⟨a₁, b₁⟩
a₂ : α
h₂ : c ⟨a₂, b₂⟩
h✝ : ⟨a₁, b₁⟩ ⊑ ⟨a₂, b₂⟩
⊢ b₁ ⊑ b₂ ∨ b₂ ⊑ b₁

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

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

Tactic:
exact h.2

Result:
no goals

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

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

Result:
no goals

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

Tactic:
left

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

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

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

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

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