-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_flatten {L : List (List α)} :
    Pairwise R (flatten L) ↔
      (∀ l ∈ L, Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, R x y) L

Proof state:
case cons
α : Type u_1
R : α → α → Prop
l : List α
L : List (List α)
IH :
  Pairwise R L.flatten ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
⊢ Pairwise R (l :: L).flatten ↔
    (∀ (l_1 : List α), l_1 ∈ l :: L → Pairwise R l_1) ∧
      Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) (l :: L)

Tactic:
simp only [flatten, pairwise_append, IH, mem_flatten, exists_imp, and_imp, forall_mem_cons,
  pairwise_cons, and_assoc, and_congr_right_iff]

Result:
case cons
α : Type u_1
R : α → α → Prop
l : List α
L : List (List α)
IH :
  Pairwise R L.flatten ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
⊢ Pairwise R l →
    (∀ (l : List α), l ∈ L → Pairwise R l) →
      ((Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L ∧
          ∀ (a : α), a ∈ l → ∀ (b : α) (x : List α), x ∈ L → b ∈ x → R a b) ↔
        (∀ (a' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y) ∧
          Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L)

Proof state:
α : Type u_1
R : α → α → Prop
L : List (List α)
⊢ Pairwise R L.flatten ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L

Tactic:
induction L with
| nil => simp
| cons l L IH =>
  simp only [flatten, pairwise_append, IH, mem_flatten, exists_imp, and_imp, forall_mem_cons,
    pairwise_cons, and_assoc, and_congr_right_iff]
  rw [and_comm, and_congr_left_iff]
  intros; exact ⟨fun h a b c d e => h c d e a b, fun h c d e a b => h a b c d e⟩

Result:
no goals

Proof state:
case cons
α : Type u_1
R : α → α → Prop
l : List α
L : List (List α)
IH :
  Pairwise R L.flatten ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
⊢ Pairwise R l →
    (∀ (l : List α), l ∈ L → Pairwise R l) →
      ((Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L ∧
          ∀ (a : α), a ∈ l → ∀ (b : α) (x : List α), x ∈ L → b ∈ x → R a b) ↔
        (∀ (a' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y) ∧
          Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L)

Tactic:
rw [and_comm, and_congr_left_iff]

Result:
case cons
α : Type u_1
R : α → α → Prop
l : List α
L : List (List α)
IH :
  Pairwise R L.flatten ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
⊢ Pairwise R l →
    (∀ (l : List α), l ∈ L → Pairwise R l) →
      Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L →
        ((∀ (a : α), a ∈ l → ∀ (b : α) (x : List α), x ∈ L → b ∈ x → R a b) ↔
          ∀ (a' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y)

Proof state:
case nil
α : Type u_1
R : α → α → Prop
⊢ Pairwise R [].flatten ↔
    (∀ (l : List α), l ∈ [] → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
R : α → α → Prop
l : List α
L : List (List α)
IH :
  Pairwise R L.flatten ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
a✝² : Pairwise R l
a✝¹ : ∀ (l : List α), l ∈ L → Pairwise R l
a✝ : Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
⊢ (∀ (a : α), a ∈ l → ∀ (b : α) (x : List α), x ∈ L → b ∈ x → R a b) ↔
    ∀ (a' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y

Tactic:
exact ⟨fun h a b c d e => h c d e a b, fun h c d e a b => h a b c d e⟩

Result:
no goals

Proof state:
case cons
α : Type u_1
R : α → α → Prop
l : List α
L : List (List α)
IH :
  Pairwise R L.flatten ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
⊢ Pairwise R l →
    (∀ (l : List α), l ∈ L → Pairwise R l) →
      Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L →
        ((∀ (a : α), a ∈ l → ∀ (b : α) (x : List α), x ∈ L → b ∈ x → R a b) ↔
          ∀ (a' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y)

Tactic:
intros

Result:
case cons
α : Type u_1
R : α → α → Prop
l : List α
L : List (List α)
IH :
  Pairwise R L.flatten ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
a✝² : Pairwise R l
a✝¹ : ∀ (l : List α), l ∈ L → Pairwise R l
a✝ : Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
⊢ (∀ (a : α), a ∈ l → ∀ (b : α) (x : List α), x ∈ L → b ∈ x → R a b) ↔
    ∀ (a' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y