[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
⊢ Set.PairwiseDisjoint (Set.range singleton) id
[PROOFSTEP]
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ h
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
ι' : Type u_3
a b : α
h : {a} ≠ {b}
⊢ (Disjoint on id) {a} {b}
[PROOFSTEP]
exact disjoint_singleton.2 (ne_of_apply_ne _ h)
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
hs : PairwiseDisjoint (↑s) f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ PairwiseDisjoint (↑(Finset.image g s)) f
[PROOFSTEP]
rw [coe_image]
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
hs : PairwiseDisjoint (↑s) f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ PairwiseDisjoint (g '' ↑s) f
[PROOFSTEP]
exact hs.image_of_le hf
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
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 (⋃ (i : ι') (_ : i ∈ s), ↑(g i)) f
[PROOFSTEP]
rintro a ha b hb hab
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
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 ∈ ⋃ (i : ι') (_ : i ∈ s), ↑(g i)
b : ι
hb : b ∈ ⋃ (i : ι') (_ : i ∈ s), ↑(g i)
hab : a ≠ b
⊢ (Disjoint on f) a b
[PROOFSTEP]
simp_rw [Set.mem_iUnion] at ha hb 
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
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
[PROOFSTEP]
obtain ⟨c, hc, ha⟩ := ha
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
ι' : Type u_3
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)
⊢ (Disjoint on f) a b
[PROOFSTEP]
obtain ⟨d, hd, hb⟩ := hb
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
ι' : Type u_3
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)
⊢ (Disjoint on f) a b
[PROOFSTEP]
obtain hcd | hcd := eq_or_ne (g c) (g d)
[GOAL]
case intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
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
⊢ (Disjoint on f) a b
[PROOFSTEP]
exact hg d hd (by rwa [hcd] at ha ) hb hab
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
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)
[PROOFSTEP]
rwa [hcd] at ha 
[GOAL]
case intro.intro.intro.intro.inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
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
⊢ (Disjoint on f) a b
[PROOFSTEP]
exact (hs hc hd (ne_of_apply_ne _ hcd)).mono (Finset.le_sup ha) (Finset.le_sup hb)
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
β : Type u_4
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : Set.Pairwise (↑(toFinset l)) r
hn : Nodup l
⊢ Pairwise r l
[PROOFSTEP]
rw [coe_toFinset] at hl 
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
β : Type u_4
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : Set.Pairwise {a | a ∈ l} r
hn : Nodup l
⊢ Pairwise r l
[PROOFSTEP]
exact hn.pairwise_of_set_pairwise hl
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
β : Type u_4
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hn : Nodup l
hs : Symmetric r
⊢ Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r l
[PROOFSTEP]
letI : IsSymm α r := ⟨hs⟩
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
β : Type u_4
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hn : Nodup l
hs : Symmetric r
this : IsSymm α r := { symm := hs }
⊢ Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r l
[PROOFSTEP]
rw [coe_toFinset, hn.pairwise_coe]
