/-
Copyright (c) 2021 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies

! This file was ported from Lean 3 source module data.finset.pairwise
! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finset.Lattice

/-!
# Relations holding pairwise on finite sets

In this file we prove a few results about the interaction of `Set.PairwiseDisjoint` and `Finset`,
as well as the interaction of `List.Pairwise Disjoint` and the condition of
`Disjoint` on `List.toFinset`, in `Set` form.
-/


open Finset

variable {α: Type ?u.2
α ι: Type ?u.3870
ι ι': Type ?u.8
ι' : Type _: Type (?u.3546+1)
Type _}

instance: {α : Type u_1} →
  [inst : DecidableEq α] →
    {r : α → α → Prop} → [inst : DecidableRel r] → {s : Finset α} → Decidable (Set.Pairwise (↑s) r)
instance [DecidableEq: Sort ?u.20 → Sort (max1?u.20)
DecidableEq α: Type ?u.11
α] {r: α → α → Prop
r : α: Type ?u.11
α → α: Type ?u.11
α → Prop: Type
Prop} [DecidableRel: {α : Sort ?u.35} → (α → α → Prop) → Sort (max1?u.35)
DecidableRel r: α → α → Prop
r] {s: Finset α
s : Finset: Type ?u.51 → Type ?u.51
Finset α: Type ?u.11
α} :
    Decidable: Prop → Type
Decidable ((s: Finset α
s : Set: Type ?u.55 → Type ?u.55
Set α: Type ?u.11
α).Pairwise: {α : Type ?u.157} → Set α → (α → α → Prop) → Prop
Pairwise r: α → α → Prop
r) :=
  decidable_of_iff': {a : Prop} → (b : Prop) → (a ↔ b) → [inst : Decidable b] → Decidable a
decidable_of_iff' (∀ a: ?m.180
a ∈ s: Finset α
s, ∀ b: ?m.213
b ∈ s: Finset α
s, a: ?m.180
a ≠ b: ?m.213
b → r: α → α → Prop
r a: ?m.180
a b: ?m.213
b) Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl

theorem Finset.pairwiseDisjoint_range_singleton: ∀ {α : Type u_1}, Set.PairwiseDisjoint (Set.range singleton) id
Finset.pairwiseDisjoint_range_singleton :
    (Set.range: {α : Type ?u.1024} → {ι : Sort ?u.1023} → (ι → α) → Set α
Set.range (singleton: {α : outParam (Type ?u.1032)} → {β : Type ?u.1031} → [self : Singleton α β] → α → β
singleton : α: Type ?u.1014
α → Finset: Type ?u.1030 → Type ?u.1030
Finset α: Type ?u.1014
α)).PairwiseDisjoint: {α : Type ?u.1062} → {ι : Type ?u.1061} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → Prop
PairwiseDisjoint id: {α : Sort ?u.1145} → α → α
id := by
Goals accomplished! 🐙
  α: Type u_1

ι: Type ?u.1017

ι': Type ?u.1020

Set.PairwiseDisjoint (Set.range singleton) idrintro _: Finset α
_ ⟨a, rfl⟩: x✝ ∈ Set.range singleton
⟨a: α
a⟨a, rfl⟩: x✝ ∈ Set.range singleton
, rfl: {a} = x✝
rfl⟨a, rfl⟩: x✝ ∈ Set.range singleton
⟩ _: Finset α
_ ⟨b, rfl⟩: y✝ ∈ Set.range singleton
⟨b: α
b⟨b, rfl⟩: y✝ ∈ Set.range singleton
, rfl: {b} = y✝
rfl⟨b, rfl⟩: y✝ ∈ Set.range singleton
⟩ h: {a} ≠ {b}
hα: Type u_1

ι: Type ?u.1017

ι': Type ?u.1020

a, b: α

h: {a} ≠ {b}

intro.intro(Disjoint on id) {a} {b}
  α: Type u_1

ι: Type ?u.1017

ι': Type ?u.1020

Set.PairwiseDisjoint (Set.range singleton) idexact disjoint_singleton: ∀ {α : Type ?u.1270} {a b : α}, Disjoint {a} {b} ↔ a ≠ b
disjoint_singleton.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 (ne_of_apply_ne: ∀ {α : Sort ?u.1296} {β : Sort ?u.1297} (f : α → β) {x y : α}, f x ≠ f y → x ≠ y
ne_of_apply_ne _: ?m.1298 → ?m.1299
_ h: {a} ≠ {b}
h)
Goals accomplished! 🐙
#align finset.pairwise_disjoint_range_singleton Finset.pairwiseDisjoint_range_singleton: ∀ {α : Type u_1}, Set.PairwiseDisjoint (Set.range singleton) id
Finset.pairwiseDisjoint_range_singleton

namespace Set

theorem PairwiseDisjoint.elim_finset: ∀ {s : Set ι} {f : ι → Finset α},
  PairwiseDisjoint s f → ∀ {i j : ι}, i ∈ s → j ∈ s → ∀ (a : α), a ∈ f i → a ∈ f j → i = j
PairwiseDisjoint.elim_finset {s: Set ι
s : Set: Type ?u.1347 → Type ?u.1347
Set ι: Type ?u.1341
ι} {f: ι → Finset α
f : ι: Type ?u.1341
ι → Finset: Type ?u.1352 → Type ?u.1352
Finset α: Type ?u.1338
α} (hs: PairwiseDisjoint s f
hs : s: Set ι
s.PairwiseDisjoint: {α : Type ?u.1356} → {ι : Type ?u.1355} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → Prop
PairwiseDisjoint f: ι → Finset α
f)
    {i: ι
i j: ι
j : ι: Type ?u.1341
ι} (hi: i ∈ s
hi : i: ι
i ∈ s: Set ι
s) (hj: j ∈ s
hj : j: ι
j ∈ s: Set ι
s) (a: α
a : α: Type ?u.1338
α) (hai: a ∈ f i
hai : a: α
a ∈ f: ι → Finset α
f i: ι
i) (haj: a ∈ f j
haj : a: α
a ∈ f: ι → Finset α
f j: ι
j) : i: ι
i = j: ι
j :=
  hs: PairwiseDisjoint s f
hs.elim: ∀ {α : Type ?u.1596} {ι : Type ?u.1597} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α},
  PairwiseDisjoint s f → ∀ {i j : ι}, i ∈ s → j ∈ s → ¬Disjoint (f i) (f j) → i = j
elim hi: i ∈ s
hi hj: j ∈ s
hj (Finset.not_disjoint_iff: ∀ {α : Type ?u.1668} {s t : Finset α}, ¬Disjoint s t ↔ ∃ a, a ∈ s ∧ a ∈ t
Finset.not_disjoint_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 ⟨a: α
a, hai: a ∈ f i
hai, haj: a ∈ f j
haj⟩)
#align set.pairwise_disjoint.elim_finset Set.PairwiseDisjoint.elim_finset: ∀ {α : Type u_2} {ι : Type u_1} {s : Set ι} {f : ι → Finset α},
  PairwiseDisjoint s f → ∀ {i j : ι}, i ∈ s → j ∈ s → ∀ (a : α), a ∈ f i → a ∈ f j → i = j
Set.PairwiseDisjoint.elim_finset

theorem PairwiseDisjoint.image_finset_of_le: ∀ [inst : DecidableEq ι] [inst_1 : SemilatticeInf α] [inst_2 : OrderBot α] {s : Finset ι} {f : ι → α},
  PairwiseDisjoint (↑s) f → ∀ {g : ι → ι}, (∀ (a : ι), f (g a) ≤ f a) → PairwiseDisjoint (↑(Finset.image g s)) f
PairwiseDisjoint.image_finset_of_le [DecidableEq: Sort ?u.1731 → Sort (max1?u.1731)
DecidableEq ι: Type ?u.1725
ι] [SemilatticeInf: Type ?u.1740 → Type ?u.1740
SemilatticeInf α: Type ?u.1722
α] [OrderBot: (α : Type ?u.1743) → [inst : LE α] → Type ?u.1743
OrderBot α: Type ?u.1722
α]
    {s: Finset ι
s : Finset: Type ?u.2049 → Type ?u.2049
Finset ι: Type ?u.1725
ι} {f: ι → α
f : ι: Type ?u.1725
ι → α: Type ?u.1722
α} (hs: PairwiseDisjoint (↑s) f
hs : (s: Finset ι
s : Set: Type ?u.2057 → Type ?u.2057
Set ι: Type ?u.1725
ι).PairwiseDisjoint: {α : Type ?u.2160} → {ι : Type ?u.2159} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → Prop
PairwiseDisjoint f: ι → α
f) {g: ι → ι
g : ι: Type ?u.1725
ι → ι: Type ?u.1725
ι}
    (hf: ∀ (a : ι), f (g a) ≤ f a
hf : ∀ a: ?m.2482
a, f: ι → α
f (g: ι → ι
g a: ?m.2482
a) ≤ f: ι → α
f a: ?m.2482
a) : (s: Finset ι
s.image: {α : Type ?u.2723} → {β : Type ?u.2722} → [inst : DecidableEq β] → (α → β) → Finset α → Finset β
image g: ι → ι
g : Set: Type ?u.2721 → Type ?u.2721
Set ι: Type ?u.1725
ι).PairwiseDisjoint: {α : Type ?u.2894} → {ι : Type ?u.2893} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → Prop
PairwiseDisjoint f: ι → α
f := by
Goals accomplished! 🐙
  α: Type u_2

ι: Type u_1

ι': Type ?u.1728

inst✝²: DecidableEq ι

inst✝¹: SemilatticeInf α

inst✝: OrderBot α

s: Finset ι

f: ι → α

hs: PairwiseDisjoint (↑s) f

g: ι → ι

hf: ∀ (a : ι), f (g a) ≤ f a

PairwiseDisjoint (↑(Finset.image g s)) frw [α: Type u_2

ι: Type u_1

ι': Type ?u.1728

inst✝²: DecidableEq ι

inst✝¹: SemilatticeInf α

inst✝: OrderBot α

s: Finset ι

f: ι → α

hs: PairwiseDisjoint (↑s) f

g: ι → ι

hf: ∀ (a : ι), f (g a) ≤ f a

PairwiseDisjoint (↑(Finset.image g s)) fcoe_image: ∀ {α : Type ?u.3001} {β : Type ?u.3000} [inst : DecidableEq β] {s : Finset α} {f : α → β}, ↑(Finset.image f s) = f '' ↑s
coe_imageα: Type u_2

ι: Type u_1

ι': Type ?u.1728

inst✝²: DecidableEq ι

inst✝¹: SemilatticeInf α

inst✝: OrderBot α

s: Finset ι

f: ι → α

hs: PairwiseDisjoint (↑s) f

g: ι → ι

hf: ∀ (a : ι), f (g a) ≤ f a

PairwiseDisjoint (g '' ↑s) f]α: Type u_2

ι: Type u_1

ι': Type ?u.1728

inst✝²: DecidableEq ι

inst✝¹: SemilatticeInf α

inst✝: OrderBot α

s: Finset ι

f: ι → α

hs: PairwiseDisjoint (↑s) f

g: ι → ι

hf: ∀ (a : ι), f (g a) ≤ f a

PairwiseDisjoint (g '' ↑s) f
  α: Type u_2

ι: Type u_1

ι': Type ?u.1728

inst✝²: DecidableEq ι

inst✝¹: SemilatticeInf α

inst✝: OrderBot α

s: Finset ι

f: ι → α

hs: PairwiseDisjoint (↑s) f

g: ι → ι

hf: ∀ (a : ι), f (g a) ≤ f a

PairwiseDisjoint (↑(Finset.image g s)) fexact hs: PairwiseDisjoint (↑s) f
hs.image_of_le: ∀ {α : Type ?u.3162} {ι : Type ?u.3163} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α},
  PairwiseDisjoint s f → ∀ {g : ι → ι}, f ∘ g ≤ f → PairwiseDisjoint (g '' s) f
image_of_le hf: ∀ (a : ι), f (g a) ≤ f a
hf
Goals accomplished! 🐙
#align set.pairwise_disjoint.image_finset_of_le Set.PairwiseDisjoint.image_finset_of_le: ∀ {α : Type u_2} {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : SemilatticeInf α] [inst_2 : OrderBot α] {s : Finset ι}
  {f : ι → α},
  PairwiseDisjoint (↑s) f → ∀ {g : ι → ι}, (∀ (a : ι), f (g a) ≤ f a) → PairwiseDisjoint (↑(Finset.image g s)) f
Set.PairwiseDisjoint.image_finset_of_le

variable [Lattice: Type ?u.3549 → Type ?u.3549
Lattice α: Type ?u.3867
α] [OrderBot: (α : Type ?u.3879) → [inst : LE α] → Type ?u.3879
OrderBot α: Type ?u.3540
α]

/-- Bind operation for `Set.PairwiseDisjoint`. In a complete lattice, you can use
`Set.PairwiseDisjoint.biUnion`. -/
theorem PairwiseDisjoint.biUnion_finset: ∀ {α : Type u_3} {ι : Type u_2} {ι' : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {s : Set ι'}
  {g : ι' → Finset ι} {f : ι → α},
  (PairwiseDisjoint s fun i' => sup (g i') f) →
    (∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f) → PairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) f
PairwiseDisjoint.biUnion_finset {s: Set ι'
s : Set: Type ?u.4194 → Type ?u.4194
Set ι': Type ?u.3873
ι'} {g: ι' → Finset ι
g : ι': Type ?u.3873
ι' → Finset: Type ?u.4199 → Type ?u.4199
Finset ι: Type ?u.3870
ι} {f: ι → α
f : ι: Type ?u.3870
ι → α: Type ?u.3867
α}
    (hs: PairwiseDisjoint s fun i' => sup (g i') f
hs : s: Set ι'
s.PairwiseDisjoint: {α : Type ?u.4207} → {ι : Type ?u.4206} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → Prop
PairwiseDisjoint fun i': ι'
i' : ι': Type ?u.3873
ι' => (g: ι' → Finset ι
g i': ι'
i').sup: {α : Type ?u.4290} → {β : Type ?u.4289} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: ι → α
f)
    (hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f
hg : ∀ i: ?m.4691
i ∈ s: Set ι'
s, (g: ι' → Finset ι
g i: ?m.4691
i : Set: Type ?u.4726 → Type ?u.4726
Set ι: Type ?u.3870
ι).PairwiseDisjoint: {α : Type ?u.4829} → {ι : Type ?u.4828} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → Prop
PairwiseDisjoint f: ι → α
f) : (⋃ i: ?m.4920
i ∈ s: Set ι'
s, ↑(g: ι' → Finset ι
g i: ?m.4920
i)).PairwiseDisjoint: {α : Type ?u.5064} → {ι : Type ?u.5063} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → Prop
PairwiseDisjoint f: ι → α
f := by
Goals accomplished! 🐙
  α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

PairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) frintro a: ι
a ha: a ∈ iUnion fun i => iUnion fun h => ↑(g i)
ha b: ι
b hb: b ∈ iUnion fun i => iUnion fun h => ↑(g i)
hb hab: a ≠ b
habα: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a: ι

ha: a ∈ iUnion fun i => iUnion fun h => ↑(g i)

b: ι

hb: b ∈ iUnion fun i => iUnion fun h => ↑(g i)

hab: a ≠ b

(Disjoint on f) a b
  α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

PairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) fsimp_rw [α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a: ι

ha: a ∈ iUnion fun i => iUnion fun h => ↑(g i)

b: ι

hb: b ∈ iUnion fun i => iUnion fun h => ↑(g i)

hab: a ≠ b

(Disjoint on f) a bSet.mem_iUnion: ∀ {α : Type ?u.5462} {ι : Sort ?u.5463} {x : α} {s : ι → Set α}, (x ∈ iUnion fun i => s i) ↔ ∃ i, x ∈ s i
Set.mem_iUnionα: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

ha: ∃ i i_1, a ∈ ↑(g i)

hb: ∃ i i_1, b ∈ ↑(g i)

(Disjoint on f) a b] at ha: a ∈ iUnion fun i => iUnion fun h => ↑(g i)
ha hb: b ∈ iUnion fun i => iUnion fun h => ↑(g i)
hbα: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

ha: ∃ i i_1, a ∈ ↑(g i)

hb: ∃ i i_1, b ∈ ↑(g i)

(Disjoint on f) a b
  α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

PairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) fobtain ⟨c, hc, ha⟩: ∃ i i_1, a ∈ ↑(g i)
⟨c: ι'
c⟨c, hc, ha⟩: ∃ i i_1, a ∈ ↑(g i)
, hc: c ∈ s
hc⟨c, hc, ha⟩: ∃ i i_1, a ∈ ↑(g i)
, ha: a ∈ ↑(g c)
ha⟨c, hc, ha⟩: ∃ i i_1, a ∈ ↑(g i)
⟩ := ha: ∃ i i_1, a ∈ ↑(g i)
haα: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

hb: ∃ i i_1, b ∈ ↑(g i)

c: ι'

hc: c ∈ s

ha: a ∈ ↑(g c)

intro.intro(Disjoint on f) a b
  α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

PairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) fobtain ⟨d, hd, hb⟩: ∃ i, b ∈ ↑(g d)
⟨d: ι'
d⟨d, hd, hb⟩: ∃ i, b ∈ ↑(g d)
, hd: d ∈ s
hd⟨d, hd, hb⟩: ∃ i, b ∈ ↑(g d)
, hb: b ∈ ↑(g d)
hb⟨d, hd, hb⟩: ∃ i, b ∈ ↑(g d)
⟩ := hb: ∃ i i_1, b ∈ ↑(g i)
hbα: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

c: ι'

hc: c ∈ s

ha: a ∈ ↑(g c)

d: ι'

hd: d ∈ s

hb: b ∈ ↑(g d)

intro.intro.intro.intro(Disjoint on f) a b
  α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

PairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) fobtain hcd: g c = g d
hcdhcd | hcd: g c = g d ∨ g c ≠ g d
 | hcd: g c ≠ g d
hcd := eq_or_ne: ∀ {α : Sort ?u.6178} (x y : α), x = y ∨ x ≠ y
eq_or_ne (g: ι' → Finset ι
g c: ι'
c) (g: ι' → Finset ι
g d: ι'
d)α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

c: ι'

hc: c ∈ s

ha: a ∈ ↑(g c)

d: ι'

hd: d ∈ s

hb: b ∈ ↑(g d)

hcd: g c = g d

intro.intro.intro.intro.inl(Disjoint on f) a b
α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

c: ι'

hc: c ∈ s

ha: a ∈ ↑(g c)

d: ι'

hd: d ∈ s

hb: b ∈ ↑(g d)

hcd: g c ≠ g d

intro.intro.intro.intro.inr(Disjoint on f) a b
  α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

PairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) f·α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

c: ι'

hc: c ∈ s

ha: a ∈ ↑(g c)

d: ι'

hd: d ∈ s

hb: b ∈ ↑(g d)

hcd: g c = g d

intro.intro.intro.intro.inl(Disjoint on f) a b α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

c: ι'

hc: c ∈ s

ha: a ∈ ↑(g c)

d: ι'

hd: d ∈ s

hb: b ∈ ↑(g d)

hcd: g c = g d

intro.intro.intro.intro.inl(Disjoint on f) a b
α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

c: ι'

hc: c ∈ s

ha: a ∈ ↑(g c)

d: ι'

hd: d ∈ s

hb: b ∈ ↑(g d)

hcd: g c ≠ g d

intro.intro.intro.intro.inr(Disjoint on f) a bexact hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f
hg d: ι'
d hd: d ∈ s
hd (α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

c: ι'

hc: c ∈ s

ha: a ∈ ↑(g c)

d: ι'

hd: d ∈ s

hb: b ∈ ↑(g d)

hcd: g c = g d

intro.intro.intro.intro.inl(Disjoint on f) a bby
Goals accomplished! 🐙 α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

c: ι'

hc: c ∈ s

ha: a ∈ ↑(g c)

d: ι'

hd: d ∈ s

hb: b ∈ ↑(g d)

hcd: g c = g d

a ∈ ↑(g d)rwa [α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

c: ι'

hc: c ∈ s

ha: a ∈ ↑(g c)

d: ι'

hd: d ∈ s

hb: b ∈ ↑(g d)

hcd: g c = g d

a ∈ ↑(g d)hcd: g c = g d
hcdα: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

c: ι'

hc: c ∈ s

d: ι'

ha: a ∈ ↑(g d)

hd: d ∈ s

hb: b ∈ ↑(g d)

hcd: g c = g d

a ∈ ↑(g d)]α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

c: ι'

hc: c ∈ s

d: ι'

ha: a ∈ ↑(g d)

hd: d ∈ s

hb: b ∈ ↑(g d)

hcd: g c = g d

a ∈ ↑(g d) at ha: a ∈ ↑(g c)
ha
Goals accomplished! 🐙) hb: b ∈ ↑(g d)
hb hab: a ≠ b
hab
Goals accomplished! 🐙
  α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

PairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) f·α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

c: ι'

hc: c ∈ s

ha: a ∈ ↑(g c)

d: ι'

hd: d ∈ s

hb: b ∈ ↑(g d)

hcd: g c ≠ g d

intro.intro.intro.intro.inr(Disjoint on f) a b α: Type u_3

ι: Type u_2

ι': Type u_1

inst✝¹: Lattice α

inst✝: OrderBot α

s: Set ι'

g: ι' → Finset ι

f: ι → α

hs: PairwiseDisjoint s fun i' => sup (g i') f

hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f

a, b: ι

hab: a ≠ b

c: ι'

hc: c ∈ s

ha: a ∈ ↑(g c)

d: ι'

hd: d ∈ s

hb: b ∈ ↑(g d)

hcd: g c ≠ g d

intro.intro.intro.intro.inr(Disjoint on f) a bexact (hs: PairwiseDisjoint s fun i' => sup (g i') f
hs hc: c ∈ s
hc hd: d ∈ s
hd (ne_of_apply_ne: ∀ {α : Sort ?u.6306} {β : Sort ?u.6307} (f : α → β) {x y : α}, f x ≠ f y → x ≠ y
ne_of_apply_ne _: ?m.6308 → ?m.6309
_ hcd: g c ≠ g d
hcd)).mono: ∀ {α : Type ?u.6323} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c d : α},
  a ≤ b → c ≤ d → Disjoint b d → Disjoint a c
mono (Finset.le_sup: ∀ {α : Type ?u.6424} {β : Type ?u.6423} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {b : β}, b ∈ s → f b ≤ sup s f
Finset.le_sup ha: a ∈ ↑(g c)
ha) (Finset.le_sup: ∀ {α : Type ?u.6523} {β : Type ?u.6522} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {b : β}, b ∈ s → f b ≤ sup s f
Finset.le_sup hb: b ∈ ↑(g d)
hb)
Goals accomplished! 🐙
#align set.pairwise_disjoint.bUnion_finset Set.PairwiseDisjoint.biUnion_finset: ∀ {α : Type u_3} {ι : Type u_2} {ι' : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {s : Set ι'}
  {g : ι' → Finset ι} {f : ι → α},
  (PairwiseDisjoint s fun i' => sup (g i') f) →
    (∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f) → PairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) f
Set.PairwiseDisjoint.biUnion_finset

end Set

namespace List

variable {β: Type ?u.6961
β : Type _: Type (?u.6961+1)
Type _} [DecidableEq: Sort ?u.6964 → Sort (max1?u.6964)
DecidableEq α: Type ?u.6982
α] {r: α → α → Prop
r : α: Type ?u.6982
α → α: Type ?u.6952
α → Prop: Type
Prop} {l: List α
l : List: Type ?u.7438 → Type ?u.7438
List α: Type ?u.6952
α}

theorem pairwise_of_coe_toFinset_pairwise: ∀ {α : Type u_1} [inst : DecidableEq α] {r : α → α → Prop} {l : List α},
  Set.Pairwise (↑(toFinset l)) r → Nodup l → Pairwise r l
pairwise_of_coe_toFinset_pairwise (hl: Set.Pairwise (↑(toFinset l)) r
hl : (l: List α
l.toFinset: {α : Type ?u.7014} → [inst : DecidableEq α] → List α → Finset α
toFinset : Set: Type ?u.7013 → Type ?u.7013
Set α: Type ?u.6982
α).Pairwise: {α : Type ?u.7167} → Set α → (α → α → Prop) → Prop
Pairwise r: α → α → Prop
r) (hn: Nodup l
hn : l: List α
l.Nodup: {α : Type ?u.7180} → List α → Prop
Nodup) :
    l: List α
l.Pairwise: {α : Type ?u.7186} → (α → α → Prop) → List α → Prop
Pairwise r: α → α → Prop
r := by
Goals accomplished! 🐙
  α: Type u_1

ι: Type ?u.6985

ι': Type ?u.6988

β: Type ?u.6991

inst✝: DecidableEq α

r: α → α → Prop

l: List α

hl: Set.Pairwise (↑(toFinset l)) r

hn: Nodup l

Pairwise r lrw [α: Type u_1

ι: Type ?u.6985

ι': Type ?u.6988

β: Type ?u.6991

inst✝: DecidableEq α

r: α → α → Prop

l: List α

hl: Set.Pairwise (↑(toFinset l)) r

hn: Nodup l

Pairwise r lcoe_toFinset: ∀ {α : Type ?u.7202} [inst : DecidableEq α] (l : List α), ↑(toFinset l) = { a | a ∈ l }
coe_toFinsetα: Type u_1

ι: Type ?u.6985

ι': Type ?u.6988

β: Type ?u.6991

inst✝: DecidableEq α

r: α → α → Prop

l: List α

hl: Set.Pairwise { a | a ∈ l } r

hn: Nodup l

Pairwise r l]α: Type u_1

ι: Type ?u.6985

ι': Type ?u.6988

β: Type ?u.6991

inst✝: DecidableEq α

r: α → α → Prop

l: List α

hl: Set.Pairwise { a | a ∈ l } r

hn: Nodup l

Pairwise r l at hl: Set.Pairwise (↑(toFinset l)) r
hlα: Type u_1

ι: Type ?u.6985

ι': Type ?u.6988

β: Type ?u.6991

inst✝: DecidableEq α

r: α → α → Prop

l: List α

hl: Set.Pairwise { a | a ∈ l } r

hn: Nodup l

Pairwise r l
  α: Type u_1

ι: Type ?u.6985

ι': Type ?u.6988

β: Type ?u.6991

inst✝: DecidableEq α

r: α → α → Prop

l: List α

hl: Set.Pairwise (↑(toFinset l)) r

hn: Nodup l

Pairwise r lexact hn: Nodup l
hn.pairwise_of_set_pairwise: ∀ {α : Type ?u.7372} {l : List α} {r : α → α → Prop}, Nodup l → Set.Pairwise { x | x ∈ l } r → Pairwise r l
pairwise_of_set_pairwise hl: Set.Pairwise { a | a ∈ l } r
hl
Goals accomplished! 🐙
#align list.pairwise_of_coe_to_finset_pairwise List.pairwise_of_coe_toFinset_pairwise: ∀ {α : Type u_1} [inst : DecidableEq α] {r : α → α → Prop} {l : List α},
  Set.Pairwise (↑(toFinset l)) r → Nodup l → Pairwise r l
List.pairwise_of_coe_toFinset_pairwise

theorem pairwise_iff_coe_toFinset_pairwise: ∀ {α : Type u_1} [inst : DecidableEq α] {r : α → α → Prop} {l : List α},
  Nodup l → Symmetric r → (Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r l)
pairwise_iff_coe_toFinset_pairwise (hn: Nodup l
hn : l: List α
l.Nodup: {α : Type ?u.7441} → List α → Prop
Nodup) (hs: Symmetric r
hs : Symmetric: {β : Sort ?u.7448} → (β → β → Prop) → Prop
Symmetric r: α → α → Prop
r) :
    (l: List α
l.toFinset: {α : Type ?u.7460} → [inst : DecidableEq α] → List α → Finset α
toFinset : Set: Type ?u.7459 → Type ?u.7459
Set α: Type ?u.7411
α).Pairwise: {α : Type ?u.7612} → Set α → (α → α → Prop) → Prop
Pairwise r: α → α → Prop
r ↔ l: List α
l.Pairwise: {α : Type ?u.7623} → (α → α → Prop) → List α → Prop
Pairwise r: α → α → Prop
r := by
Goals accomplished! 🐙
  α: Type u_1

ι: Type ?u.7414

ι': Type ?u.7417

β: Type ?u.7420

inst✝: DecidableEq α

r: α → α → Prop

l: List α

hn: Nodup l

hs: Symmetric r

Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r lletI : IsSymm: (α : Type ?u.7640) → (α → α → Prop) → Prop
IsSymm α: Type u_1
α r: α → α → Prop
r := ⟨hs: Symmetric r
hs⟩α: Type u_1

ι: Type ?u.7414

ι': Type ?u.7417

β: Type ?u.7420

inst✝: DecidableEq α

r: α → α → Prop

l: List α

hn: Nodup l

hs: Symmetric r

this:= { symm := hs }: IsSymm α r

Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r l
  α: Type u_1

ι: Type ?u.7414

ι': Type ?u.7417

β: Type ?u.7420

inst✝: DecidableEq α

r: α → α → Prop

l: List α

hn: Nodup l

hs: Symmetric r

Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r lrw [α: Type u_1

ι: Type ?u.7414

ι': Type ?u.7417

β: Type ?u.7420

inst✝: DecidableEq α

r: α → α → Prop

l: List α

hn: Nodup l

hs: Symmetric r

this:= { symm := hs }: IsSymm α r

Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r lcoe_toFinset: ∀ {α : Type ?u.7658} [inst : DecidableEq α] (l : List α), ↑(toFinset l) = { a | a ∈ l }
coe_toFinset,α: Type u_1

ι: Type ?u.7414

ι': Type ?u.7417

β: Type ?u.7420

inst✝: DecidableEq α

r: α → α → Prop

l: List α

hn: Nodup l

hs: Symmetric r

this:= { symm := hs }: IsSymm α r

Set.Pairwise { a | a ∈ l } r ↔ Pairwise r l α: Type u_1

ι: Type ?u.7414

ι': Type ?u.7417

β: Type ?u.7420

inst✝: DecidableEq α

r: α → α → Prop

l: List α

hn: Nodup l

hs: Symmetric r

this:= { symm := hs }: IsSymm α r

Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r lhn: Nodup l
hn.pairwise_coe: ∀ {α : Type ?u.7810} {l : List α} {r : α → α → Prop} [inst : IsSymm α r],
  Nodup l → (Set.Pairwise { a | a ∈ l } r ↔ Pairwise r l)
pairwise_coeα: Type u_1

ι: Type ?u.7414

ι': Type ?u.7417

β: Type ?u.7420

inst✝: DecidableEq α

r: α → α → Prop

l: List α

hn: Nodup l

hs: Symmetric r

this:= { symm := hs }: IsSymm α r

Pairwise r l ↔ Pairwise r l]
Goals accomplished! 🐙
#align list.pairwise_iff_coe_to_finset_pairwise List.pairwise_iff_coe_toFinset_pairwise: ∀ {α : Type u_1} [inst : DecidableEq α] {r : α → α → Prop} {l : List α},
  Nodup l → Symmetric r → (Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r l)
List.pairwise_iff_coe_toFinset_pairwise

theorem pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι] {l : List ι}
  {f : ι → α}, Set.PairwiseDisjoint (↑(toFinset l)) f → Nodup l → Pairwise (_root_.Disjoint on f) l
pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint {α: ?m.7897
α ι: Type u_2
ι} [SemilatticeInf: Type ?u.7903 → Type ?u.7903
SemilatticeInf α: ?m.7897
α] [OrderBot: (α : Type ?u.7906) → [inst : LE α] → Type ?u.7906
OrderBot α: ?m.7897
α]
    [DecidableEq: Sort ?u.8211 → Sort (max1?u.8211)
DecidableEq ι: ?m.7900
ι] {l: List ι
l : List: Type ?u.8220 → Type ?u.8220
List ι: ?m.7900
ι} {f: ι → α
f : ι: ?m.7900
ι → α: ?m.7897
α} (hl: Set.PairwiseDisjoint (↑(toFinset l)) f
hl : (l: List ι
l.toFinset: {α : Type ?u.8229} → [inst : DecidableEq α] → List α → Finset α
toFinset : Set: Type ?u.8228 → Type ?u.8228
Set ι: ?m.7900
ι).PairwiseDisjoint: {α : Type ?u.8384} → {ι : Type ?u.8383} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → Prop
PairwiseDisjoint f: ι → α
f)
    (hn: Nodup l
hn : l: List ι
l.Nodup: {α : Type ?u.8701} → List α → Prop
Nodup) : l: List ι
l.Pairwise: {α : Type ?u.8707} → (α → α → Prop) → List α → Prop
Pairwise (_root_.Disjoint: {α : Type ?u.8722} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
_root_.Disjoint on f: ι → α
f) :=
  pairwise_of_coe_toFinset_pairwise: ∀ {α : Type ?u.8886} [inst : DecidableEq α] {r : α → α → Prop} {l : List α},
  Set.Pairwise (↑(toFinset l)) r → Nodup l → Pairwise r l
pairwise_of_coe_toFinset_pairwise hl: Set.PairwiseDisjoint (↑(toFinset l)) f
hl hn: Nodup l
hn
#align list.pairwise_disjoint_of_coe_to_finset_pairwise_disjoint List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι] {l : List ι}
  {f : ι → α}, Set.PairwiseDisjoint (↑(toFinset l)) f → Nodup l → Pairwise (_root_.Disjoint on f) l
List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint

theorem pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι] {l : List ι}
  {f : ι → α}, Nodup l → (Set.PairwiseDisjoint (↑(toFinset l)) f ↔ Pairwise (_root_.Disjoint on f) l)
pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint {α: ?m.9049
α ι: ?m.9052
ι} [SemilatticeInf: Type ?u.9055 → Type ?u.9055
SemilatticeInf α: ?m.9049
α] [OrderBot: (α : Type ?u.9058) → [inst : LE α] → Type ?u.9058
OrderBot α: ?m.9049
α]
    [DecidableEq: Sort ?u.9363 → Sort (max1?u.9363)
DecidableEq ι: ?m.9052
ι] {l: List ι
l : List: Type ?u.9372 → Type ?u.9372
List ι: ?m.9052
ι} {f: ι → α
f : ι: ?m.9052
ι → α: ?m.9049
α} (hn: Nodup l
hn : l: List ι
l.Nodup: {α : Type ?u.9379} → List α → Prop
Nodup) :
    (l: List ι
l.toFinset: {α : Type ?u.9388} → [inst : DecidableEq α] → List α → Finset α
toFinset : Set: Type ?u.9387 → Type ?u.9387
Set ι: ?m.9052
ι).PairwiseDisjoint: {α : Type ?u.9542} → {ι : Type ?u.9541} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → Prop
PairwiseDisjoint f: ι → α
f ↔ l: List ι
l.Pairwise: {α : Type ?u.9789} → (α → α → Prop) → List α → Prop
Pairwise (_root_.Disjoint: {α : Type ?u.9804} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
_root_.Disjoint on f: ι → α
f) :=
  pairwise_iff_coe_toFinset_pairwise: ∀ {α : Type ?u.9967} [inst : DecidableEq α] {r : α → α → Prop} {l : List α},
  Nodup l → Symmetric r → (Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r l)
pairwise_iff_coe_toFinset_pairwise hn: Nodup l
hn (symmetric_disjoint: ∀ {α : Type ?u.10061} [inst : PartialOrder α] [inst_1 : OrderBot α], Symmetric _root_.Disjoint
symmetric_disjoint.comap: ∀ {α : Type ?u.10134} {β : Type ?u.10133} {r : β → β → Prop}, Symmetric r → ∀ (f : α → β), Symmetric (r on f)
comap f: ι → α
f)
#align list.pairwise_disjoint_iff_coe_to_finset_pairwise_disjoint List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι] {l : List ι}
  {f : ι → α}, Nodup l → (Set.PairwiseDisjoint (↑(toFinset l)) f ↔ Pairwise (_root_.Disjoint on f) l)
List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint

end List