α : 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 ∈ ⋃ (i : ι') (_ : i ∈ s), ↑(g i)
b : ι
hb : b ∈ ⋃ (i : ι') (_ : i ∈ s), ↑(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 (⋃ (i : ι') (_ : i ∈ s), ↑(g i)) f
rintro a ha b hb 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 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
a : ι
ha : a ∈ ⋃ (i : ι') (_ : i ∈ s), ↑(g i)
b : ι
hb : b ∈ ⋃ (i : ι') (_ : i ∈ s), ↑(g i)
hab : a ≠ b
⊢ (Disjoint on f) a b
simp_rw [Set.mem_iUnion] at ha hb
case intro.intro
α : 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)
⊢ (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
ha : ∃ i i_1, a ∈ ↑(g i)
hb : ∃ i i_1, b ∈ ↑(g i)
⊢ (Disjoint on f) a b
obtain ⟨c, hc, ha⟩ := ha
case intro.intro.intro.intro
α : 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)
⊢ (Disjoint on f) a b
case intro.intro
α : 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)
⊢ (Disjoint on f) a b
obtain ⟨d, hd, hb⟩ := hb
case intro.intro.intro.intro.inl
α : 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
⊢ (Disjoint on f) a b

case intro.intro.intro.intro.inr
α : 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
⊢ (Disjoint on f) a b
case intro.intro.intro.intro
α : 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)
⊢ (Disjoint on f) a b
obtain hcd | hcd := eq_or_ne (g c) (g d)
no goals
case intro.intro.intro.intro.inl
α : 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
⊢ (Disjoint on f) a b
exact hg d hd (by rwa [hcd] at ha) hb hab
no goals
α : 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 [hcd] at ha
no goals
case intro.intro.intro.intro.inr
α : 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
⊢ (Disjoint on f) a b
exact (hs hc hd (ne_of_apply_ne _ hcd)).mono (Finset.le_sup ha) (Finset.le_sup hb)