-- Mathlib/Data/List/Chain.lean
lemma chain'_flatten : ∀ {L : List (List α)}, [] ∉ L →
    (Chain' R L.flatten ↔ (∀ l ∈ L, Chain' R l) ∧
    L.Chain' (fun l₁ l₂ => ∀ᵉ (x ∈ l₁.getLast?) (y ∈ l₂.head?), R x y))
| [], _ => by simp
| [l], _ => by simp [flatten]
| (l₁ :: l₂ :: L), hL => by
    rw [mem_cons, not_or, ← Ne] at hL
    rw [flatten, chain'_append, chain'_flatten hL.2, forall_mem_cons, chain'_cons]
    rw [mem_cons, not_or, ← Ne] at hL
    simp only [forall_mem_cons, and_assoc, flatten, head?_append_of_ne_nil _ hL.2.1.symm]
    exact Iff.rfl.and (Iff.rfl.and <| Iff.rfl.and and_comm)

Proof state:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ (Chain' R l₁ ∧
      ((Chain' R l₂ ∧ ∀ (x : List α), x ∈ L → Chain' R x) ∧
          Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧
      (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
        Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)

Tactic:
rw [mem_cons, not_or, ← Ne] at hL

Result:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L
⊢ (Chain' R l₁ ∧
      ((Chain' R l₂ ∧ ∀ (x : List α), x ∈ L → Chain' R x) ∧
          Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧
      (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
        Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)

Proof state:
α : Type u
R : α → α → Prop
l : List α
x✝ : ¬[] ∈ [l]
⊢ Chain' R [l].flatten ↔
    (∀ (l_1 : List α), l_1 ∈ [l] → Chain' R l_1) ∧
      Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) [l]

Tactic:
simp [flatten]

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
x✝ : ¬[] ∈ []
⊢ Chain' R [].flatten ↔
    (∀ (l : List α), l ∈ [] → Chain' R l) ∧
      Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : ¬[] ∈ l₁ :: l₂ :: L
⊢ Chain' R (l₁ :: l₂ :: L).flatten ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧
      Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)

Tactic:
rw [mem_cons, not_or, ← Ne] at hL

Result:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ Chain' R (l₁ :: l₂ :: L).flatten ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧
      Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)

Proof state:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L
⊢ (Chain' R l₁ ∧
      ((Chain' R l₂ ∧ ∀ (x : List α), x ∈ L → Chain' R x) ∧
          Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧
      (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
        Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)

Tactic:
simp only [forall_mem_cons, and_assoc, flatten, head?_append_of_ne_nil _ hL.2.1.symm]

Result:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L
⊢ (Chain' R l₁ ∧
      Chain' R l₂ ∧
        (∀ (x : List α), x ∈ L → Chain' R x) ∧
          Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L) ∧
            ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
    Chain' R l₁ ∧
      Chain' R l₂ ∧
        (∀ (x : List α), x ∈ L → Chain' R x) ∧
          (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
            Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)

Proof state:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L
⊢ (Chain' R l₁ ∧
      Chain' R l₂ ∧
        (∀ (x : List α), x ∈ L → Chain' R x) ∧
          Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L) ∧
            ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
    Chain' R l₁ ∧
      Chain' R l₂ ∧
        (∀ (x : List α), x ∈ L → Chain' R x) ∧
          (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
            Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)

Tactic:
exact Iff.rfl.and (Iff.rfl.and <| Iff.rfl.and and_comm)

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ Chain' R (l₁ :: l₂ :: L).flatten ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧
      Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)

Tactic:
rw [flatten, chain'_append, chain'_flatten hL.2, forall_mem_cons, chain'_cons]

Result:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ (Chain' R l₁ ∧
      ((Chain' R l₂ ∧ ∀ (x : List α), x ∈ L → Chain' R x) ∧
          Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧
      (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
        Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)