α : Type u_1
β : Type ?u.8026
γ : Type ?u.8029
ι : Type ?u.8032
ι' : Type ?u.8035
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
⊢ (((∀ (x : α), x ∈ s → ∀ (x_1 : α), x_1 ∈ s → x ≠ x_1 → r x x_1) ∧
        ∀ (x : α), x ∈ t → ∀ (x_1 : α), x_1 ∈ s → x ≠ x_1 → r x x_1) ∧
      (∀ (x : α), x ∈ s → ∀ (x_1 : α), x_1 ∈ t → x ≠ x_1 → r x x_1) ∧
        ∀ (x : α), x ∈ t → ∀ (x_1 : α), x_1 ∈ t → x ≠ x_1 → r x x_1) ↔
    (∀ (x : α), x ∈ s → ∀ (x_1 : α), x_1 ∈ s → x ≠ x_1 → r x x_1) ∧
      (∀ (x : α), x ∈ t → ∀ (x_1 : α), x_1 ∈ t → x ≠ x_1 → r x x_1) ∧
        (∀ (x : α), x ∈ s → ∀ (x_1 : α), x_1 ∈ t → x ≠ x_1 → r x x_1) ∧
          ∀ (x : α), x ∈ s → ∀ (x_2 : α), x_2 ∈ t → x ≠ x_2 → r x_2 x
α : Type u_1
β : Type ?u.8026
γ : Type ?u.8029
ι : Type ?u.8032
ι' : Type ?u.8035
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
⊢ Set.Pairwise (s ∪ t) r ↔
    Set.Pairwise s r ∧ Set.Pairwise t r ∧ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b → r a b ∧ r b a
simp only [Set.Pairwise, mem_union, or_imp, forall_and]
no goals
α : Type u_1
β : Type ?u.8026
γ : Type ?u.8029
ι : Type ?u.8032
ι' : Type ?u.8035
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
⊢ (((∀ (x : α), x ∈ s → ∀ (x_1 : α), x_1 ∈ s → x ≠ x_1 → r x x_1) ∧
        ∀ (x : α), x ∈ t → ∀ (x_1 : α), x_1 ∈ s → x ≠ x_1 → r x x_1) ∧
      (∀ (x : α), x ∈ s → ∀ (x_1 : α), x_1 ∈ t → x ≠ x_1 → r x x_1) ∧
        ∀ (x : α), x ∈ t → ∀ (x_1 : α), x_1 ∈ t → x ≠ x_1 → r x x_1) ↔
    (∀ (x : α), x ∈ s → ∀ (x_1 : α), x_1 ∈ s → x ≠ x_1 → r x x_1) ∧
      (∀ (x : α), x ∈ t → ∀ (x_1 : α), x_1 ∈ t → x ≠ x_1 → r x x_1) ∧
        (∀ (x : α), x ∈ s → ∀ (x_1 : α), x_1 ∈ t → x ≠ x_1 → r x x_1) ∧
          ∀ (x : α), x ∈ s → ∀ (x_2 : α), x_2 ∈ t → x ≠ x_2 → r x_2 x
exact
  ⟨fun H => ⟨H.1.1, H.2.2, H.2.1, fun x hx y hy hne => H.1.2 y hy x hx hne.symm⟩, fun H =>
    ⟨⟨H.1, fun x hx y hy hne => H.2.2.2 y hy x hx hne.symm⟩, H.2.2.1, H.2.1⟩⟩