α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
L : List (List (Sigma β))
⊢ (∀ (l : List (Sigma β)), l ∈ L → Pairwise (fun s s' => s.fst ≠ s'.fst) l) ∧
      Pairwise (fun l₁ l₂ => ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) L ↔
    (∀ (l : List (Sigma β)), l ∈ L → NodupKeys l) ∧ Pairwise (fun a b => Disjoint (keys a) (keys b)) L
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
L : List (List (Sigma β))
⊢ NodupKeys (join L) ↔ (∀ (l : List (Sigma β)), l ∈ L → NodupKeys l) ∧ Pairwise Disjoint (map keys L)
rw [nodupKeys_iff_pairwise, pairwise_join, pairwise_map]
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
L : List (List (Sigma β))
⊢ Pairwise (fun l₁ l₂ => ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) L ↔
    Pairwise (fun a b => Disjoint (keys a) (keys b)) L
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
L : List (List (Sigma β))
⊢ (∀ (l : List (Sigma β)), l ∈ L → Pairwise (fun s s' => s.fst ≠ s'.fst) l) ∧
      Pairwise (fun l₁ l₂ => ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) L ↔
    (∀ (l : List (Sigma β)), l ∈ L → NodupKeys l) ∧ Pairwise (fun a b => Disjoint (keys a) (keys b)) L
refine' and_congr (ball_congr fun l _ => by simp [nodupKeys_iff_pairwise]) _
case a
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
L : List (List (Sigma β))
⊢ Pairwise (fun l₁ l₂ => ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) L =
    Pairwise (fun a b => Disjoint (keys a) (keys b)) L
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
L : List (List (Sigma β))
⊢ Pairwise (fun l₁ l₂ => ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) L ↔
    Pairwise (fun a b => Disjoint (keys a) (keys b)) L
apply iff_of_eq
case a.e_R.h.h.a
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
L : List (List (Sigma β))
l₁ l₂ : List (Sigma β)
⊢ (∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) ↔ Disjoint (keys l₁) (keys l₂)
case a
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
L : List (List (Sigma β))
⊢ Pairwise (fun l₁ l₂ => ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) L =
    Pairwise (fun a b => Disjoint (keys a) (keys b)) L
congr with (l₁ l₂)
no goals
case a.e_R.h.h.a
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
L : List (List (Sigma β))
l₁ l₂ : List (Sigma β)
⊢ (∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) ↔ Disjoint (keys l₁) (keys l₂)
simp [keys, disjoint_iff_ne]
no goals
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
L : List (List (Sigma β))
l : List (Sigma β)
x✝ : l ∈ L
⊢ Pairwise (fun s s' => s.fst ≠ s'.fst) l ↔ NodupKeys l
simp [nodupKeys_iff_pairwise]