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

State before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ hingeable (KVChain.cons a₁ x✝³ x✝² x✝¹) (KVChain.cons a b ys hays) → hingeable (KVChain.cons a₁ x✝³ x✝² x✝¹) ys
Tactic:
rw [cons_hingeable, cons_hingeable]
State after:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ boundLeft a₁ (KVChain.cons a b ys hays) → boundLeft a₁ ys

State before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ boundLeft a₁ (KVChain.cons a b ys hays) → boundLeft a₁ ys
Tactic:
dsimp [boundLeft, List.predHead]
State after:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ r a₁ a →
    match ys.toList with
    | [] => True
    | a :: tail => r a₁ a.fst

State before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ r a₁ a →
    match ys.toList with
    | [] => True
    | a :: tail => r a₁ a.fst
Tactic:
dsimp [boundLeft, List.predHead] at hays
State after:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ r a₁ a →
    match ys.toList with
    | [] => True
    | a :: tail => r a₁ a.fst

State before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ r a₁ a →
    match ys.toList with
    | [] => True
    | a :: tail => r a₁ a.fst
Tactic:
cases hys : ys.toList
State after:
case nil
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
hys : ys.toList = []
⊢ r a₁ a →
    match [] with
    | [] => True
    | a :: tail => r a₁ a.fst

case cons
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hys : ys.toList = head✝ :: tail✝
⊢ r a₁ a →
    match head✝ :: tail✝ with
    | [] => True
    | a :: tail => r a₁ a.fst

State before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
hys : ys.toList = []
⊢ r a₁ a →
    match [] with
    | [] => True
    | a :: tail => r a₁ a.fst
Tactic:
case nil => intros; exact True.intro
State after:
no goals

State before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hys : ys.toList = head✝ :: tail✝
⊢ r a₁ a →
    match head✝ :: tail✝ with
    | [] => True
    | a :: tail => r a₁ a.fst
Tactic:
case cons => intro h; rw [hys] at hays; exact trans (t:=r) h hays
State after:
no goals

State before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
hys : ys.toList = []
⊢ r a₁ a →
    match [] with
    | [] => True
    | a :: tail => r a₁ a.fst
Tactic:
intros
State after:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
hys : ys.toList = []
a✝ : r a₁ a
⊢ match [] with
  | [] => True
  | a :: tail => r a₁ a.fst

State before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
hys : ys.toList = []
a✝ : r a₁ a
⊢ match [] with
  | [] => True
  | a :: tail => r a₁ a.fst
Tactic:
exact True.intro
State after:
no goals

State before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hys : ys.toList = head✝ :: tail✝
⊢ r a₁ a →
    match head✝ :: tail✝ with
    | [] => True
    | a :: tail => r a₁ a.fst
Tactic:
intro h
State after:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hys : ys.toList = head✝ :: tail✝
h : r a₁ a
⊢ match head✝ :: tail✝ with
  | [] => True
  | a :: tail => r a₁ a.fst

State before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hys : ys.toList = head✝ :: tail✝
h : r a₁ a
⊢ match head✝ :: tail✝ with
  | [] => True
  | a :: tail => r a₁ a.fst
Tactic:
rw [hys] at hays
State after:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays✝ :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays✝) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hays :
  match head✝ :: tail✝ with
  | [] => True
  | a_1 :: tail => r a a_1.fst
hys : ys.toList = head✝ :: tail✝
h : r a₁ a
⊢ match head✝ :: tail✝ with
  | [] => True
  | a :: tail => r a₁ a.fst

State before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays✝ :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays✝) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hays :
  match head✝ :: tail✝ with
  | [] => True
  | a_1 :: tail => r a a_1.fst
hys : ys.toList = head✝ :: tail✝
h : r a₁ a
⊢ match head✝ :: tail✝ with
  | [] => True
  | a :: tail => r a₁ a.fst
Tactic:
exact trans (t:=r) h hays
State after:
no goals