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

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

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

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