case pos
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
⊢ SetIndependent (⋃ (i : η), s i)

case neg
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : ¬Nonempty η
⊢ SetIndependent (⋃ (i : η), s i)
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
⊢ SetIndependent (⋃ (i : η), s i)
by_cases hη : Nonempty η
case pos
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
⊢ ∀ (t : Finset α), (↑t ⊆ ⋃ (i : η), s i) → SetIndependent ↑t
case pos
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
⊢ SetIndependent (⋃ (i : η), s i)
rw [CompleteLattice.setIndependent_iff_finite]
case pos
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ (i : η), s i
⊢ SetIndependent ↑t
case pos
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
⊢ ∀ (t : Finset α), (↑t ⊆ ⋃ (i : η), s i) → SetIndependent ↑t
intro t ht
case pos.intro.intro
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ (i : η), s i
I : Set η
fi : Set.Finite I
hI : ↑t ⊆ ⋃ (i : η) (_ : i ∈ I), s i
⊢ SetIndependent ↑t
case pos
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ (i : η), s i
⊢ SetIndependent ↑t
obtain ⟨I, fi, hI⟩ := Set.finite_subset_iUnion t.finite_toSet ht
case pos.intro.intro.intro
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ (i : η), s i
I : Set η
fi : Set.Finite I
hI : ↑t ⊆ ⋃ (i : η) (_ : i ∈ I), s i
i : η
hi : ∀ (i_1 : η), i_1 ∈ Set.Finite.toFinset fi → s i_1 ⊆ s i
⊢ SetIndependent ↑t
case pos.intro.intro
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ (i : η), s i
I : Set η
fi : Set.Finite I
hI : ↑t ⊆ ⋃ (i : η) (_ : i ∈ I), s i
⊢ SetIndependent ↑t
obtain ⟨i, hi⟩ := hs.finset_le fi.toFinset
no goals
case pos.intro.intro.intro
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ (i : η), s i
I : Set η
fi : Set.Finite I
hI : ↑t ⊆ ⋃ (i : η) (_ : i ∈ I), s i
i : η
hi : ∀ (i_1 : η), i_1 ∈ Set.Finite.toFinset fi → s i_1 ⊆ s i
⊢ SetIndependent ↑t
exact (h i).mono
    (Set.Subset.trans hI <| Set.iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))
case neg.intro.intro.intro
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : ¬Nonempty η
a : α
w✝ : Set α
right✝ : a ∈ w✝
i : η
h✝ : (fun i => s i) i = w✝
⊢ Disjoint a (sSup ((⋃ (i : η), s i) \ {a}))
case neg
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : ¬Nonempty η
⊢ SetIndependent (⋃ (i : η), s i)
rintro a ⟨_, ⟨i, _⟩, _⟩
case neg.intro.intro.intro.h
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : ¬Nonempty η
a : α
w✝ : Set α
right✝ : a ∈ w✝
i : η
h✝ : (fun i => s i) i = w✝
⊢ False
case neg.intro.intro.intro
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : ¬Nonempty η
a : α
w✝ : Set α
right✝ : a ∈ w✝
i : η
h✝ : (fun i => s i) i = w✝
⊢ Disjoint a (sSup ((⋃ (i : η), s i) \ {a}))
exfalso
no goals
case neg.intro.intro.intro.h
ι : Sort ?u.107199
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ : Set α
η : Type u_1
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : ¬Nonempty η
a : α
w✝ : Set α
right✝ : a ∈ w✝
i : η
h✝ : (fun i => s i) i = w✝
⊢ False
exact hη ⟨i⟩