no goals
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
l : List α
⊢ Chain' R ([] ++ l) ↔ Chain' R [] ∧ Chain' R l ∧ ∀ (x : α), x ∈ getLast? [] → ∀ (y : α), y ∈ head? l → R x y
simp
no goals
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b a : α
l : List α
⊢ Chain' R ([a] ++ l) ↔ Chain' R [a] ∧ Chain' R l ∧ ∀ (x : α), x ∈ getLast? [a] → ∀ (y : α), y ∈ head? l → R x y
simp [chain'_cons', and_comm]
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a✝ b✝ a b : α
l₁ l₂ : List α
⊢ (R a b ∧ Chain' R (b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ getLast? (b :: l₁) → ∀ (y : α), y ∈ head? l₂ → R x y) ↔
    R a b ∧ Chain' R (b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ getLast? (a :: b :: l₁) → ∀ (y : α), y ∈ head? l₂ → R x y
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a✝ b✝ a b : α
l₁ l₂ : List α
⊢ Chain' R (a :: b :: l₁ ++ l₂) ↔
    Chain' R (a :: b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ getLast? (a :: b :: l₁) → ∀ (y : α), y ∈ head? l₂ → R x y
rw [cons_append, cons_append, chain'_cons, chain'_cons, ← cons_append, chain'_append,
  and_assoc]
no goals
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a✝ b✝ a b : α
l₁ l₂ : List α
⊢ (R a b ∧ Chain' R (b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ getLast? (b :: l₁) → ∀ (y : α), y ∈ head? l₂ → R x y) ↔
    R a b ∧ Chain' R (b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ getLast? (a :: b :: l₁) → ∀ (y : α), y ∈ head? l₂ → R x y
simp