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

State before:
α : Type u
r : α → α → Prop
β : α → Type v
x y : KVChain r β
xs : List (Sigma β)
xascend : List.Ascending (Sigma.relOnFst r) xs
ys : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) ys
h : { toList := xs, ascend := xascend }.toList = { toList := ys, ascend := ascend✝ }.toList
⊢ { toList := xs, ascend := xascend } = { toList := ys, ascend := ascend✝ }
Tactic:
cases h
State after:
case refl
α : Type u
r : α → α → Prop
β : α → Type v
x y : KVChain r β
xs : List (Sigma β)
xascend ascend✝ : List.Ascending (Sigma.relOnFst r) xs
⊢ { toList := xs, ascend := xascend } = { toList := xs, ascend := ascend✝ }

State before:
case refl
α : Type u
r : α → α → Prop
β : α → Type v
x y : KVChain r β
xs : List (Sigma β)
xascend ascend✝ : List.Ascending (Sigma.relOnFst r) xs
⊢ { toList := xs, ascend := xascend } = { toList := xs, ascend := ascend✝ }
Tactic:
rw [proofIrrel xascend _]
State after:
no goals