α : Type u_1
β : Type ?u.9493
R S T : α → α → Prop
a : α
l : List α
s : Symmetric R
l₁ l₂ : List α
this :
  ∀ (l₁ l₂ : List α), (∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) → ∀ (x : α), x ∈ l₂ → ∀ (y : α), y ∈ l₁ → R x y
⊢ Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁)
α : Type u_1
β : Type ?u.9493
R S T : α → α → Prop
a : α
l : List α
s : Symmetric R
l₁ l₂ : List α
⊢ Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁)
have : ∀ l₁ l₂ : List α, (∀ x : α, x ∈ l₁ → ∀ y : α, y ∈ l₂ → R x y) →
  ∀ x : α, x ∈ l₂ → ∀ y : α, y ∈ l₁ → R x y := fun l₁ l₂ a x xm y ym ↦ s (a y ym x xm)
α : Type u_1
β : Type ?u.9493
R S T : α → α → Prop
a : α
l : List α
s : Symmetric R
l₁ l₂ : List α
this :
  ∀ (l₁ l₂ : List α), (∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) → ∀ (x : α), x ∈ l₂ → ∀ (y : α), y ∈ l₁ → R x y
⊢ (Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → R a b) ↔
    Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₂ → ∀ (b : α), b ∈ l₁ → R a b
α : Type u_1
β : Type ?u.9493
R S T : α → α → Prop
a : α
l : List α
s : Symmetric R
l₁ l₂ : List α
this :
  ∀ (l₁ l₂ : List α), (∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) → ∀ (x : α), x ∈ l₂ → ∀ (y : α), y ∈ l₁ → R x y
⊢ Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁)
simp only [pairwise_append, and_left_comm]
no goals
α : Type u_1
β : Type ?u.9493
R S T : α → α → Prop
a : α
l : List α
s : Symmetric R
l₁ l₂ : List α
this :
  ∀ (l₁ l₂ : List α), (∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) → ∀ (x : α), x ∈ l₂ → ∀ (y : α), y ∈ l₁ → R x y
⊢ (Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → R a b) ↔
    Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₂ → ∀ (b : α), b ∈ l₁ → R a b
rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]