Theorem: KVChain.rklex_not_nil_right (Algdata/Data/KVChain/Basic.lean)

State before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
xs : KVChain r β
hcontra : KVChain.rklex s xs KVChain.nil
⊢ False
Tactic:
cases xs
State after:
case mk
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
hcontra : KVChain.rklex s { toList := toList✝, ascend := ascend✝ } KVChain.nil
⊢ False

State before:
case mk
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
hcontra : KVChain.rklex s { toList := toList✝, ascend := ascend✝ } KVChain.nil
⊢ False
Tactic:
cases hcontra
State after:
no goals