[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
⊢ Set.Pairwise (⋃ (n : κ), f n) r ↔ ∀ (n : κ), Set.Pairwise (f n) r
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
⊢ Set.Pairwise (⋃ (n : κ), f n) r → ∀ (n : κ), Set.Pairwise (f n) r
[PROOFSTEP]
intro H n
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : Set.Pairwise (⋃ (n : κ), f n) r
n : κ
⊢ Set.Pairwise (f n) r
[PROOFSTEP]
exact Pairwise.mono (subset_iUnion _ _) H
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
⊢ (∀ (n : κ), Set.Pairwise (f n) r) → Set.Pairwise (⋃ (n : κ), f n) r
[PROOFSTEP]
intro H i hi j hj hij
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : κ), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : κ), f n
j : α
hj : j ∈ ⋃ (n : κ), f n
hij : i ≠ j
⊢ r i j
[PROOFSTEP]
rcases mem_iUnion.1 hi with ⟨m, hm⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : κ), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : κ), f n
j : α
hj : j ∈ ⋃ (n : κ), f n
hij : i ≠ j
m : κ
hm : i ∈ f m
⊢ r i j
[PROOFSTEP]
rcases mem_iUnion.1 hj with ⟨n, hn⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : κ), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : κ), f n
j : α
hj : j ∈ ⋃ (n : κ), f n
hij : i ≠ j
m : κ
hm : i ∈ f m
n : κ
hn : j ∈ f n
⊢ r i j
[PROOFSTEP]
rcases h m n with ⟨p, mp, np⟩
[GOAL]
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p✝ q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : κ), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : κ), f n
j : α
hj : j ∈ ⋃ (n : κ), f n
hij : i ≠ j
m : κ
hm : i ∈ f m
n : κ
hn : j ∈ f n
p : κ
mp : f m ⊆ f p
np : f n ⊆ f p
⊢ r i j
[PROOFSTEP]
exact H p (mp hm) (np hn) hij
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r✝ p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
r : α → α → Prop
s : Set (Set α)
h : DirectedOn (fun x x_1 => x ⊆ x_1) s
⊢ Set.Pairwise (⋃₀ s) r ↔ ∀ (a : Set α), a ∈ s → Set.Pairwise a r
[PROOFSTEP]
rw [sUnion_eq_iUnion, pairwise_iUnion h.directed_val, SetCoe.forall]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s✝ : Set ι
t s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint s fun i' => ⨆ (i : ι) (_ : i ∈ g i'), f i
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
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s✝ : Set ι
t s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint s fun i' => ⨆ (i : ι) (_ : i ∈ g i'), f i
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
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s✝ : Set ι
t s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint s fun i' => ⨆ (i : ι) (_ : i ∈ g i'), f i
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
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s✝ : Set ι
t s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint s fun i' => ⨆ (i : ι) (_ : i ∈ g i'), f i
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
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s✝ : Set ι
t s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint s fun i' => ⨆ (i : ι) (_ : i ∈ g i'), f i
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
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s✝ : Set ι
t s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint s fun i' => ⨆ (i : ι) (_ : i ∈ g i'), f i
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 (hcd.subst ha) hb hab
[GOAL]
case intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s✝ : Set ι
t s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint s fun i' => ⨆ (i : ι) (_ : i ∈ g i'), f i
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 (le_iSup₂ (f := fun i (_ : i ∈ g c) => f i) a ha)
    (le_iSup₂ (f := fun i (_ : i ∈ g d) => f i) b hb)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
⊢ PairwiseDisjoint (s ×ˢ t) f
[PROOFSTEP]
rintro ⟨i, i'⟩ hi ⟨j, j'⟩ hj h
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
j : ι
j' : ι'
hj : (j, j') ∈ s ×ˢ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')
[PROOFSTEP]
rw [mem_prod] at hi hj 
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j : ι
j' : ι'
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')
[PROOFSTEP]
obtain rfl | hij := eq_or_ne i j
[GOAL]
case mk.mk.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j' : ι'
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
h : (i, i') ≠ (i, j')
⊢ (Disjoint on f) (i, i') (i, j')
[PROOFSTEP]
refine' (ht hi.2 hj.2 <| (Prod.mk.inj_left _).ne_iff.1 h).mono _ _
[GOAL]
case mk.mk.inl.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j' : ι'
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, i') ≤ (fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')) (i, i').snd
[PROOFSTEP]
convert le_iSup₂ (α := α) i hi.1
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j' : ι'
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, i') = f (i, (i, i').snd)
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.inl.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j' : ι'
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, j') ≤ (fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')) (i, j').snd
[PROOFSTEP]
convert le_iSup₂ (α := α) i hj.1
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j' : ι'
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, j') = f (i, (i, j').snd)
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j : ι
j' : ι'
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ (Disjoint on f) (i, i') (j, j')
[PROOFSTEP]
refine' (hs hi.1 hj.1 hij).mono _ _
[GOAL]
case mk.mk.inr.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j : ι
j' : ι'
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (i, i') ≤ (fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')) (i, i').fst
[PROOFSTEP]
convert le_iSup₂ (α := α) i' hi.2
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j : ι
j' : ι'
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (i, i') = f ((i, i').fst, i')
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.inr.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j : ι
j' : ι'
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (j, j') ≤ (fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')) (j, j').fst
[PROOFSTEP]
convert le_iSup₂ (α := α) j' hj.2
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j : ι
j' : ι'
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (j, j') = f ((j, j').fst, j')
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
⊢ PairwiseDisjoint (s ×ˢ t) f ↔
    (PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')) ∧
      PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
[PROOFSTEP]
refine' ⟨fun h => ⟨fun i hi j hj hij => _, fun i hi j hj hij => _⟩, fun h => h.1.prod_left h.2⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : PairwiseDisjoint (s ×ˢ t) f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ (Disjoint on fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')) i j
[PROOFSTEP]
simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : PairwiseDisjoint (s ×ˢ t) f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ (Disjoint on fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')) i j
[PROOFSTEP]
simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : PairwiseDisjoint (s ×ˢ t) f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ ∀ (i_1 : ι'), i_1 ∈ t → ∀ (i_3 : ι'), i_3 ∈ t → Disjoint (f (i, i_1)) (f (j, i_3))
[PROOFSTEP]
intro i' hi' j' hj'
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : PairwiseDisjoint (s ×ˢ t) f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ ∀ (i_1 : ι), i_1 ∈ s → ∀ (i_3 : ι), i_3 ∈ s → Disjoint (f (i_1, i)) (f (i_3, j))
[PROOFSTEP]
intro i' hi' j' hj'
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : PairwiseDisjoint (s ×ˢ t) f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
i' : ι'
hi' : i' ∈ t
j' : ι'
hj' : j' ∈ t
⊢ Disjoint (f (i, i')) (f (j, j'))
[PROOFSTEP]
exact h (mk_mem_prod hi hi') (mk_mem_prod hj hj') (ne_of_apply_ne Prod.fst hij)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : PairwiseDisjoint (s ×ˢ t) f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
i' : ι
hi' : i' ∈ s
j' : ι
hj' : j' ∈ s
⊢ Disjoint (f (i', i)) (f (j', j))
[PROOFSTEP]
exact h (mk_mem_prod hi' hi) (mk_mem_prod hj' hj) (ne_of_apply_ne Prod.snd hij)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
⊢ (⋃ (i : ι) (_ : i ∈ s), f i) \ ⋃ (i : ι) (_ : i ∈ t), f i = ⋃ (i : ι) (_ : i ∈ s \ t), f i
[PROOFSTEP]
refine'
  (biUnion_diff_biUnion_subset f s t).antisymm (iUnion₂_subset fun i hi a ha => (mem_diff _).2 ⟨mem_biUnion hi.1 ha, _⟩)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬a ∈ ⋃ (x : ι) (_ : x ∈ t), f x
[PROOFSTEP]
rw [mem_iUnion₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬∃ i j, a ∈ f i
[PROOFSTEP]
rintro ⟨j, hj, haj⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ False
[PROOFSTEP]
exact (h (Or.inl hi.1) (Or.inr hj) (ne_of_mem_of_not_mem hj hi.2).symm).le_bot ⟨ha, haj⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : ⋃ (i : ι) (_ : i ∈ s), f i ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
⊢ s ⊆ t
[PROOFSTEP]
rintro i hi
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : ⋃ (i : ι) (_ : i ∈ s), f i ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
i : ι
hi : i ∈ s
⊢ i ∈ t
[PROOFSTEP]
obtain ⟨a, hai⟩ := h₁ i hi
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : ⋃ (i : ι) (_ : i ∈ s), f i ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
⊢ i ∈ t
[PROOFSTEP]
obtain ⟨j, hj, haj⟩ := mem_iUnion₂.1 (h <| mem_iUnion₂_of_mem hi hai)
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : ⋃ (i : ι) (_ : i ∈ s), f i ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ i ∈ t
[PROOFSTEP]
rwa [h₀.eq (subset_union_left _ _ hi) (subset_union_right _ _ hj) (not_disjoint_iff.2 ⟨a, hai, haj⟩)]
