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

State before:
α : Type u
r : α → α → Prop
β : α → Type v
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hay : boundLeft a ys
⊢ hingeable xs (KVChain.cons a b ys hay) = boundLeft a xs
Tactic:
unfold hingeable
State after:
α : Type u
r : α → α → Prop
β : α → Type v
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hay : boundLeft a ys
⊢ List.relHead (Sigma.relOnFst r) xs.toList (KVChain.cons a b ys hay).toList = boundLeft a xs

State before:
α : Type u
r : α → α → Prop
β : α → Type v
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hay : boundLeft a ys
⊢ List.relHead (Sigma.relOnFst r) xs.toList (KVChain.cons a b ys hay).toList = boundLeft a xs
Tactic:
rw [List.relHead_cons_right]
State after:
α : Type u
r : α → α → Prop
β : α → Type v
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hay : boundLeft a ys
⊢ List.predHead (fun a_1 => Sigma.relOnFst r a_1 { fst := a, snd := b }) xs.toList = boundLeft a xs

State before:
α : Type u
r : α → α → Prop
β : α → Type v
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hay : boundLeft a ys
⊢ List.predHead (fun a_1 => Sigma.relOnFst r a_1 { fst := a, snd := b }) xs.toList = boundLeft a xs
Tactic:
rfl
State after:
no goals