case nil
α : Type u_1
β : Type ?u.29811
R S T : α → α → Prop
a : α
l : List α
⊢ Pairwise R (join []) ↔
    (∀ (l : List α), l ∈ [] → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) []

case cons
α : Type u_1
β : Type ?u.29811
R S T : α → α → Prop
a : α
l✝ l : List α
L : List (List α)
IH :
  Pairwise R (join L) ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
⊢ Pairwise R (join (l :: L)) ↔
    (∀ (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)
α : Type u_1
β : Type ?u.29811
R S T : α → α → Prop
a : α
l : List α
L : List (List α)
⊢ Pairwise R (join L) ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
induction' L with l L IH
case cons
α : Type u_1
β : Type ?u.29811
R S T : α → α → Prop
a : α
l✝ l : List α
L : List (List α)
IH :
  Pairwise R (join L) ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
this :
  (∀ (x : α), x ∈ l → ∀ (y : α) (x_1 : List α), x_1 ∈ L → y ∈ x_1 → R x y) ↔
    ∀ (a' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y
⊢ Pairwise R (join (l :: L)) ↔
    (∀ (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)
case cons
α : Type u_1
β : Type ?u.29811
R S T : α → α → Prop
a : α
l✝ l : List α
L : List (List α)
IH :
  Pairwise R (join L) ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
⊢ Pairwise R (join (l :: L)) ↔
    (∀ (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)
have :
  (∀ x : α, x ∈ l → ∀ (y : α) (x_1 : List α), x_1 ∈ L → y ∈ x_1 → R x y) ↔
    ∀ a' : List α, a' ∈ L → ∀ x : α, x ∈ l → ∀ y : α, y ∈ a' → R x y :=
  ⟨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⟩
case cons
α : Type u_1
β : Type ?u.29811
R S T : α → α → Prop
a : α
l✝ l : List α
L : List (List α)
IH :
  Pairwise R (join L) ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
this :
  (∀ (x : α), x ∈ l → ∀ (y : α) (x_1 : List α), x_1 ∈ L → y ∈ x_1 → R x y) ↔
    ∀ (a' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y
⊢ (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' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y) ↔
    (Pairwise R l ∧ ∀ (l : List α), l ∈ L → Pairwise R l) ∧
      (∀ (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
case cons
α : Type u_1
β : Type ?u.29811
R S T : α → α → Prop
a : α
l✝ l : List α
L : List (List α)
IH :
  Pairwise R (join L) ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
this :
  (∀ (x : α), x ∈ l → ∀ (y : α) (x_1 : List α), x_1 ∈ L → y ∈ x_1 → R x y) ↔
    ∀ (a' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y
⊢ Pairwise R (join (l :: L)) ↔
    (∀ (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)
simp only [join, pairwise_append, IH, mem_join, exists_imp, and_imp, this, forall_mem_cons,
  pairwise_cons]
no goals
case cons
α : Type u_1
β : Type ?u.29811
R S T : α → α → Prop
a : α
l✝ l : List α
L : List (List α)
IH :
  Pairwise R (join L) ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
this :
  (∀ (x : α), x ∈ l → ∀ (y : α) (x_1 : List α), x_1 ∈ L → y ∈ x_1 → R x y) ↔
    ∀ (a' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y
⊢ (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' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y) ↔
    (Pairwise R l ∧ ∀ (l : List α), l ∈ L → Pairwise R l) ∧
      (∀ (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
simp only [and_assoc, and_comm, and_left_comm]
no goals
case nil
α : Type u_1
β : Type ?u.29811
R S T : α → α → Prop
a : α
l : List α
⊢ Pairwise R (join []) ↔
    (∀ (l : List α), l ∈ [] → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) []
simp only [join, Pairwise.nil, forall_prop_of_false (not_mem_nil _), forall_const, and_self_iff]